type-checker plugin API/behaviour change

[Simon Peyton Jones]

That looks plausible to me.

The ‘new’ bunch may not actually be new?   Maybe they are some of the inputs that are no contradictory, but not yet solved either?

What about a flag to say “I made some progress”?   Or is that deducible?  Is so, good to explain that.

Caveat: I’m not a user of plugins!  People who are should reply.

Simon

From: ghc-devs <ghc-devs-bounces at haskell.org> On Behalf Of Christiaan Baaij
Sent: 18 July 2018 12:52
To: ghc-devs at haskell.org
Cc: Adam Gundry <adam at well-typed.com>
Subject: type-checker plugin API/behaviour change

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<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fhackage.haskell.org%2Fpackage%2Fghc-8.4.1%2Fdocs%2FTcRnTypes.html%23t%3ATcPluginResult&data=02%7C01%7Csimonpj%40microsoft.com%7C28d3c329dea345e24ae608d5eca4fd21%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636675115733740054&sdata=j3EGsCOaHIIN%2FK313dFXdsMz1JUhFqfdCe3nV9qQmCo%3D&reserved=0>):

```
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/689e7d13/attachment.html>