[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 3 commits: rts: don't enforce aligned((8)) on 32-bit targets

Marge Bot (@marge-bot) gitlab at gitlab.haskell.org
Thu Oct 6 14:44:46 UTC 2022



Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC


Commits:
8a31d02e by Cheng Shao at 2022-10-05T20:40:41-04:00
rts: don't enforce aligned((8)) on 32-bit targets

We simply need to align to the word size for pointer tagging to work. On
32-bit targets, aligned((8)) is wasteful.

- - - - -
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.

- - - - -
3747e5ff by sheaf at 2022-10-06T10:44:21-04:00
Remove mention of make from README.md

- - - - -


16 changed files:

- README.md
- 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
- rts/include/Stg.h
- 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:

=====================================
README.md
=====================================
@@ -53,19 +53,22 @@ For building library documentation, you'll need [Haddock][6].  To build
 the compiler documentation, you need [Sphinx](http://www.sphinx-doc.org/)
 and Xelatex (only for PDF output).
 
-**Quick start**: the following gives you a default build:
+**Quick start**: GHC is built using the [Hadrian build system](hadrian/README.md).
+The following gives you a default build:
 
     $ ./boot
     $ ./configure
-    $ make         # can also say 'make -jX' for X number of jobs
-    $ make install
+    $ hadrian/build         # can also say '-jX' for X number of jobs
 
   On Windows, you need an extra repository containing some build tools.
   These can be downloaded for you by configure. This only needs to be done once by running:
 
     $ ./configure --enable-tarballs-autodownload
 
-(NB: **Do you have multiple cores? Be sure to tell that to `make`!** This can
+  Additionally, on Windows, to run Hadrian you should run `hadrian/build.bat`
+  instead of `hadrian/build`.
+
+(NB: **Do you have multiple cores? Be sure to tell that to `hadrian`!** This can
 save you hours of build time depending on your system configuration, and is
 almost always a win regardless of how many cores you have. As a simple rule,
 you should have about N+1 jobs, where `N` is the amount of cores you have.)


=====================================
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, [''])


=====================================
rts/include/Stg.h
=====================================
@@ -263,8 +263,8 @@ typedef StgFunPtr       F_;
 #define EB_(X)    extern const char X[]
 #define IB_(X)    static const char X[]
 /* static (non-heap) closures (requires alignment for pointer tagging): */
-#define EC_(X)    extern       StgWordArray (X) GNU_ATTRIBUTE(aligned (8))
-#define IC_(X)    static       StgWordArray (X) GNU_ATTRIBUTE(aligned (8))
+#define EC_(X)    extern       StgWordArray (X) GNU_ATTRIBUTE(aligned (SIZEOF_VOID_P))
+#define IC_(X)    static       StgWordArray (X) GNU_ATTRIBUTE(aligned (SIZEOF_VOID_P))
 /* writable data (does not require alignment): */
 #define ERW_(X)   extern       StgWordArray (X)
 #define IRW_(X)   static       StgWordArray (X)


=====================================
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/-/compare/92e77807cce348eadcecedeec839de54c5d97266...3747e5fff089a9e67f4468433e026171d91708d6

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/92e77807cce348eadcecedeec839de54c5d97266...3747e5fff089a9e67f4468433e026171d91708d6
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/20221006/74a70892/attachment-0001.html>


More information about the ghc-commits mailing list