module Data.Type.Witness.Specific.Concat where import Data.Type.Witness.General.Representative import Data.Type.Witness.Specific.List.List import Import type Concat :: forall k. [k] -> [k] -> [k] type family Concat a b where Concat '[] bb = bb Concat (a ': aa) bb = a ': (Concat aa bb) concatEmptyRefl :: ListType w a -> Concat a '[] :~: a concatEmptyRefl :: forall {k} (w :: k -> Type) (a :: [k]). ListType w a -> Concat a '[] :~: a concatEmptyRefl ListType w a NilListType = forall {k} (a :: k). a :~: a Refl concatEmptyRefl (ConsListType w a _ ListType w lt1 la) = case forall {k} (w :: k -> Type) (a :: [k]). ListType w a -> Concat a '[] :~: a concatEmptyRefl ListType w lt1 la of Concat lt1 '[] :~: lt1 Refl -> forall {k} (a :: k). a :~: a Refl concatIsDict :: forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]). (Representative w, Is (ListType w) aa, Is (ListType w) bb) => Dict (Is (ListType w) (Concat aa bb)) concatIsDict :: forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]). (Representative w, Is (ListType w) aa, Is (ListType w) bb) => Dict (Is (ListType w) (Concat aa bb)) concatIsDict = let build :: forall aa'. ListType w aa' -> Dict (Is (ListType w) (Concat aa' bb)) build :: forall (aa' :: [k]). ListType w aa' -> Dict (Is (ListType w) (Concat aa' bb)) build ListType w aa' NilListType = forall (a :: Constraint). a => Dict a Dict build (ConsListType w a wa ListType w lt1 la) = case forall (aa' :: [k]). ListType w aa' -> Dict (Is (ListType w) (Concat aa' bb)) build ListType w lt1 la of Dict (Is (ListType w) (Concat lt1 bb)) Dict -> case forall k (rep :: k -> Type). Representative rep => Subrepresentative rep rep getRepWitness w a wa of Dict (Is w a) Dict -> forall (a :: Constraint). a => Dict a Dict in forall (aa' :: [k]). ListType w aa' -> Dict (Is (ListType w) (Concat aa' bb)) build forall a b. (a -> b) -> a -> b $ forall k (rep :: k -> Type) (a :: k). Is rep a => rep a representative @_ @(ListType w) @aa withConcatIs :: forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r. (Representative w, Is (ListType w) aa, Is (ListType w) bb) => (Is (ListType w) (Concat aa bb) => r) -> r withConcatIs :: forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]) r. (Representative w, Is (ListType w) aa, Is (ListType w) bb) => (Is (ListType w) (Concat aa bb) => r) -> r withConcatIs Is (ListType w) (Concat aa bb) => r call = case forall k (w :: k -> Type) (aa :: [k]) (bb :: [k]). (Representative w, Is (ListType w) aa, Is (ListType w) bb) => Dict (Is (ListType w) (Concat aa bb)) concatIsDict @k @w @aa @bb of Dict (Is (ListType w) (Concat aa bb)) Dict -> Is (ListType w) (Concat aa bb) => r call concatListType :: forall k (w :: k -> Type) (a :: [k]) (b :: [k]). ListType w a -> ListType w b -> ListType w (Concat a b) concatListType :: forall k (w :: k -> Type) (a :: [k]) (b :: [k]). ListType w a -> ListType w b -> ListType w (Concat a b) concatListType ListType w a NilListType ListType w b lb = ListType w b lb concatListType (ConsListType w a wa ListType w lt1 la) ListType w b lb = forall {k} (w :: k -> Type) (a :: k) (lt1 :: [k]). w a -> ListType w lt1 -> ListType w (a : lt1) ConsListType w a wa forall a b. (a -> b) -> a -> b $ forall k (w :: k -> Type) (a :: [k]) (b :: [k]). ListType w a -> ListType w b -> ListType w (Concat a b) concatListType ListType w lt1 la ListType w b lb