{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE RoleAnnotations #-}

{-|
GHC's @DataKinds@ language extension lifts data constructors, natural
numbers, and strings to the type level. This module provides the
primitives needed for working with type-level numbers (the 'Nat' kind),
strings (the 'Symbol' kind), and characters (the 'Char' kind). It also defines the 'TypeError' type
family, a feature that makes use of type-level strings to support user
defined type errors.

For now, this module is the API for working with type-level literals.
However, please note that it is a work in progress and is subject to change.
Once the design of the @DataKinds@ feature is more stable, this will be
considered only an internal GHC module, and the programmer interface for
working with type-level data will be defined in a separate library.

@since base-4.6.0.0
-}

module GHC.Internal.TypeLits
  ( -- * Kinds
    N.Natural, N.Nat, Symbol  -- Symbol is declared in GHC.Types in package ghc-prim

    -- * Linking type and value level
  , N.KnownNat(natSing), natVal, natVal'
  , KnownSymbol(symbolSing), symbolVal, symbolVal'
  , KnownChar(charSing), charVal, charVal'
  , N.SomeNat(..), SomeSymbol(..), SomeChar(..)
  , someNatVal, someSymbolVal, someCharVal
  , N.sameNat, sameSymbol, sameChar
  , N.decideNat, decideSymbol, decideChar
  , 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.-)
  , type N.Div, type N.Mod, type N.Log2
  , AppendSymbol
  , N.CmpNat, CmpSymbol, CmpChar
  , ConsSymbol, UnconsSymbol
  , CharToNat, NatToChar

  -- * User-defined type errors
  , TypeError
  , ErrorMessage(..)

  ) where

import GHC.Internal.Base ( Bool(..), Eq(..), Functor(..), Ord(..), Ordering(..), String
                , (.), otherwise, withDict, Void, (++)
                , errorWithoutStackTrace)
import GHC.Types(Symbol, Char, TYPE)
import GHC.Internal.TypeError(ErrorMessage(..), TypeError)
import GHC.Internal.Num(Integer, fromInteger)
import GHC.Internal.Show(Show(..), appPrec, appPrec1, showParen, showString)
import GHC.Internal.Read(Read(..))
import GHC.Internal.Real(toInteger)
import GHC.Prim(Proxy#)
import GHC.Internal.Data.Either (Either (..))
import GHC.Internal.Data.Maybe (Maybe(..))
import GHC.Internal.Data.Proxy (Proxy(..))
import GHC.Internal.Data.Type.Coercion (Coercion(..), TestCoercion(..))
import GHC.Internal.Data.Type.Equality((:~:)(Refl), TestEquality(..))
import GHC.Internal.Data.Type.Ord(OrderingI(..))
import GHC.Internal.Unsafe.Coerce(unsafeCoerce)

import GHC.Internal.TypeLits.Internal(CmpSymbol, CmpChar)
import qualified GHC.Internal.TypeNats as N

--------------------------------------------------------------------------------

-- | This class gives the string associated with a type-level symbol.
-- There are instances of the class for every concrete literal: "hello", etc.
--
-- @since base-4.7.0.0
class KnownSymbol (n :: Symbol) where
  symbolSing :: SSymbol n

-- | @since base-4.7.0.0
natVal :: forall n proxy. N.KnownNat n => proxy n -> Integer
natVal :: forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy n
p = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (proxy n -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
N.natVal proxy n
p)

-- | @since base-4.7.0.0
symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String
symbolVal :: forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy n
_ = case SSymbol n
forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing :: SSymbol n of
                UnsafeSSymbol String
x -> String
x

-- | @since base-4.8.0.0
natVal' :: forall n. N.KnownNat n => Proxy# n -> Integer
natVal' :: forall (n :: Natural). KnownNat n => Proxy# n -> Integer
natVal' Proxy# n
p = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Proxy# n -> Natural
forall (n :: Natural). KnownNat n => Proxy# n -> Natural
N.natVal' Proxy# n
p)

-- | @since base-4.8.0.0
symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String
symbolVal' :: forall (n :: Symbol). KnownSymbol n => Proxy# n -> String
symbolVal' Proxy# n
_ = case SSymbol n
forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing :: SSymbol n of
                UnsafeSSymbol String
x -> String
x


-- | This type represents unknown type-level symbols.
data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n)
                  -- ^ @since base-4.7.0.0

-- | @since base-4.16.0.0
class KnownChar (n :: Char) where
  charSing :: SChar n

charVal :: forall n proxy. KnownChar n => proxy n -> Char
charVal :: forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal proxy n
_ = case SChar n
forall (n :: Char). KnownChar n => SChar n
charSing :: SChar n of
                 UnsafeSChar Char
x -> Char
x

charVal' :: forall n. KnownChar n => Proxy# n -> Char
charVal' :: forall (n :: Char). KnownChar n => Proxy# n -> Char
charVal' Proxy# n
_ = case SChar n
forall (n :: Char). KnownChar n => SChar n
charSing :: SChar n of
                UnsafeSChar Char
x -> Char
x

data SomeChar = forall n. KnownChar n => SomeChar (Proxy n)

-- | Convert an integer into an unknown type-level natural.
--
-- @since base-4.7.0.0
someNatVal :: Integer -> Maybe N.SomeNat
someNatVal :: Integer -> Maybe SomeNat
someNatVal Integer
n
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0        = SomeNat -> Maybe SomeNat
forall a. a -> Maybe a
Just (Natural -> SomeNat
N.someNatVal (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
n))
  | Bool
otherwise     = Maybe SomeNat
forall a. Maybe a
Nothing

-- | Convert a string into an unknown type-level symbol.
--
-- @since base-4.7.0.0
someSymbolVal :: String -> SomeSymbol
someSymbolVal :: String -> SomeSymbol
someSymbolVal String
s = String
-> (forall (s :: Symbol). SSymbol s -> SomeSymbol) -> SomeSymbol
forall r. String -> (forall (s :: Symbol). SSymbol s -> r) -> r
withSomeSSymbol String
s (\(SSymbol s
ss :: SSymbol s) ->
                  SSymbol s -> (KnownSymbol s => SomeSymbol) -> SomeSymbol
forall (s :: Symbol) r. SSymbol s -> (KnownSymbol s => r) -> r
withKnownSymbol SSymbol s
ss (forall (n :: Symbol). KnownSymbol n => Proxy n -> SomeSymbol
SomeSymbol @s Proxy s
forall {k} (t :: k). Proxy t
Proxy))

-- | @since base-4.7.0.0
instance Eq SomeSymbol where
  SomeSymbol Proxy n
x == :: SomeSymbol -> SomeSymbol -> Bool
== SomeSymbol Proxy n
y = Proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy n
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy n
y

-- | @since base-4.7.0.0
instance Ord SomeSymbol where
  compare :: SomeSymbol -> SomeSymbol -> Ordering
compare (SomeSymbol Proxy n
x) (SomeSymbol Proxy n
y) = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy n
x) (Proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy n
y)

-- | @since base-4.7.0.0
instance Show SomeSymbol where
  showsPrec :: Int -> SomeSymbol -> ShowS
showsPrec Int
p (SomeSymbol Proxy n
x) = Int -> String -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy n
x)

-- | @since base-4.7.0.0
instance Read SomeSymbol where
  readsPrec :: Int -> ReadS SomeSymbol
readsPrec Int
p String
xs = [ (String -> SomeSymbol
someSymbolVal String
a, String
ys) | (String
a,String
ys) <- Int -> ReadS String
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
xs ]


-- | Convert a character into an unknown type-level char.
--
-- @since base-4.16.0.0
someCharVal :: Char -> SomeChar
someCharVal :: Char -> SomeChar
someCharVal Char
c = Char -> (forall (c :: Char). SChar c -> SomeChar) -> SomeChar
forall r. Char -> (forall (c :: Char). SChar c -> r) -> r
withSomeSChar Char
c (\(SChar c
sc :: SChar c) ->
                SChar c -> (KnownChar c => SomeChar) -> SomeChar
forall (c :: Char) r. SChar c -> (KnownChar c => r) -> r
withKnownChar SChar c
sc (forall (n :: Char). KnownChar n => Proxy n -> SomeChar
SomeChar @c Proxy c
forall {k} (t :: k). Proxy t
Proxy))

instance Eq SomeChar where
  SomeChar Proxy n
x == :: SomeChar -> SomeChar -> Bool
== SomeChar Proxy n
y = Proxy n -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal Proxy n
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy n -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal Proxy n
y

instance Ord SomeChar where
  compare :: SomeChar -> SomeChar -> Ordering
compare (SomeChar Proxy n
x) (SomeChar Proxy n
y) = Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal Proxy n
x) (Proxy n -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal Proxy n
y)

instance Show SomeChar where
  showsPrec :: Int -> SomeChar -> ShowS
showsPrec Int
p (SomeChar Proxy n
x) = Int -> Char -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy n -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal Proxy n
x)

instance Read SomeChar where
  readsPrec :: Int -> ReadS SomeChar
readsPrec Int
p String
xs = [ (Char -> SomeChar
someCharVal Char
a, String
ys) | (Char
a,String
ys) <- Int -> ReadS Char
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
xs ]

--------------------------------------------------------------------------------

-- | Concatenation of type-level symbols.
--
-- @since base-4.10.0.0
type family AppendSymbol (m ::Symbol) (n :: Symbol) :: Symbol

-- Char-related type families

-- | Extending a type-level symbol with a type-level character
--
-- @since base-4.16.0.0
type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol

-- | This type family yields type-level `Just` storing the first character
-- of a symbol and its tail if it is defined and `Nothing` otherwise.
--
-- @since base-4.16.0.0
type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol)

-- | Convert a character to its Unicode code point (cf. `Data.Char.ord`)
--
-- @since base-4.16.0.0
type family CharToNat (c :: Char) :: N.Nat

-- | Convert a Unicode code point to a character (cf. `Data.Char.chr`)
--
-- @since base-4.16.0.0
type family NatToChar (n :: N.Nat) :: Char

--------------------------------------------------------------------------------

-- | We either get evidence that this function was instantiated with the
-- same type-level symbols, or 'Nothing'.
--
-- @since base-4.7.0.0
sameSymbol :: forall a b proxy1 proxy2.
              (KnownSymbol a, KnownSymbol b) =>
              proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameSymbol :: forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameSymbol proxy1 a
_ proxy2 b
_ = SSymbol a -> SSymbol b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (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 (forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing @a) (forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing @b)

-- | We either get evidence that this function was instantiated with the
-- same type-level symbols, or that the type-level symbols are distinct.
--
-- @since base-4.19.0.0
decideSymbol :: forall a b proxy1 proxy2.
              (KnownSymbol a, KnownSymbol b) =>
              proxy1 a -> proxy2 b -> Either (a :~: b -> Void) (a :~: b)
decideSymbol :: forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> Either ((a :~: b) -> Void) (a :~: b)
decideSymbol proxy1 a
_ proxy2 b
_ = SSymbol a -> SSymbol b -> Either ((a :~: b) -> Void) (a :~: b)
forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> Either ((a :~: b) -> Void) (a :~: b)
decSymbol (forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing @a) (forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing @b)

-- Not exported: See [Not exported decNat, decSymbol and decChar]
decSymbol :: SSymbol a -> SSymbol b -> Either (a :~: b -> Void) (a :~: b)
decSymbol :: forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> Either ((a :~: b) -> Void) (a :~: b)
decSymbol (UnsafeSSymbol String
x) (UnsafeSSymbol String
y)
  | String
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
y    = (a :~: b) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. b -> Either a b
Right ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl)
  | Bool
otherwise = ((a :~: b) -> Void) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. a -> Either a b
Left (\a :~: b
Refl -> String -> Void
forall a. String -> a
errorWithoutStackTrace (String
"decideSymbol: Impossible equality proof " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :~: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
y))

-- | We either get evidence that this function was instantiated with the
-- same type-level characters, or 'Nothing'.
--
-- @since base-4.16.0.0
sameChar :: forall a b proxy1 proxy2.
            (KnownChar a, KnownChar b) =>
            proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameChar :: forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameChar proxy1 a
_ proxy2 b
_ = SChar a -> SChar b -> Maybe (a :~: b)
forall (a :: Char) (b :: Char).
SChar a -> SChar b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (n :: Char). KnownChar n => SChar n
charSing @a) (forall (n :: Char). KnownChar n => SChar n
charSing @b)

-- | We either get evidence that this function was instantiated with the
-- same type-level characters, or that the type-level characters are distinct.
--
-- @since base-4.19.0.0
decideChar :: forall a b proxy1 proxy2.
            (KnownChar a, KnownChar b) =>
            proxy1 a -> proxy2 b -> Either (a :~: b -> Void) (a :~: b)
decideChar :: forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> Either ((a :~: b) -> Void) (a :~: b)
decideChar proxy1 a
_ proxy2 b
_ = SChar a -> SChar b -> Either ((a :~: b) -> Void) (a :~: b)
forall (a :: Char) (b :: Char).
SChar a -> SChar b -> Either ((a :~: b) -> Void) (a :~: b)
decChar (forall (n :: Char). KnownChar n => SChar n
charSing @a) (forall (n :: Char). KnownChar n => SChar n
charSing @b)

-- Not exported: See [Not exported decNat, decSymbol and decChar]
decChar :: SChar a -> SChar b -> Either (a :~: b -> Void) (a :~: b)
decChar :: forall (a :: Char) (b :: Char).
SChar a -> SChar b -> Either ((a :~: b) -> Void) (a :~: b)
decChar (UnsafeSChar Char
x) (UnsafeSChar Char
y)
  | Char
x Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
y    = (a :~: b) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. b -> Either a b
Right ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl)
  | Bool
otherwise = ((a :~: b) -> Void) -> Either ((a :~: b) -> Void) (a :~: b)
forall a b. a -> Either a b
Left (\a :~: b
Refl -> String -> Void
forall a. String -> a
errorWithoutStackTrace (String
"decideChar: Impossible equality proof " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. Show a => a -> String
show Char
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :~: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. Show a => a -> String
show Char
y))

-- | Like 'sameSymbol', but if the symbols aren't equal, this additionally
-- provides proof of LT or GT.
--
-- @since base-4.16.0.0
cmpSymbol :: forall a b proxy1 proxy2. (KnownSymbol a, KnownSymbol b)
          => proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol :: forall (a :: Symbol) (b :: Symbol) (proxy1 :: Symbol -> *)
       (proxy2 :: Symbol -> *).
(KnownSymbol a, KnownSymbol b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpSymbol proxy1 a
x proxy2 b
y = case String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (proxy1 a -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy1 a
x) (proxy2 b -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy2 b
y) of
  Ordering
EQ -> case (Any :~: Any, Any :~: Any) -> (CmpSymbol a b :~: 'EQ, a :~: b)
forall a b. a -> b
unsafeCoerce (Any :~: Any
forall {k} (a :: k). a :~: a
Refl, Any :~: Any
forall {k} (a :: k). a :~: a
Refl) :: (CmpSymbol a b :~: 'EQ, a :~: b) of
    (CmpSymbol a b :~: 'EQ
Refl, a :~: b
Refl) -> OrderingI a a
OrderingI a b
forall {k} (a :: k). (Compare a a ~ 'EQ) => OrderingI a a
EQI
  Ordering
LT -> case (Any :~: Any) -> CmpSymbol a b :~: 'LT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpSymbol a b :~: 'LT) of
    CmpSymbol a b :~: 'LT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'LT) => OrderingI a b
LTI
  Ordering
GT -> case (Any :~: Any) -> CmpSymbol a b :~: 'GT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpSymbol a b :~: 'GT) of
    CmpSymbol a b :~: 'GT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'GT) => OrderingI a b
GTI

-- | Like 'sameChar', but if the Chars aren't equal, this additionally
-- provides proof of LT or GT.
--
-- @since base-4.16.0.0
cmpChar :: forall a b proxy1 proxy2. (KnownChar a, KnownChar b)
        => proxy1 a -> proxy2 b -> OrderingI a b
cmpChar :: forall (a :: Char) (b :: Char) (proxy1 :: Char -> *)
       (proxy2 :: Char -> *).
(KnownChar a, KnownChar b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpChar proxy1 a
x proxy2 b
y = case Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (proxy1 a -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal proxy1 a
x) (proxy2 b -> Char
forall (n :: Char) (proxy :: Char -> *).
KnownChar n =>
proxy n -> Char
charVal proxy2 b
y) of
  Ordering
EQ -> case (Any :~: Any, Any :~: Any) -> (CmpChar a b :~: 'EQ, a :~: b)
forall a b. a -> b
unsafeCoerce (Any :~: Any
forall {k} (a :: k). a :~: a
Refl, Any :~: Any
forall {k} (a :: k). a :~: a
Refl) :: (CmpChar a b :~: 'EQ, a :~: b) of
    (CmpChar a b :~: 'EQ
Refl, a :~: b
Refl) -> OrderingI a a
OrderingI a b
forall {k} (a :: k). (Compare a a ~ 'EQ) => OrderingI a a
EQI
  Ordering
LT -> case (Any :~: Any) -> CmpChar a b :~: 'LT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpChar a b :~: 'LT) of
    CmpChar a b :~: 'LT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'LT) => OrderingI a b
LTI
  Ordering
GT -> case (Any :~: Any) -> CmpChar a b :~: 'GT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpChar a b :~: 'GT) of
    CmpChar a b :~: 'GT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'GT) => OrderingI a b
GTI


--------------------------------------------------------------------------------
-- 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 base-4.18.0.0
fromSNat :: N.SNat n -> Integer
fromSNat :: forall (n :: Natural). SNat n -> Integer
fromSNat SNat n
sn = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (SNat n -> Natural
forall (n :: Natural). SNat n -> Natural
N.fromSNat SNat n
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 base-4.18.0.0
withSomeSNat :: forall rep (r :: TYPE rep).
                Integer -> (forall n. Maybe (N.SNat n) -> r) -> r
withSomeSNat :: forall r.
Integer -> (forall (n :: Natural). Maybe (SNat n) -> r) -> r
withSomeSNat Integer
n forall (n :: Natural). Maybe (SNat n) -> r
k
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0    = Natural -> (forall (n :: Natural). SNat n -> r) -> r
forall r. Natural -> (forall (n :: Natural). SNat n -> r) -> r
N.withSomeSNat (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
n) (\SNat n
sn -> Maybe (SNat n) -> r
forall (n :: Natural). Maybe (SNat n) -> r
k (SNat n -> Maybe (SNat n)
forall a. a -> Maybe a
Just SNat n
sn))
  | Bool
otherwise = Maybe (SNat Any) -> r
forall (n :: Natural). Maybe (SNat n) -> r
k Maybe (SNat Any)
forall a. Maybe a
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 base-4.18.0.0
newtype SSymbol (s :: Symbol) = UnsafeSSymbol String
type role SSymbol nominal

-- | 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 = {- KnownSymbol s in scope -}
-- @
--
-- @since base-4.18.0.0
pattern SSymbol :: forall s. () => KnownSymbol s => SSymbol s
pattern $mSSymbol :: forall {r} {s :: Symbol}.
SSymbol s -> (KnownSymbol s => r) -> ((# #) -> r) -> r
$bSSymbol :: forall (n :: Symbol). KnownSymbol n => SSymbol n
SSymbol <- (knownSymbolInstance -> KnownSymbolInstance)
  where SSymbol = SSymbol s
forall (n :: Symbol). KnownSymbol n => SSymbol n
symbolSing
{-# COMPLETE SSymbol #-}

-- 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 :: forall (s :: Symbol). SSymbol s -> KnownSymbolInstance s
knownSymbolInstance SSymbol s
ss = SSymbol s
-> (KnownSymbol s => KnownSymbolInstance s)
-> KnownSymbolInstance s
forall (s :: Symbol) r. SSymbol s -> (KnownSymbol s => r) -> r
withKnownSymbol SSymbol s
ss KnownSymbolInstance s
KnownSymbol s => KnownSymbolInstance s
forall (s :: Symbol). KnownSymbol s => KnownSymbolInstance s
KnownSymbolInstance

-- | @since base-4.19.0.0
instance Eq (SSymbol s) where
  SSymbol s
_ == :: SSymbol s -> SSymbol s -> Bool
== SSymbol s
_ = Bool
True

-- | @since base-4.19.0.0
instance Ord (SSymbol s) where
  compare :: SSymbol s -> SSymbol s -> Ordering
compare SSymbol s
_ SSymbol s
_ = Ordering
EQ

-- | @since base-4.18.0.0
instance Show (SSymbol s) where
  showsPrec :: Int -> SSymbol s -> ShowS
showsPrec Int
p (UnsafeSSymbol String
s)
    = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec)
      ( 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
appPrec1 String
s
      )

-- | @since base-4.18.0.0
instance TestEquality SSymbol where
  testEquality :: forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> Maybe (a :~: b)
testEquality SSymbol a
a SSymbol b
b = case SSymbol a -> SSymbol b -> Either ((a :~: b) -> Void) (a :~: b)
forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> Either ((a :~: b) -> Void) (a :~: b)
decSymbol SSymbol a
a SSymbol b
b of
    Right a :~: b
p -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: b
p
    Left (a :~: b) -> Void
_  -> Maybe (a :~: b)
forall a. Maybe a
Nothing

-- | @since base-4.18.0.0
instance TestCoercion SSymbol where
  testCoercion :: forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> Maybe (Coercion a b)
testCoercion SSymbol a
x SSymbol b
y = ((a :~: b) -> Coercion a b)
-> Maybe (a :~: b) -> Maybe (Coercion a b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a :~: b
Refl -> Coercion a b
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion) (SSymbol a -> SSymbol b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (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 SSymbol a
x SSymbol b
y)

-- | Return the String corresponding to @s@ in an @'SSymbol' s@ value.
--
-- @since base-4.18.0.0
fromSSymbol :: SSymbol s -> String
fromSSymbol :: forall (s :: Symbol). SSymbol s -> String
fromSSymbol (UnsafeSSymbol String
s) = String
s

-- | Convert an explicit @'SSymbol' s@ value into an implicit @'KnownSymbol' s@
-- constraint.
--
-- @since base-4.18.0.0
withKnownSymbol :: forall s rep (r :: TYPE rep).
                   SSymbol s -> (KnownSymbol s => r) -> r
withKnownSymbol :: forall (s :: Symbol) r. SSymbol s -> (KnownSymbol s => r) -> r
withKnownSymbol = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(KnownSymbol s)
-- See Note [withDict] in "GHC.Tc.Instance.Class" in GHC

-- | Convert a 'String' into an @'SSymbol' s@ value, where @s@ is a fresh
-- type-level symbol.
--
-- @since base-4.18.0.0
withSomeSSymbol :: forall rep (r :: TYPE rep).
                   String -> (forall s. SSymbol s -> r) -> r
withSomeSSymbol :: forall r. String -> (forall (s :: Symbol). SSymbol s -> r) -> r
withSomeSSymbol String
s forall (s :: Symbol). SSymbol s -> r
k = SSymbol Any -> r
forall (s :: Symbol). SSymbol s -> r
k (String -> SSymbol Any
forall (s :: Symbol). String -> SSymbol s
UnsafeSSymbol String
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 base-4.18.0.0
newtype SChar (s :: Char) = UnsafeSChar Char
type role SChar nominal

-- | 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 = {- KnownChar c in scope -}
-- @
--
-- @since base-4.18.0.0
pattern SChar :: forall c. () => KnownChar c => SChar c
pattern $mSChar :: forall {r} {c :: Char}.
SChar c -> (KnownChar c => r) -> ((# #) -> r) -> r
$bSChar :: forall (n :: Char). KnownChar n => SChar n
SChar <- (knownCharInstance -> KnownCharInstance)
  where SChar = SChar c
forall (n :: Char). KnownChar n => SChar n
charSing
{-# COMPLETE SChar #-}

-- 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 :: forall (c :: Char). SChar c -> KnownCharInstance c
knownCharInstance SChar c
sc = SChar c
-> (KnownChar c => KnownCharInstance c) -> KnownCharInstance c
forall (c :: Char) r. SChar c -> (KnownChar c => r) -> r
withKnownChar SChar c
sc KnownCharInstance c
KnownChar c => KnownCharInstance c
forall (c :: Char). KnownChar c => KnownCharInstance c
KnownCharInstance

-- | @since base-4.19.0.0
instance Eq (SChar c) where
  SChar c
_ == :: SChar c -> SChar c -> Bool
== SChar c
_ = Bool
True

-- | @since base-4.19.0.0
instance Ord (SChar c) where
  compare :: SChar c -> SChar c -> Ordering
compare SChar c
_ SChar c
_ = Ordering
EQ

-- | @since base-4.18.0.0
instance Show (SChar c) where
  showsPrec :: Int -> SChar c -> ShowS
showsPrec Int
p (UnsafeSChar Char
c)
    = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec)
      ( String -> ShowS
showString String
"SChar @"
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Char -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
appPrec1 Char
c
      )

-- | @since base-4.18.0.0
instance TestEquality SChar where
  testEquality :: forall (a :: Char) (b :: Char).
SChar a -> SChar b -> Maybe (a :~: b)
testEquality SChar a
a SChar b
b = case SChar a -> SChar b -> Either ((a :~: b) -> Void) (a :~: b)
forall (a :: Char) (b :: Char).
SChar a -> SChar b -> Either ((a :~: b) -> Void) (a :~: b)
decChar SChar a
a SChar b
b of
    Right a :~: b
p -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: b
p
    Left (a :~: b) -> Void
_  -> Maybe (a :~: b)
forall a. Maybe a
Nothing

-- | @since base-4.18.0.0
instance TestCoercion SChar where
  testCoercion :: forall (a :: Char) (b :: Char).
SChar a -> SChar b -> Maybe (Coercion a b)
testCoercion SChar a
x SChar b
y = ((a :~: b) -> Coercion a b)
-> Maybe (a :~: b) -> Maybe (Coercion a b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\a :~: b
Refl -> Coercion a b
forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion) (SChar a -> SChar b -> Maybe (a :~: b)
forall (a :: Char) (b :: Char).
SChar a -> SChar b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SChar a
x SChar b
y)

-- | Return the 'Char' corresponding to @c@ in an @'SChar' c@ value.
--
-- @since base-4.18.0.0
fromSChar :: SChar c -> Char
fromSChar :: forall (c :: Char). SChar c -> Char
fromSChar (UnsafeSChar Char
c) = Char
c

-- | Convert an explicit @'SChar' c@ value into an implicit @'KnownChar' c@
-- constraint.
--
-- @since base-4.18.0.0
withKnownChar :: forall c rep (r :: TYPE rep).
                 SChar c -> (KnownChar c => r) -> r
withKnownChar :: forall (c :: Char) r. SChar c -> (KnownChar c => r) -> r
withKnownChar = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(KnownChar c)
-- See Note [withDict] in "GHC.Tc.Instance.Class" in GHC

-- | Convert a 'Char' into an @'SChar' c@ value, where @c@ is a fresh type-level
-- character.
--
-- @since base-4.18.0.0
withSomeSChar :: forall rep (r :: TYPE rep).
                 Char -> (forall c. SChar c -> r) -> r
withSomeSChar :: forall r. Char -> (forall (c :: Char). SChar c -> r) -> r
withSomeSChar Char
c forall (c :: Char). SChar c -> r
k = SChar Any -> r
forall (c :: Char). SChar c -> r
k (Char -> SChar Any
forall (s :: Char). Char -> SChar s
UnsafeSChar Char
c)
{-# NOINLINE withSomeSChar #-}
-- For details see Note [NOINLINE withSomeSNat] in "GHC.TypeNats"
-- The issue described there applies to `withSomeSChar` as well.