Hi,

> We present a simple, pure, magic-free implementation of a form of
> GADTs in OCaml that is sufficient for the common applications of GADTs
> such as data structures with embedded invariants, typed printf/scanf,
> tagless interpreters. (...)

Very interesting -- clever, yet so simple!  But note that as far as the
link-nodes-shall-not-be-ancestors-of-their-kind problem is concerned, there
is one problem with the presented implementation.  Consider the following
declarations:

let t1 = text "ola"
let t2 = href "http"
let t3 = bold [t1; t2]
let t4 = mref "http" [t1]

This causes an error upon t4.  The reason is that because of t3, t1 was
unified as "node_link node_t", whereas t4 requires it to be "node_nolink node_t".  I think the solution is to revert to using polymorphic variants
for the phantom type, and take advantage of their open-ended nature.
(Though I'm guessing some extra massaging will be required -- it's Sunday
and I don't have much time to look into this).

Anyway, perhaps the Batteries folks will consider including both versions
of the Eq module?  It will certainly prove useful for many people. (Am I
correct in assuming you are releasing the code into the public domain or
at least some open-source friendly license?)

Best regards,
Dario Teixeira