module Data.Type.Witness.Specific.List.Sum where

import Data.Type.Witness.General.Representative
import Data.Type.Witness.General.WitnessConstraint
import Data.Type.Witness.Specific.List.List
import Import
import Unsafe.Coerce

type ListSum :: [Type] -> Type
type family ListSum w = r | r -> w where
    ListSum '[] = Void
    ListSum (t : tt) = Either t (ListSum tt)

-- | workaround for https://gitlab.haskell.org/ghc/ghc/issues/10833
injectiveListSum ::
       forall (a :: [Type]) (b :: [Type]). ListSum a ~ ListSum b
    => a :~: b
injectiveListSum :: forall (a :: [Type]) (b :: [Type]).
(ListSum a ~ ListSum b) =>
a :~: b
injectiveListSum = forall a b. a -> b
unsafeCoerce forall {k} (a :: k). a :~: a
Refl

listSumEq :: (forall a. w a -> Dict (Eq a)) -> ListType w t -> Dict (Eq (ListSum t))
listSumEq :: forall (w :: Type -> Type) (t :: [Type]).
(forall a. w a -> Dict (Eq a))
-> ListType w t -> Dict (Eq (ListSum t))
listSumEq forall a. w a -> Dict (Eq a)
_ ListType w t
NilListType = forall (a :: Constraint). a => Dict a
Dict
listSumEq forall a. w a -> Dict (Eq a)
f (ConsListType w a
t ListType w lt1
tt) =
    case (forall a. w a -> Dict (Eq a)
f w a
t, forall (w :: Type -> Type) (t :: [Type]).
(forall a. w a -> Dict (Eq a))
-> ListType w t -> Dict (Eq (ListSum t))
listSumEq forall a. w a -> Dict (Eq a)
f ListType w lt1
tt) of
        (Dict (Eq a)
Dict, Dict (Eq (ListSum lt1))
Dict) -> forall (a :: Constraint). a => Dict a
Dict

listSumShow :: (forall a. w a -> Dict (Show a)) -> ListType w t -> Dict (Show (ListSum t))
listSumShow :: forall (w :: Type -> Type) (t :: [Type]).
(forall a. w a -> Dict (Show a))
-> ListType w t -> Dict (Show (ListSum t))
listSumShow forall a. w a -> Dict (Show a)
_ ListType w t
NilListType = forall (a :: Constraint). a => Dict a
Dict
listSumShow forall a. w a -> Dict (Show a)
f (ConsListType w a
t ListType w lt1
tt) =
    case (forall a. w a -> Dict (Show a)
f w a
t, forall (w :: Type -> Type) (t :: [Type]).
(forall a. w a -> Dict (Show a))
-> ListType w t -> Dict (Show (ListSum t))
listSumShow forall a. w a -> Dict (Show a)
f ListType w lt1
tt) of
        (Dict (Show a)
Dict, Dict (Show (ListSum lt1))
Dict) -> forall (a :: Constraint). a => Dict a
Dict

mapListSum :: ListType w t -> (forall a. w a -> a -> a) -> ListSum t -> ListSum t
mapListSum :: forall (w :: Type -> Type) (t :: [Type]).
ListType w t -> (forall a. w a -> a -> a) -> ListSum t -> ListSum t
mapListSum ListType w t
NilListType forall a. w a -> a -> a
_f ListSum t
v = ListSum t
v
mapListSum (ConsListType w a
wa ListType w lt1
_wr) forall a. w a -> a -> a
f (Left a
a) = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ forall a. w a -> a -> a
f w a
wa a
a
mapListSum (ConsListType w a
_wa ListType w lt1
wr) forall a. w a -> a -> a
f (Right ListSum lt1
rest) = forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (w :: Type -> Type) (t :: [Type]).
ListType w t -> (forall a. w a -> a -> a) -> ListSum t -> ListSum t
mapListSum ListType w lt1
wr forall a. w a -> a -> a
f ListSum lt1
rest

type ListSumType :: (Type -> Type) -> (Type -> Type)
data ListSumType wit t where
    MkListSumType :: forall (wit :: Type -> Type) (lt :: [Type]). ListType wit lt -> ListSumType wit (ListSum lt)

instance TestEquality wit => TestEquality (ListSumType wit) where
    testEquality :: forall a b.
ListSumType wit a -> ListSumType wit b -> Maybe (a :~: b)
testEquality (MkListSumType ListType wit lt
lt1) (MkListSumType ListType wit lt
lt2) =
        case forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality ListType wit lt
lt1 ListType wit lt
lt2 of
            Just lt :~: lt
Refl -> forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
            Maybe (lt :~: lt)
Nothing -> forall a. Maybe a
Nothing

instance WitnessConstraint Eq w => WitnessConstraint Eq (ListSumType w) where
    witnessConstraint :: forall t. ListSumType w t -> Dict (Eq t)
witnessConstraint (MkListSumType ListType w lt
lt) = forall (w :: Type -> Type) (t :: [Type]).
(forall a. w a -> Dict (Eq a))
-> ListType w t -> Dict (Eq (ListSum t))
listSumEq forall k (c :: k -> Constraint) (w :: k -> Type) (t :: k).
WitnessConstraint c w =>
w t -> Dict (c t)
witnessConstraint ListType w lt
lt

instance Representative w => Representative (ListSumType w) where
    getRepWitness :: Subrepresentative (ListSumType w) (ListSumType w)
getRepWitness (MkListSumType ListType w lt
NilListType) = forall (a :: Constraint). a => Dict a
Dict
    getRepWitness (MkListSumType (ConsListType w a
a ListType w lt1
ar)) =
        case (forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness w a
a, forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness forall a b. (a -> b) -> a -> b
$ forall (wit :: Type -> Type) (lt :: [Type]).
ListType wit lt -> ListSumType wit (ListSum lt)
MkListSumType ListType w lt1
ar) of
            (Dict (Is w a)
Dict, Dict (Is (ListSumType w) (ListSum lt1))
Dict) -> forall (a :: Constraint). a => Dict a
Dict

instance Representative w => Is (ListSumType w) Void where
    representative :: ListSumType w Void
representative = forall (wit :: Type -> Type) (lt :: [Type]).
ListType wit lt -> ListSumType wit (ListSum lt)
MkListSumType forall {k} (w :: k -> Type). ListType w '[]
NilListType

instance (Is w a, Is (ListSumType w) ar) => Is (ListSumType w) (Either a ar) where
    representative :: ListSumType w (Either a ar)
representative =
        case forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative @_ @(ListSumType w) @ar of
            MkListSumType ListType w lt
r -> forall (wit :: Type -> Type) (lt :: [Type]).
ListType wit lt -> ListSumType wit (ListSum lt)
MkListSumType forall a b. (a -> b) -> a -> b
$ forall {k} (w :: k -> Type) (a :: k) (lt1 :: [k]).
w a -> ListType w lt1 -> ListType w (a : lt1)
ConsListType forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative ListType w lt
r