F# recursive type: method vs function type inference differences

Question

Can someone explain please why in F# type-inference seems to work differently (or some other aspect I don't understand?) between class methods and functions.

Imagine the following (simplified):

type Node<'T> = Node2 of 'T * 'T
type Digit<'T> = One of 'T | Two of 'T * 'T
type Tree<'T> =
    | Empty
    | Single of 'T
    | Deep of prefix : Digit<'T> * deeper : Tree<Node<'T>>
    with
    static member Add (value : 'T) (tree : Tree<'T>) : Tree<'T> =
        match tree with
        | Empty -> Single value
        | Single a -> Deep (One value, Empty)
        | Deep (One a, deeper) -> Deep (Two (value, a), deeper)
        | Deep (Two (b, a), deeper) -> Deep (One value, deeper |> Tree.Add (Node2 (b, a)))

let rec add (value : 'T) (tree : Tree<'T>) : Tree<'T> =
    match tree with
    | Empty -> Single value
    | Single a -> Deep (One value, Empty)
    | Deep (One a, deeper) -> Deep (Two (value, a), deeper)
    | Deep (Two (b, a), deeper) -> Deep (One value, deeper |> add (Node2 (b, a)))

Note that static method Add and function add have identical implementation and both call itself recursively.

Yet former compiles fine but latter report an error:

Type mismatch. Expecting a
    Tree<Node<'T>> -> Tree<Node<'T>>    
but given a
    Tree<'T> -> Tree<'T>    
The resulting type would be infinite when unifying ''T' and 'Node<'T>'

Answer 1

In the free floating function add, the generic type parameter belongs to the function itself (add<'T>).

However, in the static member function, the type parameter actually belongs to the class (Tree<'T>).

Why does this matter? Because when you refer to the function itself, the compiler assumes that the type parameter is unchanged unless otherwise specified. It won't guess a different one, because that could hide a huge category of type mismatch errors.

However, it doesn't make the same assumption for the type to which the function belongs.

If you check the parameters, the call to add is assumed to be a call to add<'T>, which causes an infinite generic recursion and doesn't compile.

But, the call to Tree.Add is inferred to be a call to Tree<Node<'T>>.Add, not to Tree<'T>.Add. It's a different function call altogether.

If you explicitly annotate the type:

static member Add (value : 'T) (tree : Tree<'T>) : Tree<'T> =
    // ...
    | Deep (Two (b, a), deeper) -> Deep (One value, deeper |> Tree<'T>.Add (Node2 (b, a)))

you will get the exact same type mismatch / infinite type error as on the free function.

Likewise you get the error if you make it an instance member and refer to the same instance:

member this.Add (value : 'T) (tree : Tree<'T>) : Tree<'T> =
    // ...
    | Deep (Two (b, a), deeper) -> Deep (One value, deeper |> this.Add (Node2 (b, a)))

Vice-versa, you can make the free function compile by annotating the type parameter, so that the compiler will not assume "it's the same symbol, so must refer to the same value":

let rec add<'T> (value : 'T) (tree : Tree<'T>) : Tree<'T> =
    // ...
    | Deep (Two (b, a), deeper) -> Deep (One value, deeper |> add (Node2 (b, a)))