Proposed changes to typechecker plugins API

[Jan Bracker]

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#EmbeddingCoreExprinEvTerm
>
>
>
> 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.10changestoTcPluginMAPI
> >
> > Questions/review/comments very welcome.
> >
> > Adam
> >
> >
> > --
> > Adam Gundry, Haskell Consultant
> > Well-Typed LLP, http://www.well-typed.com/
> > _______________________________________________
> > ghc-devs mailing list
> > ghc-devs at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20150528/63daf31b/attachment.html>