Re: Help with coercion & roles?

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] _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] _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] _N)))_R

And still I get "Role incompatibility: expected nominal, got representational in `Sym (Simple.NTCo:HasIf[0] _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] _N)))_R

-- Conal On Mon, Apr 14, 2014 at 4:39 AM, Richard Eisenberg wrote:

I agree with Simon, but just `Sub` the `_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] _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 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-bounces@haskell.org] *On Behalf Of *Conal Elliott *Sent:* 14 April 2014 06:00 *To:* ghc-devs@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` (_N (Sym (Simple.NTCo:HasIf[0] _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 _N (Sym (Simple.NTCo:HasIf[0] _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