Data.Type.Witness.Specific.List.Sum

Documentation

type family ListSum w = r | r -> w where ...

Equations

ListSum '[] = Void

ListSum (t ': tt) = Either t (ListSum tt)

injectiveListSum :: forall (a :: [Type]) (b :: [Type]). ListSum a ~ ListSum b => a :~: b

workaround for https://gitlab.haskell.org/ghc/ghc/issues/10833

listSumEq :: (forall a. w a -> Dict (Eq a)) -> ListType w t -> Dict (Eq (ListSum t))

listSumShow :: (forall a. w a -> Dict (Show a)) -> ListType w t -> Dict (Show (ListSum t))

mapListSum :: ListType w t -> (forall a. w a -> a -> a) -> ListSum t -> ListSum t

data ListSumType wit t where

Constructors

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

Instances

WitnessConstraint Eq w => WitnessConstraint Eq (ListSumType w :: Type -> Type)

Defined in Data.Type.Witness.Specific.List.Sum

Methods

witnessConstraint :: forall (t :: k). ListSumType w t -> Dict (Eq t)

TestEquality wit => TestEquality (ListSumType wit :: Type -> Type)

Defined in Data.Type.Witness.Specific.List.Sum

Methods

testEquality :: forall (a :: k) (b :: k). ListSumType wit a -> ListSumType wit b -> Maybe (a :~: b)

Representative w => Representative (ListSumType w :: Type -> Type)

Defined in Data.Type.Witness.Specific.List.Sum

Methods

getRepWitness :: Subrepresentative (ListSumType w) (ListSumType w)

Representative w => Is (ListSumType w :: Type -> Type) Void

Defined in Data.Type.Witness.Specific.List.Sum

Methods

representative :: ListSumType w Void

(Is w a, Is (ListSumType w) ar) => Is (ListSumType w :: Type -> Type) (Either a ar :: Type)

Defined in Data.Type.Witness.Specific.List.Sum

Methods

representative :: ListSumType w (Either a ar)