more specific method inference

[Rafkind, Jon]

I don't quite understand how more specific method inference (18.5.4) is
supposed to work. Given these functions

<Q extends Integer> void f(Q q){}
<K extends Number> void f(K k){}

f(12) // will call Integer

I'm assuming for the moment that determining which function to choose
requires the logic of 18.5.4, and if so I don't see how treating the
type parameters of m1 as type variables allows reduction to take place.

Using the terminology from 18.5.4:

let m1 = <Q extends Integer> void f(Q q)
let m2 = <K extends Number> void f(K k)

S1 = Q
P1 = K
theta = [K:=a1]
T1 = a1
B = [a1 <: Number]

S1 is a proper type (Q) but T1 is not (a1), so generate the constraint
{Q <: a1}.

B' = reduce({Q <: a1}, B)

{Q <: a1} is reduced to the bound (S <: a1).

B' = incorporate((S <: a1), [a1 <: Number])
= S <: Number

And thats all. Technically B' is not false so I suppose the logic
'worked', but if m1 and m2 were reversed (so m1 = Number and m2 =
Integer) then we would have selected the method that uses Number as a
bound to be more specific. Also 'Integer' is no where in sight during
the process.

If S was simply replaced by an inference variable and a bound created
using Integer then it seems to work out.

S1 = Q
P1 = K
theta1 = [Q := a1]
theta2 = [K := b1]
# R1 is theta1 applied to S1
R1 = a1
T1 := b1
B = [a1 <: Integer, b1 <: Number]
B' = reduce({a1 <: b1}, B)
B' = incorporate((a1 <: b1), B)
B' = [a1 <: b1, a1 <: Number, a1 <: Integer, b1 <: Number]

resolve(B') =
  T1 = a1, T2 = b1
  T1 = glb(Number, Integer) = Number
  T2 = glb(Number) = Number
  incorporate([T1, T2], B) = {Number <: Number} reduces to true

And if m1/m2 were switched then you would eventually have (a1 <: b1, a1
<: Number, b1 <: Integer), which reduces to false. But 18.5.4 clearly says

  "Note that no substitution is applied to S1, ..., Sk; even if m1 is
generic, the type parameters of m1 are treated as type variables, not
inference variables."

----
I wonder about the point of all of this in the first place. If we just
instantiate the functions with their bounds and compare them as normal
it seems to have the same result.

<Q extends Integer> void f(Q q)
<K extends Number> void f(K k)

instantiate to

void f(Integer q)
void f(Number k)

But maybe inference matters for poly expressions.. If so, would it be
fair to say something like 'if none of exp1...expk contain a poly
expression then it is safe to instantiate both methods with their type
bounds and compare them as normal' ?