Interactions between type-checker plugins

Tue May 19 16:44:15 UTC 2015

I have yet to test this properly, but I don't think your suggestions (which
you happen to give with 1 minute of eachother...) play nicely with error
reporting.
Here is an output of my testsuite:

```
 [1 of 2] Compiling ErrorTests       ( tests/ErrorTests.hs,
dist/build/test-ghc-tynat-normalise/test-ghc-tynat-normalise-tmp/ErrorTests.o
) [GHC.TypeLits.Normalise changed]

tests/ErrorTests.hs:1:1: Warning:
   Couldn't match type ‘GCD 6 9’ with ‘GCD 6 8’
   NB: ‘GCD’ is a type function, and may not be injective
   Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)
     Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)

tests/ErrorTests.hs:14:13: Warning:
   Couldn't match type ‘GCD 6 8’ with ‘4’
   Expected type: Proxy (GCD 6 8) -> Proxy 4
     Actual type: Proxy 4 -> Proxy 4
   In the expression: id
   In an equation for ‘testFail1’: testFail1 = id
[2 of 2] Compiling Main             ( tests/Main.hs,
dist/build/test-ghc-tynat-normalise/test-ghc-tynat-normalise-tmp/Main.o )
[GHC.TypeLits.Normalise changed]
Linking dist/build/test-ghc-tynat-normalise/test-ghc-tynat-normalise ...
Running 1 test suites...
Test suite test-ghc-tynat-normalise: RUNNING...
ghc-typelits-natnormalise
 Basic functionality
   GCD 6 8 ~ 2:                OK
   GCD 6 8 + x ~ x + GCD 10 8: OK
 errors
   GCD 6 8 ~ 4:                OK
   GCD 6 8 + x ~ x + GCD 9 6:  FAIL
     No exception!

1 out of 4 tests failed (0.00s)
 ```

Note that 'ErrorTest.hs' is compiled with '-fdefer-type-errors'.
There's a two things you may notice
* The first error message's location is '1:1'
* Evaluation the function with the type-error does not raise an exception.

So by solving the constraint
"GCD 6 8 + x ~ x + GCD 9 6"
The boxed/run-time coercion no longer errors.
Also, I'm using newSimpleWanted (
https://downloads.haskell.org/~ghc/7.10.1/docs/html/libraries/ghc-7.10.1/TcMType.html#v:newSimpleWanted)
to create the new wanted constraint.
But for some reason the errror message doesn't get the source-error
location of the original constraint.
Perhaps I shouldn't be using 'newSimpleWanted' to create new wanted
constraints?

The sources for the plugins are over here:
https://github.com/christiaanb/ghc-typelits-natnormalise
https://github.com/christiaanb/ghc-typelits-extra

Cheers,

Christiaan

On 19 May 2015 at 18:01, Iavor Diatchki <iavor.diatchki at gmail.com> wrote:

> Hi Christiaan,
>
>
> Plugins should return the solved constraints in the first field of
> `TcPLuginOk`, and additional sub-goals in the second.
> The constraints in the first list are marked as solved, and do not need to
> be processed further,  while the constraints
> in the second list will be added to the work queue, for further
> processing.  Also, the solutions of wanted goals may be in terms of other
> as yet unsolved things.
>
> I think that there are two situations when a plugin might return an empty
> first list, but new work in the second list.
> Both are about computing new facts, and thus "communicating" with other
> plugins:
>    1. Discover new given facts:  the plugin was presented with some
> givens, and it computed some additional givens that it thinks might be of
> use to someone else (typically these are equality constraints)
>    2. Discover new derived facts:  the plugin was presented with a mixture
> of wanted and givens, and it thinks that the new derived facts might be
> useful by specializing the problem----derived facts help with type
> inference by instantiating unification variables.
>
> Generally, I don't think a plugin should ever need to emit new wanted
> constraints without solving anything. It'd be interesting if that could
> happen though...
>
> Another thing that might be relevant: at present, GHC's constraint solver
> does not do back tracking.  So there is no way for a plugin (or other parts
> of the constraint solver) to say: "I'll emit this new wanted constraint,
> and depending on if it was proved or disproved do something".   Another way
> to think of his is that constraints are either solved or unsolved, but
> being unsolved does not mean that they are disproved.  Now, there is a
> mechanism to mark a constraint as "never solvable", but currently this is
> mostly used for error reporting.
>
> For your concrete example though, the plugin can actually commit to the
> given path because the only way to solve "GCD 6 8 + x ~ x + GCD 9 6" is if
> "GCD 6 8 ~ GCD 9 6".  So I'd imagine you want these steps:
>
> Plugin A: Solve "GCD 6 8 + x ~ x + GCD 9 6", new wanted "GCD 6 8 ~ GCD 9 6"
> Plugin B: "GCD 6 8 ~ GCD 9 6" --> impossible
> Done.
>
>
> -Iavor
>
>
>
> On Tue, May 19, 2015 at 3:35 AM, Christiaan Baaij <
> christiaan.baaij at gmail.com> wrote:
>
>> 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
>>
>>
>>
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20150519/349e91d2/attachment-0001.html>