{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Control.Monad.Stack.Internal
        ( module Control.Monad.Stack.Internal
        , module GHC.TypeNats
        ) where

import Data.Constraint
import Data.Kind
import Data.Proxy
import Data.Type.Equality
import GHC.TypeNats
import Unsafe.Coerce

type family Pop (c :: k) (m :: k') :: k'

type family IteratePop (n :: Nat) (c :: k) (m :: Type -> Type) :: Type -> Type where
        IteratePop 0 c m = m
        IteratePop n c m = IteratePop (n-1) c (Pop c m)

type family StackConstraints (n :: Nat) (c :: k) (cSucc :: k' -> Constraint) (m :: k') :: Constraint where
        StackConstraints 0 c cSucc m = ()
        StackConstraints n c cSucc m = (cSucc m, StackConstraints (n-1) c cSucc (Pop c m))

predNat :: forall n. KnownNat n => Either (n :~: 0) (Dict (KnownNat (n-1)))
predNat = case sameNat (Proxy @0) (Proxy @n) of
        Just Refl -> Left Refl
        Nothing -> case someNatVal (natVal @n Proxy - 1) of
                SomeNat p -> Right (unsafeCoerce (wrap p))
        where
        wrap :: KnownNat n' => Proxy n' -> Dict (KnownNat n')
        wrap _ = Dict

nonZeroNat :: forall n c cSucc m a.
        KnownNat (n-1) =>
        ( IteratePop n c m a :~: IteratePop (n-1) c (Pop c m) a
        , StackConstraints n c cSucc m :~: (cSucc m, StackConstraints (n-1) c cSucc (Pop c m))
        )
nonZeroNat = unsafeCoerce (Refl, Refl)

depth :: forall n c cSucc m a.
        (KnownNat n, StackConstraints n c cSucc m) =>
        (forall m. cSucc m => Pop c m a -> m a) ->
        IteratePop n c m a ->
        m a
depth lift act = case predNat @n of
        Left Refl -> act
        Right Dict -> case nonZeroNat @n @c @cSucc @m of
                (Refl, Refl) -> lift (depth @(n-1) @c @cSucc lift act)

-- | ContT is polykinded, which leads to issues checking that ContT ~ ContT!
data ContTag