Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Type.Witness.General.TestHetEquality

Synopsis

data (a :: k1) :~~: (b :: k2) where
- HRefl :: forall {k1} (a :: k1). a :~~: a
withHRefl :: forall ka (a :: ka) kb (b :: kb) (r :: Type). (a :~~: b) -> (a ~~ b => r) -> r
hetHomoEq :: forall (k :: Type) (a :: k) (b :: k). (a :~~: b) -> a :~: b
class TestHetEquality (w :: forall k. k -> Type) where
- testHetEquality :: forall (ka :: Type) (a :: ka) (kb :: Type) (b :: kb). w a -> w b -> Maybe (a :~~: b)
data HetEqual a b where
- HetRefl :: forall k (a :: k). HetEqual a a

Documentation

data (a :: k1) :~~: (b :: k2) where infix 4 #

Kind heterogeneous propositional equality. Like :~:, a :~~: b is inhabited by a terminating value if and only if a is the same type as b.

Since: base-4.10.0.0

Constructors

HRefl :: forall {k1} (a :: k1). a :~~: a

Instances

Instances details

Category ((:~~:) :: k -> k -> Type)	Since: base-4.10.0.0
Instance details Defined in Control.Category Methods id :: forall (a :: k0). a :~~: a # (.) :: forall (b :: k0) (c :: k0) (a :: k0). (b :~~: c) -> (a :~~: b) -> a :~~: c #
TestEquality ((:~~:) a :: k -> Type)	Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) #
a ~~ b => Bounded (a :~~: b)	Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods minBound :: a :~~: b # maxBound :: a :~~: b #
a ~~ b => Enum (a :~~: b)	Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods succ :: (a :~~: b) -> a :~~: b # pred :: (a :~~: b) -> a :~~: b # toEnum :: Int -> a :~~: b # fromEnum :: (a :~~: b) -> Int # enumFrom :: (a :~~: b) -> [a :~~: b] # enumFromThen :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] # enumFromTo :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] # enumFromThenTo :: (a :~~: b) -> (a :~~: b) -> (a :~~: b) -> [a :~~: b] #
a ~~ b => Read (a :~~: b)	Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~~: b) # readList :: ReadS [a :~~: b] # readPrec :: ReadPrec (a :~~: b) # readListPrec :: ReadPrec [a :~~: b] #
Show (a :~~: b)	Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~~: b) -> ShowS # show :: (a :~~: b) -> String # showList :: [a :~~: b] -> ShowS #
Eq (a :~~: b)	Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods (==) :: (a :~~: b) -> (a :~~: b) -> Bool # (/=) :: (a :~~: b) -> (a :~~: b) -> Bool #
Ord (a :~~: b)	Since: base-4.10.0.0
Instance details Defined in Data.Type.Equality Methods compare :: (a :~~: b) -> (a :~~: b) -> Ordering # (<) :: (a :~~: b) -> (a :~~: b) -> Bool # (<=) :: (a :~~: b) -> (a :~~: b) -> Bool # (>) :: (a :~~: b) -> (a :~~: b) -> Bool # (>=) :: (a :~~: b) -> (a :~~: b) -> Bool # max :: (a :~~: b) -> (a :~~: b) -> a :~~: b # min :: (a :~~: b) -> (a :~~: b) -> a :~~: b #
HasDict (a ~~ b) (a :~~: b)
Instance details Defined in Data.Constraint Methods evidence :: (a :~~: b) -> Dict (a ~~ b) #

withHRefl :: forall ka (a :: ka) kb (b :: kb) (r :: Type). (a :~~: b) -> (a ~~ b => r) -> r Source #

hetHomoEq :: forall (k :: Type) (a :: k) (b :: k). (a :~~: b) -> a :~: b Source #

somewhat awkwardly named

class TestHetEquality (w :: forall k. k -> Type) where Source #

Methods

testHetEquality :: forall (ka :: Type) (a :: ka) (kb :: Type) (b :: kb). w a -> w b -> Maybe (a :~~: b) Source #

Instances

Instances details

TestHetEquality (HetEqual a) Source #
Instance details Defined in Data.Type.Witness.General.TestHetEquality Methods testHetEquality :: forall ka (a0 :: ka) kb (b :: kb). HetEqual a a0 -> HetEqual a b -> Maybe (a0 :~~: b) Source #

data HetEqual a b where Source #

Equivalent to :~~:, but can be made an instance of TestHetEquality

Constructors

HetRefl :: forall k (a :: k). HetEqual a a

Instances

Instances details

TestHetEquality (HetEqual a) Source #
Instance details Defined in Data.Type.Witness.General.TestHetEquality Methods testHetEquality :: forall ka (a0 :: ka) kb (b :: kb). HetEqual a a0 -> HetEqual a b -> Maybe (a0 :~~: b) Source #