The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Fri, Sep 12, 2014 at 1:52 PM, Jonathan 
<jonikelee AT gmail.com>
 wrote:
> But, if one is willing, one can exploit the Prop universe to get such things
> erased.  This can complicate things a bit - for example, you would need an
> alternate definition of Vector - but that is fairly easy (if lengthy) to
> achieve.  To exploit the Prop universe this way requires adding an axiom -
> with the usual consistency risks of doing so - but it is a very simple axiom
> that, as far as I know, is only incompatible with general proof-irrelevance
> (among the typical other axioms that are frequently added to Coq), but not
> with specific proof-irrelevance (defined separately for each Prop one wishes
> to be irrelevant, such as equality).  The idea of this axiom is to make a
> single Prop relevant by adding an injectivity axiom to its sole constructor,
> and to use "lifted" (into that single Prop) versions of types and values you
> want erased in those spots where you want them erased - and then allow Coq's
> normal Prop removal to do its thing.  With careful handling, one can get
> OCaml output from Coq with this addition that is quite clean.

And here, all this time, I thought you were using something more like
a singleton monad: passing an argument of type (nat -> Prop) in place
of nat which is understood (or maybe even restricted) to be a
singleton set.  That should probably work along with proof
irrelevance, maybe with an axiom like Extensionality_Ensembles but
maybe even without it.
-- 
Daniel Schepler