Safe Haskell	Trustworthy
Language	Haskell2010

Data.Type.Equality.Hetero

Description

This module shims kind heterogeneous propositional equality.

Note: some instances: Read, Enum, Bounded and Data would be available only since GHC-8.0 as we need ~~ constraint. Also GH-7.10.3 is nitpicky data constructor ‘HRefl’ cannot be GADT-like in its *kind* arguments, thus this module is available only with GHC >= 8.0

Documentation

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

Constructors

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

Instances

Instances details

TestEquality ((:~~:) a :: k -> Type)
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)
Instance details Defined in Data.Type.Equality Methods minBound :: a :~~: b maxBound :: a :~~: b
a ~~ b => Enum (a :~~: b)
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]
Eq (a :~~: b)
Instance details Defined in Data.Type.Equality Methods (==) :: (a :~~: b) -> (a :~~: b) -> Bool (/=) :: (a :~~: b) -> (a :~~: b) -> Bool
Ord (a :~~: b)
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
a ~~ b => Read (a :~~: b)
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)
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~~: b) -> ShowS show :: (a :~~: b) -> String showList :: [a :~~: b] -> ShowS