Description : Template Haskell primitives for working with large GADTs

This module declares template Haskell primitives so that it is easier to work with GADTs that have many constructors.

The Template Haskell instance generators structuralEquality, structuralTypeEquality, structuralTypeOrd, and structuralTraversal employ heuristics to generate valid instances in the majority of cases. Most failures in the heuristics occur on sub-terms that are type indexed. To handle cases where these functions fail to produce a valid instance, they take a list of exceptions in the form of their second parameter, which has type [(TypePat, ExpQ)]. Each TypePat is a matcher that tells the TH generator to use the ExpQ to process the matched sub-term. Consider the following example:

data T a b where
  C1 :: NatRepr n -> T () n

instance TestEquality (T a) where
  testEquality = $(structuralTypeEquality [t|T|]
                   [ (ConType [t|NatRepr|] `TypeApp` AnyType, [|testEquality|])
                   ])

The exception list says that structuralTypeEquality should use testEquality to compare any sub-terms of type NatRepr n in a value of type T.

• AnyType means that the type parameter in that position can be instantiated as any type
• DataArg n means that the type parameter in that position is the n-th type parameter of the GADT being traversed (T in the example)
• TypeApp is type application
• ConType specifies a base type

The exception list could have equivalently (and more precisely) have been specified as:

[(ConType [t|NatRepr|] `TypeApp` DataArg 1, [|testEquality|])]

The use of DataArg says that the type parameter of the NatRepr must be the same as the second type parameter of T.