TcPluginContradiction understanding problem and converting Type to Typeable
Hello, I'm writing a type-checker plugin for ghc, and I'm stuck on two problems. I can't understand how does TcPluginContradiction work. My problem is, when I do TcPluginContradiction listOfFailedConstraints and run the plugin on something which should fail, compiler output contains strange errors for places which doesn't produce any errors when the rest type checks. And it can be seen from debug that listOfFailedConstraints does contain only the constraints that are expected to fail.
For example my plugin should type check Set '[Int]) ~ Set '[Int, Int], and should not Set '[Int, Bool, Int] ~ Set '[Int]. And everything is great when I run it on the first case, but if I run it on the both first and second, the compiler output will contain «Couldn't match type ‘Set '[Int]’ with ‘Set '[Int, Int]’» and «Couldn't match type ‘Set '[Int, Bool, Int]’ with ‘Set '[Int]’».
Re: TcPluginContradiction understanding problem and converting Type to Typeable
TcPluginContradiction is intended to be used when the set of constraints
provided to the plugin is inherently impossible to solve (and that GHC
or other plugins should give up trying). Unfortunately it doesn't
provide a way to say "I solved some constraints, but not others".
Instead, I think you can simply return TcPluginOk with the constraint
you have solved, and no new constraints. The unsolved constraint will
still be reported as an error.
No doubt this interface could be improved and better documented!