OCaml insist that function is not polymorphic, but don't specify the type

Question

Is it possible to explicitly write down a type that's non-polymorphic but has delayed unification like underscore types?

So, OCaml will sometimes produce a type that the top-level prints with a leading underscore (e.g. _a) in the course of type checking. Specifically, these appear when instantiating an empty Hashtbl.t and under some other circumstances.

# Hashtbl.create 1;;
- : ('_a, '_b) Hashtbl.t = <abstr>

However, these types cannot be explicitly referred by the user in source code.

# (5: int);;
- : int = 5
# (5: 'a);;
- : int = 5
# (5: '_a);;
Error: The type variable name '_a is not allowed in programs

You can create an explicitly non-polymorphic function by exploiting the lack of higher-rank polymorphism in OCaml

# let id = snd ((), fun y -> y);;
val id : '_a -> '_a = <fun>
# (fun () -> fun y -> y) ();;
- : '_a -> '_a = <fun>

I'd like to be able to do something like

let id : <some magical type> = fun x -> x

and not rely on a limitation of the type system that could conceivably go away in the future.

Answer 1

You could use the fact that references are not generalizable.

# let id = let rx = ref [] in fun x -> rx := [x]; rx := []; x;;
val id : '_weak1 -> '_weak1 = <fun>

I'm thinking this property of references isn't likely to change.

I assume what you want is for this version of id to assume a single monomorphic type the first time it's actually used:

# id "yes";;
- : string = "yes"
# id;;
- : string -> string = <fun>

If you use this in real code, it will need to get a concrete type before the end of its module. You can't leave the weak type variable undefined or you get this error:

Error: The type of this expression, '_weak1 -> '_weak1,
       contains type variables that cannot be generalized

Answer 2

The two other answers basically exploits the fact that only values are generalized, and so if you wrap your definition in something that is not a value, it doesn't get generalized. Hence the trick of giving it to the id function.

However, it doesn't work if you take the relaxed value restriction in account:

# let nil = id [] ;;
val nil : 'a list = []

You thus need to make sure the type variable you want doesn't appear in covariant position. In your first example, it appears on the left of the arrow, so it's fine. Otherwise, you need to make sure it works by hiding the type definition and ommiting the variance annotation.

module M : sig
  type 'a t
  val make : 'a list -> 'a t
end = struct
  type 'a t = 'a list
  let make x = x
end

let x = M.make []
val x : '_weak1 M.t

Answer 3

I agree with Jeffrey Scofield's answer but, in my opinion, it's better to avoid references, you can achieve the same behavior without them:

# let id = let id = fun x -> x in id id;;
val id : '_weak1 -> '_weak1 = <fun>

After that, if you need function with some other signature, for example eq : '_weak2 -> '_weak2 -> bool, then all you need is to implement eq in a normal way and pass it to id:

# let eq =
    let id = let id = fun x -> x in id id in
    let eq = (=) in (id (eq));;
val eq : '_weak2 -> '_weak2 -> bool = <fun>