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 combinat
> Richard Eisenberg 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 s
