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 infix 4 Source #
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
Instances
TestEquality ((:~~:) a :: k -> Type) | Since: base-4.10.0.0 |
Defined in Data.Type.Equality | |
a ~~ b => Bounded (a :~~: b) | Since: base-4.10.0.0 |
a ~~ b => Enum (a :~~: b) | Since: base-4.10.0.0 |
Defined in Data.Type.Equality Methods succ :: (a :~~: b) -> a :~~: b Source # pred :: (a :~~: b) -> a :~~: b Source # toEnum :: Int -> a :~~: b Source # fromEnum :: (a :~~: b) -> Int Source # enumFrom :: (a :~~: b) -> [a :~~: b] Source # enumFromThen :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] Source # enumFromTo :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] Source # enumFromThenTo :: (a :~~: b) -> (a :~~: b) -> (a :~~: b) -> [a :~~: b] Source # | |
a ~~ b => Read (a :~~: b) | Since: base-4.10.0.0 |
Show (a :~~: b) | Since: base-4.10.0.0 |
Eq (a :~~: b) | Since: base-4.10.0.0 |
Ord (a :~~: b) | Since: base-4.10.0.0 |
Defined in Data.Type.Equality Methods compare :: (a :~~: b) -> (a :~~: b) -> Ordering Source # (<) :: (a :~~: b) -> (a :~~: b) -> Bool Source # (<=) :: (a :~~: b) -> (a :~~: b) -> Bool Source # (>) :: (a :~~: b) -> (a :~~: b) -> Bool Source # (>=) :: (a :~~: b) -> (a :~~: b) -> Bool Source # |