Type inference wants explicit upcast sometimes even when flexible type is used for interface constraints?

Question

I had expected that flexible type would minimize the need of explicit upcast, but

type IB =
    abstract B : int

type A() =
    interface IB with
        member this.B = 1

let a = A()

let test (x) = x

let aa = [|a; a|]
let case1 = aa |> Array.map (fun (x: #IB) -> test (x.B))
let case2 = Array.map (fun (x: #IB) -> test (x.B)) aa

Here, there are warnings (less generic than type annotation) on the last 2 lines. The compiler is able to compile case2, but fails at case1, why is that?

It feels odd that the more detailed the compiler can infer, the more code I need to write.

@kvb pointed out there is a simple fix, just to refactor the lambda function into a non inline version.

let fix (x: #IB) =
    test x.B

let case1 = aa |> Array.map fix
let case2 = Array.map fix

This works well.

kvb kvb · Accepted Answer · 2014-10-12T19:40:07

Type inference in F# flows from left to right, so it's not too surprising that piping can break or fix things. However, it's almost always the case that having more type information earlier is helpful, so this result is a bit surprising. The warnings are a subtle indicator that you're doing something wrong. Flexible types seem like they ought to be applicable in many tricky situations, but there are really only a few places where they help. Array.map takes a function of some type 'a -> 'b for some particular 'a and 'b (though there's a little bit of nuance here, since the "particular" types could be type variables), so having a "more generic" argument like #IB -> int is not especially helpful; the compiler will pick some particular subtype of IB during compilation - this is what the warnings are attempting to communicate.

As I said, the different results you see on the different lines are due to the fact that type inference in F# works left to right. In the first case, the information about the type of aa flows into the type checking of the remainder of the expression and so when compiling the lambda the compiler knows that the only possible subtype of IB that will work is A, but because interface implementations are always implicit this causes a compile time error because A doesn't have a publicly available member B. On the other hand, in the second case, when the compiler's trying to check Array.map it doesn't yet know the type of the array it will be applied to, but can check the call in any case because regardless of the subtype it will support the interface method IB.B (implicitly upcasting the argument from whatever subtype of IB it has to just IB). Then when this is applied to aa the compiler specializes the implementation to A, but because of the implicit upcast this still works okay. Intuitively, it seems like the compiler ought to have been able to have inserted the same implicit upcast in the former case, but I think this is probably just a surprising result of the inference algorithm and not an actual bug.

Perhaps more surprising, one possible fix is to just use a let-bound definition (for either the lambda or even as a type-restricted version of Array.map) and skip the flexible type:

let f (x:IB) = test (x.B)
let g (f:IB -> int) = Array.map f
let d' = aa |> g (fun x -> test (x.B))
let d'' = aa |> Array.map f
let c' = g (fun x -> test (x.B)) aa
let c'' = Array.map f aa

So what's happening here? It turns out the compiler does something called "Implicit Insertion of Flexibility for Uses of Functions and Members" (section 14.4.3 of the spec for F# 3.1) which does exactly what you want.

Type inference wants explicit upcast sometimes even when flexible type is used for interface constraints?

2 Answers