[Git][ghc/ghc][master] Add role annotations to SNat, SSymbol and SChar
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Fri Jun 9 22:51:04 UTC 2023
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
4639100b by Matthew Pickering at 2023-06-09T18:50:43-04: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.
CLC Proposal: https://github.com/haskell/core-libraries-committee/issues/170
Fixes #23454
- - - - -
7 changed files:
- libraries/base/GHC/TypeLits.hs
- libraries/base/GHC/TypeNats.hs
- libraries/base/changelog.md
- + libraries/base/tests/T23454.hs
- + libraries/base/tests/T23454.stderr
- libraries/base/tests/all.T
- testsuite/tests/ghci/scripts/T9181.stdout
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/changelog.md
=====================================
@@ -32,6 +32,7 @@
* Make `(&)` representation polymorphic in the return type ([CLC proposal #158](https://github.com/haskell/core-libraries-committee/issues/158))
* Implement `GHC.IORef.atomicSwapIORef` via a new dedicated primop `atomicSwapMutVar#` ([CLC proposal #139](https://github.com/haskell/core-libraries-committee/issues/139))
* Change codebuffers to use an unboxed implementation, while providing a compatibility layer using pattern synonyms. ([CLC proposal #134](https://github.com/haskell/core-libraries-committee/issues/134))
+ * Add nominal role annotations to SNat/SSymbol/SChar ([CLC proposal #170](https://github.com/haskell/core-libraries-committee/issues/170))
## 4.18.0.0 *March 2023*
* Shipped with GHC 9.6.1
=====================================
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, [''])
=====================================
testsuite/tests/ghci/scripts/T9181.stdout
=====================================
@@ -18,12 +18,12 @@ type GHC.TypeLits.NatToChar :: GHC.Num.Natural.Natural -> Char
type family GHC.TypeLits.NatToChar a
pattern GHC.TypeLits.SChar
:: () => GHC.TypeLits.KnownChar c => GHC.TypeLits.SChar c
-type role GHC.TypeLits.SChar phantom
+type role GHC.TypeLits.SChar nominal
type GHC.TypeLits.SChar :: Char -> *
newtype GHC.TypeLits.SChar s = GHC.TypeLits.UnsafeSChar Char
pattern GHC.TypeLits.SSymbol
:: () => GHC.TypeLits.KnownSymbol s => GHC.TypeLits.SSymbol s
-type role GHC.TypeLits.SSymbol phantom
+type role GHC.TypeLits.SSymbol nominal
type GHC.TypeLits.SSymbol :: GHC.Types.Symbol -> *
newtype GHC.TypeLits.SSymbol s = GHC.TypeLits.UnsafeSSymbol String
type GHC.TypeLits.SomeChar :: *
@@ -166,7 +166,7 @@ data Data.Type.Ord.OrderingI a b where
Data.Type.Ord.OrderingI a b
pattern GHC.TypeNats.SNat
:: () => GHC.TypeNats.KnownNat n => GHC.TypeNats.SNat n
-type role GHC.TypeNats.SNat phantom
+type role GHC.TypeNats.SNat nominal
type GHC.TypeNats.SNat :: GHC.TypeNats.Nat -> *
newtype GHC.TypeNats.SNat n
= GHC.TypeNats.UnsafeSNat GHC.Num.Natural.Natural
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4639100b5dd19fe2cabb36f7e457826e44a579aa
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/4639100b5dd19fe2cabb36f7e457826e44a579aa
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/20230609/cd84d46d/attachment-0001.html>
More information about the ghc-commits
mailing list