ú΀Z      Experimental$Erik Hesselink <hesselink@gmail.com> Safe-Inferred7A type class for constructing equality proofs for type D constructor with three parameters. If you find a use for this, let  me know. 7A type class for constructing equality proofs for type B constructor with two parameters. Can be useful when representing  relations between types. @A type class for constructing equality proofs. This is as close 9 as we can get to decidable equality on types. Note that f must be  a GADT to be able to define . Type equality. A value of a :=: b is a proof that types a and  b# are equal. By pattern matching on Refl this fact is ! introduced to the type checker. Equality is symmetric. ;Equality is transitive. This is the same as (>>>) from the  & instance, but also works in GHC 6.8. AEquality is substitutive. This is defined directly, but can also  be defined as    . BSubstitution inside nested type constructors. This is equivalent  to       . Equality is congruential. 6Congruence for type constructors with two parameters. 8Congruence for type constructors with three parameters. 2Coerce a type to another using an equality proof. )We can only read values if the result is a :=: a, not a :=: b > since that is not true, in general. We just parse the string  Refl5, optionally surrounded with parentheses, and return . Any value is just shown as Refl!, but this cannot be derived for ) a GADT, so it is defined here manually.          type-equality-0.1.2Data.Type.EqualityEqT3eqT3EqT2eqT2EqTeqT:=:Reflsymtranssubstsubst2congcong2cong3coercebaseControl.CategoryCategory. $fRead:=: $fShow:=: $fEqTk:=: $fCategory:=: