<div dir="ltr">Hi devs,<div><br></div><div>Currently, type-checker plugins get to tell the solver its progress using a [TcPluginResult](</div><div><a href="http://hackage.haskell.org/package/ghc-8.4.1/docs/TcRnTypes.html#t:TcPluginResult">http://hackage.haskell.org/package/ghc-8.4.1/docs/TcRnTypes.html#t:TcPluginResult</a>):<br></div><div><br></div><div>```</div><div><div>data TcPluginResult</div><div>  = TcPluginContradiction [Ct]</div><div>    -- ^ The plugin found a contradiction.</div><div>    -- The returned constraints are removed from the inert set,</div><div>    -- and recorded as insoluble.</div><div><br></div><div>  | TcPluginOk [(EvTerm,Ct)] [Ct]</div><div>    -- ^ The first field is for constraints that were solved.</div><div>    -- These are removed from the inert set,</div><div>    -- and the evidence for them is recorded.</div><div>    -- The second field contains new work, that should be processed by</div><div>    -- the constraint solver.</div></div><div>```</div><div><br></div><div>So when asked to solve a _set_ of constraints, a tc plugin basically gets to say:</div><div><br></div><div>A) This _one_ constraint out of the entire set is wrong, or</div><div>B) The following _subset_ of constraints is solved (plus some new wanted constraints)</div><div><br></div><div>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.</div><div>This is "bad" because it leads to very confusing error messages, when</div><div><br></div><div>1. Start with a correct program: All constraints solvable => no errors reported</div><div>2. Add one line of code that doesn't type check</div><div>3. All constraints unsolvable => errors reported in parts of the program that used to type-check.</div><div><br></div><div>I thought of multiple possible solutions, but changing TcPluginResult to:</div><div><br></div><div>```</div><div><div>data TcPluginResult</div><div>  = TcPluginResult</div><div>  { contradictions :: [Ct]</div><div>  -- ^ All of the contradictions the plugin found</div><div>  , solved :: [(EvTerm,Ct)]</div><div>  -- ^ Constraints that were solved</div><div>  , new :: [Ct]</div><div>  -- ^ New work to be processed by the rest of the constraint solver</div><div>  }</div></div><div>```</div><div><br></div><div>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.</div><div><br></div><div>Thoughts? Perhaps a better solution?</div><div><br></div><div>Thanks,</div><div><br></div><div>Christiaan</div></div>