Skip to main content

Faq

Here we answer to some questions you may have when using coq-of-ocaml.

Why is there an -impredicative-set option to Coq?​

To compile the files generated by coq-of-ocaml, we need to use the -impredicative-set option with Coq. The Impredicative Set page of the Coq wiki gives some details about this option. The reason for that is to avoid getting into universe inconsistency errors. If we take the following example:

type t =
  | Empty
  | Node : 'a -> t

(* This function could be a deserializing function from [string] to [t]. We
   use lists for the sake of simplicity. *)
let rec t_of_list (l : 'a list) : t =
  match l with
  | [] -> Empty
  | _ :: l -> Node (t_of_list l)

we generate the Coq translation:

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Inductive t : Set :=
| Empty : t
| Node : forall {a : Set}, a -> t.

Fixpoint t_of_list {a : Set} (l : list a) : t :=
  match l with
  | [] => Empty
  | cons _ l => Node (t_of_list l)
  end.

The type t has a constructor Node with an existential type a. With the function t_of_list we generate a value with a number of nested existential types equals to the length of the list l. This generated Coq code is valid.

In contrast, if we were using Type instead of Set this would not work. Indeed, an existential type increases the universe level by one in Type. So this function would have a universe level for its result equals to the length on the list. This does not seem easy to express, even with polymorphic universes.