[TYPES] Erasure and equality proofs

[Stefan Monnier]

I'm trying to get my head around the practical use of
erasure/irrelevant/implicit arguments, as discussed in papers such as

    The Implicit Calculus of Constructions as a Programming Language
    with Dependent Types
    Bruno Barras and Bruno Bernardo, fossacs08

    Erasure and polymorphism in pure type systems
    Nathan Mishra-Linger and Tim Sheard

    On the strength of proof-irrelevant type theories
    Benjamin Werner, IJCAR06

One of the desired benefits is to erase equality proofs, but those can't
be erased naively, since they're not only used in type annotations but
they're fundamentally passed to the corresponding elimination function
(or "match" expression).  Eliminating them naively could introduce
inconsistencies (if we remove them in those cases where the equality
proposition is actually an uninhabited type).

Benjamin suggests we can erase those equality proofs under one
condition: if the elimination rule is adjusted so that it checks
equality before performing the reduction.
But this, in turn requires that the 2 equal terms are not erasable.

Bruno Barras et al. suggests other restrictions: basically he suggests
to add a new elimination "eq_ind2" with all args erasable but without
reduction rule (i.e. as a mere axiom).

So I'm looking for some further info/work on actual uses of such
systems, where the practical impact of such restrictions are
investigated.  I'm especially interested in this, because I have the
impression (just gut feeling) that equality is not really special in
this respect and that many/most other places where proofs are passed end
up needing special treatment as well in order for those proofs to
be erasable.

IOW while I see that erasable arguments work fine for System-F style
parametric type arguments, most of the times when I try to make
a proof "erasable", I end up bumping into some place in the code where
I need the proof to appear in a non-erasable part of the code (unless
I add ad-hoc special rules along the lines suggested above for the
equality type).

I get the impression that we'd need erasability to be extended along the
lines of Coq's special treatment of single-constructor elimination from
Prop to Set, but such an extension doesn't seem to be consistent with
the use of "convertibility modulo erasure".


        Stefan