{-# LANGUAGE CPP                  #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE EmptyCase            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE KindSignatures       #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE Trustworthy          #-}
{-# 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(..),
    snat,
    withSNat,
    reify,
    reflect,
    reflectToNum,
    -- * Equality
    eqNat,
    EqNat,
    discreteNat,
    -- * Induction
    induction1,
    -- ** 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.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
import TrustworthyCompat

-- $setup
-- >>> :set -XTypeOperators -XDataKinds
-- >>> import qualified GHC.TypeLits as GHC
-- >>> import Data.Type.Dec (Dec (..), decShow)
-- >>> import Data.Type.Equality
-- >>> import Control.Applicative (Const (..))
-- >>> import Data.Coerce (coerce)

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

-- | Implicit 'SNat'.
--
-- In an unorthodox singleton way, it actually provides an induction function.
--
-- The induction should often be fully inlined.
-- See @test/Inspection.hs@.
--
-- >>> :set -XPolyKinds
-- >>> newtype Const a b = Const a deriving (Show)
-- >>> induction (Const 0) (coerce ((+2) :: Int -> Int)) :: Const Int Nat3
-- Const 6
--
class SNatI (n :: Nat) where
    induction
        :: f 'Z                                    -- ^ zero case
        -> (forall m. SNatI m => f m -> f ('S m))  -- ^ induction step
        -> f n

instance SNatI 'Z where
    induction :: f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f 'Z
induction f 'Z
n forall (m :: Nat). SNatI m => f m -> f ('S m)
_c = f 'Z
n

instance SNatI n => SNatI ('S n) where
    induction :: f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f ('S n)
induction f 'Z
n forall (m :: Nat). SNatI m => f m -> f ('S m)
c = f n -> f ('S n)
forall (m :: Nat). SNatI m => f m -> f ('S m)
c (f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction f 'Z
n forall (m :: Nat). SNatI m => f m -> f ('S m)
c)

-- | Construct explicit 'SNat' value.
snat :: SNatI n => SNat n
snat :: SNat n
snat = SNat 'Z
-> (forall (m :: Nat). SNatI m => SNat m -> SNat ('S m)) -> SNat n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction SNat 'Z
SZ (\SNat m
_ -> SNat ('S m)
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
_ = Konst Nat n -> Nat
forall a (n :: Nat). Konst a n -> a
unKonst (Konst Nat 'Z
-> (forall (m :: Nat). SNatI m => Konst Nat m -> Konst Nat ('S m))
-> Konst Nat n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (Nat -> Konst Nat 'Z
forall a (n :: Nat). a -> Konst a n
Konst Nat
Z) ((Nat -> Nat) -> Konst Nat m -> Konst Nat ('S m)
forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Konst a n -> Konst b m
kmap Nat -> Nat
S) :: Konst Nat n)

-- | 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
_ = Konst m n -> m
forall a (n :: Nat). Konst a n -> a
unKonst (Konst m 'Z
-> (forall (m :: Nat). SNatI m => Konst m m -> Konst m ('S m))
-> Konst m n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (m -> Konst m 'Z
forall a (n :: Nat). a -> Konst a n
Konst m
0) ((m -> m) -> Konst m m -> Konst m ('S m)
forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Konst a n -> Konst b m
kmap (m
1m -> m -> m
forall a. Num a => a -> a -> a
+)) :: Konst m n)

-- | 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 = Konst Nat n -> Nat
forall a (n :: Nat). Konst a n -> a
unKonst (Konst Nat 'Z
-> (forall (m :: Nat). SNatI m => Konst Nat m -> Konst Nat ('S m))
-> Konst Nat n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (Nat -> Konst Nat 'Z
forall a (n :: Nat). a -> Konst a n
Konst Nat
Z) ((Nat -> Nat) -> Konst Nat m -> Konst Nat ('S m)
forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Konst a n -> Konst b m
kmap Nat -> Nat
S) :: Konst Nat n)

-- | 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 = Konst Natural n -> Natural
forall a (n :: Nat). Konst a n -> a
unKonst (Konst Natural 'Z
-> (forall (m :: Nat).
    SNatI m =>
    Konst Natural m -> Konst Natural ('S m))
-> Konst Natural n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (Natural -> Konst Natural 'Z
forall a (n :: Nat). a -> Konst a n
Konst Natural
0) ((Natural -> Natural) -> Konst Natural m -> Konst Natural ('S m)
forall a b (n :: Nat) (m :: Nat).
(a -> b) -> Konst a n -> Konst b m
kmap Natural -> Natural
forall a. Enum a => a -> a
succ) :: Konst Natural n)

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

newtype Konst a (n :: Nat) = Konst { Konst a n -> a
unKonst :: a }

kmap :: (a -> b) -> Konst a n -> Konst b m
kmap :: (a -> b) -> Konst a n -> Konst b m
kmap = (a -> b) -> Konst a n -> Konst b m
coerce

newtype Flipped f a (b :: Nat) = Flip { Flipped f a b -> f b a
unflip :: f b a }

-- | Induction on 'Nat', functor form. Useful for computation.
--
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 = Flipped f a n -> f n a
forall (f :: Nat -> * -> *) a (b :: Nat). Flipped f a b -> f b a
unflip (Flipped f a 'Z
-> (forall (m :: Nat).
    SNatI m =>
    Flipped f a m -> Flipped f a ('S m))
-> Flipped f a n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction (f 'Z a -> Flipped f a 'Z
forall (f :: Nat -> * -> *) a (b :: Nat). f b a -> Flipped f a b
Flip f 'Z a
z) (\(Flip f m a
x) -> f ('S m) a -> Flipped f a ('S m)
forall (f :: Nat -> * -> *) a (b :: Nat). f b a -> Flipped f a b
Flip (f m a -> f ('S m) a
forall (m :: Nat). SNatI m => f m a -> f ('S m) a
f f m a
x)))
{-# INLINE induction1 #-}

-- | 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. SNatI n => proxy n -> (a -> a) -> a
unfoldedFix :: proxy n -> (a -> a) -> a
unfoldedFix proxy n
_ = Fix a n -> (a -> a) -> a
forall a (n :: Nat). Fix a n -> (a -> a) -> a
getFix (Fix a 'Z
-> (forall (m :: Nat). SNatI m => Fix a m -> Fix a ('S m))
-> Fix a n
forall (n :: Nat) (f :: Nat -> *).
SNatI n =>
f 'Z -> (forall (m :: Nat). SNatI m => f m -> f ('S m)) -> f n
induction Fix a 'Z
start forall (m :: Nat). Fix a m -> Fix a ('S m)
forall (m :: Nat). SNatI m => Fix a m -> Fix a ('S m)
step :: Fix a n) where
    start :: Fix a 'Z
    start :: Fix a 'Z
start = ((a -> a) -> a) -> Fix a 'Z
forall a (n :: Nat). ((a -> a) -> a) -> Fix a n
Fix (a -> a) -> a
forall a. (a -> a) -> a
fix

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

newtype Fix a (n :: Nat) = Fix { Fix a n -> (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