[Git][ghc/ghc][master] Export symbolSing, SSymbol, and friends (CLC#85)
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Fri Oct 7 11:36:14 UTC 2022
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
532de368 by Ryan Scott at 2022-10-06T07:45:46-04:00
Export symbolSing, SSymbol, and friends (CLC#85)
This implements this Core Libraries Proposal:
https://github.com/haskell/core-libraries-committee/issues/85
In particular, it:
1. Exposes the `symbolSing` method of `KnownSymbol`,
2. Exports the abstract `SSymbol` type used in `symbolSing`, and
3. Defines an API for interacting with `SSymbol`.
This also makes corresponding changes for `natSing`/`KnownNat`/`SNat` and
`charSing`/`KnownChar`/`SChar`. This fixes #15183 and addresses part (2)
of #21568.
- - - - -
14 changed files:
- compiler/GHC/Tc/Instance/Class.hs
- libraries/base/GHC/TypeLits.hs
- libraries/base/GHC/TypeNats.hs
- libraries/base/changelog.md
- + libraries/base/tests/T15183.hs
- + libraries/base/tests/T15183.stdout
- libraries/base/tests/all.T
- testsuite/tests/dependent/should_compile/RaeJobTalk.hs
- testsuite/tests/ghci/scripts/T19667Ghci.hs
- testsuite/tests/ghci/scripts/T4175.stdout
- testsuite/tests/ghci/scripts/T9181.stdout
- testsuite/tests/ghci/scripts/ghci064.stdout
- testsuite/tests/typecheck/should_run/T16646.hs
- testsuite/tests/typecheck/should_run/T19667.hs
Changes:
=====================================
compiler/GHC/Tc/Instance/Class.hs
=====================================
@@ -571,15 +571,15 @@ Some further observations about `withDict`:
(WD3) As an alternative to `withDict`, one could define functions like `withT`
above in terms of `unsafeCoerce`. This is more error-prone, however.
-(WD4) In order to define things like `reifySymbol` below:
+(WD4) In order to define things like `withKnownNat` below:
- reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => r) -> r
+ withKnownNat :: SNat n -> (KnownNat n => r) -> r
`withDict` needs to be instantiated with `Any`, like so:
- reifySymbol n k = withDict @(KnownSymbol Any) @String @r n (k @Any)
+ withKnownNat = withDict @(KnownNat Any) @(SNat Any) @r
- The use of `Any` is explained in Note [NOINLINE someNatVal] in
+ The use of `Any` is explained in Note [NOINLINE withSomeSNat] in
base:GHC.TypeNats.
(WD5) In earlier implementations, `withDict` was implemented as an identifier
=====================================
libraries/base/GHC/TypeLits.hs
=====================================
@@ -11,6 +11,10 @@
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ViewPatterns #-}
{-|
GHC's @DataKinds@ language extension lifts data constructors, natural
@@ -34,15 +38,20 @@ module GHC.TypeLits
N.Natural, N.Nat, Symbol -- Symbol is declared in GHC.Types in package ghc-prim
-- * Linking type and value level
- , N.KnownNat, natVal, natVal'
- , KnownSymbol, symbolVal, symbolVal'
- , KnownChar, charVal, charVal'
+ , N.KnownNat(natSing), natVal, natVal'
+ , KnownSymbol(symbolSing), symbolVal, symbolVal'
+ , KnownChar(charSing), charVal, charVal'
, N.SomeNat(..), SomeSymbol(..), SomeChar(..)
, someNatVal, someSymbolVal, someCharVal
, N.sameNat, sameSymbol, sameChar
, OrderingI(..)
, N.cmpNat, cmpSymbol, cmpChar
-
+ -- ** Singleton values
+ , N.SNat, SSymbol, SChar
+ , pattern N.SNat, pattern SSymbol, pattern SChar
+ , fromSNat, fromSSymbol, fromSChar
+ , withSomeSNat, withSomeSSymbol, withSomeSChar
+ , N.withKnownNat, withKnownSymbol, withKnownChar
-- * Functions on type literals
, type (N.<=), type (N.<=?), type (N.+), type (N.*), type (N.^), type (N.-)
@@ -58,17 +67,19 @@ module GHC.TypeLits
) where
-import GHC.Base(Eq(..), Ord(..), Ordering(..), String, otherwise, withDict)
-import GHC.Types(Symbol, Char)
+import GHC.Base ( Eq(..), Functor(..), Ord(..), Ordering(..), String
+ , (.), otherwise, withDict )
+import GHC.Types(Symbol, Char, TYPE)
import GHC.TypeError(ErrorMessage(..), TypeError)
import GHC.Num(Integer, fromInteger)
-import GHC.Show(Show(..))
+import GHC.Show(Show(..), appPrec, appPrec1, showParen, showString)
import GHC.Read(Read(..))
import GHC.Real(toInteger)
import GHC.Prim(Proxy#)
import Data.Maybe(Maybe(..))
import Data.Proxy (Proxy(..))
-import Data.Type.Equality((:~:)(Refl))
+import Data.Type.Coercion (Coercion(..), TestCoercion(..))
+import Data.Type.Equality((:~:)(Refl), TestEquality(..))
import Data.Type.Ord(OrderingI(..))
import Unsafe.Coerce(unsafeCoerce)
@@ -91,7 +102,7 @@ natVal p = toInteger (N.natVal p)
-- | @since 4.7.0.0
symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String
symbolVal _ = case symbolSing :: SSymbol n of
- SSymbol x -> x
+ UnsafeSSymbol x -> x
-- | @since 4.8.0.0
natVal' :: forall n. N.KnownNat n => Proxy# n -> Integer
@@ -100,7 +111,7 @@ natVal' p = toInteger (N.natVal' p)
-- | @since 4.8.0.0
symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String
symbolVal' _ = case symbolSing :: SSymbol n of
- SSymbol x -> x
+ UnsafeSSymbol x -> x
-- | This type represents unknown type-level symbols.
@@ -113,11 +124,11 @@ class KnownChar (n :: Char) where
charVal :: forall n proxy. KnownChar n => proxy n -> Char
charVal _ = case charSing :: SChar n of
- SChar x -> x
+ UnsafeSChar x -> x
charVal' :: forall n. KnownChar n => Proxy# n -> Char
charVal' _ = case charSing :: SChar n of
- SChar x -> x
+ UnsafeSChar x -> x
data SomeChar = forall n. KnownChar n => SomeChar (Proxy n)
@@ -133,10 +144,8 @@ someNatVal n
--
-- @since 4.7.0.0
someSymbolVal :: String -> SomeSymbol
-someSymbolVal n = withSSymbol SomeSymbol (SSymbol n) Proxy
-{-# NOINLINE someSymbolVal #-}
--- For details see Note [NOINLINE someNatVal] in "GHC.TypeNats"
--- The issue described there applies to `someSymbolVal` as well.
+someSymbolVal s = withSomeSSymbol s (\(ss :: SSymbol s) ->
+ withKnownSymbol ss (SomeSymbol @s Proxy))
-- | @since 4.7.0.0
instance Eq SomeSymbol where
@@ -159,8 +168,8 @@ instance Read SomeSymbol where
--
-- @since 4.16.0.0
someCharVal :: Char -> SomeChar
-someCharVal n = withSChar SomeChar (SChar n) Proxy
-{-# NOINLINE someCharVal #-}
+someCharVal c = withSomeSChar c (\(sc :: SChar c) ->
+ withKnownChar sc (SomeChar @c Proxy))
instance Eq SomeChar where
SomeChar x == SomeChar y = charVal x == charVal y
@@ -210,22 +219,20 @@ type family NatToChar (n :: N.Nat) :: Char
-- same type-level symbols, or 'Nothing'.
--
-- @since 4.7.0.0
-sameSymbol :: (KnownSymbol a, KnownSymbol b) =>
+sameSymbol :: forall a b proxy1 proxy2.
+ (KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
-sameSymbol x y
- | symbolVal x == symbolVal y = Just (unsafeCoerce Refl)
- | otherwise = Nothing
+sameSymbol _ _ = testEquality (symbolSing @a) (symbolSing @b)
-- | We either get evidence that this function was instantiated with the
-- same type-level characters, or 'Nothing'.
--
-- @since 4.16.0.0
-sameChar :: (KnownChar a, KnownChar b) =>
- proxy1 a -> proxy2 b -> Maybe (a :~: b)
-sameChar x y
- | charVal x == charVal y = Just (unsafeCoerce Refl)
- | otherwise = Nothing
+sameChar :: forall a b proxy1 proxy2.
+ (KnownChar a, KnownChar b) =>
+ proxy1 a -> proxy2 b -> Maybe (a :~: b)
+sameChar _ _ = testEquality (charSing @a) (charSing @b)
-- | Like 'sameSymbol', but if the symbols aren't equal, this additionally
-- provides proof of LT or GT.
@@ -257,20 +264,217 @@ cmpChar x y = case compare (charVal x) (charVal y) of
--------------------------------------------------------------------------------
--- PRIVATE:
+-- Singleton values
+
+-- | Return the 'Integer' corresponding to @n@ in an @'SNat' n@ value.
+-- The returned 'Integer' is always non-negative.
+--
+-- For a version of this function that returns a 'Natural' instead of an
+-- 'Integer', see 'N.fromSNat' in "GHC.TypeNats".
+--
+-- @since 4.18.0.0
+fromSNat :: N.SNat n -> Integer
+fromSNat sn = toInteger (N.fromSNat sn)
+
+-- | Attempt to convert an 'Integer' into an @'SNat' n@ value, where @n@ is a
+-- fresh type-level natural number. If the 'Integer' argument is non-negative,
+-- invoke the continuation with @Just sn@, where @sn@ is the @'SNat' n@ value.
+-- If the 'Integer' argument is negative, invoke the continuation with
+-- 'Nothing'.
+--
+-- For a version of this function where the continuation uses @'SNat@ n@
+-- instead of @'Maybe' ('SNat' n)@, see 'N.withSomeSNat' in "GHC.TypeNats".
+--
+-- @since 4.18.0.0
+withSomeSNat :: forall rep (r :: TYPE rep).
+ Integer -> (forall n. Maybe (N.SNat n) -> r) -> r
+withSomeSNat n k
+ | n >= 0 = N.withSomeSNat (fromInteger n) (\sn -> k (Just sn))
+ | otherwise = k Nothing
+
+-- | A value-level witness for a type-level symbol. This is commonly referred
+-- to as a /singleton/ type, as for each @s@, there is a single value that
+-- inhabits the type @'SSymbol' s@ (aside from bottom).
+--
+-- The definition of 'SSymbol' is intentionally left abstract. To obtain an
+-- 'SSymbol' value, use one of the following:
+--
+-- 1. The 'symbolSing' method of 'KnownSymbol'.
+--
+-- 2. The @SSymbol@ pattern synonym.
+--
+-- 3. The 'withSomeSSymbol' function, which creates an 'SSymbol' from a
+-- 'String'.
+--
+-- @since 4.18.0.0
+newtype SSymbol (s :: Symbol) = UnsafeSSymbol String
-newtype SSymbol (s :: Symbol) = SSymbol String
+-- | A explicitly bidirectional pattern synonym relating an 'SSymbol' to a
+-- 'KnownSymbol' constraint.
+--
+-- As an __expression__: Constructs an explicit @'SSymbol' s@ value from an
+-- implicit @'KnownSymbol' s@ constraint:
+--
+-- @
+-- SSymbol @s :: 'KnownSymbol' s => 'SSymbol' s
+-- @
+--
+-- As a __pattern__: Matches on an explicit @'SSymbol' s@ value bringing
+-- an implicit @'KnownSymbol' s@ constraint into scope:
+--
+-- @
+-- f :: 'SSymbol' s -> ..
+-- f SSymbol = {- SSymbol s in scope -}
+-- @
+--
+-- @since 4.18.0.0
+pattern SSymbol :: forall s. () => KnownSymbol s => SSymbol s
+pattern SSymbol <- (knownSymbolInstance -> KnownSymbolInstance)
+ where SSymbol = symbolSing
+
+-- An internal data type that is only used for defining the SSymbol pattern
+-- synonym.
+data KnownSymbolInstance (s :: Symbol) where
+ KnownSymbolInstance :: KnownSymbol s => KnownSymbolInstance s
+
+-- An internal function that is only used for defining the SSymbol pattern
+-- synonym.
+knownSymbolInstance :: SSymbol s -> KnownSymbolInstance s
+knownSymbolInstance ss = withKnownSymbol ss KnownSymbolInstance
+
+-- | @since 4.18.0.0
+instance Show (SSymbol s) where
+ showsPrec p (UnsafeSSymbol s)
+ = showParen (p > appPrec)
+ ( showString "SSymbol @"
+ . showsPrec appPrec1 s
+ )
+
+-- | @since 4.18.0.0
+instance TestEquality SSymbol where
+ testEquality (UnsafeSSymbol x) (UnsafeSSymbol y)
+ | x == y = Just (unsafeCoerce Refl)
+ | otherwise = Nothing
+
+-- | @since 4.18.0.0
+instance TestCoercion SSymbol where
+ testCoercion x y = fmap (\Refl -> Coercion) (testEquality x y)
+
+-- | Return the String corresponding to @s@ in an @'SSymbol' s@ value.
+--
+-- @since 4.18.0.0
+fromSSymbol :: SSymbol s -> String
+fromSSymbol (UnsafeSSymbol s) = s
+-- | Convert an explicit @'SSymbol' s@ value into an implicit @'KnownSymbol' s@
+-- constraint.
+--
+-- @since 4.18.0.0
+withKnownSymbol :: forall s rep (r :: TYPE rep).
+ SSymbol s -> (KnownSymbol s => r) -> r
+withKnownSymbol = withDict @(KnownSymbol s)
-- See Note [withDict] in "GHC.Tc.Instance.Class" in GHC
-withSSymbol :: forall a b.
- (KnownSymbol a => Proxy a -> b)
- -> SSymbol a -> Proxy a -> b
-withSSymbol f x y = withDict @(KnownSymbol a) x f y
-newtype SChar (s :: Char) = SChar Char
+-- | Convert a 'String' into an @'SSymbol' s@ value, where @s@ is a fresh
+-- type-level symbol.
+--
+-- @since 4.18.0.0
+withSomeSSymbol :: forall rep (r :: TYPE rep).
+ String -> (forall s. SSymbol s -> r) -> r
+withSomeSSymbol s k = k (UnsafeSSymbol s)
+{-# NOINLINE withSomeSSymbol #-}
+-- For details see Note [NOINLINE withSomeSNat] in "GHC.TypeNats"
+-- The issue described there applies to `withSomeSSymbol` as well.
+
+-- | A value-level witness for a type-level character. This is commonly referred
+-- to as a /singleton/ type, as for each @c@, there is a single value that
+-- inhabits the type @'SChar' c@ (aside from bottom).
+--
+-- The definition of 'SChar' is intentionally left abstract. To obtain an
+-- 'SChar' value, use one of the following:
+--
+-- 1. The 'charSing' method of 'KnownChar'.
+--
+-- 2. The @SChar@ pattern synonym.
+--
+-- 3. The 'withSomeSChar' function, which creates an 'SChar' from a 'Char'.
+--
+-- @since 4.18.0.0
+newtype SChar (s :: Char) = UnsafeSChar Char
+-- | A explicitly bidirectional pattern synonym relating an 'SChar' to a
+-- 'KnownChar' constraint.
+--
+-- As an __expression__: Constructs an explicit @'SChar' c@ value from an
+-- implicit @'KnownChar' c@ constraint:
+--
+-- @
+-- SChar @c :: 'KnownChar' c => 'SChar' c
+-- @
+--
+-- As a __pattern__: Matches on an explicit @'SChar' c@ value bringing
+-- an implicit @'KnownChar' c@ constraint into scope:
+--
+-- @
+-- f :: 'SChar' c -> ..
+-- f SChar = {- SChar c in scope -}
+-- @
+--
+-- @since 4.18.0.0
+pattern SChar :: forall c. () => KnownChar c => SChar c
+pattern SChar <- (knownCharInstance -> KnownCharInstance)
+ where SChar = charSing
+
+-- An internal data type that is only used for defining the SChar pattern
+-- synonym.
+data KnownCharInstance (n :: Char) where
+ KnownCharInstance :: KnownChar c => KnownCharInstance c
+
+-- An internal function that is only used for defining the SChar pattern
+-- synonym.
+knownCharInstance :: SChar c -> KnownCharInstance c
+knownCharInstance sc = withKnownChar sc KnownCharInstance
+
+-- | @since 4.18.0.0
+instance Show (SChar c) where
+ showsPrec p (UnsafeSChar c)
+ = showParen (p > appPrec)
+ ( showString "SChar @"
+ . showsPrec appPrec1 c
+ )
+
+-- | @since 4.18.0.0
+instance TestEquality SChar where
+ testEquality (UnsafeSChar x) (UnsafeSChar y)
+ | x == y = Just (unsafeCoerce Refl)
+ | otherwise = Nothing
+
+-- | @since 4.18.0.0
+instance TestCoercion SChar where
+ testCoercion x y = fmap (\Refl -> Coercion) (testEquality x y)
+
+-- | Return the 'Char' corresponding to @c@ in an @'SChar' c@ value.
+--
+-- @since 4.18.0.0
+fromSChar :: SChar c -> Char
+fromSChar (UnsafeSChar c) = c
+
+-- | Convert an explicit @'SChar' c@ value into an implicit @'KnownChar' c@
+-- constraint.
+--
+-- @since 4.18.0.0
+withKnownChar :: forall c rep (r :: TYPE rep).
+ SChar c -> (KnownChar c => r) -> r
+withKnownChar = withDict @(KnownChar c)
-- See Note [withDict] in "GHC.Tc.Instance.Class" in GHC
-withSChar :: forall a b.
- (KnownChar a => Proxy a -> b)
- -> SChar a -> Proxy a -> b
-withSChar f x y = withDict @(KnownChar a) x f y
+
+-- | Convert a 'Char' into an @'SChar' c@ value, where @c@ is a fresh type-level
+-- character.
+--
+-- @since 4.18.0.0
+withSomeSChar :: forall rep (r :: TYPE rep).
+ Char -> (forall c. SChar c -> r) -> r
+withSomeSChar c k = k (UnsafeSChar c)
+{-# NOINLINE withSomeSChar #-}
+-- For details see Note [NOINLINE withSomeSNat] in "GHC.TypeNats"
+-- The issue described there applies to `withSomeSChar` as well.
=====================================
libraries/base/GHC/TypeNats.hs
=====================================
@@ -13,6 +13,9 @@
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
{-| This module is an internal GHC module. It declares the constants used
in the implementation of type-level natural numbers. The programmer interface
@@ -26,10 +29,16 @@ module GHC.TypeNats
Natural -- declared in GHC.Num.Natural in package ghc-bignum
, Nat
-- * Linking type and value level
- , KnownNat, natVal, natVal'
+ , KnownNat(natSing), natVal, natVal'
, SomeNat(..)
, someNatVal
, sameNat
+ -- ** Singleton values
+ , SNat
+ , pattern SNat
+ , fromSNat
+ , withSomeSNat
+ , withKnownNat
-- * Functions on type literals
, type (<=), type (<=?), type (+), type (*), type (^), type (-)
@@ -39,15 +48,16 @@ module GHC.TypeNats
) where
-import GHC.Base(Eq(..), Ord(..), otherwise, WithDict(..))
+import GHC.Base(Eq(..), Functor(..), Ord(..), WithDict(..), (.), otherwise)
import GHC.Types
import GHC.Num.Natural(Natural)
-import GHC.Show(Show(..))
+import GHC.Show(Show(..), appPrec, appPrec1, showParen, showString)
import GHC.Read(Read(..))
import GHC.Prim(Proxy#)
import Data.Maybe(Maybe(..))
import Data.Proxy (Proxy(..))
-import Data.Type.Equality((:~:)(Refl))
+import Data.Type.Coercion (Coercion(..), TestCoercion(..))
+import Data.Type.Equality((:~:)(Refl), TestEquality(..))
import Data.Type.Ord(OrderingI(..), type (<=), type (<=?))
import Unsafe.Coerce(unsafeCoerce)
@@ -73,12 +83,12 @@ class KnownNat (n :: Nat) where
-- | @since 4.10.0.0
natVal :: forall n proxy. KnownNat n => proxy n -> Natural
natVal _ = case natSing :: SNat n of
- SNat x -> x
+ UnsafeSNat x -> x
-- | @since 4.10.0.0
natVal' :: forall n. KnownNat n => Proxy# n -> Natural
natVal' _ = case natSing :: SNat n of
- SNat x -> x
+ UnsafeSNat x -> x
-- | This type represents unknown type-level natural numbers.
--
@@ -89,66 +99,72 @@ data SomeNat = forall n. KnownNat n => SomeNat (Proxy n)
--
-- @since 4.10.0.0
someNatVal :: Natural -> SomeNat
-someNatVal n = withSNat SomeNat (SNat n) Proxy
-{-# NOINLINE someNatVal #-} -- See Note [NOINLINE someNatVal]
+someNatVal n = withSomeSNat n (\(sn :: SNat n) ->
+ withKnownNat sn (SomeNat @n Proxy))
{-
-Note [NOINLINE someNatVal]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-`someNatVal` converts a natural number to an existentially quantified
-dictionary for `KnownNat` (aka `SomeNat`). The existential quantification
-is very important, as it captures the fact that we don't know the type
-statically, although we do know that it exists. Because this type is
-fully opaque, we should never be able to prove that it matches anything else.
-This is why coherence should still hold: we can manufacture a `KnownNat k`
-dictionary, but it can never be confused with a `KnownNat 33` dictionary,
-because we should never be able to prove that `k ~ 33`.
-
-But how to implement `someNatVal`? We can't quite implement it "honestly"
-because `SomeNat` needs to "hide" the type of the newly created dictionary,
-but we don't know what the actual type is! If `someNatVal` was built into
-the language, then we could manufacture a new skolem constant,
-which should behave correctly.
-
-Since extra language constructors have additional maintenance costs,
-we use a trick to implement `someNatVal` in the library. The idea is that
-instead of generating a "fresh" type for each use of `someNatVal`, we simply
-use GHC's placeholder type `Any` (of kind `Nat`). So, the elaborated
-version of the code is:
-
- someNatVal n = withSNat @T (SomeNat @T) (SNat @T n) (Proxy @T)
- where type T = Any Nat
+Note [NOINLINE withSomeSNat]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The function
-After inlining and simplification, this ends up looking something like this:
+ withSomeSNat :: forall rep (r :: TYPE rep).
+ Natural -> (forall k. SNat k -> r) -> r
- someNatVal n = SomeNat @T (KnownNat @T (SNat @T n)) (Proxy @T)
- where type T = Any Nat
+converts a `Natural` number to a singleton natural `SNat k`, where the `k` is
+locally quantified in a continuation (hence the `forall k`). The local
+quantification is important: we can manufacture an `SNat k` value, but it can
+never be confused with (say) an `SNat 33` value, because we should never be
+able to prove that `k ~ 33`. Moreover, if we call `withSomeSNat` twice, we'll
+get an `SNat k1` value and an `SNat k2` value, but again we can't confuse them.
+`SNat` is a singleton type!
-`KnownNat` is the constructor for dictionaries for the class `KnownNat`.
-See Note [withDict] in "GHC.Tc.Instance.Class" for details on how
-we actually construct the dictionary.
+But how to implement `withSomeSNat`? We have no way to make up a fresh type
+variable. To do that we need `runExists`: see #19675.
-Note that using `Any Nat` is not really correct, as multiple calls to
-`someNatVal` would violate coherence:
+Lacking `runExists`, we use a trick to implement `withSomeSNat`: instead of
+generating a "fresh" type for each use of `withSomeSNat`, we simply use GHC's
+placeholder type `Any` (of kind `Nat`), thus (in Core):
- type T = Any Nat
+ withSomeSNat n f = f @T (UnsafeSNat @T n)
+ where type T = Any @Nat
- x = SomeNat @T (KnownNat @T (SNat @T 1)) (Proxy @T)
- y = SomeNat @T (KnownNat @T (SNat @T 2)) (Proxy @T)
+*** BUT we must mark `withSomeSNat` as NOINLINE! ***
+(And the same for withSomeSSymbol and withSomeSChar in GHC.TypeLits.)
-Note that now the code has two dictionaries with the same type, `KnownNat Any`,
-but they have different implementations, namely `SNat 1` and `SNat 2`. This
-is not good, as GHC assumes coherence, and it is free to interchange
-dictionaries of the same type, but in this case this would produce an incorrect
-result. See #16586 for examples of this happening.
+If we inline it we'll lose the type distinction between separate calls (those
+"fresh" type variables just turn into `T`). And that can interact badly with
+GHC's type-class specialiser. Consider this definition, where
+`foo :: KnownNat n => blah`:
-We can avoid this problem by making the definition of `someNatVal` opaque
-and we do this by using a `NOINLINE` pragma. This restores coherence, because
-GHC can only inspect the result of `someNatVal` by pattern matching on the
-existential, which would generate a new type. This restores correctness,
-at the cost of having a little more allocation for the `SomeNat` constructors.
--}
+ ex :: Natural
+ ex = withSomeSNat 1 (\(s1 :: SNat one) -> withKnownNat @one s1 $
+ withSomeSNat 2 (\(s2 :: SNat two) -> withKnownNat @two s2 $
+ foo @one ... + foo @two ...))
+
+In the last line we have in scope two distinct dictionaries of types
+`KnownNat one` and `KnownNat two`. The calls `foo @one` and `foo @two` each pick
+out one of those dictionaries to pass to `foo`.
+But if we inline `withSomeSNat` we'll get (switching to Core):
+
+ ex = withKnownNat @T (UnsafeSNat @T 1) (\(kn1 :: KnownNat T) ->
+ withKnownNat @T (UnsafeSNat @T 2) (\(kn2 :: KnownNat T) ->
+ foo @T kn1 ... + foo @T kn2 ...))
+ where type T = Any Nat
+
+We are now treading on thin ice. We have two dictionaries `kn1` and `kn2`, both
+of type `KnownNat T`, but with different implementations. GHC may specialise
+`foo` at type `T` using one of these dictionaries and use that same
+specialisation for the other. See #16586 for more examples of where something
+like this has actually happened.
+
+`KnownNat` should be a singleton type, but if we allow `withSomeSNat` to inline
+it won't be a singleton type any more. We have lost the "fresh type variable".
+
+TL;DR. We avoid this problem by making the definition of `withSomeSNat` opaque,
+using an `NOINLINE` pragma. When we get `runExists` (#19675) we will be able to
+stop using this hack.
+-}
-- | @since 4.7.0.0
@@ -218,11 +234,10 @@ type family Log2 (m :: Nat) :: Nat
-- same type-level numbers, or 'Nothing'.
--
-- @since 4.7.0.0
-sameNat :: (KnownNat a, KnownNat b) =>
+sameNat :: forall a b proxy1 proxy2.
+ (KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
-sameNat x y
- | natVal x == natVal y = Just (unsafeCoerce Refl)
- | otherwise = Nothing
+sameNat _ _ = testEquality (natSing @a) (natSing @b)
-- | Like 'sameNat', but if the numbers aren't equal, this additionally
-- provides proof of LT or GT.
@@ -241,12 +256,96 @@ cmpNat x y = case compare (natVal x) (natVal y) of
--------------------------------------------------------------------------------
--- PRIVATE:
+-- Singleton values
-newtype SNat (n :: Nat) = SNat Natural
+-- | A value-level witness for a type-level natural number. This is commonly
+-- referred to as a /singleton/ type, as for each @n@, there is a single value
+-- that inhabits the type @'SNat' n@ (aside from bottom).
+--
+-- The definition of 'SNat' is intentionally left abstract. To obtain an 'SNat'
+-- value, use one of the following:
+--
+-- 1. The 'natSing' method of 'KnownNat'.
+--
+-- 2. The @SNat@ pattern synonym.
+--
+-- 3. The 'withSomeSNat' function, which creates an 'SNat' from a 'Natural'
+-- number.
+--
+-- @since 4.18.0.0
+newtype SNat (n :: Nat) = UnsafeSNat Natural
+-- | A explicitly bidirectional pattern synonym relating an 'SNat' to a
+-- 'KnownNat' constraint.
+--
+-- As an __expression__: Constructs an explicit @'SNat' n@ value from an
+-- implicit @'KnownNat' n@ constraint:
+--
+-- @
+-- SNat @n :: 'KnownNat' n => 'SNat' n
+-- @
+--
+-- As a __pattern__: Matches on an explicit @'SNat' n@ value bringing
+-- an implicit @'KnownNat' n@ constraint into scope:
+--
+-- @
+-- f :: 'SNat' n -> ..
+-- f SNat = {- SNat n in scope -}
+-- @
+--
+-- @since 4.18.0.0
+pattern SNat :: forall n. () => KnownNat n => SNat n
+pattern SNat <- (knownNatInstance -> KnownNatInstance)
+ where SNat = natSing
+
+-- An internal data type that is only used for defining the SNat pattern
+-- synonym.
+data KnownNatInstance (n :: Nat) where
+ KnownNatInstance :: KnownNat n => KnownNatInstance n
+
+-- An internal function that is only used for defining the SNat pattern
+-- synonym.
+knownNatInstance :: SNat n -> KnownNatInstance n
+knownNatInstance sn = withKnownNat sn KnownNatInstance
+
+-- | @since 4.18.0.0
+instance Show (SNat n) where
+ showsPrec p (UnsafeSNat n)
+ = showParen (p > appPrec)
+ ( showString "SNat @"
+ . showsPrec appPrec1 n
+ )
+
+-- | @since 4.18.0.0
+instance TestEquality SNat where
+ testEquality (UnsafeSNat x) (UnsafeSNat y)
+ | x == y = Just (unsafeCoerce Refl)
+ | otherwise = Nothing
+
+-- | @since 4.18.0.0
+instance TestCoercion SNat where
+ testCoercion x y = fmap (\Refl -> Coercion) (testEquality x y)
+
+-- | Return the 'Natural' number corresponding to @n@ in an @'SNat' n@ value.
+--
+-- @since 4.18.0.0
+fromSNat :: SNat n -> Natural
+fromSNat (UnsafeSNat n) = n
+
+-- | Convert an explicit @'SNat' n@ value into an implicit @'KnownNat' n@
+-- constraint.
+--
+-- @since 4.18.0.0
+withKnownNat :: forall n rep (r :: TYPE rep).
+ SNat n -> (KnownNat n => r) -> r
+withKnownNat = withDict @(KnownNat n)
-- See Note [withDict] in "GHC.Tc.Instance.Class" in GHC
-withSNat :: forall a b.
- (KnownNat a => Proxy a -> b)
- -> SNat a -> Proxy a -> b
-withSNat f x y = withDict @(KnownNat a) x f y
+
+-- | Convert a 'Natural' number into an @'SNat' n@ value, where @n@ is a fresh
+-- type-level natural number.
+--
+-- @since 4.18.0.0
+withSomeSNat :: forall rep (r :: TYPE rep).
+ Natural -> (forall n. SNat n -> r) -> r
+withSomeSNat n k = k (UnsafeSNat n)
+{-# NOINLINE withSomeSNat #-} -- See Note [NOINLINE withSomeSNat]
=====================================
libraries/base/changelog.md
=====================================
@@ -37,6 +37,12 @@
related discussion, as well as [the migration
guide](https://github.com/haskell/core-libraries-committee/blob/main/guides/functor-combinator-instances-and-class1s.md).
* Add `gcdetails_block_fragmentation_bytes` to `GHC.Stats.GCDetails` to track heap fragmentation.
+ * `GHC.TypeLits` and `GHC.TypeNats` now export the `natSing`, `symbolSing`,
+ and `charSing` methods of `KnownNat`, `KnownSymbol`, and `KnownChar`,
+ respectively. They also export the `SNat`, `SSymbol`, and `SChar` types
+ that are used in these methods and provide an API to interact with these
+ types, per
+ [CLC proposal #85](https://github.com/haskell/core-libraries-committee/issues/85).
## 4.17.0.0 *August 2022*
=====================================
libraries/base/tests/T15183.hs
=====================================
@@ -0,0 +1,31 @@
+{-# LANGUAGE DataKinds #-}
+module Main (main) where
+
+import Control.Exception (ArithException(..), throw)
+import Data.Proxy (Proxy(..))
+import GHC.TypeLits ( KnownChar, KnownNat, KnownSymbol
+ , SChar, Nat, SNat, Symbol, SSymbol
+ , charVal, natVal, symbolVal
+ , withKnownChar, withKnownNat, withKnownSymbol
+ , withSomeSChar, withSomeSNat, withSomeSSymbol )
+
+-- As found in the `reflection` library
+reifyNat :: Integer -> (forall (n :: Nat). KnownNat n => Proxy n -> r) -> r
+reifyNat n k = withSomeSNat n $ \(mbSn :: Maybe (SNat n)) ->
+ case mbSn of
+ Just sn -> withKnownNat sn $ k @n Proxy
+ Nothing -> throw Underflow
+
+reifySymbol :: String -> (forall (s :: Symbol). KnownSymbol s => Proxy s -> r) -> r
+reifySymbol s k = withSomeSSymbol s $ \(ss :: SSymbol s) ->
+ withKnownSymbol ss $ k @s Proxy
+
+reifyChar :: Char -> (forall (c :: Char). KnownChar c => Proxy c -> r) -> r
+reifyChar c k = withSomeSChar c $ \(sc :: SChar c) ->
+ withKnownChar sc (k @c Proxy)
+
+main :: IO ()
+main = do
+ reifyNat 42 $ \(_ :: Proxy n) -> print $ natVal $ Proxy @n
+ reifySymbol "hi" $ \(_ :: Proxy s) -> print $ symbolVal $ Proxy @s
+ reifyChar 'a' $ \(_ :: Proxy c) -> print $ charVal $ Proxy @c
=====================================
libraries/base/tests/T15183.stdout
=====================================
@@ -0,0 +1,3 @@
+42
+"hi"
+'a'
=====================================
libraries/base/tests/all.T
=====================================
@@ -257,6 +257,7 @@ test('T13167',
[when(opsys('mingw32'), only_ways(['winio', 'winio_threaded'])),
fragile_for(16536, concurrent_ways)],
compile_and_run, [''])
+test('T15183', normal, compile_and_run, [''])
test('T15349', [exit_code(1), expect_broken_for(15349, ['ghci'])], compile_and_run, [''])
test('T16111', exit_code(1), compile_and_run, [''])
test('T16943a', normal, compile_and_run, [''])
=====================================
testsuite/tests/dependent/should_compile/RaeJobTalk.hs
=====================================
@@ -13,7 +13,7 @@ module RaeJobTalk where
import Data.Type.Bool
import Data.Type.Equality hiding ((:~~:)(..))
-import GHC.TypeLits
+import GHC.TypeLits hiding (SSymbol)
import Data.Proxy
import GHC.Exts hiding (Lifted, BoxedRep)
import Data.Kind
=====================================
testsuite/tests/ghci/scripts/T19667Ghci.hs
=====================================
@@ -18,7 +18,7 @@ class KnownSymbol (n :: Symbol) where
symbolVal :: forall n proxy . KnownSymbol n => proxy n -> String
symbolVal _ = case symbolSing :: SSymbol n of SSymbol x -> x
--- See Note [NOINLINE someNatVal] in GHC.TypeNats
+-- See Note [NOINLINE withSomeSNat] in GHC.TypeNats
{-# NOINLINE reifySymbol #-}
reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
reifySymbol n k = withDict @(KnownSymbol Any) @(SSymbol Any) (SSymbol n) (k @Any) (Proxy @(Any @Symbol))
=====================================
testsuite/tests/ghci/scripts/T4175.stdout
=====================================
@@ -30,10 +30,10 @@ instance Monoid () -- Defined in ‘GHC.Base’
instance Semigroup () -- Defined in ‘GHC.Base’
instance Bounded () -- Defined in ‘GHC.Enum’
instance Enum () -- Defined in ‘GHC.Enum’
-instance Eq () -- Defined in ‘GHC.Classes’
instance Ord () -- Defined in ‘GHC.Classes’
instance Read () -- Defined in ‘GHC.Read’
instance Show () -- Defined in ‘GHC.Show’
+instance Eq () -- Defined in ‘GHC.Classes’
data instance B () = MkB -- Defined at T4175.hs:14:15
type instance D Int () = String -- Defined at T4175.hs:20:10
type instance D () () = Bool -- Defined at T4175.hs:23:10
@@ -49,24 +49,24 @@ instance Monad Maybe -- Defined in ‘GHC.Base’
instance Semigroup a => Monoid (Maybe a) -- Defined in ‘GHC.Base’
instance Semigroup a => Semigroup (Maybe a)
-- Defined in ‘GHC.Base’
-instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Maybe’
instance Ord a => Ord (Maybe a) -- Defined in ‘GHC.Maybe’
instance Read a => Read (Maybe a) -- Defined in ‘GHC.Read’
instance Show a => Show (Maybe a) -- Defined in ‘GHC.Show’
+instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Maybe’
type instance A (Maybe a) a = a -- Defined at T4175.hs:10:15
type Int :: *
data Int = GHC.Types.I# GHC.Prim.Int#
-- Defined in ‘GHC.Types’
instance [safe] C Int -- Defined at T4175.hs:19:10
-instance Integral Int -- Defined in ‘GHC.Real’
-instance Num Int -- Defined in ‘GHC.Num’
-instance Real Int -- Defined in ‘GHC.Real’
instance Bounded Int -- Defined in ‘GHC.Enum’
instance Enum Int -- Defined in ‘GHC.Enum’
-instance Eq Int -- Defined in ‘GHC.Classes’
+instance Integral Int -- Defined in ‘GHC.Real’
+instance Num Int -- Defined in ‘GHC.Num’
instance Ord Int -- Defined in ‘GHC.Classes’
instance Read Int -- Defined in ‘GHC.Read’
+instance Real Int -- Defined in ‘GHC.Real’
instance Show Int -- Defined in ‘GHC.Show’
+instance Eq Int -- Defined in ‘GHC.Classes’
type instance A Int Int = () -- Defined at T4175.hs:9:15
type instance D Int () = String -- Defined at T4175.hs:20:10
type Z :: * -> Constraint
=====================================
testsuite/tests/ghci/scripts/T9181.stdout
=====================================
@@ -16,6 +16,16 @@ class GHC.TypeLits.KnownSymbol n where
{-# MINIMAL symbolSing #-}
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 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 GHC.TypeLits.SSymbol :: GHC.Types.Symbol -> *
+newtype GHC.TypeLits.SSymbol s = GHC.TypeLits.UnsafeSSymbol String
type GHC.TypeLits.SomeChar :: *
data GHC.TypeLits.SomeChar
= forall (n :: Char).
@@ -38,6 +48,9 @@ GHC.TypeLits.cmpChar ::
GHC.TypeLits.cmpSymbol ::
(GHC.TypeLits.KnownSymbol a, GHC.TypeLits.KnownSymbol b) =>
proxy1 a -> proxy2 b -> Data.Type.Ord.OrderingI a b
+GHC.TypeLits.fromSChar :: GHC.TypeLits.SChar c -> Char
+GHC.TypeLits.fromSNat :: GHC.TypeNats.SNat n -> Integer
+GHC.TypeLits.fromSSymbol :: GHC.TypeLits.SSymbol s -> String
GHC.TypeLits.natVal ::
GHC.TypeNats.KnownNat n => proxy n -> Integer
GHC.TypeLits.natVal' ::
@@ -55,6 +68,21 @@ GHC.TypeLits.symbolVal ::
GHC.TypeLits.KnownSymbol n => proxy n -> String
GHC.TypeLits.symbolVal' ::
GHC.TypeLits.KnownSymbol n => GHC.Prim.Proxy# n -> String
+GHC.TypeLits.withKnownChar ::
+ GHC.TypeLits.SChar c -> (GHC.TypeLits.KnownChar c => r) -> r
+GHC.TypeLits.withKnownSymbol ::
+ GHC.TypeLits.SSymbol s -> (GHC.TypeLits.KnownSymbol s => r) -> r
+GHC.TypeLits.withSomeSChar ::
+ Char -> (forall (c :: Char). GHC.TypeLits.SChar c -> r) -> r
+GHC.TypeLits.withSomeSNat ::
+ Integer
+ -> (forall (n :: GHC.TypeNats.Nat).
+ Maybe (GHC.TypeNats.SNat n) -> r)
+ -> r
+GHC.TypeLits.withSomeSSymbol ::
+ String
+ -> (forall (s :: GHC.Types.Symbol). GHC.TypeLits.SSymbol s -> r)
+ -> r
type (GHC.TypeNats.*) :: GHC.Num.Natural.Natural
-> GHC.Num.Natural.Natural -> GHC.Num.Natural.Natural
type family (GHC.TypeNats.*) a b
@@ -123,6 +151,12 @@ data Data.Type.Ord.OrderingI a b where
Data.Type.Ord.GTI :: forall {k} (a :: k) (b :: k).
(Data.Type.Ord.Compare a b ~ 'GT) =>
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 GHC.TypeNats.SNat :: GHC.TypeNats.Nat -> *
+newtype GHC.TypeNats.SNat n
+ = GHC.TypeNats.UnsafeSNat GHC.Num.Natural.Natural
type GHC.TypeNats.SomeNat :: *
data GHC.TypeNats.SomeNat
= forall (n :: GHC.TypeNats.Nat).
@@ -142,3 +176,5 @@ GHC.TypeNats.cmpNat ::
GHC.TypeNats.sameNat ::
(GHC.TypeNats.KnownNat a, GHC.TypeNats.KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a Data.Type.Equality.:~: b)
+GHC.TypeNats.withKnownNat ::
+ GHC.TypeNats.SNat n -> (GHC.TypeNats.KnownNat n => r) -> r
=====================================
testsuite/tests/ghci/scripts/ghci064.stdout
=====================================
@@ -36,14 +36,14 @@ instance Foreign.Storable.Storable Bool
-- Defined in ‘Foreign.Storable’
instance GHC.Generics.Generic Bool -- Defined in ‘GHC.Generics’
instance GHC.Bits.Bits Bool -- Defined in ‘GHC.Bits’
-instance GHC.Bits.FiniteBits Bool -- Defined in ‘GHC.Bits’
-instance GHC.Ix.Ix Bool -- Defined in ‘GHC.Ix’
instance Bounded Bool -- Defined in ‘GHC.Enum’
instance Enum Bool -- Defined in ‘GHC.Enum’
-instance Eq Bool -- Defined in ‘GHC.Classes’
+instance GHC.Bits.FiniteBits Bool -- Defined in ‘GHC.Bits’
+instance GHC.Ix.Ix Bool -- Defined in ‘GHC.Ix’
instance Ord Bool -- Defined in ‘GHC.Classes’
instance Read Bool -- Defined in ‘GHC.Read’
instance Show Bool -- Defined in ‘GHC.Show’
+instance Eq Bool -- Defined in ‘GHC.Classes’
instance Traversable ((,) Int) -- Defined in ‘Data.Traversable’
instance Foldable ((,) Int) -- Defined in ‘Data.Foldable’
instance Functor ((,) Int) -- Defined in ‘GHC.Base’
=====================================
testsuite/tests/typecheck/should_run/T16646.hs
=====================================
@@ -21,7 +21,7 @@ instance KnownNat n => Reifies n Integer where
reflect = natVal
reify :: forall a r. a -> (forall (s :: Type). Reifies s a => Proxy s -> r) -> r
-{-# NOINLINE reify #-} -- See Note [NOINLINE someNatVal] in GHC.TypeNats
+{-# NOINLINE reify #-} -- See Note [NOINLINE withSomeSNat] in GHC.TypeNats
reify a k = withDict @(Reifies (Any @Type) a)
@(forall (proxy :: Type -> Type). proxy Any -> a)
(const a) (k @Any) Proxy
=====================================
testsuite/tests/typecheck/should_run/T19667.hs
=====================================
@@ -18,7 +18,7 @@ class KnownSymbol (n :: Symbol) where
symbolVal :: forall n proxy . KnownSymbol n => proxy n -> String
symbolVal _ = case symbolSing :: SSymbol n of SSymbol x -> x
--- See Note [NOINLINE someNatVal] in GHC.TypeNats
+-- See Note [NOINLINE withSomeSNat] in GHC.TypeNats
{-# NOINLINE reifySymbol #-}
reifySymbol :: forall r. String -> (forall (n :: Symbol). KnownSymbol n => Proxy n -> r) -> r
reifySymbol n k = withDict @(KnownSymbol Any) @(SSymbol Any) (SSymbol n) (k @Any) (Proxy @(Any @Symbol))
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/532de36870ed9e880d5f146a478453701e9db25d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/532de36870ed9e880d5f146a478453701e9db25d
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/20221007/95fc3759/attachment-0001.html>
More information about the ghc-commits
mailing list