TypeChecker plugins and the TcS monad; given constraints in GHC HEAD
Simon Peyton Jones
simonpj at microsoft.com
Wed May 27 22:42:03 UTC 2015
I am back from vacation!
Well I am ON vacation, but the children are in bed...
Two thoughts:
· 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.
· 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.
Lastly: would someone like to add Adam’s explanation to the Commentary somewhere?
Simon
From: Iavor Diatchki [mailto:iavor.diatchki at gmail.com]
Sent: 27 May 2015 17:26
To: Adam Gundry; Richard Eisenberg; Simon Peyton Jones
Cc: Christiaan Baaij
Subject: Re: TypeChecker plugins and the TcS monad; given constraints in GHC HEAD
Hi guys,
I am back from vacation! (cc-ing Richard and Simon, as they might also be interested in some of these changes).
I am very much on board with the changes suggested by Adam.
A couple of thoughts:
* GHC already has some support for evaluation of custom type-families, we added it for evaluating + and friends. It might be good to use the same system for custom evaluation in tc-plugins too, even if we have to modify it some. Currently, this is done by having another "flavor" of type constructor (see `FamTyConFlav` in module `TyCon`), namely one that has built-in evaluation rules. The actual details of how the evaluation happens are in module `CoAxiom`, see `BuiltInSynFamily`: the first field is for evaluating the constructor applied to some arguments (the other two are for emitting derived constraints, `sfInteractTop` is for improvements of a constraint on it's own, and `sfInteractIntert` is for interactions with another constraint that already existis).
* If we are going to be modifying `TcEvidence`, I'd be really keen on integrating the evidence for coersions and other evidence a bit more: in particular, it really make sense to allow class predicates in the assumptions of equality constraints. This would allow us to generate evidence for improvements due to interactions of given classes with functional dependencies (e.g., we could express axioms like this: `forall a b c. (C a b, C a c) => (b ~ c)`)
-Iavor
On Tue, May 26, 2015 at 6:34 AM, Adam Gundry <adam at well-typed.com<mailto:adam at well-typed.com>> wrote:
Thanks Christiaan,
Nice work on ghc-tcplugins-extra. Providing a common package that
abstracts away GHC API variations between versions (as far as possible)
seems really useful. I notice you also include a workaround for GHC
#10301, which is good. I'll try to switch over uom-plugin to use it.
As far as I can see, there's no way to bind EvTerms outside TcS; indeed
that's a major part of the point of TcS. I'm inclining towards making
TcPluginM into a wrapper around TcS, then exposing a nice API to create
givens etc.
Perhaps we should put together a list of proposed changes to the plugins
API, in the light of experience writing the things? There are a few
other things I'd like:
* the ability to embed arbitrary Core expressions in EvTerms;
* a new field in TcPlugin to define type-family reductions directly,
rather than having to look for equality constraints involving them;
* serializable CoAxiomRules to allow proper evidence in place of UnivCo
(doing this for families of rules is a bit tricky, but it should be easy
enough to define single axioms).
Anything you'd like to add? Iavor?
Cheers,
Adam
On 21/05/15 18:46, Christiaan Baaij wrote:
> Hi Adam, Iavor,
>
> 1. typechecker-plugins-extra package:
>
> I started on a typechecker-plugin-extra package
> at: https://github.com/clash-lang/ghc-tcplugins-extra
> Which currently
> contains: https://github.com/clash-lang/ghc-tcplugins-extra/blob/master/src/GHC/TcPluginM/Extra.hs
>
> It currently compiles with both GHC 7.10.1 and HEAD.
> Althought the 'newSimpleGiven' function is basically broken in HEAD
> because there is no way to bind the evidence anywhere.
>
> 2. wanted & error messages:
>
> Indeed, I fixed the error message location by using the correct 'CtLoc'.
> I needed the chain of wanted 'EvVar' to get deferred-type-errors working
> properly.
> However, as you say, the proper way to solve this problem it to create
> evidence for the 'parent' wanted in terms of the discharged wanteds.
> Currently I've been using the same thing you can Iavor are using:
> UnivCo, the unsafeCoerce of EvTerms.
> I'll investigate if I can somehow manage to properly solve this problem.
> At least the fallback mechanism I've implemented already is currently
> working.
>
> 3. TcS vs TcM
> If we keep TcPluginM as a wrapper around TcM, do you know "where" we
> could bind EvTerms so that other parts of the constraint solving
> pipeline can also access them?
> Are these EvTerms bound in some IORef'd environment which we can access
> in TcM?
>
> Cheers,
>
> Christiaan
>
> On 21 May 2015 at 18:51, Adam Gundry <adam at well-typed.com<mailto:adam at well-typed.com>
> <mailto:adam at well-typed.com<mailto:adam at well-typed.com>>> wrote:
>
> Hi Christiaan,
>
> Thanks for your emails, and sorry I can't quite keep up with them! Let
> me try to tackle the issues you raise, in no particular order:
>
>
> 1. TcS vs. TcM
>
> There's no immediate problem with running plugins in TcS rather than
> TcM. Indeed, this was my original proposal, but we decided otherwise
> because TcS is really supposed to capture the internal state of GHC's
> constraint solver, which shouldn't (in principle) be of interest to
> plugins. That is, plugins are deliberately not given access to the inert
> set (and hence its cache of solved constraints), because we want to
> build an interface that is independent of GHC's particular constraint
> solving algorithm. At least that's the goal...
>
>
> 2. Disappearance of ctev_evtm
>
> I don't follow HEAD closely enough to have spotted this, so thanks for
> pointing it out. It looks like the change is indeed a problem for
> plugins, because the plugin interface indeed doesn't offer the
> integration with TcS necessary to create evidence variables that are
> already bound. I guess we should add a function to TcPluginM to bind an
> evidence variable. In fact, probably we should offer functions in
> TcPluginM that look something like
>
> newWanted :: CtLoc -> PredType -> TcPluginM CtEvidence
> newDerived :: CtLoc -> PredType -> TcPluginM CtEvidence
> newGiven :: CtLoc -> PredType -> EvTerm -> TcPluginM CtEvidence
>
> (or perhaps CtOrigin instead of CtLoc? I can never remember the
> difference).
>
>
> 3. On wanteds and error messages
>
> I've not come across the issues you mention with error message locations
> and deferred type errors, but I guess that might be because my plugin
> tends to spot insoluble constraints fairly early (rather than
> simplifying constraints that subsequently turn out to be insoluble on a
> later iteration).
>
> The way this ought to work is that a plugin should solve a wanted with
> an evidence term that contains a reference to a new wanted, rather than
> completely bogus evidence; this should ensure that deferred type errors
> fire correctly. But in practice that might be difficult at the moment.
>
> In general, I like the idea of a typechecker-plugin-extra package to
> bundle up useful common plugin functionality, some of which may later be
> moved into GHC itself. (We could start with those functions above!)
> Perhaps it could also provide some measure of stability across GHC
> releases. I've not yet convinced myself that the trick you describe for
> creating chains of wanteds is really necessary to get good error
> locations, but if it is, making it part of such a package is a good
> plan.
>
> Cheers,
>
> Adam
>
>
>
> On 21/05/15 09:39, Christiaan Baaij wrote:
> > Hi Adam, Hi Iavor,
> >
> > While working on creating my type-checker plugins, I noticed that
> there are some functions in operate in the ’TcS’ monad that I would
> like to use.
> > In an earlier email, for example, Iavor suggested that I use
> ‘newWantedEvVar’ to create new wanted constraints, but this operates
> in the ’TcS’ monad.
> > Of course, there’s ‘runTcS’, but this creates a TcS monad with an
> empty ‘Bag' of ‘EvBind’.
> > What this means, is that (I think), ‘newWantedEvVar’ and
> ‘newWantedEvVarNC’, basically behave the same when run inside
> ‘runTcS’, because ‘newWantedEvVar’ is going to look for existing
> evidence in an empty ‘Bag’…
> >
> > Also, I saw that plugins are run by the functions in the
> ‘TcInteract’ module, which all run inside the ‘TcS’ monad.
> > So my question is, would it make sense to make ‘TcPluginM’ a
> wrapper around ‘TcS’ instead of ‘TcM’?
> > I understand that it would mean
> >
> > tcPluginIO :: IO a -> TcPluginM a
> >
> > would have to be specified in terms of either
> ‘TcSMonad.wrapErrTcS’ or ‘TsSMonad.wrapErrTcS’ and violate the
> purpose of those functions.
> > Anyhow, that’s my question/suggestion with regards to the TcS monad.
> > On to the other part.
> >
> >
> > I noticed that both your plugins store the Coercion/Evidence for a
> new Given constraint in the ‘ctev_evtm’ field of the ‘CtGiven’
> constructor.
> > However, in GHC HEAD, this field no longer exists…
> > In GHC HEAD, there is only ‘ctev_evar’, of type ‘EvVar’, in the
> ‘CtGiven’ constructor.
> > I think Simon PJ refactored this because nowhere else in the GHC
> compiler was ‘ctev_evtm’ used to store anything else than an identifier…
> > The reason being that the evidence was stored ‘TcSEnv’ passed
> around in the TcS monad.
> > So in GHC HEAD, I think there’s no longer any way create new
> Givens of which their evidence can be stored somewhere…
> > Perhaps one of you two knows how to store evidence of a Given in
> GHC HEAD?
> >
> > Best regards,
> >
> > Christiaan
> >
--
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20150527/b0e2887b/attachment-0001.html>
More information about the ghc-devs
mailing list