[Git][ghc/ghc][wip/t23454] Add role annotations to SNat, SSymbol and SChar

[Matthew Pickering (@mpickering)]

Matthew Pickering pushed to branch wip/t23454 at Glasgow Haskell Compiler / GHC


Commits:
5988803e by Matthew Pickering at 2023-06-05T17:59:15+01:00
Add role annotations to SNat, SSymbol and SChar

Ticket #23454 explained it was possible to implement unsafeCoerce
because SNat was lacking a role annotation.

As these are supposed to be singleton types but backed by an efficient
representation the correct annotation is nominal to ensure these kinds
of coerces are forbidden.

These annotations were missed from https://github.com/haskell/core-libraries-committee/issues/85
which was implemented in 532de36870ed9e880d5f146a478453701e9db25d.

Fixes #23454

- - - - -


5 changed files:

- libraries/base/GHC/TypeLits.hs
- libraries/base/GHC/TypeNats.hs
- + libraries/base/tests/T23454.hs
- + libraries/base/tests/T23454.stderr
- libraries/base/tests/all.T


Changes:

=====================================
libraries/base/GHC/TypeLits.hs
=====================================
@@ -15,6 +15,7 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE RoleAnnotations #-}
 
 {-|
 GHC's @DataKinds@ language extension lifts data constructors, natural
@@ -340,6 +341,7 @@ withSomeSNat n k
 --
 -- @since 4.18.0.0
 newtype SSymbol (s :: Symbol) = UnsafeSSymbol String
+type role SSymbol nominal
 
 -- | A explicitly bidirectional pattern synonym relating an 'SSymbol' to a
 -- 'KnownSymbol' constraint.
@@ -442,6 +444,7 @@ withSomeSSymbol s k = k (UnsafeSSymbol s)
 --
 -- @since 4.18.0.0
 newtype SChar (s :: Char) = UnsafeSChar Char
+type role SChar nominal
 
 -- | A explicitly bidirectional pattern synonym relating an 'SChar' to a
 -- 'KnownChar' constraint.


=====================================
libraries/base/GHC/TypeNats.hs
=====================================
@@ -16,6 +16,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE RoleAnnotations #-}
 
 {-| This module is an internal GHC module.  It declares the constants used
 in the implementation of type-level natural numbers.  The programmer interface
@@ -344,6 +345,7 @@ cmpNat x y = case compare (natVal x) (natVal y) of
 --
 -- @since 4.18.0.0
 newtype SNat (n :: Nat) = UnsafeSNat Natural
+type role SNat nominal
 
 -- | A explicitly bidirectional pattern synonym relating an 'SNat' to a
 -- 'KnownNat' constraint.


=====================================
libraries/base/tests/T23454.hs
=====================================
@@ -0,0 +1,27 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T23454 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))


=====================================
libraries/base/tests/T23454.stderr
=====================================
@@ -0,0 +1,21 @@
+
+T23454.hs:12:38: error: [GHC-25897]
+    • Couldn't match type ‘a’ with ‘b’ arising from a use of ‘coerce’
+      ‘a’ is a rigid type variable bound by
+        the type signature for:
+          bogus :: forall (a :: Nat) (b :: Nat). KnownNat a => a :~: b
+        at T23454.hs:11:1-43
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          bogus :: forall (a :: Nat) (b :: Nat). KnownNat a => a :~: b
+        at T23454.hs:11:1-43
+    • In the second argument of ‘testEquality’, namely
+        ‘(coerce (SNat @a) :: SNat b)’
+      In the expression:
+        testEquality (SNat @a) (coerce (SNat @a) :: SNat b)
+      In the expression:
+        case testEquality (SNat @a) (coerce (SNat @a) :: SNat b) of
+          Just r -> r
+          Nothing -> error "bug fixed"
+    • Relevant bindings include
+        bogus :: a :~: b (bound at T23454.hs:12:1)


=====================================
libraries/base/tests/all.T
=====================================
@@ -300,3 +300,4 @@ test('listThreads1', normal, compile_and_run, [''])
 test('inits1tails1', normal, compile_and_run, [''])
 test('CLC149', normal, compile, [''])
 test('AtomicSwapIORef', normal, compile_and_run, [''])
+test('T23454', normal, compile_fail, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5988803eb2d823cb95c0fbfd7f175f61761620b3

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5988803eb2d823cb95c0fbfd7f175f61761620b3
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230605/6d6fdde4/attachment-0001.html>