{-# OPTIONS -Wno-redundant-constraints #-}

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 = (Any :~: Any) -> a :~: b
forall a b. a -> b
unsafeCoerce Any :~: Any
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 = Dict (Eq Void)
Dict (Eq (ListSum t))
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 (w a -> Dict (Eq a)
forall a. w a -> Dict (Eq a)
f w a
t, (forall a. w a -> Dict (Eq a))
-> ListType w lt1 -> Dict (Eq (ListSum lt1))
forall (w :: Type -> Type) (t :: [Type]).
(forall a. w a -> Dict (Eq a))
-> ListType w t -> Dict (Eq (ListSum t))
listSumEq w a -> Dict (Eq a)
forall a. w a -> Dict (Eq a)
f ListType w lt1
tt) of
        (Dict (Eq a)
Dict, Dict (Eq (ListSum lt1))
Dict) -> Dict (Eq (Either a (ListSum lt1)))
Dict (Eq (ListSum t))
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 = Dict (Show Void)
Dict (Show (ListSum t))
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 (w a -> Dict (Show a)
forall a. w a -> Dict (Show a)
f w a
t, (forall a. w a -> Dict (Show a))
-> ListType w lt1 -> Dict (Show (ListSum lt1))
forall (w :: Type -> Type) (t :: [Type]).
(forall a. w a -> Dict (Show a))
-> ListType w t -> Dict (Show (ListSum t))
listSumShow w a -> Dict (Show a)
forall a. w a -> Dict (Show a)
f ListType w lt1
tt) of
        (Dict (Show a)
Dict, Dict (Show (ListSum lt1))
Dict) -> Dict (Show (Either a (ListSum lt1)))
Dict (Show (ListSum t))
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) = a -> Either a (ListSum lt1)
forall a b. a -> Either a b
Left (a -> Either a (ListSum lt1)) -> a -> Either a (ListSum lt1)
forall a b. (a -> b) -> a -> b
$ w a -> a -> a
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) = ListSum lt1 -> Either a (ListSum lt1)
forall a b. b -> Either a b
Right (ListSum lt1 -> Either a (ListSum lt1))
-> ListSum lt1 -> Either a (ListSum lt1)
forall a b. (a -> b) -> a -> b
$ ListType w lt1
-> (forall a. w a -> a -> a) -> ListSum lt1 -> ListSum lt1
forall (w :: Type -> Type) (t :: [Type]).
ListType w t -> (forall a. w a -> a -> a) -> ListSum t -> ListSum t
mapListSum ListType w lt1
wr w a -> a -> a
forall a. w a -> a -> a
f ListSum lt1
rest

type ListSumType :: (Type -> Type) -> (Type -> Type)
type role ListSumType representational nominal
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 ListType wit lt -> ListType wit lt -> Maybe (lt :~: lt)
forall (a :: [Type]) (b :: [Type]).
ListType wit a -> ListType wit b -> Maybe (a :~: b)
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 -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
            Maybe (lt :~: lt)
Nothing -> Maybe (a :~: b)
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 a. w a -> Dict (Eq a))
-> ListType w lt -> Dict (Eq (ListSum lt))
forall (w :: Type -> Type) (t :: [Type]).
(forall a. w a -> Dict (Eq a))
-> ListType w t -> Dict (Eq (ListSum t))
listSumEq w a -> Dict (Eq a)
forall a. w a -> Dict (Eq a)
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) = Dict (Is (ListSumType w) a)
forall (a :: Constraint). a => Dict a
Dict
    getRepWitness (MkListSumType (ConsListType w a
a ListType w lt1
ar)) =
        case (w a -> Dict (Is w a)
Subrepresentative w w
forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness w a
a, ListSumType w (ListSum lt1)
-> Dict (Is (ListSumType w) (ListSum lt1))
Subrepresentative (ListSumType w) (ListSumType w)
forall k (rep :: k -> Type).
Representative rep =>
Subrepresentative rep rep
getRepWitness (ListSumType w (ListSum lt1)
 -> Dict (Is (ListSumType w) (ListSum lt1)))
-> ListSumType w (ListSum lt1)
-> Dict (Is (ListSumType w) (ListSum lt1))
forall a b. (a -> b) -> a -> b
$ ListType w lt1 -> ListSumType w (ListSum lt1)
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) -> Dict (Is (ListSumType w) a)
forall (a :: Constraint). a => Dict a
Dict

instance Representative w => Is (ListSumType w) Void where
    representative :: ListSumType w Void
representative = ListType w '[] -> ListSumType w (ListSum '[])
forall (wit :: Type -> Type) (lt :: [Type]).
ListType wit lt -> ListSumType wit (ListSum lt)
MkListSumType ListType w '[]
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 -> ListType w (a : lt) -> ListSumType w (ListSum (a : lt))
forall (wit :: Type -> Type) (lt :: [Type]).
ListType wit lt -> ListSumType wit (ListSum lt)
MkListSumType (ListType w (a : lt) -> ListSumType w (ListSum (a : lt)))
-> ListType w (a : lt) -> ListSumType w (ListSum (a : lt))
forall a b. (a -> b) -> a -> b
$ w a -> ListType w lt -> ListType w (a : lt)
forall {k} (w :: k -> Type) (a :: k) (lt1 :: [k]).
w a -> ListType w lt1 -> ListType w (a : lt1)
ConsListType w a
forall k (rep :: k -> Type) (a :: k). Is rep a => rep a
representative ListType w lt
r