__ in Ocaml extracted from Coq

Question

Ocaml code extracted from Coq includes (in some cases) a type `__` and a function `__` defined as follows: ``` type __ = Obj.t let __ = let rec f _ = Obj.repr f in Obj.repr f ``` The documentation says that in the past, such type was defined as `unit` (and thus `__` could be taken as `()`) but there exist (rare) cases where a value of type `__` is applied to a value of type `__`. `__` uses undocumented functions of the `Obj` module from OCaml, but it seems that what is defined is essentially a totally polymorphic function that eats all its arguments (whatever their number). Is there some documentation regarding the cases where `__` cannot be eliminated and values of this type are applied to values of the same type, both from a theoretical (construct Coq terms where elimination is impossible) and from a practical (show a realistic case where this occurs) point of view?

Accepted Answer

The references cited in the README give a nice overview of the erasure problem. Specifically, both this report and this article exaplain in detail how the type schemes and logical parts of CIC terms are erased, and why one must have `__ x = __`. The problem is not exactly that `__` may be applied to itself, but that it may be applied to anything at all.

Unfortunately, it is not at all clear if having this behavior is important in any non-pathological case. The motivation given there is to be able to extract any Coq term, and the documents do not mention any cases that are really interesting from a practical standpoint. The example given on 3 is this one:

```
Definition foo (X : Type) (f : nat -> X) (g : X -> nat) := g (f 0).
Definition bar := foo True (fun _ => I).
```

Executing `Recursive Extraction bar.` gives the following result:

```
type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

type nat =
| O
| S of nat

(** val foo : (nat -> 'a1) -> ('a1 -> nat) -> nat **)

let foo f g =
  g (f O)

(** val bar : (__ -> nat) -> nat **)

let bar =
  foo (Obj.magic __)
```

Since `foo` is polymorphic on `Type`, there is no way of simplifying the `f O` application on its body, because it could have computational content. However, since `Prop` is a subtype of `Type`, `foo` can also be applied to `True`, which is what happens in `bar`. When we try to reduce `bar`, thus, we will have `__` being applied to `O`.

This particular case is not very interesting, because it would be possible to fully inline `foo`:

```
let bar g =
  g __
```

Since `True` can't be applied to anything, if `g` corresponds to any legal Coq term, its `__` argument also wouldn't be applied to anything, and therefore it would be safe to have `__ = ()` (I believe). However, there are cases where it is not possible to know in advance whether an erased term can be further applied or not, which makes the general definition for `__` necessary. Check out for instance the `Fun` example here, near the end of the file.

__ in Ocaml extracted from Coq

Solution

Problem