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

{-| 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
    Natural -- declared in GHC.Num.Natural in package ghc-bignum
  , Nat
    -- * Linking type and value level
  , KnownNat(natSing), natVal, natVal'
  , SomeNat(..)
  , someNatVal
  , sameNat
    -- ** Singleton values
  , SNat
  , pattern SNat
  , fromSNat
  , withSomeSNat
  , withKnownNat

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

  ) where

import GHC.Base(Eq(..), Functor(..), Ord(..), WithDict(..), (.), otherwise)
import GHC.Types
import GHC.Num.Natural(Natural)
import GHC.Show(Show(..), appPrec, appPrec1, showParen, showString)
import GHC.Read(Read(..))
import GHC.Prim(Proxy#)
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(..), type (<=), type (<=?))
import Unsafe.Coerce(unsafeCoerce)

import GHC.TypeNats.Internal(CmpNat)

-- | A type synonym for 'Natural'.
--
-- Prevously, this was an opaque data type, but it was changed to a type
-- synonym.
--
-- @since 4.16.0.0

type Nat = Natural
--------------------------------------------------------------------------------

-- | 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 -> Nat
natVal proxy n
_ = case SNat n
forall (n :: Nat). KnownNat n => SNat n
natSing :: SNat n of
             UnsafeSNat Nat
x -> Nat
x

-- | @since 4.10.0.0
natVal' :: forall n. KnownNat n => Proxy# n -> Natural
natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Nat
natVal' Proxy# n
_ = case SNat n
forall (n :: Nat). KnownNat n => SNat n
natSing :: SNat n of
             UnsafeSNat Nat
x -> Nat
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 :: Nat -> SomeNat
someNatVal Nat
n = Nat -> (forall (n :: Nat). SNat n -> SomeNat) -> SomeNat
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeSNat Nat
n (\(SNat n
sn :: SNat n) ->
               SNat n -> (KnownNat n => SomeNat) -> SomeNat
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn (forall (n :: Nat). KnownNat n => Proxy n -> SomeNat
SomeNat @n Proxy n
forall {k} (t :: k). Proxy t
Proxy))

{-
Note [NOINLINE withSomeSNat]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The function

    withSomeSNat :: forall rep (r :: TYPE rep).
                    Natural -> (forall k. SNat k -> r) -> r

converts a `Natural` number to a singleton natural `SNat k`, where the `k` is
locally quantified in a continuation (hence the `forall k`). The local
quantification is important: we can manufacture an `SNat k` value, but it can
never be confused with (say) an `SNat 33` value, because we should never be
able to prove that `k ~ 33`. Moreover, if we call `withSomeSNat` twice, we'll
get an `SNat k1` value and an `SNat k2` value, but again we can't confuse them.
`SNat` is a singleton type!

But how to implement `withSomeSNat`? We have no way to make up a fresh type
variable. To do that we need `runExists`: see #19675.

Lacking `runExists`, we use a trick to implement `withSomeSNat`: instead of
generating a "fresh" type for each use of `withSomeSNat`, we simply use GHC's
placeholder type `Any` (of kind `Nat`), thus (in Core):

  withSomeSNat n f = f @T (UnsafeSNat @T n)
    where type T = Any @Nat

***  BUT we must mark `withSomeSNat` as NOINLINE! ***
(And the same for withSomeSSymbol and withSomeSChar in GHC.TypeLits.)

If we inline it we'll lose the type distinction between separate calls (those
"fresh" type variables just turn into `T`). And that can interact badly with
GHC's type-class specialiser. Consider this definition, where
`foo :: KnownNat n => blah`:

  ex :: Natural
  ex = withSomeSNat 1 (\(s1 :: SNat one) -> withKnownNat @one s1 $
       withSomeSNat 2 (\(s2 :: SNat two) -> withKnownNat @two s2 $
       foo @one ... + foo @two ...))

In the last line we have in scope two distinct dictionaries of types
`KnownNat one` and `KnownNat two`. The calls `foo @one` and `foo @two` each pick
out one of those dictionaries to pass to `foo`.

But if we inline `withSomeSNat` we'll get (switching to Core):

  ex = withKnownNat @T (UnsafeSNat @T 1) (\(kn1 :: KnownNat T) ->
       withKnownNat @T (UnsafeSNat @T 2) (\(kn2 :: KnownNat T) ->
       foo @T kn1 ... + foo @T kn2 ...))
    where type T = Any Nat

We are now treading on thin ice. We have two dictionaries `kn1` and `kn2`, both
of type `KnownNat T`, but with different implementations. GHC may specialise
`foo` at type `T` using one of these dictionaries and use that same
specialisation for the other. See #16586 for more examples of where something
like this has actually happened.

`KnownNat` should be a singleton type, but if we allow `withSomeSNat` to inline
it won't be a singleton type any more. We have lost the "fresh type variable".

TL;DR. We avoid this problem by making the definition of `withSomeSNat` opaque,
using an `NOINLINE` pragma. When we get `runExists` (#19675) we will be able to
stop using this hack.
-}


-- | @since 4.7.0.0
instance Eq SomeNat where
  SomeNat Proxy n
x == :: SomeNat -> SomeNat -> Bool
== SomeNat Proxy n
y = Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal Proxy n
x Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
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) = Nat -> Nat -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal Proxy n
x) (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
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 -> Nat -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal Proxy n
x)

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

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

infixl 6 +, -
infixl 7 *, `Div`, `Mod`
infixr 8 ^

-- | 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 :: forall a b proxy1 proxy2.
           (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
_ proxy2 b
_ = SNat a -> SNat b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (n :: Nat). KnownNat n => SNat n
natSing @a) (forall (n :: Nat). KnownNat n => SNat n
natSing @b)

-- | Like 'sameNat', but if the numbers aren't equal, this additionally
-- provides proof of LT or GT.
--
-- @since 4.16.0.0
cmpNat :: forall a b proxy1 proxy2. (KnownNat a, KnownNat b)
       => proxy1 a -> proxy2 b -> OrderingI a b
cmpNat :: forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> Type)
       (proxy2 :: Nat -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat proxy1 a
x proxy2 b
y = case Nat -> Nat -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (proxy1 a -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal proxy1 a
x) (proxy2 b -> Nat
forall (n :: Nat) (proxy :: Nat -> Type).
KnownNat n =>
proxy n -> Nat
natVal proxy2 b
y) of
  Ordering
EQ -> case (Any :~: Any, Any :~: Any) -> (CmpNat 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) :: (CmpNat a b :~: 'EQ, a :~: b) of
    (CmpNat 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) -> CmpNat a b :~: 'LT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpNat a b :~: 'LT) of
    CmpNat 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) -> CmpNat a b :~: 'GT
forall a b. a -> b
unsafeCoerce Any :~: Any
forall {k} (a :: k). a :~: a
Refl :: (CmpNat a b :~: 'GT) of
    CmpNat a b :~: 'GT
Refl -> OrderingI a b
forall {k} (a :: k) (b :: k). (Compare a b ~ 'GT) => OrderingI a b
GTI



--------------------------------------------------------------------------------
-- Singleton values

-- | A value-level witness for a type-level natural number. This is commonly
-- referred to as a /singleton/ type, as for each @n@, there is a single value
-- that inhabits the type @'SNat' n@ (aside from bottom).
--
-- The definition of 'SNat' is intentionally left abstract. To obtain an 'SNat'
-- value, use one of the following:
--
-- 1. The 'natSing' method of 'KnownNat'.
--
-- 2. The @SNat@ pattern synonym.
--
-- 3. The 'withSomeSNat' function, which creates an 'SNat' from a 'Natural'
--    number.
--
-- @since 4.18.0.0
newtype SNat (n :: Nat) = UnsafeSNat Natural

-- | A explicitly bidirectional pattern synonym relating an 'SNat' to a
-- 'KnownNat' constraint.
--
-- As an __expression__: Constructs an explicit @'SNat' n@ value from an
-- implicit @'KnownNat' n@ constraint:
--
-- @
-- SNat @n :: 'KnownNat' n => 'SNat' n
-- @
--
-- As a __pattern__: Matches on an explicit @'SNat' n@ value bringing
-- an implicit @'KnownNat' n@ constraint into scope:
--
-- @
-- f :: 'SNat' n -> ..
-- f SNat = {- SNat n in scope -}
-- @
--
-- @since 4.18.0.0
pattern SNat :: forall n. () => KnownNat n => SNat n
pattern $mSNat :: forall {r} {n :: Nat}.
SNat n -> (KnownNat n => r) -> ((# #) -> r) -> r
$bSNat :: forall (n :: Nat). KnownNat n => SNat n
SNat <- (knownNatInstance -> KnownNatInstance)
  where SNat = SNat n
forall (n :: Nat). KnownNat n => SNat n
natSing

-- An internal data type that is only used for defining the SNat pattern
-- synonym.
data KnownNatInstance (n :: Nat) where
  KnownNatInstance :: KnownNat n => KnownNatInstance n

-- An internal function that is only used for defining the SNat pattern
-- synonym.
knownNatInstance :: SNat n -> KnownNatInstance n
knownNatInstance :: forall (n :: Nat). SNat n -> KnownNatInstance n
knownNatInstance SNat n
sn = SNat n -> (KnownNat n => KnownNatInstance n) -> KnownNatInstance n
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn KnownNatInstance n
KnownNat n => KnownNatInstance n
forall (n :: Nat). KnownNat n => KnownNatInstance n
KnownNatInstance

-- | @since 4.18.0.0
instance Show (SNat n) where
  showsPrec :: Int -> SNat n -> ShowS
showsPrec Int
p (UnsafeSNat Nat
n)
    = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
appPrec)
      ( String -> ShowS
showString String
"SNat @"
        ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Nat -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
appPrec1 Nat
n
      )

-- | @since 4.18.0.0
instance TestEquality SNat where
  testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
testEquality (UnsafeSNat Nat
x) (UnsafeSNat Nat
y)
    | Nat
x Nat -> Nat -> Bool
forall a. Eq a => a -> a -> Bool
== Nat
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

-- | @since 4.18.0.0
instance TestCoercion SNat where
  testCoercion :: forall (a :: Nat) (b :: Nat).
SNat a -> SNat b -> Maybe (Coercion a b)
testCoercion SNat a
x SNat 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 :: Type -> Type) 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) (SNat a -> SNat b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SNat a
x SNat b
y)

-- | Return the 'Natural' number corresponding to @n@ in an @'SNat' n@ value.
--
-- @since 4.18.0.0
fromSNat :: SNat n -> Natural
fromSNat :: forall (n :: Nat). SNat n -> Nat
fromSNat (UnsafeSNat Nat
n) = Nat
n

-- | Convert an explicit @'SNat' n@ value into an implicit @'KnownNat' n@
-- constraint.
--
-- @since 4.18.0.0
withKnownNat :: forall n rep (r :: TYPE rep).
                SNat n -> (KnownNat n => r) -> r
withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(KnownNat n)
-- See Note [withDict] in "GHC.Tc.Instance.Class" in GHC

-- | Convert a 'Natural' number into an @'SNat' n@ value, where @n@ is a fresh
-- type-level natural number.
--
-- @since 4.18.0.0
withSomeSNat :: forall rep (r :: TYPE rep).
                Natural -> (forall n. SNat n -> r) -> r
withSomeSNat :: forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeSNat Nat
n forall (n :: Nat). SNat n -> r
k = SNat Any -> r
forall (n :: Nat). SNat n -> r
k (Nat -> SNat Any
forall (n :: Nat). Nat -> SNat n
UnsafeSNat Nat
n)
{-# NOINLINE withSomeSNat #-} -- See Note [NOINLINE withSomeSNat]