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-devs@haskell.org; glasgow-haskell-us...@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-us...@haskell.org > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs