{-# LANGUAGE ConstraintKinds           #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE LambdaCase                #-}
{-# LANGUAGE PatternSynonyms           #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE StandaloneDeriving        #-}
{-# LANGUAGE NoStarIsType              #-}
{-# LANGUAGE TypeInType                #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE ViewPatterns              #-}

-- |
-- Module      : GHC.TypeLits.Witnesses
-- Copyright   : (c) Justin Le 2016
-- License     : MIT
-- Maintainer  : justin@jle.im
-- Stability   : unstable
-- Portability : non-portable
--
-- This module essentially provides a lightweight subset of the
-- /singletons/ library specifically for 'Nat' and 'Symbol', from
-- "GHC.TypeLits".
--
-- Its main functionality is for first-class manipulation of 'KnownNat' and
-- 'KnownSymbol' constraints.  For example, in general, if you have
-- @'KnownNat' n@, GHC can't infer @'KnownNat' (n + 1)@.  And, if you have
-- both @'KnownNat' n@ and @'KnownNat' m@, GHC can't infer @'KnownNat (n
-- + m)@.
--
-- This can be annoying when dealing with libraries and applications where
-- one regularly adds and subtracts type-level nats and expects 'KnownNat'
-- instances to follow.  For example, vector concatenation of
-- length-encoded vector types can be:
--
-- @
-- concat :: ('KnownNat' n, 'KnownNat' m) => Vector n a -> Vector m a -> Vector (n + m) a
-- @
--
-- But, now @n + m@ does not have a 'KnownNat' instance...which makes
-- operations like this much less useful.
--
-- Usually, the easiest way to get around this is to use a typechecker
-- plugin, like
-- <https://hackage.haskell.org/package/ghc-typelits-knownnat>.  However,
-- we can do this without the help of a typechecker plugin using
-- first-class values, at the cost of some increased verbosity.
--
-- We introduce @'SNat' n@, which is a term-level witness of knownnat-ness
-- that can be manipulated as a first-class value.
--
-- If we have @'KnownNat' n@, we can construct an @'SNat' n@:
--
-- @
-- 'SNat' :: KnownNat n -> SNat n
-- @
--
-- Furthermore, if we have an @'SNat' n@, we can /pattern match/ on the
-- 'SNat' constructor to get a @'KnownNat' n@ constraint:
--
-- @
-- myFunc :: SNat n -> Bool
-- myFunc SNat = ...  -- in this body, we have `KnownNat n`
-- @
--
-- So if we have @'KnownNat' n@ and @'KnownNat' m@, we can get @'KnownNat'
-- (n + m)@ by using '%+', which adds together 'SNat's:
--
-- @
-- case (SNat :: SNat n) %+ (SNat :: SNat m) of
--   SNat -> -- in this branch, we have `KnownNat (n + m)`
-- @
--
-- Note that this module converts between 'SNat' and 'Natural', and not
-- 'SNat' and 'Integer', in "GHC.TypeNats"-style.
--
-- Of course, all of this functionality is provided by the /singletons/
-- library, in "Data.Singletons.TypeLits".  This module can be useful if
-- you want a lightweight alternative without the full might of
-- /singletons/.  The main benefit of the /singletons/ library is providing
-- a unified interface for singletons of /all/ different kinds/types, and
-- not just 'Natural' and 'String'.
module GHC.TypeLits.Witnesses (
  -- * Nats
    SNat(..)
  , SomeNat(SomeNat_)
  , Natural(FromSNat)
  , fromSNat
  , withKnownNat
  , withSomeNat
  , toSomeNat
  -- ** Operations
  , (%+)
  , (%-)
  , minusSNat
  , minusSNat_
  , (%*)
  , (%^)
  -- ** Compare
  , (%<=?)
  , sCmpNat
  -- ** Unsafe
  , unsafeLiftNatOp1
  , unsafeLiftNatOp2
  -- * Symbols
  , SSymbol(..)
  , SomeSymbol(SomeSymbol_)
  , pattern FromSSymbol
  , fromSSymbol
  , withKnownSymbol
  , withSomeSymbol
  , toSomeSymbol
  ) where

import           Data.GADT.Compare
import           Data.GADT.Show
import           Data.Proxy
import           Data.Type.Equality
import           GHC.Natural
import           GHC.TypeLits ( KnownSymbol, SomeSymbol(..)
                              , symbolVal, someSymbolVal, sameSymbol )
import           GHC.TypeLits.Compare hiding ((%<=?))
import           GHC.TypeNats ( KnownNat, SomeNat(..), CmpNat
                              , type (+), type (-), type (*), type (^)
                              , natVal, someNatVal, sameNat )
import           Unsafe.Coerce
import qualified GHC.TypeLits.Compare        as Comp

-- | An @'SNat' n@ is a witness for @'KnownNat' n@.
--
-- This means that if you pattern match on the 'SNat' constructor, in that
-- branch you will have a @'KnownNat' n@ constraint.
--
-- @
-- myFunc :: SNat n -> Bool
-- myFunc SNat = ...  -- in this body, we have `KnownNat n`
-- @
--
-- This is essentially a singleton for 'Nat', and stands in for the
-- /singletons/ 'SNat' and 'Data.Singleton.Sing' types.
data SNat n = KnownNat n => SNat

deriving instance Eq (SNat n)
deriving instance Ord (SNat n)

instance Show (SNat n) where
    showsPrec :: Int -> SNat n -> ShowS
showsPrec Int
d x :: SNat n
x@SNat n
SNat = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString String
"SNat @" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 (forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
x)

instance GShow SNat where
    gshowsPrec :: forall (n :: Nat). Int -> SNat n -> ShowS
gshowsPrec = forall a. Show a => Int -> a -> ShowS
showsPrec

instance TestEquality SNat where
    testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
testEquality (SNat a
SNat :: SNat n) (SNat b
SNat :: SNat m) =
      forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (forall {k} (t :: k). Proxy t
Proxy :: Proxy m)) forall a b. (a -> b) -> a -> b
$ \case
        a :~: b
Refl -> forall {k} (a :: k). a :~: a
Refl

instance GEq SNat where
    geq :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
geq = forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality

instance GCompare SNat where
    gcompare :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> GOrdering a b
gcompare SNat a
x = forall (n :: Nat) (m :: Nat). SCmpNat n m -> GOrdering n m
cmpNatGOrdering forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SCmpNat n m
sCmpNat SNat a
x

data SomeNat__ = forall n. SomeNat__ (SNat n)

-- | A useful pattern synonym for matching on a 'SomeNat' as if it
-- contained an @'SNat' n@, and not a @'Proxy' n@ as it exists in
-- "GHC.TypeLits".
--
-- A layer of compatibility letting us use the original 'SomeNat' type in
-- a way that works well with 'SNat'.
--
-- This stands in for the /singletons/ 'Data.Singleton.SomeSing' constructor.
pattern SomeNat_ :: SNat n -> SomeNat
pattern $bSomeNat_ :: forall (n :: Nat). SNat n -> SomeNat
$mSomeNat_ :: forall {r}.
SomeNat -> (forall {n :: Nat}. SNat n -> r) -> ((# #) -> r) -> r
SomeNat_ x <- ((\case SomeNat (Proxy n
Proxy :: Proxy n) -> forall (n :: Nat). SNat n -> SomeNat__
SomeNat__ (forall (n :: Nat). KnownNat n => SNat n
SNat :: SNat n)) -> SomeNat__ x)
  where
    SomeNat_ (SNat n
SNat :: SNat n) = forall (n :: Nat). KnownNat n => Proxy n -> SomeNat
SomeNat (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# COMPLETE SomeNat_ #-}

-- | A useful pattern synonym for matching on a 'Natural' as if it "were"
-- a 'SNat':
--
-- @
-- myFunc :: Natural -> Bool
-- myFunc (FromSNat x) = ...  -- x is `SNat n`, with `n` coming from the input
-- @
--
-- It can be used as a function, as well, to convert an @'SNat' n@ back
-- into the 'Natural' that it represents.
--
-- This stands in for the /singletons/ 'Data.Singleton.FromSing' pattern synonym.
pattern FromSNat :: SNat n -> Natural
pattern $bFromSNat :: forall (n :: Nat). SNat n -> Nat
$mFromSNat :: forall {r}.
Nat -> (forall {n :: Nat}. SNat n -> r) -> ((# #) -> r) -> r
FromSNat x <- ((\Nat
i -> forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeNat Nat
i forall (n :: Nat). SNat n -> SomeNat
SomeNat_) -> SomeNat_ x)
  where
    FromSNat = forall (n :: Nat). SNat n -> Nat
fromSNat
{-# COMPLETE FromSNat #-}

-- | Given an @'SNat' n@ and a value that would require a @'KnownNat' n@
-- instance, create that value.
--
-- This stands in for the function of the same name from
-- "Data.Singletons.TypeLits".
withKnownNat :: SNat n -> (KnownNat n => r) -> r
withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
SNat KnownNat n => r
x = KnownNat n => r
x

-- | Promote ("reify") a 'Natural' to an @'SNat' n@, by providing
-- a continuation that would handle it in a way that is polymorphic over
-- all possible @n@.
--
-- This stands in the /singletons/ 'Data.Singleton.withSomeSing' function.
withSomeNat :: Natural -> (forall n. SNat n -> r) -> r
withSomeNat :: forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeNat (Nat -> SomeNat
someNatVal->SomeNat (Proxy n
Proxy :: Proxy n)) forall (n :: Nat). SNat n -> r
x = forall (n :: Nat). SNat n -> r
x (forall (n :: Nat). KnownNat n => SNat n
SNat :: SNat n)

-- | Promote ("reify") a 'Natural' to an @'SNat' n@ existentially hidden
-- inside a 'SomeNat'.  To use it, pattern match using 'SomeNat_'.
--
-- This stands in the /singletons/ 'Data.Singleton.toSomeSing' function.
toSomeNat :: Natural -> SomeNat
toSomeNat :: Nat -> SomeNat
toSomeNat = Nat -> SomeNat
someNatVal

-- | Convert ("reflect") an 'SNat' back into the 'Natural' it represents.
--
-- This stands in the /singletons/ 'Data.Singleton.fromSing' function.
fromSNat :: SNat n -> Natural
fromSNat :: forall (n :: Nat). SNat n -> Nat
fromSNat x :: SNat n
x@SNat n
SNat = forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal SNat n
x

-- | Lift a unary operation to act on an @'SNat' n@ that returns an @'SNat'
-- m@.  The function given must properly describe the relationship between
-- @n@ and @m@.
--
-- For example:
--
-- @
-- double :: SNat n -> SNat (n * 2)
-- double = unsafeLiftNatOp1 (*2)
-- @
--
-- The correctness of the relationship is not checked, so be aware that
-- this can cause programs to break.
unsafeLiftNatOp1
    :: (Natural -> Natural)
    -> SNat n
    -> SNat m
unsafeLiftNatOp1 :: forall (n :: Nat) (m :: Nat). (Nat -> Nat) -> SNat n -> SNat m
unsafeLiftNatOp1 Nat -> Nat
f SNat n
x = forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeNat (Nat -> Nat
f (forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
x)) forall a b. a -> b
unsafeCoerce

-- | Lift a binary operation to act on an @'SNat' n@ and @'SNat' m@ that
-- returns an @'SNat' o@.  The function given must properly describe the
-- relationship between @n@, @m@, and @o@.
--
-- For example:
--
-- @
-- multiply :: SNat n -> SNat m -> SNat (n * m)
-- multiply = unsafeLiftNatOp2 (*)
-- @
--
-- The correctness of the relationship is not checked, so be aware that
-- this can cause programs to break.
unsafeLiftNatOp2
    :: (Natural -> Natural -> Natural)
    -> SNat n
    -> SNat m
    -> SNat o
unsafeLiftNatOp2 :: forall (n :: Nat) (m :: Nat) (o :: Nat).
(Nat -> Nat -> Nat) -> SNat n -> SNat m -> SNat o
unsafeLiftNatOp2 Nat -> Nat -> Nat
f SNat n
x SNat m
y = forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeNat (Nat -> Nat -> Nat
f (forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
x) (forall (n :: Nat). SNat n -> Nat
fromSNat SNat m
y)) forall a b. a -> b
unsafeCoerce

-- | Addition of 'SNat's.
--
-- This also will provide the correct 'KnownNat' instance for @'SNat' (n
-- + m)@, so can be used as a way to "add" 'KnownNat' instances.
--
-- This stands in for the function with the same name from
-- "Data.Singletons.Prelude.Num".
(%+) :: SNat n -> SNat m -> SNat (n + m)
%+ :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
(%+) = forall (n :: Nat) (m :: Nat) (o :: Nat).
(Nat -> Nat -> Nat) -> SNat n -> SNat m -> SNat o
unsafeLiftNatOp2 forall a. Num a => a -> a -> a
(+)

-- | Subtraction of 'SNat's.  Note that this is unsafe, as will trigger
-- a run-time underflow if @m@ is bigger than @n@ even though it will always
-- succeed at compiletime.
--
-- This also will provide the correct 'KnownNat' instance for @'SNat' (n
-- - m)@, so can be used as a way to "subtract" 'KnownNat' instances.
--
-- This stands in for the function with the same name from
-- "Data.Singletons.Prelude.Num".
(%-) :: SNat n -> SNat m -> SNat (n - m)
%- :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
(%-) = forall (n :: Nat) (m :: Nat) (o :: Nat).
(Nat -> Nat -> Nat) -> SNat n -> SNat m -> SNat o
unsafeLiftNatOp2 (-)

-- | A safe version of '%-': it will return 'Left' if @n@ is less than @m@
-- (with a witness that it is), or else return the subtracted 'SNat' in
-- 'Right' in a way that is guarunteed to not have runtime underflow.
minusSNat
    :: SNat n
    -> SNat m
    -> Either (CmpNat n m :~: 'LT) (SNat (n - m))
minusSNat :: forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> Either (CmpNat n m :~: 'LT) (SNat (n - m))
minusSNat (forall (n :: Nat). SNat n -> Nat
fromSNat->Nat
x) (forall (n :: Nat). SNat n -> Nat
fromSNat->Nat
y) = case Nat -> Nat -> Maybe Nat
minusNaturalMaybe Nat
x Nat
y of
    Maybe Nat
Nothing -> forall a b. a -> Either a b
Left (forall a b. a -> b
unsafeCoerce forall {k} (a :: k). a :~: a
Refl)
    Just Nat
z  -> forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeNat Nat
z (forall a b. b -> Either a b
Right forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b
unsafeCoerce)

-- | A version of 'minusSNat' that just returns a 'Maybe'.
minusSNat_ :: SNat n -> SNat m -> Maybe (SNat (n - m))
minusSNat_ :: forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> Maybe (SNat (n - m))
minusSNat_ SNat n
x = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) (m :: Nat).
SNat n -> SNat m -> Either (CmpNat n m :~: 'LT) (SNat (n - m))
minusSNat SNat n
x

-- | Multiplication of 'SNat's.
--
-- This also will provide the correct 'KnownNat' instance for @'SNat' (n
-- * m)@, so can be used as a way to "multiply" 'KnownNat' instances.
--
-- This stands in for the function with the same name from
-- "Data.Singletons.Prelude.Num".
(%*) :: SNat n -> SNat m -> SNat (n * m)
%* :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n * m)
(%*) = forall (n :: Nat) (m :: Nat) (o :: Nat).
(Nat -> Nat -> Nat) -> SNat n -> SNat m -> SNat o
unsafeLiftNatOp2 forall a. Num a => a -> a -> a
(*)

-- | Exponentiation of 'SNat's.
--
-- This also will provide the correct 'KnownNat' instance for @'SNat' (n
-- ^ m)@, so can be used as a way to "exponentiate" 'KnownNat' instances.
--
-- This stands in for the function with the same name from
-- "Data.Singletons.TypeLits".
(%^) :: SNat n -> SNat m -> SNat (n ^ m)
%^ :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n ^ m)
(%^) = forall (n :: Nat) (m :: Nat) (o :: Nat).
(Nat -> Nat -> Nat) -> SNat n -> SNat m -> SNat o
unsafeLiftNatOp2 forall a b. (Num a, Integral b) => a -> b -> a
(^)

-- | Compare @n@ and @m@, categorizing them into one of the constructors of
-- ':<=?'.
(%<=?) :: SNat n -> SNat m -> n :<=? m
x :: SNat n
x@SNat n
SNat %<=? :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> n :<=? m
%<=? y :: SNat m
y@SNat m
SNat = SNat n
x forall (m :: Nat) (n :: Nat) (p :: Nat -> Type) (q :: Nat -> Type).
(KnownNat m, KnownNat n) =>
p m -> q n -> m :<=? n
Comp.%<=? SNat m
y

-- | Compare @n@ and @m@, categorizing them into one of the constructors of
-- 'SCmpNat'.
sCmpNat :: SNat n -> SNat m -> SCmpNat n m
sCmpNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SCmpNat n m
sCmpNat x :: SNat n
x@SNat n
SNat y :: SNat m
y@SNat m
SNat = forall (m :: Nat) (n :: Nat) (p :: Nat -> Type) (q :: Nat -> Type).
(KnownNat m, KnownNat n) =>
p m -> q n -> SCmpNat m n
GHC.TypeLits.Compare.cmpNat SNat n
x SNat m
y

-- | An @'SSymbol' n@ is a witness for @'KnownSymbol' n@.
--
-- This means that if you pattern match on the 'SSymbol' constructor, in that
-- branch you will have a @'KnownSymbol' n@ constraint.
--
-- @
-- myFunc :: SSymbol n -> Bool
-- myFunc SSymbol = ...  -- in this body, we have `KnownSymbol n`
-- @
--
-- This is essentially a singleton for 'Symbol', and stands in for the
-- /singletons/ 'SSymbol' and 'Data.Singleton.Sing' types.
data SSymbol n = KnownSymbol n => SSymbol

deriving instance Eq (SSymbol n)
deriving instance Ord (SSymbol n)

instance Show (SSymbol n) where
    showsPrec :: Int -> SSymbol n -> ShowS
showsPrec Int
d x :: SSymbol n
x@SSymbol n
SSymbol = Bool -> ShowS -> ShowS
showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
10) forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString String
"SSymbol @" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 (forall (n :: Symbol). SSymbol n -> String
fromSSymbol SSymbol n
x)

instance GShow SSymbol where
    gshowsPrec :: forall (n :: Symbol). Int -> SSymbol n -> ShowS
gshowsPrec = forall a. Show a => Int -> a -> ShowS
showsPrec

instance TestEquality SSymbol where
    testEquality :: forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> Maybe (a :~: b)
testEquality (SSymbol a
SSymbol :: SSymbol n) (SSymbol b
SSymbol :: SSymbol m) =
      forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> Type)
       (proxy2 :: Symbol -> Type).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameSymbol (forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (forall {k} (t :: k). Proxy t
Proxy :: Proxy m)) forall a b. (a -> b) -> a -> b
$ \case
        a :~: b
Refl -> forall {k} (a :: k). a :~: a
Refl

instance GEq SSymbol where
    geq :: forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> Maybe (a :~: b)
geq = forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality

instance GCompare SSymbol where
    gcompare :: forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> GOrdering a b
gcompare SSymbol a
x SSymbol b
y = case forall a. Ord a => a -> a -> Ordering
compare (forall (n :: Symbol). SSymbol n -> String
fromSSymbol SSymbol a
x) (forall (n :: Symbol). SSymbol n -> String
fromSSymbol SSymbol b
y) of
      Ordering
LT -> forall {k} (a :: k) (b :: k). GOrdering a b
GLT
      Ordering
EQ -> forall a b. a -> b
unsafeCoerce forall {k} (a :: k). GOrdering a a
GEQ
      Ordering
GT -> forall {k} (a :: k) (b :: k). GOrdering a b
GGT

data SomeSymbol__ = forall n. SomeSymbol__ (SSymbol n)

-- | A useful pattern synonym for matching on a 'SomeSymbol' as if it
-- contained an @'SSymbol' n@, and not a @'Proxy' n@ as it exists in
-- "GHC.TypeLits".
--
-- A layer of compatibility letting us use the original 'SomeSymbol' type in
-- a way that works well with 'SSymbol'.
--
-- This stands in for the /singletons/ 'Data.Singleton.SomeSing' constructor.
pattern SomeSymbol_ :: SSymbol n -> SomeSymbol
pattern $bSomeSymbol_ :: forall (n :: Symbol). SSymbol n -> SomeSymbol
$mSomeSymbol_ :: forall {r}.
SomeSymbol
-> (forall {n :: Symbol}. SSymbol n -> r) -> ((# #) -> r) -> r
SomeSymbol_ x <- ((\case SomeSymbol (Proxy n
Proxy :: Proxy n) -> forall (n :: Symbol). SSymbol n -> SomeSymbol__
SomeSymbol__ (forall (n :: Symbol). KnownSymbol n => SSymbol n
SSymbol :: SSymbol n)) -> SomeSymbol__ x)
  where
    SomeSymbol_ (SSymbol n
SSymbol :: SSymbol n) = forall (n :: Symbol). KnownSymbol n => Proxy n -> SomeSymbol
SomeSymbol (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
{-# COMPLETE SomeSymbol_ #-}

-- | A useful pattern synonym for matching on a 'String' as if it "were"
-- a 'SSymbol':
--
-- @
-- myFunc :: String -> Bool
-- myFunc (FromSSymbol x) = ...  -- x is `SSymbol n`, with `n` coming from the input
-- @
--
-- It can be used as a function, as well, to convert an @'SSymbol' n@ back
-- into the 'String' that it represents.
--
-- This stands in for the /singletons/ 'Data.Singleton.FromSing' pattern synonym, except
-- it matches on a 'String' instead of a 'Data.Text.Text'.
pattern FromSSymbol :: SSymbol n -> String
pattern $bFromSSymbol :: forall (n :: Symbol). SSymbol n -> String
$mFromSSymbol :: forall {r}.
String
-> (forall {n :: Symbol}. SSymbol n -> r) -> ((# #) -> r) -> r
FromSSymbol x <- ((\String
i -> forall r. String -> (forall (n :: Symbol). SSymbol n -> r) -> r
withSomeSymbol String
i forall (n :: Symbol). SSymbol n -> SomeSymbol
SomeSymbol_) -> SomeSymbol_ x)
  where
    FromSSymbol = forall (n :: Symbol). SSymbol n -> String
fromSSymbol
{-# COMPLETE FromSSymbol #-}

-- | Given an @'SSymbol' n@ and a value that would require a @'KnownSymbol' n@
-- instance, create that value.
--
-- This stands in for the function of the same name from
-- "Data.Singletons.TypeLits".
withKnownSymbol :: SSymbol n -> (KnownSymbol n => r) -> r
withKnownSymbol :: forall (n :: Symbol) r. SSymbol n -> (KnownSymbol n => r) -> r
withKnownSymbol SSymbol n
SSymbol KnownSymbol n => r
x = KnownSymbol n => r
x

-- | Promote ("reify") a 'String' to an @'SSymbol' n@, by providing
-- a continuation that would handle it in a way that is polymorphic over
-- all possible @n@.
--
-- This stands in the /singletons/ 'Data.Singleton.withSomeSing' function, except it takes
-- a 'String' instead of 'Data.Text.Text'.
withSomeSymbol :: String -> (forall n. SSymbol n -> r) -> r
withSomeSymbol :: forall r. String -> (forall (n :: Symbol). SSymbol n -> r) -> r
withSomeSymbol (String -> SomeSymbol
someSymbolVal->SomeSymbol (Proxy n
Proxy :: Proxy n)) forall (n :: Symbol). SSymbol n -> r
x = forall (n :: Symbol). SSymbol n -> r
x (forall (n :: Symbol). KnownSymbol n => SSymbol n
SSymbol :: SSymbol n)

-- | Promote ("reify") a 'String' to an @'SSymbol' n@ existentially hidden
-- inside a 'SomeNat'.  To use it, pattern match using 'SomeSymbol_'.
--
-- This stands in the /singletons/ 'Data.Singleton.toSomeSing' function, except it takes
-- a 'String' instead of 'Data.Text.Text'.
toSomeSymbol :: String -> SomeSymbol
toSomeSymbol :: String -> SomeSymbol
toSomeSymbol = String -> SomeSymbol
someSymbolVal

-- | Convert ("reflect") an 'SSymbol' back into the 'String' it represents.
--
-- This stands in the /singletons/ 'Data.Singleton.fromSing' function, except it returns
-- a 'String' instead of 'Data.Text.Text'.
fromSSymbol :: SSymbol n -> String
fromSSymbol :: forall (n :: Symbol). SSymbol n -> String
fromSSymbol x :: SSymbol n
x@SSymbol n
SSymbol = forall (n :: Symbol) (proxy :: Symbol -> Type).
KnownSymbol n =>
proxy n -> String
symbolVal SSymbol n
x