[Git][ghc/ghc][wip/UnsafeSNat-pattern-synonyms] Make UnsafeSNat et al. into pattern synonyms

Matthew Craven (@clyring) gitlab at gitlab.haskell.org
Thu May 23 01:36:12 UTC 2024



Matthew Craven pushed to branch wip/UnsafeSNat-pattern-synonyms at Glasgow Haskell Compiler / GHC


Commits:
324a7433 by Matthew Craven at 2024-05-22T21:35:34-04:00
Make UnsafeSNat et al. into pattern synonyms

...so that they do not cause coerce to bypass the nominal
role on the corresponding singleton types when they are imported.
See Note [Preventing unsafe coercions for singleton types] and
the discussion at #23478.

This also introduces unsafeWithSNatCo (and analogues for Char
and Symbol) so that users can still access the dangerous coercions
that importing the real constructors would allow, but only in a
very localized way.

- - - - -


2 changed files:

- libraries/ghc-internal/src/GHC/Internal/TypeLits.hs
- libraries/ghc-internal/src/GHC/Internal/TypeNats.hs


Changes:

=====================================
libraries/ghc-internal/src/GHC/Internal/TypeLits.hs
=====================================
@@ -16,6 +16,7 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 
 {-|
 GHC's @DataKinds@ language extension lifts data constructors, natural
@@ -49,11 +50,18 @@ module GHC.Internal.TypeLits
   , OrderingI(..)
   , N.cmpNat, cmpSymbol, cmpChar
     -- ** Singleton values
-  , N.SNat (..), SSymbol (..), SChar (..)
+  , N.SNat (..)
+  , SSymbol (UnsafeSSymbol)
+      -- We export a pattern synonym instead of the real constructor:
+      -- See Note [Preventing unsafe coercions for singleton types].
+  , SChar (UnsafeSChar)
+      -- We export a pattern synonym instead of the real constructor:
+      -- See Note [Preventing unsafe coercions for singleton types].
   , pattern N.SNat, pattern SSymbol, pattern SChar
   , fromSNat, fromSSymbol, fromSChar
   , withSomeSNat, withSomeSSymbol, withSomeSChar
   , N.withKnownNat, withKnownSymbol, withKnownChar
+  , N.unsafeWithSNatCo, unsafeWithSSymbolCo, unsafeWithSCharCo
 
     -- * Functions on type literals
   , type (N.<=), type (N.<=?), type (N.+), type (N.*), type (N.^), type (N.-)
@@ -72,7 +80,7 @@ module GHC.Internal.TypeLits
 import GHC.Internal.Base ( Bool(..), Eq(..), Functor(..), Ord(..), Ordering(..), String
                 , (.), otherwise, withDict, Void, (++)
                 , errorWithoutStackTrace)
-import GHC.Types(Symbol, Char, TYPE)
+import GHC.Types(Symbol, Char, TYPE, Coercible)
 import GHC.Internal.TypeError(ErrorMessage(..), TypeError)
 import GHC.Internal.Num(Integer, fromInteger)
 import GHC.Internal.Show(Show(..), appPrec, appPrec1, showParen, showString)
@@ -340,7 +348,9 @@ withSomeSNat n k
 --    'String'.
 --
 -- @since base-4.18.0.0
-newtype SSymbol (s :: Symbol) = UnsafeSSymbol String
+newtype SSymbol (s :: Symbol) = UnsafeSSymbol_ String
+-- nominal role: See Note [Preventing unsafe coercions for singleton types]
+-- in GHC.Internal.TypeNats
 type role SSymbol nominal
 
 -- | A explicitly bidirectional pattern synonym relating an 'SSymbol' to a
@@ -377,6 +387,26 @@ data KnownSymbolInstance (s :: Symbol) where
 knownSymbolInstance :: SSymbol s -> KnownSymbolInstance s
 knownSymbolInstance ss = withKnownSymbol ss KnownSymbolInstance
 
+-- | A pattern that can be used to manipulate the
+-- 'String' that an @SSymbol s@ contains under the hood.
+--
+-- When using this pattern to construct an @SSymbol s@, the actual
+-- @String@ being stored in the @SSymbol@ /must/ be equal to (the
+-- contents of) @s at .  The compiler will not help you verify this,
+-- hence the \'unsafe\' name.
+pattern UnsafeSSymbol :: forall s. String -> SSymbol s
+pattern UnsafeSSymbol guts = UnsafeSSymbol_ guts
+{-# COMPLETE UnsafeSSymbol #-}
+
+-- | 'unsafeWithSSymbolCo' allows uses of @coerce@ in its argument to see the
+-- real representation of @SSymbol s@, without undermining the type-safety of
+-- @coerce@ elsewhere in the module.
+--
+-- See also the documentation for 'UnsafeSSymbol'.
+unsafeWithSSymbolCo
+  :: forall r. ((forall s. Coercible (SSymbol s) String) => r) -> r
+unsafeWithSSymbolCo v = v
+
 -- | @since base-4.19.0.0
 instance Eq (SSymbol s) where
   _ == _ = True
@@ -443,7 +473,9 @@ withSomeSSymbol s k = k (UnsafeSSymbol s)
 -- 3. The 'withSomeSChar' function, which creates an 'SChar' from a 'Char'.
 --
 -- @since base-4.18.0.0
-newtype SChar (s :: Char) = UnsafeSChar Char
+newtype SChar (s :: Char) = UnsafeSChar_ Char
+-- nominal role: See Note [Preventing unsafe coercions for singleton types]
+-- in GHC.Internal.TypeNats
 type role SChar nominal
 
 -- | A explicitly bidirectional pattern synonym relating an 'SChar' to a
@@ -480,6 +512,25 @@ data KnownCharInstance (n :: Char) where
 knownCharInstance :: SChar c -> KnownCharInstance c
 knownCharInstance sc = withKnownChar sc KnownCharInstance
 
+-- | A pattern that can be used to manipulate the
+-- 'Char' that an @SChar c@ contains under the hood.
+--
+-- When using this pattern to construct an @SChar c@, the actual
+-- @Char@ being stored in the @SChar c@ /must/ be equal to @c at .
+-- The compiler will not help you verify this, hence the \'unsafe\' name.
+pattern UnsafeSChar :: forall c. Char -> SChar c
+pattern UnsafeSChar guts = UnsafeSChar_ guts
+{-# COMPLETE UnsafeSChar #-}
+
+-- | 'unsafeWithSCharCo' allows uses of @coerce@ in its argument to see the
+-- real representation of @SChar c@, without undermining the type-safety of
+-- @coerce@ elsewhere in the module.
+--
+-- See also the documentation for 'UnsafeSChar'.
+unsafeWithSCharCo
+  :: forall r. ((forall c. Coercible (SChar c) Char) => r) -> r
+unsafeWithSCharCo v = v
+
 -- | @since base-4.19.0.0
 instance Eq (SChar c) where
   _ == _ = True


=====================================
libraries/ghc-internal/src/GHC/Internal/TypeNats.hs
=====================================
@@ -17,6 +17,7 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE QuantifiedConstraints #-}
 
 {-| This module is an internal GHC module.  It declares the constants used
 in the implementation of type-level natural numbers.  The programmer interface
@@ -36,11 +37,14 @@ module GHC.Internal.TypeNats
   , sameNat
   , decideNat
     -- ** Singleton values
-  , SNat (..)
+  , SNat (UnsafeSNat)
+      -- We export a pattern synonym instead of the real constructor:
+      -- See Note [Preventing unsafe coercions for singleton types].
   , pattern SNat
   , fromSNat
   , withSomeSNat
   , withKnownNat
+  , unsafeWithSNatCo
 
     -- * Functions on type literals
   , type (<=), type (<=?), type (+), type (*), type (^), type (-)
@@ -344,9 +348,59 @@ cmpNat x y = case compare (natVal x) (natVal y) of
 --    number.
 --
 -- @since base-4.18.0.0
-newtype SNat (n :: Nat) = UnsafeSNat Natural
+newtype SNat (n :: Nat) = UnsafeSNat_ Natural
+-- nominal role: See Note [Preventing unsafe coercions for singleton types]
 type role SNat nominal
 
+{-
+Note [Preventing unsafe coercions for singleton types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider a singleton type like this one:
+
+  newtype SNat (n :: Nat) = UnsafeSNat_ Natural
+
+We operate under the fiction that a (non-bottom) value
+``UnsafeSNat_ v :: SNat n`` also contains evidence that the value
+``v :: Natural`` is the same as the type ``n :: Natural``,
+And obviously it's evidence that ``v`` is the same as ``n``
+cannot be safely `coerce`d to evidence that ``v`` is the same as ``n2``,
+unless we know that ``n ~ n2``, at nominal role. (This is #23454.)
+
+So, to preserve that fiction, we:
+
+ 1. Provide a role annotation indicating that ``SNat``'s type argument has
+    nominal role rather than the phantom role that would be inferred.
+ 2. Ensure that the real newtype constructor ``UnsafeSNat_`` is not exported
+    even from ghc-internal.  Whenever that constructor is in scope, typechecking
+    of ``coerce`` will ignore the role annotation and just unwrap the newtype.
+
+But users may wish to write functions like this one (#23478):
+
+  plusSNat :: SNat a -> SNat b -> SNat (a + b)
+
+We could ask them to use ``unsafeCoerce``, but it seems a bit more polite
+to provide a pattern synonym ``UnsafeSNat :: forall n. Natural -> SNat n``
+as an escape hatch (exported from ghc-internal only), so that such a function
+can be written as follows:
+
+  plusSNat (UnsafeSNat x) (UnsafeSNat y) = UnsafeSNat (x + y)
+
+Crucially, these pattern synonyms (unlike real newtype constructors) do not
+cause ``coerce`` to bypass our role annotation when they are in scope.
+
+To allow casting data structures containing SNats, we provide a
+further escape hatch in ``unsafeWithSNatCo``, enables ``coerce`` to
+bypass our role annotation on ``SNat``, but /only within its argument/:
+
+  unsafeWithSNatCo
+    :: forall r. ((forall n. Coercible (SNat n) Natural) => r) -> r
+
+
+The above reasoning applies identically for the other singleton types
+'SChar' and 'SSymbol' as well.
+-}
+
+
 -- | A explicitly bidirectional pattern synonym relating an 'SNat' to a
 -- 'KnownNat' constraint.
 --
@@ -381,6 +435,25 @@ data KnownNatInstance (n :: Nat) where
 knownNatInstance :: SNat n -> KnownNatInstance n
 knownNatInstance sn = withKnownNat sn KnownNatInstance
 
+-- | A pattern that can be used to manipulate the
+-- 'Natural' that an @SNat n@ contains under the hood.
+--
+-- When using this pattern to construct an @SNat n@, the actual
+-- @Natural@ being stored in the @SNat n@ /must/ be equal to @n at .
+-- The compiler will not help you verify this, hence the \'unsafe\' name.
+pattern UnsafeSNat :: forall n. Natural -> SNat n
+pattern UnsafeSNat guts = UnsafeSNat_ guts
+{-# COMPLETE UnsafeSNat #-}
+
+-- | 'unsafeWithSNatCo' allows uses of @coerce@ in its argument to see the
+-- real representation of @SNat n@, without undermining the type-safety of
+-- @coerce@ elsewhere in the module.
+--
+-- See also the documentation for 'UnsafeSNat'.
+unsafeWithSNatCo
+  :: forall r. ((forall n. Coercible (SNat n) Natural) => r) -> r
+unsafeWithSNatCo v = v
+
 -- | @since base-4.19.0.0
 instance Eq (SNat n) where
   _ == _ = True



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/324a7433e9c2ce504d9d1151cb45ca01118c8b54

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/324a7433e9c2ce504d9d1151cb45ca01118c8b54
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/20240522/7e5ad0b4/attachment-0001.html>


More information about the ghc-commits mailing list