Re: RFC: Native -XCPP Proposal

2015-05-19 Thread Bardur Arantsson
On 05/19/2015 07:31 AM, Carter Schonwald wrote:
 I imagine your ghc build uses gcc to invoke the system assembler and linker
 on your Linux servers, :-) and that's gplv3!

That is of no consequence licensing-wise since those are

   a) separate programs/executables, thus derived work doesn't enter
  into it at any level, except...

   b) if the output contains bits of of the programs themselves, but
  e.g. gcc (and one assumes the linker, etc.) have specific
  licensing exemptions for the output.

(And this *is* something that you can quickly explain to the lawyerly
types.)

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Non-deterministic package IDs are really bad in 7.10

2015-05-19 Thread Mateusz Kowalczyk
On 05/19/2015 06:46 AM, Daniel Peebles wrote:
 Don't Nix builds all happen in a randomly generated temporary directory by
 default? Then you just copy to $out in installPhase. Perhaps stabilizing
 the build directory would help alleviate some of the immediate problems, if
 what Joachim is describing affects us too.

Oh, I was far too hasty in reading the bug on the Debian tracker. Yes, I
suppose this could be a problem for us though I'd like to see it first
before trying to work around it.

 On Mon, May 18, 2015 at 10:13 PM, Mateusz Kowalczyk fuuze...@fuuzetsu.co.uk
 wrote:
 
 On 05/14/2015 05:43 PM, Joachim Breitner wrote:
 Hi,

 Am Sonntag, den 10.05.2015, 19:39 +0100 schrieb Mateusz Kowalczyk:
 I'd like to bring some attention to ticket #4012 about non-determinism.
 As many of you may know, the nix package manager distributes binaries
 throughout its binary caches. The binaries are shared as long as the
 hash of some of their inputs matches: this means that we can end up with
 two of the same hashes of inputs but thanks to #4012 means that the
 actual contents can differ. You end up with machines with some packages
 built locally and some elsewhere and due to non-determinism, the GHC
 package IDs don't line up and everything is broken.

 is NixOS sensitive to changes in the build directory. Debian is, and
 since 7.8 the build path creeps into the interface files and affects the
 hash: https://bugs.debian.org/785282

 But you probably are not, otherwise you’d have complained when 7.8 was
 out, and not now :-)

 Greetings,
 Joachim


 Not a problem for nix, the paths are are calculated based on the
 derivation inputs. I don't want to go into details but if same
 expression goes in, same path comes out. If the path that comes out is
 different, you simply don't get to use it. More or less nix does
 ‘calculate the store path from this expression, check if it exists in
 binary caches and fetch it if it does, build if it does not’.

 So for us the store paths in the interface files would always be the
 same for the same inputs hence no problem there.

 --


-- 
Mateusz K.
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: RFC: Native -XCPP Proposal

2015-05-19 Thread Bardur Arantsson
On 05/19/2015 08:26 AM, Bardur Arantsson wrote:
 On 05/19/2015 07:31 AM, Carter Schonwald wrote:
 I imagine your ghc build uses gcc to invoke the system assembler and linker
 on your Linux servers, :-) and that's gplv3!
 
 That is of no consequence licensing-wise since those are
 
a) separate programs/executables, thus derived work doesn't enter
   into it at any level, except...
 
b) if the output contains bits of of the programs themselves, but
   e.g. gcc (and one assumes the linker, etc.) have specific
   licensing exemptions for the output.
 
 (And this *is* something that you can quickly explain to the lawyerly
 types.)
 

Oh, and it's also pretty well-established at this point, though I'm not
aware of any specific cases that have gone to the courts.

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: RFC: Native -XCPP Proposal

2015-05-19 Thread Boespflug, Mathieu
On 19 May 2015 at 08:26, Bardur Arantsson s...@scientician.net wrote:

 On 05/19/2015 07:31 AM, Carter Schonwald wrote:
  I imagine your ghc build uses gcc to invoke the system assembler and
 linker
  on your Linux servers, :-) and that's gplv3!

 That is of no consequence licensing-wise since those are

a) separate programs/executables, thus derived work doesn't enter
   into it at any level, except...

b) if the output contains bits of of the programs themselves, but
   e.g. gcc (and one assumes the linker, etc.) have specific
   licensing exemptions for the output.

 (And this *is* something that you can quickly explain to the lawyerly
 types.)


Both conditions likewise hold true for
cpphs-as-an-external-process-bundled-with-GHC. So any particular remaining
concern there?
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: [Haskell-cafe] RFC: Native -XCPP Proposal

2015-05-19 Thread malcolm.wallace

How does your company deal with the Integer type, whose standard implementation 
in ghc is via the LGPL'd Gnu multi-precision routines?
Regards,
   Malcolm

On 18 May, 2015,at 09:19 PM, Lars Kuhtz hask...@kuhtz.eu wrote:

I work for PivotCloud. We use Haskell/GHC in our production system on 
the server side and on the client side.


My experience is that any license that contains the string GPL can 
cause problems in an corporate context, no matter if it actually is a 
legal issue or not.


Folks who are responsible for making decisions about legal implications 
of the usage of third party software don't always have experience with 
open source software. Also they are often not familiar with the 
technical details of derived work, different types of linking, or the 
subtleties of distinguishing between build-, link-, and run-time 
dependencies in modern software engineering pipelines. So, any 
mentioning of LGPL (or similar) potentially causes overhead in the 
adaption.


Regards,
Lars

On 5/7/15 11:10 PM, Malcolm Wallace wrote:
Exactly. My post was an attempt to elicit response from anyone to whom it 
matters. There is no point in worrying about hypothetical licensing problems - 
let's hear about the real ones.

Regards,
Malcolm

On 7 May 2015, at 22:15, Tomas Carnecky wrote:

That doesn't mean those people don't exist. Maybe they do but are too afraid to 
speak up (due to corporate policy or whatever).

On Thu, May 7, 2015 at 10:41 PM, Malcolm Wallace malcolm.wall...@me.com wrote:
I also note that in this discussion, so far not a single person has said that 
the cpphs licence would actually be a problem for them.

Regards,
Malcolm

On 7 May 2015, at 20:54, Herbert Valerio Riedel wrote:

On 2015-05-06 at 13:38:16 +0200, Jan Stolarek wrote:

[...]

Regarding licensing issues: perhaps we should simply ask Malcolm
Wallace if he would consider changing the license for the sake of GHC?
Or perhaps he could grant a custom-tailored license to the GHC
project? After all, the project page [1] says:  If that's a problem
for you, contact me to make other arrangements.

Fyi, Neil talked to him[1]:

| I talked to Malcolm. His contention is that it doesn't actually change
| the license of the ghc package. As such, it's just a single extra
| license to add to a directory full of licenses, which is no big deal.


[1]: 
http://www.reddit.com/r/haskell/comments/351pur/rfc_native_xcpp_for_ghc_proposal/cr1e5n3

___
Haskell-Cafe mailing list
haskell-c...@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe


___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Interactions between type-checker plugins

2015-05-19 Thread Christiaan Baaij
Hi,

My apologies for this rather lengthy email.

I have a question about how type-checker plugins should interact.
My situation is the following:
I have two type-checker plugins, one that can solve equalities involving the 
standard type-level operations on kind Nat (+,*,-,^), and another type-checker 
plugin that can prove equalities involving a new type-level operation GCD.
In the following, the type-checker plugin involving the stand type-level 
operations is called ‘A’, and the type checker involving the new GCD operations 
is called ‘B’.

When type-checker plugin A encounters:
[W] GCD 6 8 + x ~ x + GCD 9 6

It knows that (+) is commutative, so it can prove the above equality _given_ 
that GCD 6 8 ~ GCD 9 6” holds.
So what type-checker plugin A does now is emits a new wanted constraints:
[W] GCD 6 8 ~ GCD 9 6
And remembers that it emitted this wanted constraint.
In type-checker plugin lingo, it returns:
TcPluginOk [] [[W] GCD 6 8 ~ GCD 9 6”]

Now whenever type-checker plugin encounters
[W] GCD 6 8 + x ~ x + GCD 9 6
again, it checks to see if the discharged constraint
[W] GCD 6 8 ~ GCD 9 6
Is already solved, is disproven, or unsolved.
If the discharged constraint is solved, it will return:
TcPluginOk [[W] GCD 6 8 + x ~ x + GCD 9 6”] []
If the discharged constraint is dis proven, it returns:
TcPluginContradiction [[W] GCD 6 8 + x ~ x + GCD 9 6”]
And otherwise, it doesn’t do anything:
TcPluginOk [] []

Now, type-checker plugin B, the one that knows about GCD, comes along.
It sees:
[W] GCD 6 8 + x ~ x + GCD 9 6
[W] GCD 6 8 ~ GCD 9 6
I doesn’t know anything about (+); but it does know about GCD, and clearly sees 
that GCD 6 8 is not equal to GCD 9 6.
So it tells that GCD 6 8 ~ GCD 9 6 is insoluble.
In type-checker plugin lingo it says:
TcPluginContradiction [[W] GCD 6 8 ~ GCD 9 6”]

According to 
https://github.com/ghc/ghc/blob/228ddb95ee137e7cef02dcfe2521233892dd61e0/compiler/typecheck/TcInteract.hs#L547
What happens next is that the insoluble constraint
[W] GCD 6 8 ~ GCD 9 6
is taken of the work list for all plugins.
However! the same thing happens when a plugin is able to prove a constraint.
That is, if B would have (erroneously) returned: 
TcPluginOk [[W] GCD 6 8 ~ GCD 9 6”] []

Then there is _no_ way for type-checker plugin A to know what happened.
Were its discharged constraints taken from the work-list because it was 
insoluble? or because it was solved?
This is a problem because to me it seems that the work list is the only way 
that two type-checker plugins can communicate.

I guess my question is: if not through the work list, how are type-checker 
plugins supposed to communicate?
Am I going about it all wrong in terms how I should be writing type-checker 
plugins?
Or, should the type of ‘TcPluginSolver’ 
(https://downloads.haskell.org/~ghc/7.10.1/docs/html/libraries/ghc-7.10.1/TcRnTypes.html#t:TcPluginSolver)
 be updated to?:

```
type TcPluginSolver =  [Ct] -- ^ Given constraints
- [Ct] -- ^ Derived constraints
- [Ct] -- ^ Wanted constraints
- [Ct] -- ^ Insoluble constraints
- TcPluginM TcPluginResult
```

Best regards,

Christiaan




___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


RE: [Diffusion] [Build Failed] rGHCfc8c5e7a5168: Test Trac #8799, #8555

2015-05-19 Thread Simon Peyton Jones
Devs,

The failure seems to be for ghci.debugger/print007.  I can't see the build log 
on Phabricator, so I can't see what went wrong.  Works on my machine.

I do see print007.stderr

no location info: Warning:
-O conflicts with --interactive; -O ignored.

which seems odd.  Why not fix the test?

Simon

|  -Original Message-
|  From: nore...@phabricator.haskell.org
|  [mailto:nore...@phabricator.haskell.org]
|  Sent: 19 May 2015 12:20
|  To: Simon Peyton Jones
|  Subject: [Diffusion] [Build Failed] rGHCfc8c5e7a5168: Test Trac #8799,
|  #8555
|  
|  Harbormaster failed to build B4076: rGHCfc8c5e7a5168: Test Trac #8799,
|  #8555!
|  
|  USERS
|simonpj (Author)
|GHC - Testsuite (Auditor)
|  
|  COMMIT
|https://phabricator.haskell.org/rGHCfc8c5e7a5168
|  
|  EMAIL PREFERENCES
|https://phabricator.haskell.org/settings/panel/emailpreferences/
|  
|  To: simonpj, GHC - Testsuite
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: SV: [Haskell-cafe] RFC: Native -XCPP Proposal

2015-05-19 Thread malcolm.wallace

Yes, this is what I am asking.  Is the LGPL so dangerous to your business, that 
you have taken the steps necessary to build a special GHC using integer-simple 
instead of integer-gmp?  Or are the lawyers happy simply for the option to be 
available, but unexercised?  (If the latter, then I could suggest that ghc 
using cpphs by default, but allowing the option of a different preprocessor, 
might suffice?)
Regards,
   Malcolm

On 19 May, 2015,at 02:51 PM, Niklas Larsson metanik...@gmail.com wrote:

Hi!

GMP is optional, anyone who cares about the license can build with 
integer-simple.

Regards,
Niklas
Från: malcolm.wallace
Skickat: ‎2015-‎05-‎19 13:11
Till: Lars Kuhtz
Kopia: ghc-devs@haskell.org
Ämne: Re: [Haskell-cafe] RFC: Native -XCPP Proposal

How does your company deal with the Integer type, whose standard implementation 
in ghc is via the LGPL'd Gnu multi-precision routines?
Regards,
   Malcolm

On 18 May, 2015,at 09:19 PM, Lars Kuhtz hask...@kuhtz.eu wrote:

I work for PivotCloud. We use Haskell/GHC in our production system on 
the server side and on the client side.


My experience is that any license that contains the string GPL can 
cause problems in an corporate context, no matter if it actually is a 
legal issue or not.


Folks who are responsible for making decisions about legal implications 
of the usage of third party software don't always have experience with 
open source software. Also they are often not familiar with the 
technical details of derived work, different types of linking, or the 
subtleties of distinguishing between build-, link-, and run-time 
dependencies in modern software engineering pipelines. So, any 
mentioning of LGPL (or similar) potentially causes overhead in the 
adaption.


Regards,
Lars

On 5/7/15 11:10 PM, Malcolm Wallace wrote:
Exactly. My post was an attempt to elicit response from anyone to whom it 
matters. There is no point in worrying about hypothetical licensing problems - 
let's hear about the real ones.

Regards,
Malcolm

On 7 May 2015, at 22:15, Tomas Carnecky wrote:

That doesn't mean those people don't exist. Maybe they do but are too afraid to 
speak up (due to corporate policy or whatever).

On Thu, May 7, 2015 at 10:41 PM, Malcolm Wallace malcolm.wall...@me.com wrote:
I also note that in this discussion, so far not a single person has said that 
the cpphs licence would actually be a problem for them.

Regards,
Malcolm

On 7 May 2015, at 20:54, Herbert Valerio Riedel wrote:

On 2015-05-06 at 13:38:16 +0200, Jan Stolarek wrote:

[...]

Regarding licensing issues: perhaps we should simply ask Malcolm
Wallace if he would consider changing the license for the sake of GHC?
Or perhaps he could grant a custom-tailored license to the GHC
project? After all, the project page [1] says:  If that's a problem
for you, contact me to make other arrangements.

Fyi, Neil talked to him[1]:

| I talked to Malcolm. His contention is that it doesn't actually change
| the license of the ghc package. As such, it's just a single extra
| license to add to a directory full of licenses, which is no big deal.


[1]: 
http://www.reddit.com/r/haskell/comments/351pur/rfc_native_xcpp_for_ghc_proposal/cr1e5n3

___
Haskell-Cafe mailing list
haskell-c...@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe


___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


SV: [Haskell-cafe] RFC: Native -XCPP Proposal

2015-05-19 Thread Niklas Larsson
Hi!

GMP is optional, anyone who cares about the license can build with 
integer-simple.

Regards,
Niklas 

- Ursprungligt meddelande -
Från: malcolm.wallace malcolm.wall...@me.com
Skickat: ‎2015-‎05-‎19 13:11
Till: Lars Kuhtz hask...@kuhtz.eu
Kopia: ghc-devs@haskell.org ghc-devs@haskell.org
Ämne: Re: [Haskell-cafe] RFC: Native -XCPP Proposal

How does your company deal with the Integer type, whose standard implementation 
in ghc is via the LGPL'd Gnu multi-precision routines?
Regards,
Malcolm
On 18 May, 2015,at 09:19 PM, Lars Kuhtz hask...@kuhtz.eu wrote:


I work for PivotCloud. We use Haskell/GHC in our production system on 
the server side and on the client side.

My experience is that any license that contains the string GPL can 
cause problems in an corporate context, no matter if it actually is a 
legal issue or not.

Folks who are responsible for making decisions about legal implications 
of the usage of third party software don't always have experience with 
open source software. Also they are often not familiar with the 
technical details of derived work, different types of linking, or the 
subtleties of distinguishing between build-, link-, and run-time 
dependencies in modern software engineering pipelines. So, any 
mentioning of LGPL (or similar) potentially causes overhead in the 
adaption.

Regards,
Lars

On 5/7/15 11:10 PM, Malcolm Wallace wrote:

Exactly. My post was an attempt to elicit response from anyone to whom it 
matters. There is no point in worrying about hypothetical licensing problems - 
let's hear about the real ones.


Regards,
Malcolm


On 7 May 2015, at 22:15, Tomas Carnecky wrote:


That doesn't mean those people don't exist. Maybe they do but are too afraid to 
speak up (due to corporate policy or whatever).


On Thu, May 7, 2015 at 10:41 PM, Malcolm Wallace malcolm.wall...@me.com wrote:
I also note that in this discussion, so far not a single person has said that 
the cpphs licence would actually be a problem for them.


Regards,
Malcolm


On 7 May 2015, at 20:54, Herbert Valerio Riedel wrote:


On 2015-05-06 at 13:38:16 +0200, Jan Stolarek wrote:


[...]


Regarding licensing issues: perhaps we should simply ask Malcolm
Wallace if he would consider changing the license for the sake of GHC?
Or perhaps he could grant a custom-tailored license to the GHC
project? After all, the project page [1] says:  If that's a problem
for you, contact me to make other arrangements.


Fyi, Neil talked to him[1]:


| I talked to Malcolm. His contention is that it doesn't actually change
| the license of the ghc package. As such, it's just a single extra
| license to add to a directory full of licenses, which is no big deal.




[1]: 
http://www.reddit.com/r/haskell/comments/351pur/rfc_native_xcpp_for_ghc_proposal/cr1e5n3


___
Haskell-Cafe mailing list
haskell-c...@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe




___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs



___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: [Diffusion] [Build Failed] rGHCfc8c5e7a5168: Test Trac #8799, #8555

2015-05-19 Thread Austin Seipp
I've reverted this change - it also passes perfectly fine on my
machine, which is why I reverted so I could investigate further, so it
wouldn't hold up any patches people submit (it's much more important
to have HEAD always building because of that!)

I can look into it on the buildbot soon. At the very least, this build
machine seems to be very good at exposing weird edge cases...

On Tue, May 19, 2015 at 6:31 AM, Simon Peyton Jones
simo...@microsoft.com wrote:
 Devs,

 The failure seems to be for ghci.debugger/print007.  I can't see the build 
 log on Phabricator, so I can't see what went wrong.  Works on my machine.

 I do see print007.stderr

 no location info: Warning:
 -O conflicts with --interactive; -O ignored.

 which seems odd.  Why not fix the test?

 Simon

 |  -Original Message-
 |  From: nore...@phabricator.haskell.org
 |  [mailto:nore...@phabricator.haskell.org]
 |  Sent: 19 May 2015 12:20
 |  To: Simon Peyton Jones
 |  Subject: [Diffusion] [Build Failed] rGHCfc8c5e7a5168: Test Trac #8799,
 |  #8555
 |
 |  Harbormaster failed to build B4076: rGHCfc8c5e7a5168: Test Trac #8799,
 |  #8555!
 |
 |  USERS
 |simonpj (Author)
 |GHC - Testsuite (Auditor)
 |
 |  COMMIT
 |https://phabricator.haskell.org/rGHCfc8c5e7a5168
 |
 |  EMAIL PREFERENCES
 |https://phabricator.haskell.org/settings/panel/emailpreferences/
 |
 |  To: simonpj, GHC - Testsuite
 ___
 ghc-devs mailing list
 ghc-devs@haskell.org
 http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs




-- 
Regards,

Austin Seipp, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: RFC: Native -XCPP Proposal

2015-05-19 Thread Bardur Arantsson
On 05/19/2015 11:04 AM, Boespflug, Mathieu wrote:
 On 19 May 2015 at 08:26, Bardur Arantsson s...@scientician.net wrote:
 
 On 05/19/2015 07:31 AM, Carter Schonwald wrote:
 I imagine your ghc build uses gcc to invoke the system assembler and
 linker
 on your Linux servers, :-) and that's gplv3!

 That is of no consequence licensing-wise since those are

a) separate programs/executables, thus derived work doesn't enter
   into it at any level, except...

b) if the output contains bits of of the programs themselves, but
   e.g. gcc (and one assumes the linker, etc.) have specific
   licensing exemptions for the output.

 (And this *is* something that you can quickly explain to the lawyerly
 types.)
 
 
 Both conditions likewise hold true for
 cpphs-as-an-external-process-bundled-with-GHC. So any particular remaining
 concern there?
 
 

Not from me, certainly. I was just trying to point out that the example
given (Linux, gcc, ...) was invalid.

I would be more worried about e.g. Linux distributions *if* cpphs were
under some weird license, but since it's LGPL that shouldn't prompt any
issues. (We're talking mere aggregation in the terms used in the GPL.)

As always, IANAL and in particular I am not *your* or anybody else's
lawyer :).

Regards,


___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs


Re: Interactions between type-checker plugins

2015-05-19 Thread Adam Gundry
Hi Christiaan,

It may well be that we can improve the typechecker plugin interface. In
particular, I at least haven't devoted a great deal of thought to how
multiple plugins work together in practice (although theoretically it is
possible to compose constraint solvers, even establishing termination of
the composition is a bit fiddly).

The thing that surprises me about your email is that when your plugin A sees
[W] GCD 6 8 + x ~ x + GCD 9 6
it emits
[W] GCD 6 8 ~ GCD 9 6
without solving the original constraint, so we end up with
[W] GCD 6 8 + x ~ x + GCD 9 6
[W] GCD 6 8 ~ GCD 9 6
and proceed from there. What I'd expect is for the original constraint
to be declared as solved (because it follows from the new wanted). Then
plugin B will run and notice that the constraint is insoluble; there's
no need for plugin A to keep track of the relationship between the
constraints. Does that make sense? Why does plugin A need to remember
the relationship between constraints it has seen on previous iterations?

Hope this helps,

Adam




On 19/05/15 11:35, Christiaan Baaij wrote:
 Hi,
 
 My apologies for this rather lengthy email.
 
 I have a question about how type-checker plugins should interact.
 My situation is the following:
 I have two type-checker plugins, one that can solve equalities involving the 
 standard type-level operations on kind Nat (+,*,-,^), and another 
 type-checker plugin that can prove equalities involving a new type-level 
 operation GCD.
 In the following, the type-checker plugin involving the stand type-level 
 operations is called ‘A’, and the type checker involving the new GCD 
 operations is called ‘B’.
 
 When type-checker plugin A encounters:
 [W] GCD 6 8 + x ~ x + GCD 9 6
 
 It knows that (+) is commutative, so it can prove the above equality _given_ 
 that GCD 6 8 ~ GCD 9 6” holds.
 So what type-checker plugin A does now is emits a new wanted constraints:
 [W] GCD 6 8 ~ GCD 9 6
 And remembers that it emitted this wanted constraint.
 In type-checker plugin lingo, it returns:
 TcPluginOk [] [[W] GCD 6 8 ~ GCD 9 6”]
 
 Now whenever type-checker plugin encounters
 [W] GCD 6 8 + x ~ x + GCD 9 6
 again, it checks to see if the discharged constraint
 [W] GCD 6 8 ~ GCD 9 6
 Is already solved, is disproven, or unsolved.
 If the discharged constraint is solved, it will return:
 TcPluginOk [[W] GCD 6 8 + x ~ x + GCD 9 6”] []
 If the discharged constraint is dis proven, it returns:
 TcPluginContradiction [[W] GCD 6 8 + x ~ x + GCD 9 6”]
 And otherwise, it doesn’t do anything:
 TcPluginOk [] []
 
 Now, type-checker plugin B, the one that knows about GCD, comes along.
 It sees:
 [W] GCD 6 8 + x ~ x + GCD 9 6
 [W] GCD 6 8 ~ GCD 9 6
 I doesn’t know anything about (+); but it does know about GCD, and clearly 
 sees that GCD 6 8 is not equal to GCD 9 6.
 So it tells that GCD 6 8 ~ GCD 9 6 is insoluble.
 In type-checker plugin lingo it says:
 TcPluginContradiction [[W] GCD 6 8 ~ GCD 9 6”]
 
 According to 
 https://github.com/ghc/ghc/blob/228ddb95ee137e7cef02dcfe2521233892dd61e0/compiler/typecheck/TcInteract.hs#L547
 What happens next is that the insoluble constraint
 [W] GCD 6 8 ~ GCD 9 6
 is taken of the work list for all plugins.
 However! the same thing happens when a plugin is able to prove a constraint.
 That is, if B would have (erroneously) returned: 
 TcPluginOk [[W] GCD 6 8 ~ GCD 9 6”] []
 
 Then there is _no_ way for type-checker plugin A to know what happened.
 Were its discharged constraints taken from the work-list because it was 
 insoluble? or because it was solved?
 This is a problem because to me it seems that the work list is the only way 
 that two type-checker plugins can communicate.
 
 I guess my question is: if not through the work list, how are type-checker 
 plugins supposed to communicate?
 Am I going about it all wrong in terms how I should be writing type-checker 
 plugins?
 Or, should the type of ‘TcPluginSolver’ 
 (https://downloads.haskell.org/~ghc/7.10.1/docs/html/libraries/ghc-7.10.1/TcRnTypes.html#t:TcPluginSolver)
  be updated to?:
 
 ```
 type TcPluginSolver =  [Ct] -- ^ Given constraints
 - [Ct] -- ^ Derived constraints
 - [Ct] -- ^ Wanted constraints
 - [Ct] -- ^ Insoluble constraints
 - TcPluginM TcPluginResult
 ```
 
 Best regards,
 
 Christiaan


-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs