Help with coercion & roles?

[Richard Eisenberg]

Hi Conal,

In your case, the `_N` on the argument to NTCo:HasIf[0] is correct -- the `HasIf` class indeed has a nominal parameter. So, it seems that this part, at least, is OK.

What's the -ddump-tc on EP? Is EP's role nominal? (I think so, given what you're saying.) If that's the case, you won't be able to pass the result of NTCo:HasIf[0] to a coercion built from EP.

Popping up a level, what are you trying to do here? If EP's role is indeed nominal, then I don't believe there's a fix here, as the coercion it seems you're trying to build may be unsound. (It looks to me like you want something proving `EP (Bool -> Bool -> Bool -> Bool) ~R EP (HasIf Bool)`, but if EP's role is nominal, then this is indeed bogus.)

Richard

On Apr 14, 2014, at 2:23 PM, Conal Elliott <conal at conal.net> wrote:

> 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/05fc8c94/attachment-0001.html>