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