Generics.RepLib

Basic infrastructure

Basic Representations of types

module Generics.RepLib.R

Parameterized Representations of types

module Generics.RepLib.R1

Representations of Prelude Types

module Generics.RepLib.PreludeReps

Template Haskell for deriving representations

module Generics.RepLib.Derive

Libraries for defining Generic Operations

Library code for defining generic operations

module Generics.RepLib.RepAux

Scrap your boilerplate operations

module Generics.RepLib.SYB.Aliases

module Generics.RepLib.SYB.Schemes

Generic Utilities and Applications

Library of generic operations

module Generics.RepLib.Lib

Derivable type classes written as generic operations

module Generics.RepLib.PreludeLib

data a :~: b :: k -> k -> * where infix 4

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.

Since: 4.7.0.0

Constructors

Refl :: (:~:) k a1 a1

Instances

TestEquality k ((:~:) k a)

(Rep a, Rep b, Sat (ctx a), Sat (ctx b)) => Rep1 ctx ((:~:) * a b)

Typeable (k -> k -> *) ((:~:) k)

(~) k a b => Bounded ((:~:) k a b)

(~) k a b => Enum ((:~:) k a b)

Eq ((:~:) k a b)

((~) * a b, Data a) => Data ((:~:) * a b)

Ord ((:~:) k a b)

(~) k a b => Read ((:~:) k a b)

Show ((:~:) k a b)

(Rep a, Rep b) => Rep ((:~:) * a b)

class TestEquality f where

This class contains types where you can learn the equality of two types from information contained in terms. Typically, only singleton types should inhabit this class.

Methods

testEquality :: f a -> f b -> Maybe ((:~:) k a b)

Conditionally prove the equality of a and b.

Instances

TestEquality * R

TestEquality k ((:~:) k a)