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/com... 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/TcR...) 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/