Interactions between type-checker plugins

[Christiaan Baaij]

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