{-# 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 #-}
{-# LANGUAGE QuantifiedConstraints #-}

{-|
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.Internal.Types

    -- * 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 (UnsafeSSymbol)
      -- We export a pattern synonym instead of the real constructor:
      -- See Note [Preventing unsafe coercions for singleton types].
  , SChar (UnsafeSChar)
      -- We export a pattern synonym instead of the real constructor:
      -- See Note [Preventing unsafe coercions for singleton types].
  , data N.SNat, data SSymbol, data SChar
  , fromSNat, fromSSymbol, fromSChar
  , withSomeSNat, withSomeSSymbol, withSomeSChar
  , N.withKnownNat, withKnownSymbol, withKnownChar
  , N.unsafeWithSNatCo, unsafeWithSSymbolCo, unsafeWithSCharCo

    -- * 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(Functor(..), String, (.), otherwise, Void, (++))
import GHC.Internal.Classes(Eq(..), Ord(..))
import GHC.Internal.Err(errorWithoutStackTrace)
import GHC.Internal.Magic.Dict(WithDict(..))
import GHC.Internal.Types(Bool(..), Char, Coercible, Ordering(..), Symbol, 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.Internal.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 ((a_6 :~: a_6) -> a :~: b
forall a b. a -> b
unsafeCoerce a_6 :~: a_6
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 ((a_4 :~: a_4) -> a :~: b
forall a b. a -> b
unsafeCoerce a_4 :~: a_4
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 (a_16 :~: a_16, a_18 :~: a_18) -> (CmpSymbol a b :~: 'EQ, a :~: b)
forall a b. a -> b
unsafeCoerce (a_16 :~: a_16
forall {k} (a :: k). a :~: a
Refl, a_18 :~: a_18
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 (a_20 :~: a_20) -> CmpSymbol a b :~: 'LT
forall a b. a -> b
unsafeCoerce a_20 :~: a_20
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 (a_22 :~: a_22) -> CmpSymbol a b :~: 'GT
forall a b. a -> b
unsafeCoerce a_22 :~: a_22
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 (a_8 :~: a_8, a_10 :~: a_10) -> (CmpChar a b :~: 'EQ, a :~: b)
forall a b. a -> b
unsafeCoerce (a_8 :~: a_8
forall {k} (a :: k). a :~: a
Refl, a_10 :~: a_10
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 (a_12 :~: a_12) -> CmpChar a b :~: 'LT
forall a b. a -> b
unsafeCoerce a_12 :~: a_12
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 (a_14 :~: a_14) -> CmpChar a b :~: 'GT
forall a b. a -> b
unsafeCoerce a_14 :~: a_14
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 n_2) -> r
forall (n :: Natural). Maybe (SNat n) -> r
k Maybe (SNat n_2)
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
-- nominal role: See Note [Preventing unsafe coercions for singleton types]
-- in GHC.Internal.TypeNats
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

-- | A pattern that can be used to manipulate the
-- 'String' that an @SSymbol s@ contains under the hood.
--
-- When using this pattern to construct an @SSymbol s@, the actual
-- @String@ being stored in the @SSymbol@ /must/ be equal to (the
-- contents of) @s@.  The compiler will not help you verify this,
-- hence the \'unsafe\' name.
pattern UnsafeSSymbol :: forall s. String -> SSymbol s
pattern $mUnsafeSSymbol :: forall {r} {s :: Symbol}.
SSymbol s -> (String -> r) -> ((# #) -> r) -> r
$bUnsafeSSymbol :: forall (s :: Symbol). String -> SSymbol s
UnsafeSSymbol guts = UnsafeSSymbol_ guts
{-# COMPLETE UnsafeSSymbol #-}

-- | 'unsafeWithSSymbolCo' allows uses of @coerce@ in its argument to see the
-- real representation of @SSymbol s@, without undermining the type-safety of
-- @coerce@ elsewhere in the module.
--
-- See also the documentation for 'UnsafeSSymbol'.
unsafeWithSSymbolCo
  :: forall r. ((forall s. Coercible (SSymbol s) String) => r) -> r
unsafeWithSSymbolCo :: forall r.
((forall (s :: Symbol). Coercible (SSymbol s) String) => r) -> r
unsafeWithSSymbolCo (forall (s :: Symbol). Coercible (SSymbol s) String) => r
v = r
(forall (s :: Symbol). Coercible (SSymbol s) String) => r
v

-- | @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 s_1 -> r
forall (s :: Symbol). SSymbol s -> r
k (String -> SSymbol s_1
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
-- nominal role: See Note [Preventing unsafe coercions for singleton types]
-- in GHC.Internal.TypeNats
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

-- | A pattern that can be used to manipulate the
-- 'Char' that an @SChar c@ contains under the hood.
--
-- When using this pattern to construct an @SChar c@, the actual
-- @Char@ being stored in the @SChar c@ /must/ be equal to @c@.
-- The compiler will not help you verify this, hence the \'unsafe\' name.
pattern UnsafeSChar :: forall c. Char -> SChar c
pattern $mUnsafeSChar :: forall {r} {c :: Char}. SChar c -> (Char -> r) -> ((# #) -> r) -> r
$bUnsafeSChar :: forall (c :: Char). Char -> SChar c
UnsafeSChar guts = UnsafeSChar_ guts
{-# COMPLETE UnsafeSChar #-}

-- | 'unsafeWithSCharCo' allows uses of @coerce@ in its argument to see the
-- real representation of @SChar c@, without undermining the type-safety of
-- @coerce@ elsewhere in the module.
--
-- See also the documentation for 'UnsafeSChar'.
unsafeWithSCharCo
  :: forall r. ((forall c. Coercible (SChar c) Char) => r) -> r
unsafeWithSCharCo :: forall r.
((forall (c :: Char). Coercible (SChar c) Char) => r) -> r
unsafeWithSCharCo (forall (c :: Char). Coercible (SChar c) Char) => r
v = r
(forall (c :: Char). Coercible (SChar c) Char) => r
v

-- | @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 c_0 -> r
forall (c :: Char). SChar c -> r
k (Char -> SChar c_0
forall (c :: Char). Char -> SChar c
UnsafeSChar Char
c)
{-# NOINLINE withSomeSChar #-}
-- For details see Note [NOINLINE withSomeSNat] in "GHC.TypeNats"
-- The issue described there applies to `withSomeSChar` as well.