úÎTBRY        '-like class for 1-type-parameter GADTs     IType class for orderable GADT-like structures. When 2 things are equal, K must return a witness that their parameter types are equal as well (GEQ). L |Type class for comparable GADT-like structures. When 2 things are equal, E must return a witness that their parameter types are equal as well ( ). JA type for the result of comparing GADT constructors; the type parameters K of the GADT values being compared are included so that in the case where 6 they are equal their parameter types can be unified. ;A class for type-contexts which contain enough information ; to (at least in some cases) decide the equality of types  occurring within them. 3Produce a witness of type-equality, if one exists. OA handy idiom for using this would be to pattern-bind in the Maybe monad, eg.:  4 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:  6 extractMany :: GEq tag => tag a -> [DSum tag] -> [a] V 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) AA GADT witnessing equality of two types. Its only inhabitant is . If f has a 3 instance, this function makes a suitable default  implementation of '(==)'. If f has a 3 instance, this function makes a suitable default  implementation of '(/=)'. TODO: Think of a better name .This operation forgets the phantom types of a   value.        In order to compare DSum tag values, tag must know how to compare % both itself and its tagged values.  defines the 0 interface by which they are expected to do so. Continuing the Tag example from the  section, we can define:   instance GCompare Tag where $ gcompare AString AString = GEQ $ gcompare AString AnInt = GLT $ gcompare AnInt AString = GGT $ gcompare AnInt AnInt = GEQ  instance OrdTag Tag where - compareTagged AString AString = compare - compareTagged AnInt AnInt = compare As with , $ only needs to consider cases where    returns  . Given two values of type tag a (for which   returns  ),  return the ! function for the type a. In order to test DSum tag for equality, tag must know how to test 2 both itself and its tagged values for equality.  defines 4 the interface by which they are expected to do so. Continuing the Tag example from the  section, we can define:   instance GEq Tag where % geq AString AString = Just Refl # geq AString AnInt = Nothing # geq AnInt AString = Nothing % geq AnInt AnInt = Just Refl  instance EqTag Tag where % eqTagged AString AString = (==) % eqTagged AnInt AnInt = (==)  Note that . is not called until after the tags have been 8 compared, so it only needs to consider the cases where   returns  . Given two values of type tag a (for which   returns  ),  return the " function for the type a. In order to make a   instance for DSum tag, tag must be able : to show itself as well as any value of the tagged type.  together ? with this class provides the interface by which it can do so. GShow tag => t3 is conceptually equivalent to something like this  imaginary syntax: ,(forall a. Inhabited (tag a) => Show a) => t,  where  Inhabited/ is an imaginary predicate that characterizes  non-empty types, and a does not occur free in t. The Tag example type introduced in the  section could be given the  following instances:  instance GShow Tag where @ gshowsPrec _showsValPrec _p AString = showString "AString" > gshowsPrec _showsValPrec _p AnInt = showString "AnInt"  instance ShowTag Tag where ( showTaggedPrec AString = showsPrec ( showTaggedPrec AnInt = showsPrec Given a value of type tag a , return the # function for  the type parameter a. IA basic dependent sum type; the first component is a tag that specifies @ the type of the second; for example, think of a GADT such as:   data Tag a where  AString :: Tag String  AnInt :: Tag Int 6Then, we have the following valid expressions of type DSum Tag:   AString :=> "hello!"  AnInt :=> 42 (And we can write functions that consume DSum Tag values by matching,  such as:   toString :: DSum Tag -> String " toString (AString :=> str) = str ' toString (AnInt :=> int) = show int IBy analogy to the (key => value) construction for dictionary entries in H many dynamic languages, we use (key :=> value) as the constructor for I dependent sums. The :=> operator has very low precedence and binds to  the right, so if the Tag1 GADT is extended with an additional constructor  Rec :: Tag (DSum Tag), then Rec :=> AnInt :=> 3 + 4 is parsed as  would be expected (Rec :=> (AnInt :=> (3 + 4))) and has type DSum Tag. & Its precedence is just above that of $, so foo bar $ AString :=> eep  is equivalent to foo bar (AString :=> eep).    %      !"#$%&$'($')$%*$+,-dependent-sum-0.2Data.GADT.ShowData.GADT.CompareData.Dependent.SumGRead greadsPrecGReadSGShow gshowsPrecgshowsgshowgreadsgreadGComparegcompare GOrderingGGTGEQGLTGEqgeq:=Refl defaultEq defaultNeqweakenOrderingOrdTag compareTaggedEqTageqTaggedReadTagreadTaggedPrecShowTagshowTaggedPrecDSum:=>baseGHC.ShowShow GHC.Classescompare== showsPrecGHC.Base$