Richard Eisenberg eir at cis.upenn.edu writes:
And, in response to your closing paragraph, having type-level equality
is the prime motivator for a lot of
this work, so we will indeed have it!
Thank you Richard, I'll take comfort in that.
I'd beware this though: the Nonlinearity wikipage
Ah -- I think the waters have been muddied somewhat as our thoughts have
evolved. The plan of action (of history, at this point -- I merged into HEAD
yesterday) is to use the check labeled (B) on the wiki page. This check does
*not* ban all nonlinear type families. It just makes certain
