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 <[email protected]>
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
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
