Interactions between type-checker plugins

Wed May 20 07:26:12 UTC 2015

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 <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 <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-natnormalise>
> https://github.com/christiaanb/ghc-typelits-extra <https://github.com/christiaanb/ghc-typelits-extra>
> 
> Cheers,
> 
> Christiaan
> 
> 
> 
> On 19 May 2015 at 18:01, Iavor Diatchki <iavor.diatchki at gmail.com <mailto: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 <mailto: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 <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 <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/6ea65909/attachment-0001.html>