Interactions between type-checker plugins

Wed May 20 21:51:14 UTC 2015

Hi,

I am not sure about the "deferred type errors", as I never use that feature.

To create new wanted variables, usually you use "newWantedEvVar".
This gives you some evidence (well, really a place-holder for the actual
evidence), and a "freshness" flag.   You do two different things depending
on the freshness:

   - If the evidence is "Fresh", then you have a brand new wanted
constraint and you emit it as a new sub-goal (i.e., the usual thing)
   - if the evidence is cached, this means that this same constraint
already exists;  in that case you can use the returned evidence as needed,
but you don't emit a new wanted constraint.

This is a bit nicer than the "newWantedEvVarNC" as it generates fewer
constraints.

-Iavor

On Wed, May 20, 2015 at 12:26 AM, Christiaan Baaij <
christiaan.baaij at gmail.com> wrote:

> Hi Iavor, Adam, List,
>
> I managed to fix the error message location by using:
> `newWantedEvVarNC`(
> https://downloads.haskell.org/~ghc/7.10.1/docs/html/libraries/ghc-7.10.1/TcSMonad.html#v:newWantedEvVarNC
> )
>
> So now the output of my test suite is:
> ```
> [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: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
>
> tests/ErrorTests.hs:17:13: 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)
>     In the expression: id
>     In an equation for ‘testFail2’: testFail2 = 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.01s)
> ```
>
> But evaluating the expression still doesn’t throw an exception because I
> solved the original constraint.
>
> — Christiaan
>
> On 19 May 2015, at 18:44, Christiaan Baaij <christiaan.baaij at gmail.com>
> wrote:
>
> 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/20150520/051ae422/attachment-0001.html>