module Data.Type.Witness.General.AllConstraint where import Import type AllConstraint :: forall kw kt. (kw -> Constraint) -> (kt -> kw) -> Constraint class AllConstraint c w where allConstraint :: forall t. Dict (c (w t)) withAllConstraint :: forall k (c :: Type -> Constraint) (w :: k -> Type) (a :: k) (r :: Type). AllConstraint c w => w a -> (c (w a) => r) -> r withAllConstraint :: forall k (c :: Type -> Constraint) (w :: k -> Type) (a :: k) r. AllConstraint c w => w a -> (c (w a) => r) -> r withAllConstraint w a _ c (w a) => r call = case forall kw kt (c :: kw -> Constraint) (w :: kt -> kw) (t :: kt). AllConstraint c w => Dict (c (w t)) allConstraint @Type @k @c @w @a of Dict (c (w a)) Dict -> c (w a) => r call instance AllConstraint Show ((:~:) t) where allConstraint :: forall (t :: kt). Dict (Show (t :~: t)) allConstraint = forall (a :: Constraint). a => Dict a Dict allShow :: forall k (w :: k -> Type) (t :: k). AllConstraint Show w => w t -> String allShow :: forall k (w :: k -> Type) (t :: k). AllConstraint Show w => w t -> String allShow w t wt = case forall kw kt (c :: kw -> Constraint) (w :: kt -> kw) (t :: kt). AllConstraint c w => Dict (c (w t)) allConstraint @_ @_ @Show @w @t of Dict (Show (w t)) Dict -> forall a. Show a => a -> String show w t wt