Let’s try to reproduce how the compiler tries to infer types here.
let rec Foo(a,b) = match a () with | None -> Some(b) | Some(c) -> Some(Foo(c,b))
“Ok, so I see
a must be a function from
unit to some type, I don’t know which one yet. I’ll call it
a : unit -> 'a
“The result of
a () is matched with
Some patterns. So
'a must be a
'b option and
c has the type
'b stands for an unknown, as of yet, type).
a : unit -> 'b option с : 'b
“No functions or methods are called on
Some, which doesn’t narrow the type down, and
Foo, the type of which we don’t know so far). I’ll denote its type by
a : unit -> 'b option b : 'c c : 'b
Some(b) in one of the branches, so the return type must be
Foo : (unit -> 'b option) * 'c -> 'c option
“Am I done yet? No, I need to check that all types in the expression make sense. Let’s see, in the
Some(Foo(c,b)) is returned. So
Foo(c,b) : 'c. Since
Foo returns an
option, I know
'c must be
'd option for some
b : 'd. Wait, I already have
b : 'c, that is,
b : 'd option.
'd option have to be the same type, but this is impossible! There must be an error in the definition. I need to report it.” So it does.
Originally posted 2013-11-09 23:04:41.