Thanks for the pointers! I don't quite know how to get to the form you recommend from the existing coercion, which is `Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N`. (Note the `_N`.) I got that coercion in GHC 7.8.2 from the following code:
> class HasIf a where > ifThenElse :: Bool -> a -> a -> a > > instance HasIf Bool where > ifThenElse i t e = (i && t) || (not i && e) With `--dump-tc`, I see > TYPE SIGNATURES > TYPE CONSTRUCTORS > HasIf :: * -> Constraint > class HasIf a > Roles: [nominal] > RecFlag NonRecursive > ifThenElse :: Bool -> a -> a -> a > COERCION AXIOMS > axiom Main.NTCo:HasIf :: HasIf a = Bool -> a -> a -> a > INSTANCES > instance HasIf Bool -- Defined at ../test/HasIf.hs:4:10 Do I need to convert the nominal coercion I got from GHC (`Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N` in this case) to a representational one? If so, how? My current formulation (tweaked to use `mkSubCo` and `mkAppCo`) is to apply `mkAppCo (mkSubCo (Refl Nominal ep))` to the given coercion, which then produces > (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N)))_R And still I get "Role incompatibility: expected nominal, got representational in `Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N)`". I also tried wrapping `mkSubCo` around the entire coercion (applying `mkSubCo . mkAppCo (Refl Nominal ep)`), and I see the same result: > (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N)))_R -- Conal On Mon, Apr 14, 2014 at 4:39 AM, Richard Eisenberg <e...@cis.upenn.edu>wrote: > I agree with Simon, but just `Sub` the `<LambdaCCC.Lambda.EP>_N`, not the > whole coercion. > > There are actually two problems here. The one Simon identified, and also > the fact that Simple.NTCo:HasIf[0] produces a representational coercion. > How do I know? Because of the `NT` -- it's a newtype axiom and must produce > representational coercions. Furthermore, unless the newtype definition is > inferred to require a nominal parameter, the newtype would expect a > representational coercion, not the nominal one you are passing. Check the > dump (using -ddump-tc) of the newtype axiom to be sure. > > Though putting a `Sub` on `<EP>` and changing the Refl constructor on > `<Bool>` would work, you would then be violating an invariant of GHC's > Coercion type: that we prefer `TyConAppCo tc ...` over `AppCo (Refl > (TyConApp tc [])) ...`. > > In sum, here is the coercion I think you want: > > (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_R)))_R > > This is one of the problems with roles -- they are *very* fiddly within > GHC, and it's hard for a non-expert in roles to get them right. > > Have you seen docs/core-spec/core-spec.pdf? That is updated w.r.t. roles > and may be of help. > > Let me know if I can help further! > Richard > > On Apr 14, 2014, at 5:45 AM, Simon Peyton Jones <simo...@microsoft.com> > wrote: > > I think you need a ‘Sub’. > > A cast (e `cast` g) requires a representational coercion. I think you > have given it a (stronger) nominal one. Sub gets from one to t’other. > > Simon > > *From:* Glasgow-haskell-users [mailto:glasgow- > haskell-users-boun...@haskell.org] *On Behalf Of *Conal Elliott > *Sent:* 14 April 2014 06:00 > *To:* ghc-d...@haskell.org; glasgow-haskell-users@haskell.org > *Subject:* Help with coercion & roles? > > > I’m working on a GHC plugin (as part of my Haskell-to-hardware work) and > running into trouble with coercions & roles. Error message from Core Lint: > > Warning: In the expression: > > > > LambdaCCC.Lambda.lamvP# > > @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) > > @ (Simple.HasIf GHC.Types.Bool) > > "tpl"# > > ((LambdaCCC.Lambda.varP# > > @ (GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) > > "tpl"#) > > `cast` (<LambdaCCC.Lambda.EP>_N (Sym (Simple.NTCo:HasIf[0] > <GHC.Types.Bool>_N)) > > ∷ LambdaCCC.Lambda.EP > > (GHC.Types.Bool > > → GHC.Types.Bool → GHC.Types.Bool → GHC.Types.Bool) > > ~# > > LambdaCCC.Lambda.EP (Simple.HasIf GHC.Types.Bool))) > > Role incompatibility: expected nominal, got representational > > in <LambdaCCC.Lambda.EP>_N (Sym (Simple.NTCo:HasIf[0] <GHC.Types.Bool>_N)) > > Do you see anything inconsistent/incompatible in the coercions or roles > above? I constructed the nominal EP Refl coercion, and applied it (AppCo) > an existing coercion of a simpler type. > > Thanks, > -- Conal > _______________________________________________ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > > >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users