module Data.Type.Witness.General.WitnessConstraint where

import Import

type WitnessConstraint :: forall k. (k -> Constraint) -> (k -> Type) -> Constraint
class WitnessConstraint c w where
    witnessConstraint :: forall t. w t -> Dict (c t)

instance WitnessConstraint c (Compose Dict c) where
    witnessConstraint :: forall (t :: k1). Compose Dict c t -> Dict (c t)
witnessConstraint (Compose Dict (c t)
d) = Dict (c t)
d

instance c t => WitnessConstraint c ((:~:) t) where
    witnessConstraint :: forall (t :: k). (t :~: t) -> Dict (c t)
witnessConstraint t :~: t
Refl = forall (a :: Constraint). a => Dict a
Dict