I am more optimistic: I think there's a good chance we could do better
than both Coq and Agda. Of course sometimes when we try new things
they flop; but we can't make progress without trying new things.
For one thing, I don't think we should conflate typical ambiguity with
cumulativity. It just so happens that Coq has both and Agda has
neither, but in principle I see no reason they have to go together. I
see typical ambiguity as basically syntactic sugar or abuse of
notation, analogous to the use of implicit arguments: the reader or
proof assistant is tasked (if they feel like it) to go through and
insert level parameters as needed, accumulating constraints on these
parameters according to how the instance are used and thereby
"elaborating" a typically ambiguous development to a fully precise one
with (polymorphic) universe levels. Usually this will be possible,
but occasionally if the writer was careless there may be a universe
inconsistency.
It seems to me that this could be done in both a cumulative and a
non-cumulative system. True, in a non-cumulative system we get
different constraints, e.g. if we ever write "A=B" then it must be
that A and B live in the same universe, whereas in a cumulative system
we could be looser about such constraints. But your evidence (and
that of other universe-polymorphic users of Agda) suggests that such
constraints arising from non-cumulativity are not in practice a
problem. In fact, the unique assignment of levels in a non-cumulative
system suggests that the universe inference algorithm in a
hypothetical typically-ambiguous non-cumulative proof assistant would
probably be *simpler*, and less error-prone, than that of Coq. So I
don't see any argument here against typical ambiguity, as long as
there is the *option* to be unambiguous when necessary (which again,
even Coq now supports).
In particular, note that when a development is formalized in a
typically ambiguous proof assistant, it's not necessary for the
universe levels to be written in the source code, or even thought
about by the author, in order for the interested reader -- or even the
author themselves! -- to learn about what the universe constraints
are. They only have to compile the code, in particular running it
through the universe checker/elaborator, and then inspect the
resulting universe levels/constraints. I've done this in present-day
Coq myself, although the proliferation of universe parameters makes
the output hard to undertsand; I expect it would only be easier in a
hypothetical typically-ambiguous non-cumulative proof assistant. So
it seems to me that it should be possible to be "fair to the reader",
as you say, and still retain (some of) the advantages of typical
ambiguity.
I also think there's a good chance we can retain some cumulativity
without losing the benefits of non-cumulativity, by using a
Tarski-style lifting coercion as I sketched in my last email. (Isn't
this in the literature somewhere? I didn't think I'd made it up.) I
agree that it's rare to need this, but neither is it unheard-of; so if
we can make it more convenient to use with no drawback, why not? (Of
course, cumulativity is also trickier to model semantically, but
probably possible.)