{-# LANGUAGE CPP                  #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE EmptyCase            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
-- | 'Nat' numbers. @DataKinds@ stuff.
--
-- This module re-exports "Data.Nat", and adds type-level things.
module Data.Type.Nat (
    -- * Natural, Nat numbers
    Nat(..),
    toNatural,
    fromNatural,
    cata,
    -- * Showing
    explicitShow,
    explicitShowsPrec,
    -- * Singleton
    SNat(..),
    snatToNat,
    snatToNatural,
    -- * Implicit
    SNatI(..),
    withSNat,
    reify,
    reflect,
    reflectToNum,
    -- * Equality
    eqNat,
    EqNat,
    discreteNat,
    -- * Induction
    induction,
    induction1,
    InlineInduction (..),
    inlineInduction,
    -- ** Example: unfoldedFix
    unfoldedFix,
    -- * Arithmetic
    Plus,
    Mult,
    Mult2,
    DivMod2,
    -- * Conversion to GHC Nat
    ToGHC,
    FromGHC,
    -- * Aliases
    -- ** Nat
    nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9,
    -- ** promoted Nat
    Nat0, Nat1, Nat2, Nat3, Nat4, Nat5, Nat6, Nat7, Nat8, Nat9,
    -- * Proofs
    proofPlusZeroN,
    proofPlusNZero,
    proofMultZeroN,
    proofMultNZero,
    proofMultOneN,
    proofMultNOne,
    )  where

import Data.Function      (fix)
import Data.Proxy         (Proxy (..))
import Data.Type.Dec      (Dec (..))
import Data.Type.Equality ((:~:) (..), TestEquality (..))
import Data.Typeable      (Typeable)
import Numeric.Natural    (Natural)

import qualified GHC.TypeLits as GHC

import Unsafe.Coerce (unsafeCoerce)

#if !MIN_VERSION_base(4,11,0)
import Data.Type.Equality (type (==))
#endif

import Data.Nat

-- $setup
-- >>> :set -XTypeOperators -XDataKinds
-- >>> import Data.Type.Dec (decShow)

-------------------------------------------------------------------------------
-- SNat
-------------------------------------------------------------------------------

-- | Singleton of 'Nat'.
data SNat (n :: Nat) where
    SZ :: SNat 'Z
    SS :: SNatI n => SNat ('S n)
  deriving (Typeable)

deriving instance Show (SNat p)

-- | Convenience class to get 'SNat'.
class               SNatI (n :: Nat) where snat :: SNat n
instance            SNatI 'Z         where snat :: SNat 'Z
snat = SNat 'Z
SZ
instance SNatI n => SNatI ('S n)     where snat :: SNat ('S n)
snat = SNat ('S n)
forall (n :: Nat). SNatI n => SNat ('S n)
SS

-- | Constructor 'SNatI' dictionary from 'SNat'.
--
-- @since 0.0.3
withSNat :: SNat n -> (SNatI n => r) -> r
withSNat :: SNat n -> (SNatI n => r) -> r
withSNat SNat n
SZ SNatI n => r
k = r
SNatI n => r
k
withSNat SNat n
SS SNatI n => r
k = r
SNatI n => r
k

-- | Reflect type-level 'Nat' to the term level.
reflect :: forall n proxy. SNatI n => proxy n -> Nat
reflect :: proxy n -> Nat
reflect proxy n
_ = Tagged n Nat -> Nat
forall (n :: Nat) a. Tagged n a -> a
unTagged (Tagged 'Z Nat
-> (forall (m :: Nat).
    SNatI m =>
    Tagged m Nat -> Tagged ('S m) Nat)
-> Tagged n Nat
forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
induction1 (Nat -> Tagged 'Z Nat
forall (n :: Nat) a. a -> Tagged n a
Tagged Nat
Z) ((Nat -> Nat) -> Tagged m Nat -> Tagged ('S m) Nat
forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Tagged n a -> Tagged m b
retagMap Nat -> Nat
S) :: Tagged n Nat)

-- | As 'reflect' but with any 'Num'.
reflectToNum :: forall n m proxy. (SNatI n, Num m) => proxy n -> m
reflectToNum :: proxy n -> m
reflectToNum proxy n
_ = Tagged n m -> m
forall (n :: Nat) a. Tagged n a -> a
unTagged (Tagged 'Z m
-> (forall (m :: Nat). SNatI m => Tagged m m -> Tagged ('S m) m)
-> Tagged n m
forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
induction1 (m -> Tagged 'Z m
forall (n :: Nat) a. a -> Tagged n a
Tagged m
0) ((m -> m) -> Tagged m m -> Tagged ('S m) m
forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Tagged n a -> Tagged m b
retagMap (m
1m -> m -> m
forall a. Num a => a -> a -> a
+)) :: Tagged n m)

-- | Reify 'Nat'.
--
-- >>> reify nat3 reflect
-- 3
reify :: forall r. Nat -> (forall n. SNatI n => Proxy n -> r) -> r
reify :: Nat -> (forall (n :: Nat). SNatI n => Proxy @Nat n -> r) -> r
reify Nat
Z     forall (n :: Nat). SNatI n => Proxy @Nat n -> r
f = Proxy @Nat 'Z -> r
forall (n :: Nat). SNatI n => Proxy @Nat n -> r
f (Proxy @Nat 'Z
forall k (t :: k). Proxy @k t
Proxy :: Proxy 'Z)
reify (S Nat
n) forall (n :: Nat). SNatI n => Proxy @Nat n -> r
f =  Nat -> (forall (n :: Nat). SNatI n => Proxy @Nat n -> r) -> r
forall r.
Nat -> (forall (n :: Nat). SNatI n => Proxy @Nat n -> r) -> r
reify Nat
n (\(Proxy @Nat n
_p :: Proxy n) -> Proxy @Nat ('S n) -> r
forall (n :: Nat). SNatI n => Proxy @Nat n -> r
f (Proxy @Nat ('S n)
forall k (t :: k). Proxy @k t
Proxy :: Proxy ('S n)))

-- | Convert 'SNat' to 'Nat'.
--
-- >>> snatToNat (snat :: SNat Nat1)
-- 1
--
snatToNat :: forall n. SNat n -> Nat
snatToNat :: SNat n -> Nat
snatToNat SNat n
SZ = Nat
Z
snatToNat SNat n
SS = Tagged n Nat -> Nat
forall (n :: Nat) a. Tagged n a -> a
unTagged (Tagged 'Z Nat
-> (forall (m :: Nat).
    SNatI m =>
    Tagged m Nat -> Tagged ('S m) Nat)
-> Tagged n Nat
forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
induction1 (Nat -> Tagged 'Z Nat
forall (n :: Nat) a. a -> Tagged n a
Tagged Nat
Z) ((Nat -> Nat) -> Tagged m Nat -> Tagged ('S m) Nat
forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Tagged n a -> Tagged m b
retagMap Nat -> Nat
S) :: Tagged n Nat)

-- | Convert 'SNat' to 'Natural'
--
-- >>> snatToNatural (snat :: SNat Nat0)
-- 0
--
-- >>> snatToNatural (snat :: SNat Nat2)
-- 2
--
snatToNatural :: forall n. SNat n -> Natural
snatToNatural :: SNat n -> Natural
snatToNatural SNat n
SZ = Natural
0
snatToNatural SNat n
SS = Tagged n Natural -> Natural
forall (n :: Nat) a. Tagged n a -> a
unTagged (Tagged 'Z Natural
-> (forall (m :: Nat).
    SNatI m =>
    Tagged m Natural -> Tagged ('S m) Natural)
-> Tagged n Natural
forall (n :: Nat) (f :: Nat -> * -> *) a.
SNatI n =>
f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
induction1 (Natural -> Tagged 'Z Natural
forall (n :: Nat) a. a -> Tagged n a
Tagged Natural
0) ((Natural -> Natural) -> Tagged m Natural -> Tagged ('S m) Natural
forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Tagged n a -> Tagged m b
retagMap Natural -> Natural
forall a. Enum a => a -> a
succ) :: Tagged n Natural)

-------------------------------------------------------------------------------
-- Equality
-------------------------------------------------------------------------------

-- | Decide equality of type-level numbers.
--
-- >>> eqNat :: Maybe (Nat3 :~: Plus Nat1 Nat2)
-- Just Refl
--
-- >>> eqNat :: Maybe (Nat3 :~: Mult Nat2 Nat2)
-- Nothing
--
eqNat :: forall n m. (SNatI n, SNatI m) => Maybe (n :~: m)
eqNat :: Maybe ((:~:) @Nat n m)
eqNat = NatEq n -> forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)
forall (n :: Nat).
NatEq n -> forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)
getNatEq (NatEq n -> forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m))
-> NatEq n -> forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)
forall a b. (a -> b) -> a -> b
$ NatEq 'Z
-> (forall (m :: Nat). SNatI m => NatEq m -> NatEq ('S m))
-> NatEq n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction ((forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat 'Z m)) -> NatEq 'Z
forall (n :: Nat).
(forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)) -> NatEq n
NatEq forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat 'Z m)
start) (\NatEq m
p -> (forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat ('S m) m))
-> NatEq ('S m)
forall (n :: Nat).
(forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)) -> NatEq n
NatEq (NatEq m -> Maybe ((:~:) @Nat ('S m) m)
forall (p :: Nat) (q :: Nat).
SNatI q =>
NatEq p -> Maybe ((:~:) @Nat ('S p) q)
step NatEq m
p)) where
    start :: forall p. SNatI p => Maybe ('Z :~: p)
    start :: Maybe ((:~:) @Nat 'Z p)
start = case SNat p
forall (n :: Nat). SNatI n => SNat n
snat :: SNat p of
        SNat p
SZ -> (:~:) @Nat 'Z 'Z -> Maybe ((:~:) @Nat 'Z 'Z)
forall a. a -> Maybe a
Just (:~:) @Nat 'Z 'Z
forall k (a :: k). (:~:) @k a a
Refl
        SNat p
SS -> Maybe ((:~:) @Nat 'Z p)
forall a. Maybe a
Nothing

    step :: forall p q. SNatI q => NatEq p -> Maybe ('S p :~: q)
    step :: NatEq p -> Maybe ((:~:) @Nat ('S p) q)
step NatEq p
hind = case SNat q
forall (n :: Nat). SNatI n => SNat n
snat :: SNat q of
        SNat q
SZ -> Maybe ((:~:) @Nat ('S p) q)
forall a. Maybe a
Nothing
        SNat q
SS -> NatEq p -> Maybe ((:~:) @Nat ('S p) ('S n))
forall (p :: Nat) (q :: Nat).
SNatI q =>
NatEq p -> Maybe ((:~:) @Nat ('S p) ('S q))
step' NatEq p
hind

    step' :: forall p q. SNatI q => NatEq p -> Maybe ('S p :~: 'S q)
    step' :: NatEq p -> Maybe ((:~:) @Nat ('S p) ('S q))
step' (NatEq forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat p m)
hind) = do
        (:~:) @Nat p q
Refl <- Maybe ((:~:) @Nat p q)
forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat p m)
hind :: Maybe (p :~: q)
        (:~:) @Nat ('S p) ('S p) -> Maybe ((:~:) @Nat ('S p) ('S p))
forall (m :: * -> *) a. Monad m => a -> m a
return (:~:) @Nat ('S p) ('S p)
forall k (a :: k). (:~:) @k a a
Refl

newtype NatEq n = NatEq { NatEq n -> forall (m :: Nat). SNatI m => Maybe ((:~:) @Nat n m)
getNatEq :: forall m. SNatI m => Maybe (n :~: m) }

-- | Decide equality of type-level numbers.
--
-- >>> decShow (discreteNat :: Dec (Nat3 :~: Plus Nat1 Nat2))
-- "Yes Refl"
--
-- @since 0.0.3
discreteNat :: forall n m. (SNatI n, SNatI m) => Dec (n :~: m)
discreteNat :: Dec ((:~:) @Nat n m)
discreteNat = DiscreteNat n -> forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m)
forall (n :: Nat).
DiscreteNat n -> forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m)
getDiscreteNat (DiscreteNat n
 -> forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m))
-> DiscreteNat n
-> forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m)
forall a b. (a -> b) -> a -> b
$ DiscreteNat 'Z
-> (forall (m :: Nat).
    SNatI m =>
    DiscreteNat m -> DiscreteNat ('S m))
-> DiscreteNat n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction ((forall (m :: Nat). SNatI m => Dec ((:~:) @Nat 'Z m))
-> DiscreteNat 'Z
forall (n :: Nat).
(forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m))
-> DiscreteNat n
DiscreteNat forall (m :: Nat). SNatI m => Dec ((:~:) @Nat 'Z m)
start) (\DiscreteNat m
p -> (forall (m :: Nat). SNatI m => Dec ((:~:) @Nat ('S m) m))
-> DiscreteNat ('S m)
forall (n :: Nat).
(forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m))
-> DiscreteNat n
DiscreteNat (DiscreteNat m -> Dec ((:~:) @Nat ('S m) m)
forall (p :: Nat) (q :: Nat).
SNatI q =>
DiscreteNat p -> Dec ((:~:) @Nat ('S p) q)
step DiscreteNat m
p))
  where
    start :: forall p. SNatI p => Dec ('Z :~: p)
    start :: Dec ((:~:) @Nat 'Z p)
start = case SNat p
forall (n :: Nat). SNatI n => SNat n
snat :: SNat p of
        SNat p
SZ -> (:~:) @Nat 'Z 'Z -> Dec ((:~:) @Nat 'Z 'Z)
forall a. a -> Dec a
Yes (:~:) @Nat 'Z 'Z
forall k (a :: k). (:~:) @k a a
Refl
        SNat p
SS -> Neg ((:~:) @Nat 'Z p) -> Dec ((:~:) @Nat 'Z p)
forall a. Neg a -> Dec a
No (Neg ((:~:) @Nat 'Z p) -> Dec ((:~:) @Nat 'Z p))
-> Neg ((:~:) @Nat 'Z p) -> Dec ((:~:) @Nat 'Z p)
forall a b. (a -> b) -> a -> b
$ \(:~:) @Nat 'Z p
p -> case (:~:) @Nat 'Z p
p of {}

    step :: forall p q. SNatI q => DiscreteNat p -> Dec ('S p :~: q)
    step :: DiscreteNat p -> Dec ((:~:) @Nat ('S p) q)
step DiscreteNat p
rec = case SNat q
forall (n :: Nat). SNatI n => SNat n
snat :: SNat q of
        SNat q
SZ -> Neg ((:~:) @Nat ('S p) q) -> Dec ((:~:) @Nat ('S p) q)
forall a. Neg a -> Dec a
No (Neg ((:~:) @Nat ('S p) q) -> Dec ((:~:) @Nat ('S p) q))
-> Neg ((:~:) @Nat ('S p) q) -> Dec ((:~:) @Nat ('S p) q)
forall a b. (a -> b) -> a -> b
$ \(:~:) @Nat ('S p) q
p -> case (:~:) @Nat ('S p) q
p of {}
        SNat q
SS -> DiscreteNat p -> Dec ((:~:) @Nat ('S p) ('S n))
forall (p :: Nat) (q :: Nat).
SNatI q =>
DiscreteNat p -> Dec ((:~:) @Nat ('S p) ('S q))
step' DiscreteNat p
rec

    step' :: forall p q. SNatI q => DiscreteNat p -> Dec ('S p :~: 'S q)
    step' :: DiscreteNat p -> Dec ((:~:) @Nat ('S p) ('S q))
step' (DiscreteNat forall (m :: Nat). SNatI m => Dec ((:~:) @Nat p m)
rec) = case Dec ((:~:) @Nat p q)
forall (m :: Nat). SNatI m => Dec ((:~:) @Nat p m)
rec :: Dec (p :~: q) of
        Yes (:~:) @Nat p q
Refl -> (:~:) @Nat ('S p) ('S p) -> Dec ((:~:) @Nat ('S p) ('S p))
forall a. a -> Dec a
Yes (:~:) @Nat ('S p) ('S p)
forall k (a :: k). (:~:) @k a a
Refl
        No Neg ((:~:) @Nat p q)
np    -> Neg ((:~:) @Nat ('S p) ('S q)) -> Dec ((:~:) @Nat ('S p) ('S q))
forall a. Neg a -> Dec a
No (Neg ((:~:) @Nat ('S p) ('S q)) -> Dec ((:~:) @Nat ('S p) ('S q)))
-> Neg ((:~:) @Nat ('S p) ('S q)) -> Dec ((:~:) @Nat ('S p) ('S q))
forall a b. (a -> b) -> a -> b
$ \(:~:) @Nat ('S p) ('S q)
Refl -> Neg ((:~:) @Nat p q)
np (:~:) @Nat p q
forall k (a :: k). (:~:) @k a a
Refl

newtype DiscreteNat n = DiscreteNat { DiscreteNat n -> forall (m :: Nat). SNatI m => Dec ((:~:) @Nat n m)
getDiscreteNat :: forall m. SNatI m => Dec (n :~: m) }

instance TestEquality SNat where
    testEquality :: SNat a -> SNat b -> Maybe ((:~:) @Nat a b)
testEquality SNat a
SZ SNat b
SZ = (:~:) @Nat a a -> Maybe ((:~:) @Nat a a)
forall a. a -> Maybe a
Just (:~:) @Nat a a
forall k (a :: k). (:~:) @k a a
Refl
    testEquality SNat a
SZ SNat b
SS = Maybe ((:~:) @Nat a b)
forall a. Maybe a
Nothing
    testEquality SNat a
SS SNat b
SZ = Maybe ((:~:) @Nat a b)
forall a. Maybe a
Nothing
    testEquality SNat a
SS SNat b
SS = Maybe ((:~:) @Nat a b)
forall (n :: Nat) (m :: Nat).
(SNatI n, SNatI m) =>
Maybe ((:~:) @Nat n m)
eqNat

-- | Type family used to implement 'Data.Type.Equality.==' from "Data.Type.Equality" module.
type family EqNat (n :: Nat) (m :: Nat) where
    EqNat 'Z     'Z     = 'True
    EqNat ('S n) ('S m) = EqNat n m
    EqNat n      m      = 'False

#if !MIN_VERSION_base(4,11,0)
type instance n == m = EqNat n m
#endif

-------------------------------------------------------------------------------
-- Induction
-------------------------------------------------------------------------------

-- | Induction on 'Nat', functor form. Useful for computation.
--
-- >>> induction1 (Tagged 0) $ retagMap (+2) :: Tagged Nat3 Int
-- Tagged 6
--
induction1
    :: forall n f a. SNatI n
    => f 'Z a                                      -- ^ zero case
    -> (forall m. SNatI m => f m a -> f ('S m) a)  -- ^ induction step
    -> f n a
induction1 :: f 'Z a
-> (forall (m :: Nat). SNatI m => f m a -> f ('S m) a) -> f n a
induction1 f 'Z a
z forall (m :: Nat). SNatI m => f m a -> f ('S m) a
f = f n a
forall (m :: Nat). SNatI m => f m a
go where
    go :: forall m. SNatI m => f m a
    go :: f m a
go = case SNat m
forall (n :: Nat). SNatI n => SNat n
snat :: SNat m of
        SNat m
SZ -> f m a
f 'Z a
z
        SNat m
SS -> f n a -> f ('S n) a
forall (m :: Nat). SNatI m => f m a -> f ('S m) a
f f n a
forall (m :: Nat). SNatI m => f m a
go

-- | Induction on 'Nat'.
--
-- Useful in proofs or with GADTs, see source of 'proofPlusNZero'.
induction
    :: forall n f. SNatI n
    => f 'Z                                    -- ^ zero case
    -> (forall m. SNatI m => f m -> f ('S m))  -- ^ induction step
    -> f n
induction :: f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction f 'Z
z forall (m :: Nat). SNatI m => f m -> f ('S m)
f = f n
forall (m :: Nat). SNatI m => f m
go where
    go :: forall m. SNatI m => f m
    go :: f m
go = case SNat m
forall (n :: Nat). SNatI n => SNat n
snat :: SNat m of
        SNat m
SZ -> f m
f 'Z
z
        SNat m
SS -> f n -> f ('S n)
forall (m :: Nat). SNatI m => f m -> f ('S m)
f f n
forall (m :: Nat). SNatI m => f m
go

-- | The induction will be fully inlined.
--
-- See @test/Inspection.hs@.
class SNatI n => InlineInduction (n :: Nat) where
    inlineInduction1 :: f 'Z a -> (forall m. InlineInduction m => f m a -> f ('S m) a) -> f n a

instance InlineInduction 'Z where
    inlineInduction1 :: f 'Z a
-> (forall (m :: Nat). InlineInduction m => f m a -> f ('S m) a)
-> f 'Z a
inlineInduction1 f 'Z a
z forall (m :: Nat). InlineInduction m => f m a -> f ('S m) a
_ = f 'Z a
z

instance InlineInduction n => InlineInduction ('S n) where
    inlineInduction1 :: f 'Z a
-> (forall (m :: Nat). InlineInduction m => f m a -> f ('S m) a)
-> f ('S n) a
inlineInduction1 f 'Z a
z forall (m :: Nat). InlineInduction m => f m a -> f ('S m) a
f = f n a -> f ('S n) a
forall (m :: Nat). InlineInduction m => f m a -> f ('S m) a
f (f 'Z a
-> (forall (m :: Nat). InlineInduction m => f m a -> f ('S m) a)
-> f n a
forall (n :: Nat) (f :: Nat -> * -> *) a.
InlineInduction n =>
f 'Z a
-> (forall (m :: Nat). InlineInduction m => f m a -> f ('S m) a)
-> f n a
inlineInduction1 f 'Z a
z forall (m :: Nat). InlineInduction m => f m a -> f ('S m) a
f)

    -- Specialise this to few first numerals.
    {-# SPECIALIZE instance InlineInduction ('S 'Z) #-}
    {-# SPECIALIZE instance InlineInduction ('S ('S 'Z)) #-}
    {-# SPECIALIZE instance InlineInduction ('S ('S ('S 'Z))) #-}
    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S 'Z)))) #-}
    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S 'Z))))) #-}
    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S 'Z)))))) #-}
    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S 'Z))))))) #-}
    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))) #-}
    {-# SPECIALIZE instance InlineInduction ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))) #-}

-- | See 'InlineInduction'.
inlineInduction
    :: forall n f. InlineInduction n
    => f 'Z                                              -- ^ zero case
    -> (forall m. InlineInduction m => f m -> f ('S m))  -- ^ induction step
    -> f n
inlineInduction :: f 'Z
-> (forall (m :: Nat). InlineInduction m => f m -> f ('S m)) -> f n
inlineInduction f 'Z
z forall (m :: Nat). InlineInduction m => f m -> f ('S m)
f = Const' f n (Any @*) -> f n
forall (f :: Nat -> *) (n :: Nat) a. Const' f n a -> f n
unConst' (Const' f n (Any @*) -> f n) -> Const' f n (Any @*) -> f n
forall a b. (a -> b) -> a -> b
$ Const' f 'Z (Any @*)
-> (forall (m :: Nat).
    InlineInduction m =>
    Const' f m (Any @*) -> Const' f ('S m) (Any @*))
-> Const' f n (Any @*)
forall (n :: Nat) (f :: Nat -> * -> *) a.
InlineInduction n =>
f 'Z a
-> (forall (m :: Nat). InlineInduction m => f m a -> f ('S m) a)
-> f n a
inlineInduction1 (f 'Z -> Const' f 'Z (Any @*)
forall (f :: Nat -> *) (n :: Nat) a. f n -> Const' f n a
Const' f 'Z
z) (f ('S m) -> Const' f ('S m) (Any @*)
forall (f :: Nat -> *) (n :: Nat) a. f n -> Const' f n a
Const' (f ('S m) -> Const' f ('S m) (Any @*))
-> (Const' f m (Any @*) -> f ('S m))
-> Const' f m (Any @*)
-> Const' f ('S m) (Any @*)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f m -> f ('S m)
forall (m :: Nat). InlineInduction m => f m -> f ('S m)
f (f m -> f ('S m))
-> (Const' f m (Any @*) -> f m) -> Const' f m (Any @*) -> f ('S m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const' f m (Any @*) -> f m
forall (f :: Nat -> *) (n :: Nat) a. Const' f n a -> f n
unConst')

newtype Const' (f :: Nat -> *) (n :: Nat) a = Const' { Const' f n a -> f n
unConst' :: f n }

-- | Unfold @n@ steps of a general recursion.
--
-- /Note:/ Always __benchmark__. This function may give you both /bad/ properties:
-- a lot of code (increased binary size), and worse performance.
--
-- For known @n@ 'unfoldedFix' will unfold recursion, for example
--
-- @
-- 'unfoldedFix' ('Proxy' :: 'Proxy' 'Nat3') f = f (f (f (fix f)))
-- @
--
unfoldedFix :: forall n a proxy. InlineInduction n => proxy n -> (a -> a) -> a
unfoldedFix :: proxy n -> (a -> a) -> a
unfoldedFix proxy n
_ = Fix n a -> (a -> a) -> a
forall (n :: Nat) a. Fix n a -> (a -> a) -> a
getFix (Fix 'Z a
-> (forall (m :: Nat).
    InlineInduction m =>
    Fix m a -> Fix ('S m) a)
-> Fix n a
forall (n :: Nat) (f :: Nat -> * -> *) a.
InlineInduction n =>
f 'Z a
-> (forall (m :: Nat). InlineInduction m => f m a -> f ('S m) a)
-> f n a
inlineInduction1 Fix 'Z a
start forall (m :: Nat). Fix m a -> Fix ('S m) a
forall (m :: Nat). InlineInduction m => Fix m a -> Fix ('S m) a
step :: Fix n a) where
    start :: Fix 'Z a
    start :: Fix 'Z a
start = ((a -> a) -> a) -> Fix 'Z a
forall (n :: Nat) a. ((a -> a) -> a) -> Fix n a
Fix (a -> a) -> a
forall a. (a -> a) -> a
fix

    step :: Fix m a -> Fix ('S m) a
    step :: Fix m a -> Fix ('S m) a
step (Fix (a -> a) -> a
go) = ((a -> a) -> a) -> Fix ('S m) a
forall (n :: Nat) a. ((a -> a) -> a) -> Fix n a
Fix (((a -> a) -> a) -> Fix ('S m) a)
-> ((a -> a) -> a) -> Fix ('S m) a
forall a b. (a -> b) -> a -> b
$ \a -> a
f -> a -> a
f ((a -> a) -> a
go a -> a
f)

newtype Fix (n :: Nat) a = Fix { Fix n a -> (a -> a) -> a
getFix :: (a -> a) -> a }

-------------------------------------------------------------------------------
-- Conversion to GHC Nat
-------------------------------------------------------------------------------

-- | Convert to GHC 'GHC.Nat'.
--
-- >>> :kind! ToGHC Nat5
-- ToGHC Nat5 :: GHC.Nat
-- = 5
--
type family ToGHC (n :: Nat) :: GHC.Nat where
    ToGHC 'Z     = 0
    ToGHC ('S n) = 1 GHC.+ ToGHC n

-- | Convert from GHC 'GHC.Nat'.
--
-- >>> :kind! FromGHC 7
-- FromGHC 7 :: Nat
-- = 'S ('S ('S ('S ('S ('S ('S 'Z))))))
--
type family FromGHC (n :: GHC.Nat) :: Nat where
    FromGHC 0 = 'Z
    FromGHC n = 'S (FromGHC (n GHC.- 1))

-------------------------------------------------------------------------------
-- Arithmetic
-------------------------------------------------------------------------------

-- | Addition.
--
-- >>> reflect (snat :: SNat (Plus Nat1 Nat2))
-- 3
type family Plus (n :: Nat) (m :: Nat) :: Nat where
    Plus 'Z     m = m
    Plus ('S n) m = 'S (Plus n m)

-- | Multiplication.
--
-- >>> reflect (snat :: SNat (Mult Nat2 Nat3))
-- 6
type family Mult (n :: Nat) (m :: Nat) :: Nat where
    Mult 'Z     m = 'Z
    Mult ('S n) m = Plus m (Mult n m)

-- | Multiplication by two. Doubling.
--
-- >>> reflect (snat :: SNat (Mult2 Nat4))
-- 8
--
type family Mult2 (n :: Nat) :: Nat where
    Mult2 'Z     = 'Z
    Mult2 ('S n) = 'S ('S (Mult2 n))

-- | Division by two. 'False' is 0 and 'True' is 1 as a remainder.
--
-- >>> :kind! DivMod2 Nat7
-- DivMod2 Nat7 :: (Nat, Bool)
-- = '( 'S ('S ('S 'Z)), 'True)
--
-- >>> :kind! DivMod2 Nat4
-- DivMod2 Nat4 :: (Nat, Bool)
-- = '( 'S ('S 'Z), 'False)
--
type family DivMod2 (n :: Nat) :: (Nat, Bool) where
    DivMod2 'Z          = '( 'Z, 'False)
    DivMod2 ('S 'Z)     = '( 'Z, 'True)
    DivMod2 ('S ('S n)) = DivMod2' (DivMod2 n)

type family DivMod2' (p :: (Nat, Bool)) :: (Nat, Bool) where
    DivMod2' '(n, b) = '( 'S n, b)

-------------------------------------------------------------------------------
-- Aliases
-------------------------------------------------------------------------------

type Nat0  = 'Z
type Nat1  = 'S Nat0
type Nat2  = 'S Nat1
type Nat3  = 'S Nat2
type Nat4  = 'S Nat3
type Nat5  = 'S Nat4
type Nat6  = 'S Nat5
type Nat7  = 'S Nat6
type Nat8  = 'S Nat7
type Nat9  = 'S Nat8

-------------------------------------------------------------------------------
-- proofs
-------------------------------------------------------------------------------

-- | @0 + n = n@
proofPlusZeroN :: Plus Nat0 n :~: n
proofPlusZeroN :: (:~:) @Nat (Plus 'Z n) n
proofPlusZeroN = (:~:) @Nat (Plus 'Z n) n
forall k (a :: k). (:~:) @k a a
Refl

-- | @n + 0 = n@
proofPlusNZero :: SNatI n => Plus n Nat0 :~: n
proofPlusNZero :: (:~:) @Nat (Plus n 'Z) n
proofPlusNZero = ProofPlusNZero n -> (:~:) @Nat (Plus n 'Z) n
forall (n :: Nat). ProofPlusNZero n -> (:~:) @Nat (Plus n 'Z) n
getProofPlusNZero (ProofPlusNZero n -> (:~:) @Nat (Plus n 'Z) n)
-> ProofPlusNZero n -> (:~:) @Nat (Plus n 'Z) n
forall a b. (a -> b) -> a -> b
$ ProofPlusNZero 'Z
-> (forall (m :: Nat).
    SNatI m =>
    ProofPlusNZero m -> ProofPlusNZero ('S m))
-> ProofPlusNZero n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction ((:~:) @Nat (Plus 'Z 'Z) 'Z -> ProofPlusNZero 'Z
forall (n :: Nat). (:~:) @Nat (Plus n 'Z) n -> ProofPlusNZero n
ProofPlusNZero (:~:) @Nat (Plus 'Z 'Z) 'Z
forall k (a :: k). (:~:) @k a a
Refl) forall (m :: Nat). ProofPlusNZero m -> ProofPlusNZero ('S m)
forall (m :: Nat).
SNatI m =>
ProofPlusNZero m -> ProofPlusNZero ('S m)
step where
    step :: forall m. ProofPlusNZero m -> ProofPlusNZero ('S m)
    step :: ProofPlusNZero m -> ProofPlusNZero ('S m)
step (ProofPlusNZero (:~:) @Nat (Plus m 'Z) m
Refl) = (:~:) @Nat (Plus ('S m) 'Z) ('S m) -> ProofPlusNZero ('S m)
forall (n :: Nat). (:~:) @Nat (Plus n 'Z) n -> ProofPlusNZero n
ProofPlusNZero (:~:) @Nat (Plus ('S m) 'Z) ('S m)
forall k (a :: k). (:~:) @k a a
Refl

{-# NOINLINE [1] proofPlusNZero #-}
{-# RULES "Nat: n + 0 = n" proofPlusNZero = unsafeCoerce (Refl :: () :~: ()) #-}

newtype ProofPlusNZero n = ProofPlusNZero { ProofPlusNZero n -> (:~:) @Nat (Plus n 'Z) n
getProofPlusNZero :: Plus n Nat0 :~: n }

-- TODO: plusAssoc

-- | @0 * n = 0@
proofMultZeroN :: Mult Nat0 n :~: Nat0
proofMultZeroN :: (:~:) @Nat (Mult 'Z n) 'Z
proofMultZeroN = (:~:) @Nat (Mult 'Z n) 'Z
forall k (a :: k). (:~:) @k a a
Refl

-- | @n * 0 = 0@
proofMultNZero :: forall n proxy. SNatI n => proxy n -> Mult n Nat0 :~: Nat0
proofMultNZero :: proxy n -> (:~:) @Nat (Mult n 'Z) 'Z
proofMultNZero proxy n
_ =
    ProofMultNZero n -> (:~:) @Nat (Mult n 'Z) 'Z
forall (n :: Nat). ProofMultNZero n -> (:~:) @Nat (Mult n 'Z) 'Z
getProofMultNZero (ProofMultNZero 'Z
-> (forall (m :: Nat).
    SNatI m =>
    ProofMultNZero m -> ProofMultNZero ('S m))
-> ProofMultNZero n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction ((:~:) @Nat (Mult 'Z 'Z) 'Z -> ProofMultNZero 'Z
forall (n :: Nat). (:~:) @Nat (Mult n 'Z) 'Z -> ProofMultNZero n
ProofMultNZero (:~:) @Nat (Mult 'Z 'Z) 'Z
forall k (a :: k). (:~:) @k a a
Refl) forall (m :: Nat). ProofMultNZero m -> ProofMultNZero ('S m)
forall (m :: Nat).
SNatI m =>
ProofMultNZero m -> ProofMultNZero ('S m)
step :: ProofMultNZero n)
  where
    step :: forall m. ProofMultNZero m -> ProofMultNZero ('S m)
    step :: ProofMultNZero m -> ProofMultNZero ('S m)
step (ProofMultNZero (:~:) @Nat (Mult m 'Z) 'Z
Refl) = (:~:) @Nat (Mult ('S m) 'Z) 'Z -> ProofMultNZero ('S m)
forall (n :: Nat). (:~:) @Nat (Mult n 'Z) 'Z -> ProofMultNZero n
ProofMultNZero (:~:) @Nat (Mult ('S m) 'Z) 'Z
forall k (a :: k). (:~:) @k a a
Refl

{-# NOINLINE [1] proofMultNZero #-}
{-# RULES "Nat: n * 0 = n" proofMultNZero = unsafeCoerce (Refl :: () :~: ()) #-}

newtype ProofMultNZero n = ProofMultNZero { ProofMultNZero n -> (:~:) @Nat (Mult n 'Z) 'Z
getProofMultNZero :: Mult n Nat0 :~: Nat0 }

-- | @1 * n = n@
proofMultOneN :: SNatI n => Mult Nat1 n :~: n
proofMultOneN :: (:~:) @Nat (Mult Nat1 n) n
proofMultOneN = (:~:) @Nat (Mult Nat1 n) n
forall (n :: Nat). SNatI n => (:~:) @Nat (Plus n 'Z) n
proofPlusNZero

{-# NOINLINE [1] proofMultOneN #-}
{-# RULES "Nat: 1 * n = n" proofMultOneN = unsafeCoerce (Refl :: () :~: ()) #-}

-- | @n * 1 = n@
proofMultNOne :: SNatI n => Mult n Nat1 :~: n
proofMultNOne :: (:~:) @Nat (Mult n Nat1) n
proofMultNOne = ProofMultNOne n -> (:~:) @Nat (Mult n Nat1) n
forall (n :: Nat). ProofMultNOne n -> (:~:) @Nat (Mult n Nat1) n
getProofMultNOne (ProofMultNOne n -> (:~:) @Nat (Mult n Nat1) n)
-> ProofMultNOne n -> (:~:) @Nat (Mult n Nat1) n
forall a b. (a -> b) -> a -> b
$ ProofMultNOne 'Z
-> (forall (m :: Nat).
    SNatI m =>
    ProofMultNOne m -> ProofMultNOne ('S m))
-> ProofMultNOne n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction ((:~:) @Nat (Mult 'Z Nat1) 'Z -> ProofMultNOne 'Z
forall (n :: Nat). (:~:) @Nat (Mult n Nat1) n -> ProofMultNOne n
ProofMultNOne (:~:) @Nat (Mult 'Z Nat1) 'Z
forall k (a :: k). (:~:) @k a a
Refl) forall (m :: Nat). ProofMultNOne m -> ProofMultNOne ('S m)
forall (m :: Nat).
SNatI m =>
ProofMultNOne m -> ProofMultNOne ('S m)
step where
    step :: forall m. ProofMultNOne m -> ProofMultNOne ('S m)
    step :: ProofMultNOne m -> ProofMultNOne ('S m)
step (ProofMultNOne (:~:) @Nat (Mult m Nat1) m
Refl) = (:~:) @Nat (Mult ('S m) Nat1) ('S m) -> ProofMultNOne ('S m)
forall (n :: Nat). (:~:) @Nat (Mult n Nat1) n -> ProofMultNOne n
ProofMultNOne (:~:) @Nat (Mult ('S m) Nat1) ('S m)
forall k (a :: k). (:~:) @k a a
Refl

{-# NOINLINE [1] proofMultNOne #-}
{-# RULES "Nat: n * 1 = n" proofMultNOne = unsafeCoerce (Refl :: () :~: ()) #-}

newtype ProofMultNOne n = ProofMultNOne { ProofMultNOne n -> (:~:) @Nat (Mult n Nat1) n
getProofMultNOne :: Mult n Nat1 :~: n }

-- TODO: multAssoc

-------------------------------------------------------------------------------
-- Tagged
-------------------------------------------------------------------------------

-- Own 'Tagged', to not depend on @tagged@
--
-- We shouldn't export this in public interface.
newtype Tagged (n :: Nat) a = Tagged a deriving Int -> Tagged n a -> ShowS
[Tagged n a] -> ShowS
Tagged n a -> String
(Int -> Tagged n a -> ShowS)
-> (Tagged n a -> String)
-> ([Tagged n a] -> ShowS)
-> Show (Tagged n a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: Nat) a. Show a => Int -> Tagged n a -> ShowS
forall (n :: Nat) a. Show a => [Tagged n a] -> ShowS
forall (n :: Nat) a. Show a => Tagged n a -> String
showList :: [Tagged n a] -> ShowS
$cshowList :: forall (n :: Nat) a. Show a => [Tagged n a] -> ShowS
show :: Tagged n a -> String
$cshow :: forall (n :: Nat) a. Show a => Tagged n a -> String
showsPrec :: Int -> Tagged n a -> ShowS
$cshowsPrec :: forall (n :: Nat) a. Show a => Int -> Tagged n a -> ShowS
Show

unTagged :: Tagged n a -> a
unTagged :: Tagged n a -> a
unTagged (Tagged a
a) = a
a

retagMap :: (a -> b) -> Tagged n a -> Tagged m b
retagMap :: (a -> b) -> Tagged n a -> Tagged m b
retagMap a -> b
f = b -> Tagged m b
forall (n :: Nat) a. a -> Tagged n a
Tagged (b -> Tagged m b) -> (Tagged n a -> b) -> Tagged n a -> Tagged m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f (a -> b) -> (Tagged n a -> a) -> Tagged n a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tagged n a -> a
forall (n :: Nat) a. Tagged n a -> a
unTagged