module Data.Type.Witness.Specific.ApplyStack where

import Data.Type.Witness.General.Representative
import Data.Type.Witness.Specific.Concat
import Data.Type.Witness.Specific.List.List
import Import

type ApplyStack :: forall k. [k -> k] -> k -> k
type family ApplyStack f a where
    ApplyStack '[] a = a
    ApplyStack (t ': tt) a = t (ApplyStack tt a)

witApplyConcatRefl ::
       forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k) w.
       ListType w f1
    -> (ApplyStack (Concat f1 f2) a) :~: (ApplyStack f1 (ApplyStack f2 a))
witApplyConcatRefl :: forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k)
       (w :: (k -> k) -> Type).
ListType w f1
-> ApplyStack (Concat f1 f2) a :~: ApplyStack f1 (ApplyStack f2 a)
witApplyConcatRefl ListType w f1
NilListType = forall {k} (a :: k). a :~: a
Refl
witApplyConcatRefl (ConsListType w a
_ ListType w lt1
lt) =
    case forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k)
       (w :: (k -> k) -> Type).
ListType w f1
-> ApplyStack (Concat f1 f2) a :~: ApplyStack f1 (ApplyStack f2 a)
witApplyConcatRefl @k @_ @f2 @a ListType w lt1
lt of
        ApplyStack (Concat lt1 f2) a :~: ApplyStack lt1 (ApplyStack f2 a)
Refl -> forall {k} (a :: k). a :~: a
Refl

applyConcatRefl ::
       forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k) w. Is (ListType w) f1
    => (ApplyStack (Concat f1 f2) a) :~: (ApplyStack f1 (ApplyStack f2 a))
applyConcatRefl :: forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k)
       (w :: (k -> k) -> Type).
Is (ListType w) f1 =>
ApplyStack (Concat f1 f2) a :~: ApplyStack f1 (ApplyStack f2 a)
applyConcatRefl = forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k)
       (w :: (k -> k) -> Type).
ListType w f1
-> ApplyStack (Concat f1 f2) a :~: ApplyStack f1 (ApplyStack f2 a)
witApplyConcatRefl @k @f1 @f2 @a forall a b. (a -> b) -> a -> b
$ forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListType w) @f1