{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE LambdaCase           #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeInType           #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module Type.Family.Nat.Util where

import           Data.Kind
import           Data.Type.Equality
import           Data.Type.Length
import           Data.Type.Nat
import           Type.Class.Witness
import           Type.Family.List
import           Type.Family.Nat
import qualified GHC.TypeLits              as GT

appendLengths
    :: Length n
    -> Length m
    -> (Len (n ++ m) :~: (Len n + Len m))
appendLengths = \case
    LZ    -> \_ -> Refl
    LS lN -> apply Refl . appendLengths lN

type family NatNat (n :: GT.Nat) = (m :: N) where
    NatNat 0 = 'Z
    NatNat n = 'S (NatNat (n GT.- 1))

data (:<=:) :: N -> N -> Type where
    LTEZ :: 'Z :<=: n
    LTES :: (m :<=: n) -> ('S m :<=: 'S n)

succAssoc
    :: forall m n. ()
    => Nat m
    -> Nat n
    -> ((m + 'S n) :~: 'S (m + n))
succAssoc = \case
    Z_   -> \_ -> Refl
    S_ m -> \n -> Refl \\ succAssoc m n

addZero
    :: Nat n
    -> ((n + 'Z) :~: n)
addZero = \case
    Z_   -> Refl
    S_ n -> Refl    \\ addZero n