module Data.Type.Witness.Specific.Either where import Data.Type.Witness.General.AllConstraint import Data.Type.Witness.General.Finite import Data.Type.Witness.General.ListElement import Data.Type.Witness.General.WitnessConstraint import Data.Type.Witness.Specific.All import Data.Type.Witness.Specific.List.Element import Data.Type.Witness.Specific.Single import Import type EitherType :: forall k. (k -> Type) -> (k -> Type) -> (k -> Type) data EitherType w1 w2 t = LeftType (w1 t) | RightType (w2 t) instance (TestEquality w1, TestEquality w2) => TestEquality (EitherType w1 w2) where testEquality :: forall (a :: k) (b :: k). EitherType w1 w2 a -> EitherType w1 w2 b -> Maybe (a :~: b) testEquality (LeftType w1 a s1) (LeftType w1 b s2) = do a :~: b Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b) testEquality w1 a s1 w1 b s2 forall (m :: Type -> Type) a. Monad m => a -> m a return forall {k} (a :: k). a :~: a Refl testEquality (RightType w2 a s1) (RightType w2 b s2) = do a :~: b Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b) testEquality w2 a s1 w2 b s2 forall (m :: Type -> Type) a. Monad m => a -> m a return forall {k} (a :: k). a :~: a Refl testEquality EitherType w1 w2 a _ EitherType w1 w2 b _ = forall a. Maybe a Nothing instance (FiniteWitness p, FiniteWitness q) => FiniteWitness (EitherType p q) where assembleAllFor :: forall (m :: Type -> Type) (f :: k -> Type). Applicative m => (forall (t :: k). EitherType p q t -> m (f t)) -> m (AllFor f (EitherType p q)) assembleAllFor forall (t :: k). EitherType p q t -> m (f t) getsel = (\(MkAllFor forall (t :: k). p t -> f t p) (MkAllFor forall (t :: k). q t -> f t q) -> forall k (f :: k -> Type) (w :: k -> Type). (forall (t :: k). w t -> f t) -> AllFor f w MkAllFor forall a b. (a -> b) -> a -> b $ \EitherType p q t wt -> case EitherType p q t wt of LeftType p t rt -> forall (t :: k). p t -> f t p p t rt RightType q t rt -> forall (t :: k). q t -> f t q q t rt) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b <$> forall k (w :: k -> Type) (m :: Type -> Type) (f :: k -> Type). (FiniteWitness w, Applicative m) => (forall (t :: k). w t -> m (f t)) -> m (AllFor f w) assembleAllFor (forall (t :: k). EitherType p q t -> m (f t) getsel forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k). Category cat => cat b c -> cat a b -> cat a c . forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k). w1 t -> EitherType w1 w2 t LeftType) forall (f :: Type -> Type) a b. Applicative f => f (a -> b) -> f a -> f b <*> forall k (w :: k -> Type) (m :: Type -> Type) (f :: k -> Type). (FiniteWitness w, Applicative m) => (forall (t :: k). w t -> m (f t)) -> m (AllFor f w) assembleAllFor (forall (t :: k). EitherType p q t -> m (f t) getsel forall {k} (cat :: k -> k -> Type) (b :: k) (c :: k) (a :: k). Category cat => cat b c -> cat a b -> cat a c . forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k). w2 t -> EitherType w1 w2 t RightType) instance (WitnessConstraint c p, WitnessConstraint c q) => WitnessConstraint c (EitherType p q) where witnessConstraint :: forall (t :: k). EitherType p q t -> Dict (c t) witnessConstraint (LeftType p t rt) = case forall k (c :: k -> Constraint) (w :: k -> Type) (t :: k). WitnessConstraint c w => w t -> Dict (c t) witnessConstraint @_ @c p t rt of Dict (c t) Dict -> forall (a :: Constraint). a => Dict a Dict witnessConstraint (RightType q t rt) = case forall k (c :: k -> Constraint) (w :: k -> Type) (t :: k). WitnessConstraint c w => w t -> Dict (c t) witnessConstraint @_ @c q t rt of Dict (c t) Dict -> forall (a :: Constraint). a => Dict a Dict instance (Show (p t), Show (q t)) => Show (EitherType p q t) where show :: EitherType p q t -> String show (LeftType p t rt) = forall a. Show a => a -> String show p t rt show (RightType q t rt) = forall a. Show a => a -> String show q t rt instance (AllConstraint Show p, AllConstraint Show q) => AllConstraint Show (EitherType p q) where allConstraint :: forall t. Dict (Show (EitherType p q t)) allConstraint :: forall (t :: kt). Dict (Show (EitherType p q t)) allConstraint = case forall kw kt (c :: kw -> Constraint) (w :: kt -> kw) (t :: kt). AllConstraint c w => Dict (c (w t)) allConstraint @_ @_ @Show @p @t of Dict (Show (p t)) Dict -> case forall kw kt (c :: kw -> Constraint) (w :: kt -> kw) (t :: kt). AllConstraint c w => Dict (c (w t)) allConstraint @_ @_ @Show @q @t of Dict (Show (q t)) Dict -> forall (a :: Constraint). a => Dict a Dict eitherAllOf :: AllOf sel1 -> AllOf sel2 -> AllOf (EitherType sel1 sel2) eitherAllOf :: forall (sel1 :: Type -> Type) (sel2 :: Type -> Type). AllOf sel1 -> AllOf sel2 -> AllOf (EitherType sel1 sel2) eitherAllOf (MkAllOf forall t. sel1 t -> t tup1) (MkAllOf forall t. sel2 t -> t tup2) = forall (w :: Type -> Type). (forall t. w t -> t) -> AllOf w MkAllOf forall a b. (a -> b) -> a -> b $ \EitherType sel1 sel2 t esel -> case EitherType sel1 sel2 t esel of LeftType sel1 t sel -> forall t. sel1 t -> t tup1 sel1 t sel RightType sel2 t sel -> forall t. sel2 t -> t tup2 sel2 t sel eitherAllFor :: AllFor f sel1 -> AllFor f sel2 -> AllFor f (EitherType sel1 sel2) eitherAllFor :: forall {k} (f :: k -> Type) (sel1 :: k -> Type) (sel2 :: k -> Type). AllFor f sel1 -> AllFor f sel2 -> AllFor f (EitherType sel1 sel2) eitherAllFor (MkAllFor forall (t :: k). sel1 t -> f t tup1) (MkAllFor forall (t :: k). sel2 t -> f t tup2) = forall k (f :: k -> Type) (w :: k -> Type). (forall (t :: k). w t -> f t) -> AllFor f w MkAllFor forall a b. (a -> b) -> a -> b $ \EitherType sel1 sel2 t esel -> case EitherType sel1 sel2 t esel of LeftType sel1 t sel -> forall (t :: k). sel1 t -> f t tup1 sel1 t sel RightType sel2 t sel -> forall (t :: k). sel2 t -> f t tup2 sel2 t sel type ConsType :: forall k. k -> (k -> Type) -> k -> Type type ConsType a = EitherType (SingleType a) instance ListElementWitness lt => ListElementWitness (ConsType a lt) where type WitnessTypeList (ConsType a lt) = a : (WitnessTypeList lt) toListElementWitness :: forall (t :: k). ConsType a lt t -> ListElementType (WitnessTypeList (ConsType a lt)) t toListElementWitness (LeftType a :~: t Refl) = forall {k} (t :: k) (tt :: [k]). ListElementType (t : tt) t FirstElementType toListElementWitness (RightType lt t sel) = forall {k} (aa :: [k]) (t :: k) (a :: k). ListElementType aa t -> ListElementType (a : aa) t RestElementType forall a b. (a -> b) -> a -> b $ forall k (w :: k -> Type) (t :: k). ListElementWitness w => w t -> ListElementType (WitnessTypeList w) t toListElementWitness lt t sel fromListElementWitness :: forall (t :: k). ListElementType (WitnessTypeList (ConsType a lt)) t -> ConsType a lt t fromListElementWitness ListElementType (WitnessTypeList (ConsType a lt)) t FirstElementType = forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k). w1 t -> EitherType w1 w2 t LeftType forall {k} (a :: k). a :~: a Refl fromListElementWitness (RestElementType ListElementType aa t lt) = forall k (w1 :: k -> Type) (w2 :: k -> Type) (t :: k). w2 t -> EitherType w1 w2 t RightType forall a b. (a -> b) -> a -> b $ forall k (w :: k -> Type) (t :: k). ListElementWitness w => ListElementType (WitnessTypeList w) t -> w t fromListElementWitness ListElementType aa t lt