[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