[TYPES] Do erasable boxes form a monad?

[Stefan Monnier]

> I'm not very sure about your impredicative encoding, but both your examples
> work if you define Erased in a more direct way in Agda extended with Prop
> (currently in the development version of Agda):

That's the thing: with Coq-style Prop's erasability I can define those
operations, indeed.  But in the context of ICC's erasability (which is
not tied to Prop and is used to strengthen the conversion rule by
checking beta-equivalence on the erased version of the code), it seems
that those properties don't hold any more.

> _>>=_ : Erase A → (A → Erase B) → Erase B
> (box (squash x) >>= f) .unbox = f x .unbox

In ICC this definition is rejected because the erasure of this code is

    >>= f = f x

where `x` is a "dangling" free variable, because the left hand side
argument is erased, but `f` takes a non-erasable argument so its
argument is not erased.


        Stefan