Export symbolSing, SSymbol, and friends (CLC#85)wip/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 files changed, 500 insertions, 120 deletions

diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs
index 2bac6fa3ab..0d96d4420e 100644
--- a/compiler/GHC/Tc/Instance/Class.hs
+++ b/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
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index a2310fd998..ebd93232e8 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/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.
diff --git a/libraries/base/GHC/TypeNats.hs b/libraries/base/GHC/TypeNats.hs
index 6a71313404..5a460d11c6 100644
--- a/libraries/base/GHC/TypeNats.hs
+++ b/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]
diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md
index 5c07350d7a..d5aa1c3537 100644
--- a/libraries/base/changelog.md
+++ b/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*
 
diff --git a/libraries/base/tests/T15183.hs b/libraries/base/tests/T15183.hs
new file mode 100644
index 0000000000..d2a50adb60
--- /dev/null
+++ b/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
diff --git a/libraries/base/tests/T15183.stdout b/libraries/base/tests/T15183.stdout
new file mode 100644
index 0000000000..b16bd2d77d
--- /dev/null
+++ b/libraries/base/tests/T15183.stdout
@@ -0,0 +1,3 @@
+42
+"hi"
+'a'
diff --git a/libraries/base/tests/all.T b/libraries/base/tests/all.T
index 9da1923e49..e50d28da12 100644
--- a/libraries/base/tests/all.T
+++ b/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, [''])
diff --git a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
index 21d68c2a2b..008ab860e9 100644
--- a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
+++ b/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
diff --git a/testsuite/tests/ghci/scripts/T19667Ghci.hs b/testsuite/tests/ghci/scripts/T19667Ghci.hs
index bc8f36de93..7cc05a8a4e 100644
--- a/testsuite/tests/ghci/scripts/T19667Ghci.hs
+++ b/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))
diff --git a/testsuite/tests/ghci/scripts/T4175.stdout b/testsuite/tests/ghci/scripts/T4175.stdout
index 0d4047425e..16b2ebc26a 100644
--- a/testsuite/tests/ghci/scripts/T4175.stdout
+++ b/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
diff --git a/testsuite/tests/ghci/scripts/T9181.stdout b/testsuite/tests/ghci/scripts/T9181.stdout
index d6bfea3843..f213526d8d 100644
--- a/testsuite/tests/ghci/scripts/T9181.stdout
+++ b/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
diff --git a/testsuite/tests/ghci/scripts/ghci064.stdout b/testsuite/tests/ghci/scripts/ghci064.stdout
index 2d1bb17423..6efaf297bb 100644
--- a/testsuite/tests/ghci/scripts/ghci064.stdout
+++ b/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’
diff --git a/testsuite/tests/typecheck/should_run/T16646.hs b/testsuite/tests/typecheck/should_run/T16646.hs
index 0976215ae9..a86b706313 100644
--- a/testsuite/tests/typecheck/should_run/T16646.hs
+++ b/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
diff --git a/testsuite/tests/typecheck/should_run/T19667.hs b/testsuite/tests/typecheck/should_run/T19667.hs
index bc8f36de93..7cc05a8a4e 100644
--- a/testsuite/tests/typecheck/should_run/T19667.hs
+++ b/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))