Re: Proposed changes to typechecker plugins API
Hi Adam, Hi Eric, At least for what I want to use them for [1] it would be nice if there was an easy way to say: If you are stuck on solving "Constraint a b TypeC", then you should pick, e.g.: - "a ~ TypeA" and "b ~ TypeB" (What I am actually trying to say is: use the instance "Constraint TypeA TypeB TypeC") - "a ~ b" Currently I am producing equality constraints, like this: mkDerivedTypeEqCt :: TcTyVar -> TcType -> TcPluginM Ct mkDerivedTypeEqCt tyVar ty = do (_, lclEnv) <- getEnvs return $ CTyEqCan { cc_ev = CtDerived -- :: CtEvidence { ctev_pred = ty -- :: TcPredType -- This matches type-wise, but I have no idea what actually belongs here. , ctev_loc = mkGivenLoc topTcLevel (UnifyForAllSkol [tyVar] ty) lclEnv -- :: CtLoc -- Again no idea what actually belongs here: -- topTcLevel :: TcLevel -- To what does this relate? I guess top level -- is ok for equality constraints -- (UnifyForAllSkol [tyVar] ty) :: SkolemInfo -- This one matches what we have at disposal (no idea if it is the right one). -- lclEnv :: TcLclEnv -- I just use the only one I know. } , cc_tyvar = tyVar -- :: TcTyVar , cc_rhs = ty -- :: TcType , cc_eq_rel = NomEq -- :: EqRel -- Alternative would be ReprEq. Whats the difference? } Which seems to be working, but still leaves a lot of open questions (see comments). Maybe my problems using the API are more related to missing documentation, then lack of API functionality. Jan [1]: https://mail.haskell.org/pipermail/ghc-devs/2015-February/008414.html On Wed, 27 May 2015 07:13:37, Eric Seidel wrote:
Hi Adam,
I like the addition of the new* functions for creating constraints, that should make for a much nicer API than dealing directly with the CtEvidence constructors!
I'm not so convinced however about embedding arbitrary CoreExprs in EvTerms. First of all, it feels a bit strange to generate CoreExprs before the desugarer (and we would have to add a `MonadThings TcPluginM` instance to generate Integer and String CoreExprs).
But more importantly, based on your wiki page [1], it sounds like what we really want is a nice API for creating dictionaries.
Eric
[1]:
https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#EmbeddingCoreExpri...
On Wed, May 27, 2015, at 01:33, Adam Gundry wrote:
Hi devs,
I thought I should flag up some proposed changes relating to typechecker plugins, which Christiaan, Iavor and I have been discussing. The quick summary:
* make it possible for plugins to create constraints (Phab:D909);
* make it easier for plugins to define special type families;
* embed CoreExpr in EvTerm.
For more details, see the wiki page:
https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Post-7.10changesto...
Questions/review/comments very welcome.
Adam
-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/ _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Hi Jan, Sadly I think your problems are more to do with lack of documentation in the GHC API in general, than the specific extension I'm proposing! Your use case should be possible with the existing setup: the easiest way is probably something like this (untested): mkNonCanonical $ CtDerived (mkTcEqPred (mkTyVarTy tyVar) ty) loc where loc = ctev_loc (cc_ev c) Here `c` should be the `Ct` you started with; reusing its `ctev_loc` makes it appear as if the new derived constraint came from the same location. Non-canonical constraints are those that have not yet been processed by GHC's constraint solver, which is fine for constraints generated by plugins. Hope this helps, Adam On 28/05/15 13:35, Jan Bracker wrote:
Hi Adam, Hi Eric,
At least for what I want to use them for [1] it would be nice if there was an easy way to say:
If you are stuck on solving "Constraint a b TypeC", then you should pick, e.g.: - "a ~ TypeA" and "b ~ TypeB" (What I am actually trying to say is: use the instance "Constraint TypeA TypeB TypeC") - "a ~ b"
Currently I am producing equality constraints, like this:
mkDerivedTypeEqCt :: TcTyVar -> TcType -> TcPluginM Ct mkDerivedTypeEqCt tyVar ty = do (_, lclEnv) <- getEnvs return $ CTyEqCan { cc_ev = CtDerived -- :: CtEvidence { ctev_pred = ty -- :: TcPredType -- This matches type-wise, but I have no idea what actually belongs here. , ctev_loc = mkGivenLoc topTcLevel (UnifyForAllSkol [tyVar] ty) lclEnv -- :: CtLoc -- Again no idea what actually belongs here: -- topTcLevel :: TcLevel -- To what does this relate? I guess top level -- is ok for equality constraints -- (UnifyForAllSkol [tyVar] ty) :: SkolemInfo -- This one matches what we have at disposal (no idea if it is the right one). -- lclEnv :: TcLclEnv -- I just use the only one I know. } , cc_tyvar = tyVar -- :: TcTyVar , cc_rhs = ty -- :: TcType , cc_eq_rel = NomEq -- :: EqRel -- Alternative would be ReprEq. Whats the difference? }
Which seems to be working, but still leaves a lot of open questions (see comments).
Maybe my problems using the API are more related to missing documentation, then lack of API functionality.
Jan
[1]: https://mail.haskell.org/pipermail/ghc-devs/2015-February/008414.html
-- Adam Gundry, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/
participants (2)
-
Adam Gundry -
Jan Bracker