Local function not polymorphic

Question

utop # let f : 'a -> 'a  = fun x -> x in (f 0, f true);;
Error: This expression has type bool but an expression was expected of type int

"This expression" refers to the true in f true.

Why does the above fail, but the below succeed?

utop # let f : 'a -> 'a  = fun x -> x;;
val f : 'a -> 'a = <fun>

utop # (f 0, f true);;
- : int * bool = (0, true)

I believe this has something to do with unification variables being scoped to the outer function. — glennsl, Apr 24 '23 at 21:58
From [the manual](https://v2.ocaml.org/manual/types.html#sss:typexpr-variables): "In general the scope of a named type variable is the whole top-level phrase where it appears, and it can only be generalized when leaving this scope. Anonymous variables have no such restriction. " — glennsl, Apr 24 '23 at 22:02
I'm sure there's an interesting reason for this that someone more familiar with the compiler internals can elaborate on. — glennsl, Apr 24 '23 at 22:03
@SilvioMayolo I don't think the value restriction is relevant here so I think marking this as a duplicate question is incorrect. — Kevin Ji, Apr 25 '23 at 07:50
@SilvioMayolo I don't think this is the value restriction, since this restriction only applies to named type variables, not anonymous ones. And in this case it's also a syntactic function, so you'd think the relaxed value restriction would allow it anyway. — glennsl, Apr 25 '23 at 07:51
BTW to fix this, all you need to do is replace unification variables with universal variables: `let f : 'a. 'a -> 'a = ...`. — Moth, Apr 26 '23 at 18:58

Chris · Accepted Answer · 2023-04-25T01:08:59.290

As noted by glennsl in comments, per the manual the type variables (e.g. 'a) are defined for the entire toplevel definition where they occur.

In general the scope of a named type variable is the whole top-level phrase where it appears

Consider defining a simple function f with a locally scoped function g which specifies a type of 'a -> 'a:

# let f x y =
    let g (x : 'a) : 'a = x in
    (g x, g y);;
val f : 'a -> 'a -> 'a * 'a = <fun>

Because 'a is scoped to the definition of f it has to be unified accordingly. The only way this can work is if x and y have the same type.

There is no such restriction if we elide the explicit type annotation on g.

# let f x y =
    let g x = x in
    (g x, g y);;
val f : 'a -> 'b -> 'a * 'b = <fun>

Another example. Starting without explicit type annotations. The compiler correctly infers that all four arguments must have wildcard types. It uses 'a through 'd'.

# let f a b c d =
    let g x y = (x, y) in
    let h x y = (x, y) in
    (g a b, h c d);;
val f : 'a -> 'b -> 'c -> 'd -> ('a * 'b) * ('c * 'd) = <fun>

And adding the explicit type annotation, the compiler infers that all four arguments must have wildcard types, but because we have already via passing them as arguments to g and h given those types names, a and c mst both save the same type, as must b and d.

# let f a b c d =
    let g (x : 'a) (y : 'b) : ('a * 'b) = (x, y) in
    let h (x : 'a) (y : 'b) : ('a * 'b) = (x, y) in
    (g a b, h c d);;
val f : 'a -> 'b -> 'a -> 'b -> ('a * 'b) * ('a * 'b) = <fun>

Local function not polymorphic

1 Answers1