{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PolyKinds #-}

{-|

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)
and strings (the 'Symbol') 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
    Nat, Symbol  -- Both declared in GHC.Types in package ghc-prim

    -- * Linking type and value level
  , N.KnownNat, natVal, natVal'
  , KnownSymbol, symbolVal, symbolVal'
  , N.SomeNat(..), SomeSymbol(..)
  , someNatVal, someSymbolVal
  , N.sameNat, sameSymbol


    -- * 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

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

  ) where

import GHC.Base(Eq(..), Ord(..), Ordering(..), otherwise)
import GHC.Types( Nat, Symbol )
import GHC.Num(Integer, fromInteger)
import GHC.Base(String)
import GHC.Show(Show(..))
import GHC.Read(Read(..))
import GHC.Real(toInteger)
import GHC.Prim(magicDict, Proxy#)
import Data.Maybe(Maybe(..))
import Data.Proxy (Proxy(..))
import Data.Type.Equality((:~:)(Refl))
import Unsafe.Coerce(unsafeCoerce)

import GHC.TypeNats (KnownNat)
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. KnownNat n => proxy n -> Integer
natVal :: forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy n
p = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
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
                SSymbol String
x -> String
x

-- | @since 4.8.0.0
natVal' :: forall n. KnownNat n => Proxy# n -> Integer
natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Integer
natVal' Proxy# n
p = Natural -> Integer
forall a. Integral a => a -> Integer
toInteger (Proxy# n -> Natural
forall (n :: Nat). 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
                SSymbol 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

-- | 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
n   = (KnownSymbol Any => Proxy Any -> SomeSymbol)
-> SSymbol Any -> Proxy Any -> SomeSymbol
forall (a :: Symbol) b.
(KnownSymbol a => Proxy a -> b) -> SSymbol a -> Proxy a -> b
withSSymbol KnownSymbol Any => Proxy Any -> SomeSymbol
forall (n :: Symbol). KnownSymbol n => Proxy n -> SomeSymbol
SomeSymbol (String -> SSymbol Any
forall (s :: Symbol). String -> SSymbol s
SSymbol String
n) Proxy Any
forall {k} (t :: k). Proxy t
Proxy
{-# NOINLINE someSymbolVal #-}
-- For details see Note [NOINLINE someNatVal] in "GHC.TypeNats"
-- The issue described there applies to `someSymbolVal` as well.

-- | @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 ]

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

-- | Comparison of type-level symbols, as a function.
--
-- @since 4.7.0.0
type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering

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

-- | A description of a custom type error.
data {-kind-} ErrorMessage = Text Symbol
                             -- ^ Show the text as is.

                           | forall t. ShowType t
                             -- ^ Pretty print the type.
                             -- @ShowType :: k -> ErrorMessage@

                           | ErrorMessage :<>: ErrorMessage
                             -- ^ Put two pieces of error message next
                             -- to each other.

                           | ErrorMessage :$$: ErrorMessage
                             -- ^ Stack two pieces of error message on top
                             -- of each other.

infixl 5 :$$:
infixl 6 :<>:

-- | The type-level equivalent of 'Prelude.error'.
--
-- The polymorphic kind of this type allows it to be used in several settings.
-- For instance, it can be used as a constraint, e.g. to provide a better error
-- message for a non-existent instance,
--
-- @
-- -- in a context
-- instance TypeError (Text "Cannot 'Show' functions." :$$:
--                     Text "Perhaps there is a missing argument?")
--       => Show (a -> b) where
--     showsPrec = error "unreachable"
-- @
--
-- It can also be placed on the right-hand side of a type-level function
-- to provide an error for an invalid case,
--
-- @
-- type family ByteSize x where
--    ByteSize Word16   = 2
--    ByteSize Word8    = 1
--    ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
--                                   Text " is not exportable.")
-- @
--
-- @since 4.9.0.0
type family TypeError (a :: ErrorMessage) :: b where


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

-- | We either get evidence that this function was instantiated with the
-- same type-level symbols, or 'Nothing'.
--
-- @since 4.7.0.0
sameSymbol :: (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
x proxy2 b
y
  | proxy1 a -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy1 a
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== proxy2 b -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal proxy2 b
y  = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just ((Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl)
  | Bool
otherwise                   = Maybe (a :~: b)
forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
-- PRIVATE:

newtype SSymbol (s :: Symbol) = SSymbol String

data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)

-- See Note [magicDictId magic] in "basicType/MkId.hs"
withSSymbol :: (KnownSymbol a => Proxy a -> b)
            -> SSymbol a      -> Proxy a -> b
withSSymbol :: forall (a :: Symbol) b.
(KnownSymbol a => Proxy a -> b) -> SSymbol a -> Proxy a -> b
withSSymbol KnownSymbol a => Proxy a -> b
f SSymbol a
x Proxy a
y = WrapS a b -> SSymbol a -> Proxy a -> b
forall a. a
magicDict ((KnownSymbol a => Proxy a -> b) -> WrapS a b
forall (a :: Symbol) b.
(KnownSymbol a => Proxy a -> b) -> WrapS a b
WrapS KnownSymbol a => Proxy a -> b
f) SSymbol a
x Proxy a
y