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/