[TYPES] Do erasable boxes form a monad?

[Stefan Monnier]

I'm playing with erasability in the sense of the Implicit Calculus of
Constructions and bumping into problems:

Say we create a datatype holding an erasable element.
We could define it as follows using the impredicative encoding:

    Erased : Type -> Type;
    Erased t = (r : Type) -> (t ≡> r) -> r;

    erase : (t : Type) ≡> t -> Erased t;
    erase t x = λ r -> λ f -> f x;

where I use ≡> to denote the "implicit" abstraction (which I like to
call "erasable", and yet others might favor "irrelevant").

With such a definition, we can implement functions such as:

    erased_liftfun : Erased (t₁ -> t₂) -> (Erased t₁ -> Erased t₂);
    erased_liftfun f x = case f
                         | erase f' => case x
                                       | erase x' => erase (f' x');

[ where I write `case e of erase x => ...x...x...` instead of
  `e (λ x ≡> ...x...x...)`  ]

But I can't seem to write the reverse function.
More puzzlingly, I can't seem to write the monad bind operator.
I.e. the below types seem not to be inhabited:

    erased_bind : Erased t₁ -> (t₁ -> Erased t₂) -> Erased t₂;
    erased_funlift : (Erased ?t₁ -> Erased ?t₂) -> Erased (?t₁ -> ?t₂);

Am I just not trying hard enough, or is there something deeper?
Would it break the consistency of the logic to add one of those as
an axiom?


        Stefan