Overload resolution and inline tricks puzzler

overloads-solution.fsx

type Term<'a>() = class end

let termint = Term<int>()
let termint2 = Term<int>(), Term<int>()

type Tuples = Tuples with
    static member Eq(a:Term<'a>,a':Term<'a>) = 0
    static member Eq((a:Term<'a>,b:Term<'b>), (c:Term<'a>, d:Term<'b>)) = 2
    static member Eq(a:bool, b:bool) = 3
    //this overload is apparantely crucial: see kvb's comment on Gustavo's answer here:http://stackoverflow.com/questions/2812084/overload-operator-in-f
    static member Eq(Tuples, Tuples) = 4

let e1 = Tuples.Eq(termint,termint)
let e2 = Tuples.Eq(termint2,termint2)
let e3 = Tuples.Eq(true, false)

let inline call_2< ^t,^a when (^t or ^a): (static member Eq: ^a * ^a -> int)> (a:^a,b:^a) : int = 
    ((^t or ^a):(static member Eq: ^a * ^a -> int)(a,b))

let t = call_2<Tuples,_> (termint,termint)
let t2 = call_2<Tuples,_> (termint2, termint2)
let t3 = call_2<Tuples,_> (true, false)

let inline call a b =
    call_2<Tuples,_> (a, b) //a unique overload for Eq could not be determined

let tt = call termint termint
let tt2 = call termint2 termint2
let tt3 = call true false

overloads.fsx

type Term<'a>() = class end

type Tuples = Tuples with
    static member Eq(Tuples, a:Term<'a>, a':Term<'a>) = 0
    static member Eq(Tuples, (a:Term<'a>,b:Term<'b>),(c:Term<'a>, d:Term<'b>)) = 2
    //without this overload, t and t2 below work but t3 doesn't (of course). With this, only t3 works...?
    //and the type of call_2 is specialized to bool.
    //static member Eq(Tuples, a:bool, b:bool) = 3

let inline call_2 (t:^t,a:^a,b:^a) : int = ((^t):(static member Eq: _ * _ * _ -> int)(t,a,b)) 

let t = call_2 (Tuples,Term<int>(),Term<int>())
let t2 = call_2 (Tuples,(Term<int>(),Term<int>()),(Term<int>(),Term<int>()))
let t3 = call_2 (Tuples, true, false)

//also, this doesn't work, even without the bool:
let inline call a b : int =
    call_2 (Tuples, a, b) //a unique overload for Eq could not be determined
    

just change it to this:

type Tuples = Tuples with
    static member Eq(_, a:Term<'a>, a':Term<'a>) = 0
    static member Eq(_, (a:Term<'a>,b:Term<'b>),(c:Term<'a>, d:Term<'b>)) = 2
    //without this overload, t and t2 below work but t3 doesn't (of course). With this, only t3 works...?
    //and the type of call_2 is specialized to bool.
    static member Eq(_, a:bool, b:bool) = 3

this should work (at least for the first part of your problem)

That's nice, and also puzzling. Why? :) I just can't seem to build a correct intuition for how this works...