Hello Richard The code at the bottom ends up compiling to core with the following cast (ParNat (dt1_dor ; (Flip (dt2_dos ; Sym dt_doq))_N ; Nat.TFCo:R:Flip[0]))_R but ParNat is nominal so (I think) shouldn't have a representational cast. The cast is safe as we can just make it nominal and then add Sub but it feels invalid. This doesn't actually create a bug in any program and it may just be a misunderstanding on my part about roles and the differences between roles in Coercible and in the core language. -dcore-lint makes no changes. {-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeFamilies, RoleAnnotations #-} module Nat where data Nat = Z | S Nat data Parity = Even | Odd type family Flip (x :: Parity) :: Parity where Flip Even = Odd Flip Odd = Even type role ParNat nominal data ParNat :: Parity -> * where PZ :: ParNat Even PS :: (x ~ Flip y, y ~ Flip x) => ParNat x -> ParNat (Flip x) halve :: ParNat Even -> Nat halve PZ = Z halve (PS a) = helper a where helper :: ParNat Odd -> Nat helper (PS b) = S (halve b) On 16/08/15 13:34, Richard Eisenberg wrote:

Hi Alex,

Do you have a concrete example? With the -dcore-lint flag, the Core is checked, including all the roles.

Thanks, Richard

On Aug 16, 2015, at 7:47 AM, Alexander Eyers-Taylor wrote:

...

Hello

I have noticed in looking at some core that GADT type constructors are often applied with a representational role. These constructors are explicitly marked as nominal.

Is this information just ignored at a Core level or is this invalid core?

Looking at the code a see that we if we downgrade a TyConAppCo we unconditionally change it to a representational role after changing its children. I think this is where it is introduced.

Alex ET _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

If you're trying to understand core, check out https://github.com/ghc/ghc/blob/master/docs/core-spec/core-spec.pdf which has all the typing rules. It might be helpful. But your analysis below is spot on. Richard On Aug 16, 2015, at 10:19 AM, Alexander Eyers-Taylor wrote:

Hello

I have reread the comment about TyConAppCo and I now understand how it works and this is all how it should work. I was just slightly confused to start with. The coercion was representational but the arguments were nominal.

Thanks

Alex

On 16/08/15 13:34, Richard Eisenberg wrote:

...

Hi Alex,

Do you have a concrete example? With the -dcore-lint flag, the Core is checked, including all the roles.

Thanks, Richard

On Aug 16, 2015, at 7:47 AM, Alexander Eyers-Taylor wrote:

...

Hello

I have noticed in looking at some core that GADT type constructors are often applied with a representational role. These constructors are explicitly marked as nominal.

Is this information just ignored at a Core level or is this invalid core?

Looking at the code a see that we if we downgrade a TyConAppCo we unconditionally change it to a representational role after changing its children. I think this is where it is introduced.

Alex ET _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs