Extraction of recursive polymorphic functions
The following program is accepted by the Why3 type checker:
let rec f x =
let rec aux y = () in
aux x
However, it gets extracted to the following OCaml program:
let rec f : 'xi . 'xi -> unit =
fun l -> let rec aux : 'xi . 'xi1 -> unit = fun l1 -> () in aux l
which fails to compile with the error message Error: This definition has type 'xi1 -> unit which is less general than 'xi. 'xi -> unit
(This bug was originally found by @bbecker)