A question about roles.

[Alexander Eyers-Taylor]

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 <aeyerstaylor11 at gmail.com> 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 at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs