{-# 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 4.6.0.0
-}

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

import GHC.TypeLits.Internal(CmpSymbol, CmpChar)
import qualified GHC.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 4.7.0.0
class KnownSymbol (n :: Symbol) where
  symbolSing :: SSymbol n

-- | @since 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 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 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 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 4.7.0.0

-- | @since 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 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 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 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 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 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 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 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 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 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 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 4.16.0.0
type family CharToNat (c :: Char) :: N.Nat

-- | Convert a Unicode code point to a character (cf. `Data.Char.chr`)
--
-- @since 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 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 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 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 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 4.16.0.0
cmpSymbol :: forall a b