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