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.

7 files changed, 49 insertions, 13 deletions

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