{-# 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 t. SingleType t t -> t) -> AllOf (SingleType t)
forall (w :: Type -> Type). (forall t. w t -> t) -> AllOf w
MkAllOf ((forall t. SingleType t t -> t) -> AllOf (SingleType t))
-> (forall t. SingleType t t -> t) -> AllOf (SingleType t)
forall a b. (a -> b) -> a -> b
$ \SingleType t t
Refl -> t
t
t

getSingleAllOf :: AllOf (SingleType t) -> t
getSingleAllOf :: forall t. AllOf (SingleType t) -> t
getSingleAllOf (MkAllOf forall t. SingleType t t -> t
f) = SingleType t t -> t
forall t. SingleType t t -> t
f SingleType t t
forall {k} (a :: k). a :~: a
Refl