TypeChecker plugins and the TcS monad; given constraints in GHC HEAD

[Adam Gundry]

On 27/05/15 23:42, Simon Peyton Jones wrote:
> I like EvTerm as a distinct data type precisely because it
> enumerates all the forms of evidence we need.  Once you allow arbitrary
> CoreExprs, we lose that explicit enumeration. 
> 
> Now, that might be OK.   Evidence terms are proof terms: any well typed
> EvTerm is a proof of the predicate described by its type.  So if a
> CoreExpr has the right type, then it **should** be the case that the
> evidence term is OK (provided it’s not bottom).  So I can’t quite nail
> down why I like the explicit EvTerm; except the relatively minor reason
> that it puts off desugaring to the desugarer.

I can see the appeal of the explicit enumeration of the evidence
generated by GHC itself, but it's obviously not modular. I don't have a
particularly strong opinion about whether the current special-case
constructors should be subsumed by the embedding; this might remove some
boilerplate, but we could also keep the embedding for plugins only. I'm
also open to Richard's idea that we use HsExpr Id instead of CoreExpr if
the former works out more easily.

Can you elaborate on your parenthetical remark "provided it’s not
bottom"? I was under the impression that EvTerms could be bottom (e.g.
`EvDelayedError`) without compromising type safety.


> On a separate matter, can we eliminate the trap-door from
> TcPluginM to TcM?  That is, can you enumerate all the things you need
> from TcPluginM?  The reason I ask is that I’d like to stop building TcS
> on top of TcM, and instead make it a free-standing monad.  Reason: we
> increasingly want to do constraint solving outside a full-blown
> typechecker.  Eg. when doing pattern-match exhaustiveness checks. 
> Faking up a TcM monad with lots of error thunks seems wrong.

It's convenient to have an escape hatch, but I think making TcS a
separate monad is a good idea and I wouldn't like plugins to hold this
up. I don't think plugins are likely to need anything not also needed by
TcS (arbitrary IO perhaps excepted, but hopefully that shouldn't be a
problem).

Beyond the changes in Phab:D909, the only thing I'm still using
unsafeTcPluginTcM for is newUnique (in order to generate new skolem
variables), which could easily be added to the TcPluginM interface as
well. Anyone need anything else?

Adam

-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/