{-# OPTIONS -fno-warn-orphans #-} module Data.Type.Witness.Specific.Single where import Data.Type.Witness.Specific.All import Import type SingleType :: forall k. k -> k -> Type type SingleType = (:~:) singleAllOf :: t -> AllOf (SingleType t) singleAllOf :: forall t. t -> AllOf (SingleType t) singleAllOf t t = forall (w :: Type -> Type). (forall t. w t -> t) -> AllOf w MkAllOf forall a b. (a -> b) -> a -> b $ \SingleType t t Refl -> t t getSingleAllOf :: AllOf (SingleType t) -> t getSingleAllOf :: forall t. AllOf (SingleType t) -> t getSingleAllOf (MkAllOf forall t. SingleType t t -> t f) = forall t. SingleType t t -> t f forall {k} (a :: k). a :~: a Refl