Interactions between type-checker plugins
Adam Gundry
adam at well-typed.com
Tue May 19 16:00:53 UTC 2015
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/
More information about the ghc-devs
mailing list