Help with coercion & roles?

[Richard Eisenberg]

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/glasgow-haskell-users/attachments/20140414/854b4aab/attachment-0001.html>