Interactions between type-checker plugins

[Adam Gundry]

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/