Unifying inferred type of method with optional parameter?

Learning
,
1

I ran into this issue:

# let test cond o =
    if cond then o#f ~x:1 2
    else o#f 2;;

Error: This function is applied to arguments
       in an order different from other calls.
       This is only allowed when the real type is known.

Is there some reason why the compiler can’t infer the type of o#f as int -> 'a in the else branch, and then unify that with x:int -> int -> 'a in the if branch to ?x:int -> int -> 'a?

2

This is what I found by some quick lookups.

The OCaml Papers page lists “Labeled and Optional Arguments for Objective Caml” by Jacques Garrigue contains the following note (emphasis mine):

In [FG95], we attempted to solve this problem by allowing label commutation in some types, but the way it was compiled created potential gaps with call-by-value semantics (it was correct in a call-by-name setting), and moreover we could not allow commutation in more complex cases, like the types of object methods, or when optional arguments are implied.

FG95 is the paper “A label-selective lambda-calculus with optional arguments and its compilation method” by Jun P. Furuse and Jacques Garrigue, containing the following example:

We do not allow to unify types with optional domains. They would introduce indeterminism. For instance, if we try to unify ?l:int → int and α, we cannot tell whether α should be unified with int or ?l:int → int, this only depends on the programmer’s intention, and we do not know it.

It’s not exactly of the same form as your example, because neither of the to-be-unified types in your example have an optional domain, only the desired result would. Perhaps that step on its own might be fine, but that optional might need to be unified further with something, leading to the cited example again.

Some type theorists could probably pinpoint more precisely, how it could lead to actual issues.

2 Likes