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 #
Instances
TestEquality ((:~~:) a :: k -> Type) | |
Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) | |
a ~~ b => Bounded (a :~~: b) | |
Defined in Data.Type.Equality | |
a ~~ b => Enum (a :~~: b) | |
Defined in Data.Type.Equality | |
a ~~ b => Read (a :~~: b) | |
Defined in Data.Type.Equality | |
Show (a :~~: b) | |
Eq (a :~~: b) | |
Ord (a :~~: b) | |
Defined in Data.Type.Equality |