A question about roles.

Alexander Eyers-Taylor aeyerstaylor11 at gmail.com
Sun Aug 16 14:12:59 UTC 2015

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

More information about the ghc-devs mailing list