Let's rework Data.Type.Equality.==

[Phil Ruffwind]

On Fri, Aug 11, 2017, at 11:39, Richard Eisenberg wrote:
> If we have a more flexible notion of equality, how can we be sure that this
> more inclusive equality is always respected? Specifically, you would want
> this: if (ty1 == ty2) and ty1 is substituted for ty2 in some context,
> everything still works.

Not too familiar with this area, but I recall at one point realizing
that the
only kind of user-defined equality that is consistent with Leibniz
equality is
when the difference occurs in rigid type variables.  That is, whereas
you
can't make Set (A, B) == Set (B, A) since they are observably different,
you
can (sometimes) make F a == F b if a and b are existentially quantified
variables (no-one would be the wiser).