[Ur] equality types and xml

[Adam Chlipala]

Gergely Buday wrote:
> do I understand correctly that only the following built-in types admit equality?
>
> class eq
> val eq : t ::: Type ->  eq t ->  t ->  t ->  bool
> val ne : t ::: Type ->  eq t ->  t ->  t ->  bool
> val eq_int : eq int
> val eq_float : eq float
> val eq_string : eq string
> val eq_char : eq char
> val eq_bool : eq bool
> val eq_time : eq time
> val mkEq : t ::: Type ->  (t ->  t ->  bool) ->  eq t
>    

You are free to add equality witnesses for any type at all.  You may 
even shadow the built-in witnesses in local contexts.  (Though I 
wouldn't want to make a strong statement about which witness would be 
chosen by automatic resolution in such a case. ;])

> And, what about xml? Is it not possible to compare two xml fragments?
>    

No [eq] instance for the [xml] family is provided in the standard 
library.  You can see that [xml] _does_ have a [show] instance, which 
provides an easy path to equality testing, but this operation (and a few 
others) frightens me in its capacity to break abstraction, by, for 
instance, revealing implementation choices for abstract types.  I may 
make the compiler by default warn about uses of such scary functionality.

> And, the only other types that have equality are those that I create
> an equality function with mkEq for?
>    

Right.