F#: Can someone explain my compiler error?

Question

Anyone know what the problem with this code is?

let rec Foo(a,b) =
    match a () with
    | None -> Some(b)
    | Some(c) -> Some(Foo(c,b))

Here's the compiler error:

"Type mismatch. Expecting a 'a but given a 'a option The resulting type would be infinite when unifying ''a' and ''a option'"

Answer 1

You are using a() as an option which is the first parameter in Foo, but, in the last line c is a type, and yet you pass it into the recursive call.

That is what is leading to the error.

You will want to either have c be an option type.

Answer 2

It always helps to break things down step-by-step. As written, Foo has the type:

val Foo : (unit -> 'a option) * 'b -> 'b option

Each expression in an active pattern must evaluate to the same type. The first pattern match in your expression has the type:

'b option

Therefore, the other pattern must also evaluate to 'b option or 'a option. The way that you have it here, it is returning 'a option option.

This is a peculiar function but you could correct the compiler error by returning any option value in the second pattern match. Here is the only example that I can think of that looks anything like the above:

let Foo2(a,b) =
    match a () with
    | None -> Some(b)
    | c    -> c

HTH.

Answer 3

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 (). a must be a function from unit to some type, I don't know which one yet. I'll call it 'a."

a : unit -> 'a

"The result of a () is matched with None/Some patterns. So 'a must be a 'b option and c has the type 'b." (Again, 'b stands for an unknown, as of yet, type).

a : unit -> 'b option
с : 'b

"No functions or methods are called on b (except 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 'c."

a : unit -> 'b option
b : 'c
c : 'b

"Foo returns Some(b) in one of the branches, so the return type must be 'c option."

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(c) case, 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 'd, and b : 'd. Wait, I already have b : 'c, that is, b : 'd option. 'd and '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.