Missing role annotations on SNat, SSymbol, SChar lead to disaster
Summary
The SNat
, SSymbol
and SChar
newtypes have no role annotation, and hence are inferred as having a phantom role. This is utterly unsafe as they need to have a nominal role.
Steps to reproduce
The following module exploits this to implement unsafeCoerce
:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
module SNatBroken where
import Data.Coerce (coerce)
import Data.Kind (Type)
import Data.Type.Equality
import GHC.TypeNats
bogus :: forall a b . KnownNat a => a :~: b
bogus = case testEquality (SNat @a) (coerce (SNat @a) :: SNat b) of
Just r -> r
Nothing -> error "bug fixed"
type G :: Nat -> Type -> Type -> Type
type family G n s t where
G 0 s _ = s
G _ _ t = t
newtype N n s t = MkN { unN :: G n s t }
oops :: forall b s t . N 0 s t -> N b s t
oops x = gcastWith (bogus @0 @b) x
unsafeCoerce :: s -> t
unsafeCoerce x = unN (oops @1 (MkN x))
Expected behavior
The definition of bogus
should be rejected. In particular coerce (SNat @a) :: SNat b
would be forbidden if SNat
had a nominal role, but since it has phantom role, the definition goes through.
Environment
GHC version used: 9.6.1
The reproducer above doesn't work with earlier GHC versions because SNat
was not directly exposed. However the underlying bug exists and may well lead to similar disasters in earlier versions.