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