<div dir="ltr"><div><div>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.<div>Here is an output of my testsuite:<br><br></div>```<br>
<div>
<div>
[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]<br><br>tests/ErrorTests.hs:1:1: Warning:<br> Couldn't match type ‘GCD 6 9’ with ‘GCD 6 8’<br> NB: ‘GCD’ is a type function, and may not be injective<br> Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 6 9)<br> Actual type: Proxy (x + GCD 6 9) -> Proxy (x + GCD 6 9)<br><br>tests/ErrorTests.hs:14:13: Warning:<br> Couldn't match type ‘GCD 6 8’ with ‘4’<br> Expected type: Proxy (GCD 6 8) -> Proxy 4<br> Actual type: Proxy 4 -> Proxy 4<br> In the expression: id<br> In an equation for ‘testFail1’: testFail1 = id<br>[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]<br>Linking dist/build/test-ghc-tynat-normalise/test-ghc-tynat-normalise ...<br>Running 1 test suites...<br>Test suite test-ghc-tynat-normalise: RUNNING...<br>ghc-typelits-natnormalise<br> Basic functionality<br> GCD 6 8 ~ 2: OK<br> GCD 6 8 + x ~ x + GCD 10 8: OK<br> errors<br> GCD 6 8 ~ 4: OK<br> GCD 6 8 + x ~ x + GCD 9 6: FAIL<br> No exception!<br><br>1 out of 4 tests failed (0.00s)<span style="font-family:monospace"><br></span></div>
<span style="font-family:monospace"></span></div>
```<br><br></div><div>Note that 'ErrorTest.hs' is compiled with '-fdefer-type-errors'.<br></div><div>There's a two things you may notice<br>* The first error message's location is '1:1'<br></div><div>* Evaluation the function with the type-error does not raise an exception.<br><br></div><div>So by solving the constraint<br>"GCD 6 8 + x ~ x + GCD 9 6"<br></div><div>The boxed/run-time coercion no longer errors.<br></div><div>Also, I'm using newSimpleWanted (<a href="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</a>) to create the new wanted constraint.<br></div><div>But for some reason the errror message doesn't get the source-error location of the original constraint.<br></div><div>Perhaps I shouldn't be using 'newSimpleWanted' to create new wanted constraints?<br></div><div><br></div><div>The sources for the plugins are over here:<br><a href="https://github.com/christiaanb/ghc-typelits-natnormalise">https://github.com/christiaanb/ghc-typelits-natnormalise</a><br><a href="https://github.com/christiaanb/ghc-typelits-extra">https://github.com/christiaanb/ghc-typelits-extra</a><br><br></div><div>Cheers,<br><br></div><div>Christiaan<br></div><div><br></div><div><br></div></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On 19 May 2015 at 18:01, Iavor Diatchki <span dir="ltr"><<a href="mailto:iavor.diatchki@gmail.com" target="_blank">iavor.diatchki@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">Hi Christiaan,<div class="gmail_extra"><br></div><div class="gmail_extra"><br></div><div class="gmail_extra"><div>Plugins should return the solved constraints in the first field of `TcPLuginOk`, and additional sub-goals in the second.</div><div></div></div><div class="gmail_extra">The constraints in the first list are marked as solved, and do not need to be processed further, while the constraints</div><div class="gmail_extra">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.</div><div class="gmail_extra"><br></div><div class="gmail_extra">I think that there are two situations when a plugin might return an empty first list, but new work in the second list.</div><div class="gmail_extra">Both are about computing new facts, and thus "communicating" with other plugins:</div><div class="gmail_extra"> 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)</div><div class="gmail_extra"> 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.</div><div class="gmail_extra"><br></div><div class="gmail_extra">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...</div><div class="gmail_extra"><br></div><div class="gmail_extra">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. </div><div class="gmail_extra"><br></div><div class="gmail_extra">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:</div><div class="gmail_extra"><br></div><div class="gmail_extra">Plugin A: Solve "GCD 6 8 + x ~ x + GCD 9 6", new wanted "GCD 6 8 ~ GCD 9 6"</div><div class="gmail_extra">Plugin B: "GCD 6 8 ~ GCD 9 6" --> impossible<br></div><div class="gmail_extra">Done.</div><span><font color="#888888"><div class="gmail_extra"><br></div><div class="gmail_extra"><br></div><div class="gmail_extra">-Iavor</div></font></span><div><div><div class="gmail_extra"><br></div><div class="gmail_extra"><br></div><div class="gmail_extra"><br></div><div class="gmail_extra">On Tue, May 19, 2015 at 3:35 AM, Christiaan Baaij <span dir="ltr"><<a href="mailto:christiaan.baaij@gmail.com" target="_blank">christiaan.baaij@gmail.com</a>></span> wrote:<br></div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">I have a question about how type-checker plugins should interact.<br>
My situation is the following:<br>
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.<br>
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’.<br>
<br>
When type-checker plugin A encounters:<br>
[W] GCD 6 8 + x ~ x + GCD 9 6<br>
<br>
It knows that (+) is commutative, so it can prove the above equality _given_ that "GCD 6 8 ~ GCD 9 6” holds.<br>
So what type-checker plugin A does now is emits a new wanted constraints:<br>
[W] GCD 6 8 ~ GCD 9 6<br>
And remembers that it emitted this wanted constraint.<br>
In type-checker plugin lingo, it returns:<br>
TcPluginOk [] ["[W] GCD 6 8 ~ GCD 9 6”]<br>
<br></blockquote><div><br></div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Now whenever type-checker plugin encounters<br>
[W] GCD 6 8 + x ~ x + GCD 9 6<br>
again, it checks to see if the discharged constraint<br>
[W] GCD 6 8 ~ GCD 9 6<br>
Is already solved, is disproven, or unsolved.<br>
If the discharged constraint is solved, it will return:<br>
TcPluginOk ["[W] GCD 6 8 + x ~ x + GCD 9 6”] []<br>
If the discharged constraint is dis proven, it returns:<br>
TcPluginContradiction ["[W] GCD 6 8 + x ~ x + GCD 9 6”]<br>
And otherwise, it doesn’t do anything:<br>
TcPluginOk [] []<br>
<br></blockquote><div><br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Now, type-checker plugin B, the one that knows about GCD, comes along.<br>
It sees:<br>
[W] GCD 6 8 + x ~ x + GCD 9 6<br>
[W] GCD 6 8 ~ GCD 9 6<br>
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.<br>
So it tells that GCD 6 8 ~ GCD 9 6 is insoluble.<br>
In type-checker plugin lingo it says:<br>
TcPluginContradiction ["[W] GCD 6 8 ~ GCD 9 6”]<br>
<br>
According to <a href="https://github.com/ghc/ghc/blob/228ddb95ee137e7cef02dcfe2521233892dd61e0/compiler/typecheck/TcInteract.hs#L547" target="_blank">https://github.com/ghc/ghc/blob/228ddb95ee137e7cef02dcfe2521233892dd61e0/compiler/typecheck/TcInteract.hs#L547</a><br>
What happens next is that the insoluble constraint<br>
[W] GCD 6 8 ~ GCD 9 6<br>
is taken of the work list for all plugins.<br>
However! the same thing happens when a plugin is able to prove a constraint.<br>
That is, if B would have (erroneously) returned:<br>
TcPluginOk ["[W] GCD 6 8 ~ GCD 9 6”] []<br>
<br>
Then there is _no_ way for type-checker plugin A to know what happened.<br>
Were its discharged constraints taken from the work-list because it was insoluble? or because it was solved?<br>
This is a problem because to me it seems that the work list is the only way that two type-checker plugins can communicate.<br>
<br>
I guess my question is: if not through the work list, how are type-checker plugins supposed to communicate?<br>
Am I going about it all wrong in terms how I should be writing type-checker plugins?<br>
Or, should the type of ‘TcPluginSolver’ (<a href="https://downloads.haskell.org/~ghc/7.10.1/docs/html/libraries/ghc-7.10.1/TcRnTypes.html#t:TcPluginSolver" target="_blank">https://downloads.haskell.org/~ghc/7.10.1/docs/html/libraries/ghc-7.10.1/TcRnTypes.html#t:TcPluginSolver</a>) be updated to?:<br>
<br>
```<br>
type TcPluginSolver = [Ct] -- ^ Given constraints<br>
-> [Ct] -- ^ Derived constraints<br>
-> [Ct] -- ^ Wanted constraints<br>
-> [Ct] -- ^ Insoluble constraints<br>
-> TcPluginM TcPluginResult<br>
```<br>
<br>
Best regards,<br>
<br>
Christiaan<br>
<br>
<br>
<br>
<br>
</blockquote></div><br></div></div></div></div>
</blockquote></div><br></div></div></div></div>