Here is the algorithm for overload resolution. It is quite simple. For a set of candidate functions, we will consider only the set of domains D. We also have an argument, with a type A. We have a partial order based on subtyping. In the first step we throw out domains in D for unless d >= A so A is now a subtype of each domain. We now have to pick the most specialised.

We start with an empty set S, which satisfies the invariant that no member of S is greater than any other, and every step will preserve this property. Therefore at the end, if S is empty, there is no matching function, if it has one member, that is the most specialised, and if it has two or more is is ambiguous.

We now consider each element d of D in turn. If d > s, for any domain in S, discard d and try the next element. The invariant is preserved. The candidate d cannot be the most specialised because we found an element s that is a subtype of it.

Now, for every element s in S, if d < s, throw that s out of S, then, add d into S. The invariant is preserved because (a) if there is an element s such that d > s, the first case would have been executed, otherwise, if d < s, the s gets thrown out, so the only remaining possibility is that d is incomparable with every s.

Therefore by induction the invariant is preserved when S is exhausted and the result follows and is proven correct.

In particular, the algorithm depends *only* on a binary relation between types expressing whether a type is a strict subtype of another or not. Given a transitive set of orderings between primitive monomorphic types, and type constructors with known properties such as tuple formation, the algorithm for determining this relation is well known modification of unification. Note in particular it handles both subtyping and subsumption simultaneously (that is a concrete type is a subtype of a type variable also).

It needs to noted that tuple formation is covariant for example, to write the algorithm to include tuples. The key thing here is that none of this can work unless the subtyping relation is a partial order which means it MUST BE TRANSITIVE.

The subtyping rules do not have to agree with the set of implicit conversion. However implicit conversions which are not subtypes will never be invoked (since all type resolution uses the specialisation algorithm) so they might as well be thrown out. On the other hand a subtyping relation MUST be an implicit conversion, because the compiler is going to insert one around the argument of every function call (noting the special case of an exact match will indeed insert the identity as an implicit conversion which can of course be discarded).

There is more than one encoding of the specialisation routine, The one I use is inefficient but it works. I can spell that out if necessary.

Finally: finding the most specialised overload is used in TWO PLACES. The first place is ordinary overloading. The second place is choice of the most specialised implementation of an (CG) interface. Note that this second case is not set up the same way because you are NOT selecting the most specialised function, but the most specialised implementation, which contains multiple functions (because the interface does). The specialisation algorithm is the same, but the candidates are the implementation specialisations of the interface (not the domains of functions).