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