Why won't OCaml specialize weak type variables in dead code?

Learning
1

Here is a small example of code that approximates what I get when using Coq’s Extraction:

type zrange = { lower : string }

let show0 show1 =
  show1

let showLevel_of_Show h t0 _ =
  show0 h t0

let show_zrange r = r.lower

let show_lvl_zrange =
  showLevel_of_Show show_zrange

let main : unit = ()

When I put this in foo.ml and invoke ocamlopt foo.ml -o foo, I get

File "foo.ml", line 11, characters 4-19:
11 | let show_lvl_zrange =
         ^^^^^^^^^^^^^^^
Error: The type of this expression, zrange -> '_weak1 -> string,
       contains type variables that cannot be generalized

I was under the impression that this applied only when trying to expose such weak definitions in module types. However, there is no module type here, as I’m just compiling a binary, and ocaml should be able to see that this code is dead. (In my actual example, the code is not dead, but the type of the argument cannot be inferred because show_lvl_zrange is only ever invoked when wrapped in Obj.magic, so again it should not matter if OCaml instantiates it with int or string or unit or anything at all.) How do I get the compiler to stop complaining here and ignore weak type variables in dead types? (I tried touch foo.mli, but then I get “Error: Could not find the .cmi file for interface foo.mli.”)

2

You need to make sure the arguments are in the correct order:

ocamlopt foo.mli foo.ml -o foo

Notice that the .mli is before the .ml

1 Like
3

You can also wrap all your code in module Toplevel : sig end = struct ... end. It has the same effect as the empty .mli, but you don’t even have to bother compiling another file.
With a recent enough version of OCaml (at least 4.10.0), you can even use module _ : sig end = struct ... end.

1 Like