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

{-| This module is an internal GHC module.  It declares the constants used
in the implementation of type-level natural numbers.  The programmer interface
for working with type-level naturals should be defined in a separate library.

@since 4.10.0.0
-}

module GHC.TypeNats
  ( -- * Nat Kind
    Nat -- declared in GHC.Types in package ghc-prim

    -- * Linking type and value level
  , KnownNat, natVal, natVal'
  , SomeNat(..)
  , someNatVal
  , sameNat

    -- * Functions on type literals
  , type (<=), type (<=?), type (+), type (*), type (^), type (-)
  , CmpNat
  , Div, Mod, Log2

  ) where

import GHC.Base(Eq(..), Ord(..), Bool(True), Ordering(..), otherwise)
import GHC.Types( Nat )
import GHC.Num.Natural(Natural)
import GHC.Show(Show(..))
import GHC.Read(Read(..))
import GHC.Prim(magicDict, Proxy#)
import Data.Maybe(Maybe(..))
import Data.Proxy (Proxy(..))
import Data.Type.Equality((:~:)(Refl))
import Unsafe.Coerce(unsafeCoerce)

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

-- | This class gives the integer associated with a type-level natural.
-- There are instances of the class for every concrete literal: 0, 1, 2, etc.
--
-- @since 4.7.0.0
class KnownNat (n :: Nat) where
  natSing :: SNat n

-- | @since 4.10.0.0
natVal :: forall n proxy. KnownNat n => proxy n -> Natural
natVal :: forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal proxy n
_ = case SNat n
forall (n :: Nat). KnownNat n => SNat n
natSing :: SNat n of
             SNat Natural
x -> Natural
x

-- | @since 4.10.0.0
natVal' :: forall n. KnownNat n => Proxy# n -> Natural
natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Natural
natVal' Proxy# n
_ = case SNat n
forall (n :: Nat). KnownNat n => SNat n
natSing :: SNat n of
             SNat Natural
x -> Natural
x

-- | This type represents unknown type-level natural numbers.
--
-- @since 4.10.0.0
data SomeNat    = forall n. KnownNat n    => SomeNat    (Proxy n)

-- | Convert an integer into an unknown type-level natural.
--
-- @since 4.10.0.0
someNatVal :: Natural -> SomeNat
someNatVal :: Natural -> SomeNat
someNatVal Natural
n = (KnownNat Any => Proxy Any -> SomeNat)
-> SNat Any -> Proxy Any -> SomeNat
forall (a :: Nat) b.
(KnownNat a => Proxy a -> b) -> SNat a -> Proxy a -> b
withSNat KnownNat Any => Proxy Any -> SomeNat
forall (n :: Nat). KnownNat n => Proxy n -> SomeNat
SomeNat (Natural -> SNat Any
forall (n :: Nat). Natural -> SNat n
SNat Natural
n) Proxy Any
forall {k} (t :: k). Proxy t
Proxy
{-# NOINLINE someNatVal #-} -- See Note [NOINLINE someNatVal]

{- Note [NOINLINE someNatVal]

`someNatVal` converts a natural number to an existentially quantified
dictionary for `KnowNat` (aka `SomeNat`).  The existential quantification
is very important, as it captures the fact that we don't know the type
statically, although we do know that it exists.   Because this type is
fully opaque, we should never be able to prove that it matches anything else.
This is why coherence should still hold:  we can manufacture a `KnownNat k`
dictionary, but it can never be confused with a `KnownNat 33` dictionary,
because we should never be able to prove that `k ~ 33`.

But how to implement `someNatVal`?  We can't quite implement it "honestly"
because `SomeNat` needs to "hide" the type of the newly created dictionary,
but we don't know what the actual type is!  If `someNatVal` was built into
the language, then we could manufacture a new skolem constant,
which should behave correctly.

Since extra language constructors have additional maintenance costs,
we use a trick to implement `someNatVal` in the library.  The idea is that
instead of generating a "fresh" type for each use of `someNatVal`, we simply
use GHC's placeholder type `Any` (of kind `Nat`). So, the elaborated
version of the code is:

  someNatVal n = withSNat @T (SomeNat @T) (SNat @T n) (Proxy @T)
    where type T = Any Nat

After inlining and simplification, this ends up looking something like this:

  someNatVal n = SomeNat @T (KnownNat @T (SNat @T n)) (Proxy @T)
    where type T = Any Nat

`KnownNat` is the constructor for dictionaries for the class `KnownNat`.
See Note [magicDictId magic] in "basicType/MkId.hs" for details on how
we actually construct the dictionary.

Note that using `Any Nat` is not really correct, as multilple calls to
`someNatVal` would violate coherence:

  type T = Any Nat

  x = SomeNat @T (KnownNat @T (SNat @T 1)) (Proxy @T)
  y = SomeNat @T (KnownNat @T (SNat @T 2)) (Proxy @T)

Note that now the code has two dictionaries with the same type, `KnownNat Any`,
but they have different implementations, namely `SNat 1` and `SNat 2`.  This
is not good, as GHC assumes coherence, and it is free to interchange
dictionaries of the same type, but in this case this would produce an incorrect
result.   See #16586 for examples of this happening.

We can avoid this problem by making the definition of `someNatVal` opaque
and we do this by using a `NOINLINE` pragma.  This restores coherence, because
GHC can only inspect the result of `someNatVal` by pattern matching on the
existential, which would generate a new type.  This restores correctness,
at the cost of having a little more allocation for the `SomeNat` constructors.
-}



-- | @since 4.7.0.0
instance Eq SomeNat where
  SomeNat Proxy n
x == :: SomeNat -> SomeNat -> Bool
== SomeNat Proxy n
y = Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal Proxy n
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal Proxy n
y

-- | @since 4.7.0.0
instance Ord SomeNat where
  compare :: SomeNat -> SomeNat -> Ordering
compare (SomeNat Proxy n
x) (SomeNat Proxy n
y) = Natural -> Natural -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal Proxy n
x) (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal Proxy n
y)

-- | @since 4.7.0.0
instance Show SomeNat where
  showsPrec :: Int -> SomeNat -> ShowS
showsPrec Int
p (SomeNat Proxy n
x) = Int -> Natural -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal Proxy n
x)

-- | @since 4.7.0.0
instance Read SomeNat where
  readsPrec :: Int -> ReadS SomeNat
readsPrec Int
p String
xs = do (Natural
a,String
ys) <- Int -> ReadS Natural
forall a. Read a => Int -> ReadS a
readsPrec Int
p String
xs
                      [(Natural -> SomeNat
someNatVal Natural
a, String
ys)]

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

infix  4 <=?, <=
infixl 6 +, -
infixl 7 *, `Div`, `Mod`
infixr 8 ^

-- | Comparison of type-level naturals, as a constraint.
--
-- @since 4.7.0.0
type x <= y = (x <=? y) ~ 'True

-- | Comparison of type-level naturals, as a function.
--
-- @since 4.7.0.0
type family CmpNat    (m :: Nat)    (n :: Nat)    :: Ordering

{- | Comparison of type-level naturals, as a function.
NOTE: The functionality for this function should be subsumed
by 'CmpNat', so this might go away in the future.
Please let us know, if you encounter discrepancies between the two. -}
type family (m :: Nat) <=? (n :: Nat) :: Bool

-- | Addition of type-level naturals.
--
-- @since 4.7.0.0
type family (m :: Nat) + (n :: Nat) :: Nat

-- | Multiplication of type-level naturals.
--
-- @since 4.7.0.0
type family (m :: Nat) * (n :: Nat) :: Nat

-- | Exponentiation of type-level naturals.
--
-- @since 4.7.0.0
type family (m :: Nat) ^ (n :: Nat) :: Nat

-- | Subtraction of type-level naturals.
--
-- @since 4.7.0.0
type family (m :: Nat) - (n :: Nat) :: Nat

-- | Division (round down) of natural numbers.
-- @Div x 0@ is undefined (i.e., it cannot be reduced).
--
-- @since 4.11.0.0
type family Div (m :: Nat) (n :: Nat) :: Nat

-- | Modulus of natural numbers.
-- @Mod x 0@ is undefined (i.e., it cannot be reduced).
--
-- @since 4.11.0.0
type family Mod (m :: Nat) (n :: Nat) :: Nat

-- | Log base 2 (round down) of natural numbers.
-- @Log 0@ is undefined (i.e., it cannot be reduced).
--
-- @since 4.11.0.0
type family Log2 (m :: Nat) :: Nat

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

-- | We either get evidence that this function was instantiated with the
-- same type-level numbers, or 'Nothing'.
--
-- @since 4.7.0.0
sameNat :: (KnownNat a, KnownNat b) =>
           proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat :: forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat proxy1 a
x proxy2 b
y
  | proxy1 a -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal proxy1 a
x Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== proxy2 b -> Natural
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Natural
natVal 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 SNat    (n :: Nat)    = SNat    Natural

data WrapN a b = WrapN (KnownNat    a => Proxy a -> b)

-- See Note [magicDictId magic] in "basicType/MkId.hs"
withSNat :: (KnownNat a => Proxy a -> b)
         -> SNat a      -> Proxy a -> b
withSNat :: forall (a :: Nat) b.
(KnownNat a => Proxy a -> b) -> SNat a -> Proxy a -> b
withSNat KnownNat a => Proxy a -> b
f SNat a
x Proxy a
y = WrapN a b -> SNat a -> Proxy a -> b
forall a. a
magicDict ((KnownNat a => Proxy a -> b) -> WrapN a b
forall (a :: Nat) b. (KnownNat a => Proxy a -> b) -> WrapN a b
WrapN KnownNat a => Proxy a -> b
f) SNat a
x Proxy a
y