Hi devs,
Currently, type-checker plugins get to tell the solver its progress using a [TcPluginResult](
```
data TcPluginResult
= TcPluginContradiction [Ct]
-- ^ The plugin found a contradiction.
-- The returned constraints are removed from the inert set,
-- and recorded as insoluble.
| TcPluginOk [(EvTerm,Ct)] [Ct]
-- ^ The first field is for constraints that were solved.
-- These are removed from the inert set,
-- and the evidence for them is recorded.
-- The second field contains new work, that should be processed by
-- the constraint solver.
```
So when asked to solve a _set_ of constraints, a tc plugin basically gets to say:
A) This _one_ constraint out of the entire set is wrong, or
B) The following _subset_ of constraints is solved (plus some new wanted constraints)
Supposedly, picking A leads to better error messages when a constraint is obviously bad (i.e. Int ~ Char). However, the issue is that when a tc plugin picks A, then it will not be called again for the whole set of constraint it originally got; which in my use-case basically leads to a complete set of (actually solvable) unsolved constraints.
This is "bad" because it leads to very confusing error messages, when
1. Start with a correct program: All constraints solvable => no errors reported
2. Add one line of code that doesn't type check
3. All constraints unsolvable => errors reported in parts of the program that used to type-check.
I thought of multiple possible solutions, but changing TcPluginResult to:
```
data TcPluginResult
= TcPluginResult
{ contradictions :: [Ct]
-- ^ All of the contradictions the plugin found
, solved :: [(EvTerm,Ct)]
-- ^ Constraints that were solved
, new :: [Ct]
-- ^ New work to be processed by the rest of the constraint solver
}
```
seems the best one as it allows a tc plugin to report _all_ the constraints that are bad, and _all_ the constraints that are bad.
Thoughts? Perhaps a better solution?
Thanks,
Christiaan