Help with coercion & roles?

[Conal Elliott]

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 <eir at 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 <simonpj at 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-bounces at haskell.org] *On Behalf Of *Conal Elliott
> *Sent:* 14 April 2014 06:00
> *To:* ghc-devs at haskell.org; glasgow-haskell-users at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20140414/f10d64d9/attachment.html>