The Coq mailing list

["Lukasz Stafiniak" <lukstafi AT gmail.com>]

On 10/15/07, Pierre Letouzey 
<Pierre.Letouzey AT pps.jussieu.fr>
 wrote:
> On Sun, Oct 14, 2007 at 06:18:39PM +0200, Lukasz Stafiniak wrote:
> > OK, it seems it would defy type erasure, so not much sense in thinking 
> > about it.
> >
> By the way, could you commment more on your point concerning
> "defy type erasure" ?
>
I was too quick and a bit provocative. Types seem still (always?) to
be computationally relevant when they are needed for nonparametric
polymorphism (e.g. (forall A) A -> A translates into typerepr('a) ->
'a -> 'a; the type argument cannot be erased).

Does someone have a simple example, where "Obj.magic" cannot be
removed by translating into a GADT type "relaxed" w.r.t. original?
(Translation doesn't introduce new computations compared to generic
translation, and types ensure only "type preservation" and "progress",
not logical invariants).

Thanks,
£ukasz