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)) 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