Unclear behaviour of the type inference engine for polymorphic function

Learning
1

Hi everyone,

I have some trouble understanding how the type inference engine manages polymorphic functions and their type annotation, and, more specifically, why its behaviour regarding them changes depending in which scope the function is declared.
Let me give you an example (I use OCaml 4.07) :

let f : 'a -> 'a = fun x -> x

let () =
  let g : 'a -> 'a = fun x -> x in
  ignore (f 1);
  ignore (f "a");
  ignore (g 1);
  ignore (g "a")

This example would fail to compile, because of a typing error occuring on the last line :

`This expression has type string but an expression was expected of type int

Basically, it seems that the existence of the term g 1 somehow “specializes” the type of g, making it an int -> int function in the type inference engine’s point of view rather than a polymorphic 'a -> 'a function, thus making the term g "a" unsound.

What I don’t understand is :
1/ Why does this occur for g and not for f ? They have the exact same definition but are declared in different scopes. What is it supposed to demonstrate regarding the way the type inference engine manages them ?

2/ I have explicitely annotated g as a 'a -> 'a function when declaring it. If I hadn’t, and had let the compiler infer its type, it would have worked ! i.e. the following code :

 let () =
    let g = fun x -> x in
    ignore (g 1);
    ignore (g "a")

would compile neatly. So would the following :

 let () =
    let g : type a. a -> a = fun x -> x in
    ignore (g 1);
    ignore (g "a")

where I explicitely state that I expect the type term a -> a to be universally quantificated over type a.
Does it mean that typing let g : 'a -> 'a = ... implies an existential quantification over type 'a ?

At this point, all I know is that I’m no longer sure how the type inference works, so any explanation would be very welcome :slight_smile:

Thanks in advance !

2

Unification types variables are indeed implicitly existentially quantified, and they are only generalized when they go out of scope. In other words, your issue is that 'a is still in scope as you can see with

let () =
  let g : 'a -> 'a = fun x -> x in
  ignore (f 1);
  ignore (f ("a":'a));
  ignore (g 1);
  ignore (g "a");;

Line 5, characters 12-13:
Error: This expression has type int but an expression was expected of type
string

Notice that the error is now on the first use of g because 'a was unified with string.
Consequently, we can avoid the issue by only introducing the unification variable 'ainside an inner submodule:

let () =
  let module M = struct let g : 'a -> 'a = fun x -> x end in
  ignore (f 1);
  ignore (f ("a":'a));
  ignore (M.g 1);
  ignore (M.g "a");;
2 Likes
3

Interesting. Is there a reference or a simple rule for what the scope of a type variable is? I notice that this doesn’t work:

let () =
  let g =
    let g : 'a -> 'a = fun x -> x in
    g
  in
  ignore (g 1);
  ignore (g "a")
4

Basically, user defined type variables only get out of scope at the end of toplevel definition group:

let f: 'a = 0 and g: 'a = "hi";;

Error: This expression has type string but an expression was expected of type
int

(Local modules make it possible to have a nested toplevel definitions).