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