__ 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?

Answer 1

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.