module Data.Type.Witness.Specific.All where import Data.Type.Witness.General.WitnessConstraint import Data.Type.Witness.Specific.Some import Import type AllFor :: forall k. (k -> Type) -> (k -> Type) -> Type newtype AllFor f w = MkAllFor { forall k (f :: k -> Type) (w :: k -> Type). AllFor f w -> forall (t :: k). w t -> f t unAllFor :: forall t. w t -> f t } type AllOf :: (Type -> Type) -> Type newtype AllOf w = MkAllOf { forall (w :: Type -> Type). AllOf w -> forall t. w t -> t unAllOf :: forall t. w t -> t } setAllOf :: forall (w :: Type -> Type) (a :: Type). TestEquality w => w a -> a -> AllOf w -> AllOf w setAllOf :: forall (w :: Type -> Type) a. TestEquality w => w a -> a -> AllOf w -> AllOf w setAllOf w a wa a a (MkAllOf forall t. w t -> t wtt) = forall (w :: Type -> Type). (forall t. w t -> t) -> AllOf w MkAllOf forall a b. (a -> b) -> a -> b $ \w t wa' -> case forall {k} (f :: k -> Type) (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b) testEquality w a wa w t wa' of Just a :~: t Refl -> a a Maybe (a :~: t) Nothing -> forall t. w t -> t wtt w t wa' allForToAllOf :: forall (w :: Type -> Type). AllFor Identity w -> AllOf w allForToAllOf :: forall (w :: Type -> Type). AllFor Identity w -> AllOf w allForToAllOf (MkAllFor forall t. w t -> Identity t wtit) = forall (w :: Type -> Type). (forall t. w t -> t) -> AllOf w MkAllOf forall a b. (a -> b) -> a -> b $ \w t wt -> forall a. Identity a -> a runIdentity forall a b. (a -> b) -> a -> b $ forall t. w t -> Identity t wtit w t wt allOfToAllFor :: forall (w :: Type -> Type). AllOf w -> AllFor Identity w allOfToAllFor :: forall (w :: Type -> Type). AllOf w -> AllFor Identity w allOfToAllFor (MkAllOf forall t. w t -> t wtt) = 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 $ \w t wt -> forall a. a -> Identity a Identity forall a b. (a -> b) -> a -> b $ forall t. w t -> t wtt w t wt allMapSome :: AllFor f w -> SomeFor g w -> SomeFor g f allMapSome :: forall {k} (f :: k -> Type) (w :: k -> Type) (g :: k -> Type). AllFor f w -> SomeFor g w -> SomeFor g f allMapSome (MkAllFor forall (t :: k). w t -> f t f) = forall k (g :: k -> Type) (w1 :: k -> Type) (w2 :: k -> Type). (forall (t :: k). w1 t -> w2 t) -> SomeFor g w1 -> SomeFor g w2 mapSome forall (t :: k). w t -> f t f type UnAllOf :: Type -> Type -> Type type family UnAllOf aw where UnAllOf (AllOf w) = w splitSomeOfList :: forall (w :: Type -> Type). TestEquality w => [SomeOf w] -> AllFor [] w splitSomeOfList :: forall (w :: Type -> Type). TestEquality w => [SomeOf w] -> AllFor [] w splitSomeOfList [] = 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 $ \w t _ -> [] splitSomeOfList ((MkSomeOf w a wt a t):[SomeOf w] rr) = 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 $ \w t wt' -> case forall {k} (f :: k -> Type) (a :: k) (b :: k). TestEquality f => f a -> f b -> Maybe (a :~: b) testEquality w a wt w t wt' of Just a :~: t Refl -> a t forall a. a -> [a] -> [a] : (forall k (f :: k -> Type) (w :: k -> Type). AllFor f w -> forall (t :: k). w t -> f t unAllFor (forall (w :: Type -> Type). TestEquality w => [SomeOf w] -> AllFor [] w splitSomeOfList [SomeOf w] rr) w t wt') Maybe (a :~: t) Nothing -> forall k (f :: k -> Type) (w :: k -> Type). AllFor f w -> forall (t :: k). w t -> f t unAllFor (forall (w :: Type -> Type). TestEquality w => [SomeOf w] -> AllFor [] w splitSomeOfList [SomeOf w] rr) w t wt' allForWitnessConstraint :: forall k (c :: k -> Constraint) (w :: k -> Type). WitnessConstraint c w => AllFor (Compose Dict c) w allForWitnessConstraint :: forall k (c :: k -> Constraint) (w :: k -> Type). WitnessConstraint c w => AllFor (Compose Dict c) w allForWitnessConstraint = 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 $ \w t wt -> forall {k} {k1} (f :: k -> Type) (g :: k1 -> k) (a :: k1). f (g a) -> Compose f g a Compose forall a b. (a -> b) -> a -> b $ forall k (c :: k -> Constraint) (w :: k -> Type) (t :: k). WitnessConstraint c w => w t -> Dict (c t) witnessConstraint w t wt