type-checker plugin API/behaviour change

Christiaan Baaij christiaan.baaij at gmail.com
Wed Jul 18 11:52:19 UTC 2018


Hi devs,

Currently, type-checker plugins get to tell the solver its progress using a
[TcPluginResult](
http://hackage.haskell.org/package/ghc-8.4.1/docs/TcRnTypes.html#t: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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20180718/03b46143/attachment.html>


More information about the ghc-devs mailing list