Proposed changes to typechecker plugins API

[Adam Gundry]

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/