module Data.Type.Witness.General.ListElement where

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

type ListElementWitness :: forall k. (k -> Type) -> Constraint
class Is (ListType Proxy) (WitnessTypeList w) => ListElementWitness (w :: k -> Type) where
    type WitnessTypeList w :: [k]
    toListElementWitness :: forall t. w t -> ListElementType (WitnessTypeList w) t
    fromListElementWitness :: forall t. ListElementType (WitnessTypeList w) t -> w t

instance Is (ListType Proxy) tt => ListElementWitness (ListElementType tt) where
    type WitnessTypeList (ListElementType tt) = tt
    toListElementWitness :: forall (t :: k).
ListElementType tt t
-> ListElementType (WitnessTypeList (ListElementType tt)) t
toListElementWitness = forall {k} (cat :: k -> k -> Type) (a :: k).
Category cat =>
cat a a
id
    fromListElementWitness :: forall (t :: k).
ListElementType (WitnessTypeList (ListElementType tt)) t
-> ListElementType tt t
fromListElementWitness = forall {k} (cat :: k -> k -> Type) (a :: k).
Category cat =>
cat a a
id