Type inference fails horribly when omitting argument label on a function call

user_7943564 0
Viewed 176

Given the following function

let get_or ~default =
  function | Some a -> a
           | None -> default

If this function is called with the argument labeled, it works as expected:

let works = get_or ~default:4 (Some 2)

But if the label is omitted it somehow fails:

let fails = get_or 4 (Some 2)

It gets weirder, however, the error message given here by the compiler is:

This expression has type int but an expression was expected of type ('a -> 'b) option

Not only has the compiler incorrectly inferred it to be an option, but for some reason it also pulls a function type out of the proverbial magician's hat! So naturally I wonder: where on earth does that come from? And somewhat less immediately important to my curiosity, why doesn't omitting the label work in this specific case?

See this reason playground for an interactive example.

Credit for this puzzle goes to @nachotoday on the Reason Discord.

parameter-passing type-inference ocaml label
1 Answers

This is a case of destructive interference between labelled arguments, currying and first class functions. The function get_or has for type

 val get_or: default:'a -> 'a option -> 'a

The rule with labelled arguments is that labels can be omitted when the application is total. At first glance, this means that if one apply get_or to two arguments, then it is a total application. But the fact that the return type of get_or is polymorphic (aka 'a) spells trouble. Consider for instance:

let id x = x
let x : _ -> _ = get_or (Some id) id ~default:id

This is valid code, where get_or was applied to three arguments and where the default argument was provided at the third position!

Going even further, as surprising at it might see, this is still valid:

let y : default:_ -> _ -> - = get_or (Some id) id id

And it yields a quite complicated type for y.

The generic rule here is that if the return type of a function is polymorphic then the type-checker can never know if a function application is total or not; and thus labels can never be ommited.

Going back to your example, this means that the type-checker reads

 get_or (4) (Some 2)

as

  • First, get_or has for type default:'a -> 'a option -> 'a. The default label has not been provided yet, so the result will have for type default:'r -> 'r
  • Looking at r, in get_or 2 (Some 4), get_or has for type 'a option -> 'a, thus get_or x:'a
  • Then get_or x:'a is applied to y; thus 'a = 'b -> 'c
  • In other words, I should have x: ('b -> ' c) option but I know that x:int.

Which leads to the contradiction reported by the type-checker, 2 was expected to be a function option ('a -> 'b) option, but was obviously a int.

user_73693660
Related