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

-- |
-- Module      : GHC.TypeLits.Witnesses
-- Copyright   : (c) Justin Le 2024
-- 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 (SNat),
  SomeNat (SomeNat_),
  Natural (FromSNat),
  fromSNat,
  withKnownNat,
  withSomeNat,
  toSomeNat,

  -- ** Operations
  (%+),
  (%-),
  minusSNat,
  minusSNat_,
  (%*),
  (%^),

  -- ** Compare
  (%<=?),
  sCmpNat,

  -- ** Unsafe
  unsafeLiftNatOp1,
  unsafeLiftNatOp2,

  -- * Symbols
  SSymbol (SSymbol),
  SomeSymbol (SomeSymbol_),
  pattern FromSSymbol,
  fromSSymbol,
  withKnownSymbol,
  withSomeSymbol,
  toSomeSymbol,
) where

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

#if MIN_VERSION_base(4,20,0)
import GHC.TypeLits (SSymbol, pattern SSymbol)
import GHC.TypeNats (SNat, pattern SNat)
#else
import Data.GADT.Compare
import Data.GADT.Show
import GHC.TypeLits (sameSymbol)
import GHC.TypeNats (sameNat)
#endif

{-# ANN module "HLint: ignore Use fewer imports" #-}

#if !MIN_VERSION_base(4,20,0)
-- | 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.
--
-- Note that this type exists in base as of base 4.18.0 (GHC 9.6)
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString String
"SNat @" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Nat -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 (SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
x)

instance GShow SNat where
  gshowsPrec :: forall (n :: Nat). Int -> SNat n -> ShowS
gshowsPrec = Int -> SNat a -> ShowS
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) =
    (((a :~: b) -> a :~: b) -> Maybe (a :~: b) -> Maybe (a :~: b))
-> Maybe (a :~: b) -> ((a :~: b) -> a :~: b) -> Maybe (a :~: b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a :~: b) -> a :~: b) -> Maybe (a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)) (((a :~: b) -> a :~: b) -> Maybe (a :~: b))
-> ((a :~: b) -> a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case
      a :~: b
Refl -> a :~: a
a :~: b
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 = SNat a -> SNat b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
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 = SCmpNat a b -> GOrdering a b
forall (n :: Nat) (m :: Nat). SCmpNat n m -> GOrdering n m
cmpNatGOrdering (SCmpNat a b -> GOrdering a b)
-> (SNat b -> SCmpNat a b) -> SNat b -> GOrdering a b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat a -> SNat b -> SCmpNat a b
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SCmpNat n m
sCmpNat SNat a
x
#endif

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 $mSomeNat_ :: forall {r}.
SomeNat -> (forall {n :: Nat}. SNat n -> r) -> ((# #) -> r) -> r
$bSomeNat_ :: forall (n :: Nat). SNat n -> SomeNat
SomeNat_ x <- (\case SomeNat (Proxy n
Proxy :: Proxy n) -> SNat n -> SomeNat__
forall (n :: Nat). SNat n -> SomeNat__
SomeNat__ (SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat :: SNat n) -> SomeNat__ x)
  where
    SomeNat_ (SNat n
SNat :: SNat n) = Proxy n -> SomeNat
forall (n :: Nat). KnownNat n => Proxy n -> SomeNat
SomeNat (Proxy n
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 $mFromSNat :: forall {r}.
Nat -> (forall {n :: Nat}. SNat n -> r) -> ((# #) -> r) -> r
$bFromSNat :: forall (n :: Nat). SNat n -> Nat
FromSNat x <- ((`withSomeNat` SomeNat_) -> SomeNat_ x)
  where
    FromSNat = SNat n -> Nat
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 = r
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 = SNat n -> r
forall (n :: Nat). SNat n -> r
x (SNat n
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 = SNat n -> Nat
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 = Nat -> (forall (n :: Nat). SNat n -> SNat m) -> SNat m
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeNat (Nat -> Nat
f (SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
x)) SNat n -> SNat m
forall (n :: Nat). SNat n -> SNat m
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 = Nat -> (forall (n :: Nat). SNat n -> SNat o) -> SNat o
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeNat (Nat -> Nat -> Nat
f (SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
x) (SNat m -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat m
y)) SNat n -> SNat o
forall (n :: Nat). SNat n -> SNat o
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)
(%+) = (Nat -> Nat -> 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 Nat -> Nat -> Nat
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)
(%-) = (Nat -> Nat -> 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 (SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat -> Nat
x) (SNat m -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat -> Nat
y) = case Nat -> Nat -> Maybe Nat
minusNaturalMaybe Nat
x Nat
y of
  Maybe Nat
Nothing -> (CmpNat n m :~: 'LT) -> Either (CmpNat n m :~: 'LT) (SNat (n - m))
forall a b. a -> Either a b
Left ((Any :~: Any) -> CmpNat n m :~: 'LT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl)
  Just Nat
z -> Nat
-> (forall (n :: Nat).
    SNat n -> Either (CmpNat n m :~: 'LT) (SNat (n - m)))
-> Either (CmpNat n m :~: 'LT) (SNat (n - m))
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeNat Nat
z (SNat (n - m) -> Either (CmpNat n m :~: 'LT) (SNat (n - m))
forall a b. b -> Either a b
Right (SNat (n - m) -> Either (CmpNat n m :~: 'LT) (SNat (n - m)))
-> (SNat n -> SNat (n - m))
-> SNat n
-> Either (CmpNat n m :~: 'LT) (SNat (n - m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat n -> SNat (n - m)
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 = ((CmpNat n m :~: 'LT) -> Maybe (SNat (n - m)))
-> (SNat (n - m) -> Maybe (SNat (n - m)))
-> Either (CmpNat n m :~: 'LT) (SNat (n - m))
-> Maybe (SNat (n - m))
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (SNat (n - m))
-> (CmpNat n m :~: 'LT) -> Maybe (SNat (n - m))
forall a b. a -> b -> a
const Maybe (SNat (n - m))
forall a. Maybe a
Nothing) SNat (n - m) -> Maybe (SNat (n - m))
forall a. a -> Maybe a
Just (Either (CmpNat n m :~: 'LT) (SNat (n - m))
 -> Maybe (SNat (n - m)))
-> (SNat m -> Either (CmpNat n m :~: 'LT) (SNat (n - m)))
-> SNat m
-> Maybe (SNat (n - m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat n -> SNat m -> Either (CmpNat n m :~: 'LT) (SNat (n - m))
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)
(%*) = (Nat -> Nat -> 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 Nat -> Nat -> Nat
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)
(%^) = (Nat -> Nat -> 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 Nat -> Nat -> Nat
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 SNat n -> SNat m -> n :<=? m
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 = SNat n -> SNat m -> SCmpNat n m
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

#if !MIN_VERSION_base(4,20,0)
-- | 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.
--
-- Note that this type exists in base as of base 4.18.0 (GHC 9.6)
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString String
"SSymbol @" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 (SSymbol n -> String
forall (n :: Symbol). SSymbol n -> String
fromSSymbol SSymbol n
x)

instance GShow SSymbol where
  gshowsPrec :: forall (n :: Symbol). Int -> SSymbol n -> ShowS
gshowsPrec = Int -> SSymbol a -> ShowS
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) =
    (((a :~: b) -> a :~: b) -> Maybe (a :~: b) -> Maybe (a :~: b))
-> Maybe (a :~: b) -> ((a :~: b) -> a :~: b) -> Maybe (a :~: b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((a :~: b) -> a :~: b) -> Maybe (a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> Type)
       (proxy2 :: Symbol -> Type).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameSymbol (Proxy a
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy b
forall {k} (t :: k). Proxy t
Proxy :: Proxy m)) (((a :~: b) -> a :~: b) -> Maybe (a :~: b))
-> ((a :~: b) -> a :~: b) -> Maybe (a :~: b)
forall a b. (a -> b) -> a -> b
$ \case
      a :~: b
Refl -> a :~: a
a :~: b
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 = SSymbol a -> SSymbol b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol 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 String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (SSymbol a -> String
forall (n :: Symbol). SSymbol n -> String
fromSSymbol SSymbol a
x) (SSymbol b -> String
forall (n :: Symbol). SSymbol n -> String
fromSSymbol SSymbol b
y) of
    Ordering
LT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GLT
    Ordering
EQ -> GOrdering Any Any -> GOrdering a b
forall a b. a -> b
unsafeCoerce GOrdering Any Any
forall {k} (a :: k). GOrdering a a
GEQ
    Ordering
GT -> GOrdering a b
forall {k} (a :: k) (b :: k). GOrdering a b
GGT
#endif

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 $mSomeSymbol_ :: forall {r}.
SomeSymbol
-> (forall {n :: Symbol}. SSymbol n -> r) -> ((# #) -> r) -> r
$bSomeSymbol_ :: forall (n :: Symbol). SSymbol n -> SomeSymbol
SomeSymbol_ x <-
  (\case SomeSymbol (Proxy n
Proxy :: Proxy n) -> SSymbol n -> SomeSymbol__
forall (n :: Symbol). SSymbol n -> SomeSymbol__
SomeSymbol__ (SSymbol n
forall (n :: Symbol). KnownSymbol n => SSymbol n
SSymbol :: SSymbol n) -> SomeSymbol__ x)
  where
    SomeSymbol_ (SSymbol n
SSymbol :: SSymbol n) = Proxy n -> SomeSymbol
forall (n :: Symbol). KnownSymbol n => Proxy n -> SomeSymbol
SomeSymbol (Proxy n
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 $mFromSSymbol :: forall {r}.
String
-> (forall {n :: Symbol}. SSymbol n -> r) -> ((# #) -> r) -> r
$bFromSSymbol :: forall (n :: Symbol). SSymbol n -> String
FromSSymbol x <- ((`withSomeSymbol` SomeSymbol_) -> SomeSymbol_ x)
  where
    FromSSymbol = SSymbol n -> String
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 = r
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 = SSymbol n -> r
forall (n :: Symbol). SSymbol n -> r
x (SSymbol n
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 = SSymbol n -> String
forall (n :: Symbol) (proxy :: Symbol -> Type).
KnownSymbol n =>
proxy n -> String
symbolVal SSymbol n
x