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