HORIZON HASKELLDocslts/ghc-9.14.x3e2d5682026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 9.14.1 · lts/ghc-9.14.x · 3e2d568 · 2026-10-11

Moduledependent-sum-0.6.2.0Haskell98

Data.GADT.Compare

  • 3 types
  • 2 classes
  • 4 values
valuedefaultEq :: GEq f => f a -> f b -> Bool
#

If f has a GEq instance, this function makes a suitable default implementation of (==).

valuedefaultNeq :: GEq f => f a -> f b -> Bool
#

If f has a GEq instance, this function makes a suitable default implementation of (/=).

typetype (:=) = (:~:)
#

Deprecated. use (:~:) from 'Data.Type,Equality'.

Backwards compatibility alias; as of GHC 7.8, this is the same as (:~:).

classclass GEq f => GCompare (f :: k -> Type) where
#

Type class for comparable GADT-like structures. When 2 things are equal, must return a witness that their parameter types are equal as well (GEQ).

Methods

Instances4GCompare
classclass GEq (f :: k -> Type) where
#

A class for type-contexts which contain enough information to (at least in some cases) decide the equality of types occurring within them.

Methods

  • geq :: f a -> f b -> Maybe (a :~: b)

    Produce a witness of type-equality, if one exists.

    A handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:

    extract :: GEq tag => tag a -> DSum tag -> Maybe a
extract t1 (t2 :=> x) = do
    Refl <- geq t1 t2
    return x

    Or in a list comprehension:

    extractMany :: GEq tag => tag a -> [DSum tag] -> [a]
extractMany t1 things = [ x | (t2 :=> x) <- things, Refl <- maybeToList (geq t1 t2)]

    (Making use of the DSum type from Data.Dependent.Sum in both examples)

Instances4GEq
  • GEq TypeRepDefined in dependent-sum-0.6.2.0 · Data.GADT.Compare
  • GEq ((:~:) a)Defined in dependent-sum-0.6.2.0 · Data.GADT.Compare
  • (GEq a, GEq b) => GEq (Product a b)Defined in dependent-sum-0.6.2.0 · Data.GADT.Compare
  • (GEq a, GEq b) => GEq (Sum a b)Defined in dependent-sum-0.6.2.0 · Data.GADT.Compare
datadata GOrdering (a :: k) (b :: k) where
#

A type for the result of comparing GADT constructors; the type parameters of the GADT values being compared are included so that in the case where they are equal their parameter types can be unified.

Constructors

Instances5GRead, GShow, Eq, Ord, Show
  • GRead (GOrdering a)Defined in dependent-sum-0.6.2.0 · Data.GADT.Compare
  • GShow (GOrdering a)Defined in dependent-sum-0.6.2.0 · Data.GADT.Compare
  • Eq (GOrdering a b)Defined in dependent-sum-0.6.2.0 · Data.GADT.Compare
  • Ord (GOrdering a b)Defined in dependent-sum-0.6.2.0 · Data.GADT.Compare
  • Show (GOrdering a b)Defined in dependent-sum-0.6.2.0 · Data.GADT.Compare
datadata (:~:) (a :: k) (b :: k) where
#

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Constructors

Instances19Category, TestCoercion, TestEquality, GEq, GCompare, GRead, …
  • Category (:~:)Defined in ghc-internal-9.1401.0 · GHC.Internal.Control.Category
  • TestCoercion ((:~:) a)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Coercion
  • TestEquality ((:~:) a)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • GEq ((:~:) a)Defined in dependent-sum-0.6.2.0 · Data.GADT.Compare
  • GCompare ((:~:) a)Defined in dependent-sum-0.6.2.0 · Data.GADT.Compare
  • GRead ((:~:) a)Defined in dependent-sum-0.6.2.0 · Data.GADT.Show
  • GShow ((:~:) a)Defined in dependent-sum-0.6.2.0 · Data.GADT.Show
  • NFData2 (:~:)Defined in deepseq-1.5.1.0 · Control.DeepSeq
  • NFData1 ((:~:) a)Defined in deepseq-1.5.1.0 · Control.DeepSeq
  • a ~ b => Bounded (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • a ~ b => Enum (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • Eq (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • (a ~ b, Data a) => Data (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Data
  • Ord (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • a ~ b => Read (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • Show (a :~: b)Defined in ghc-internal-9.1401.0 · GHC.Internal.Data.Type.Equality
  • NFData (a :~: b)Defined in deepseq-1.5.1.0 · Control.DeepSeq
  • a ~ b => Boring (a :~: b)Defined in boring-0.2.2.1 · Data.Boring

    Homogeneous type equality is Boring too.

  • HasDict (a ~ b) (a :~: b)Defined in constraints-0.14.4 · Data.Constraint