@darksnake I did some investigation on how the Kotlin compiler resolves extension functions and I have come to the conclusion that your take on how extension function should resolve is closer to how the compiler works than mine.
However, I would make some changes because,
 The
G
in your example doesn’t appear necessary as the global scope (file level scope) is never passed as a parameter so doesn’t need to be in the list of contexts.
 The normalization step seems unnecessary as it would fall out in resolution. Also the distinction between “compiler types” is unnecessary as the compiler only deals with compiler types and Java types for example is a platform mapping.
 The compiler refers to what you call a context as an implicit receiver so we should switch to this vernacular to avoid confusion.
I would then recast your steps to the following,

Create an ordered list of implicit receivers This already exists in the compiler as the ImplicitScopeTower

Checking given an extension function with receivers T^{1}
…T^{n}
and a receiver scope type of R
and implicit receiver scopes in the scope tower of I^{1}
…I^{m}
an extension is valid if R
:> T^{n}
and there exists some permutation of (T^{i}
, I^{j}
) in i
1
…n1
and j
in 1
…m
where I^{j}
:> T^{i}
and for each element in the permutation all i
and j
values are in increasing order. If multiple valid permutations are possible then the last permutation is selected when the permutations are ordered by the values of i
and j
.

Report ambiguous calls If multiple valid candidates are possible the call is ambiguous and an error is reported.
For example, a declaration fun [A, B, C].foo()
would have a receiver type list with three elements T^{1}
= A
, T^{2}
= B
and T^{3}
= C
. For the following invocation of foo
.
class A {}
class B {}
class C {}
fun [A, B, C].foo() {}
fun t(a: A, b: B, c: C) {
with (a) {
with (b) {
c.foo()
}
}
}
It would have an implicit scope tower of a, b
with I^{1}
= A
and I^{2}
= B
. The R
would be C
and is valid because C
:> C
. The permutation receivers [(T^{1}
, I^{1}
), (T^{2}
,I^{2}
)] which is valid as A
:> A
and B
:> B
.
This is compatible with the current semantics as the current semantics are the above without the permutation of the remaining receivers with the implicit scope tower as n
is always 1 which results in a valid empty permutation [ ].
This can be done fairly efficiently if the permutations are produced by pairing T^{n1}
to some I^{j}
and then pairing T^{n2}
to some I^{k}
where k
< j
until a valid permutation is found. The first valid pairing found will be the last permutation given the ordering described above. This can be accomplished in worst case O(n*m) steps.
One thing to consider is whether the ordering of j
is strictly necessary. That is would the following permutation be valid [(T^{1}
, I^{2}
), (T^{2}
,I^{1}
)] which is what you would get for,
fun t(a: A, b: B, c: C) {
with (b) {
with (a) {
c.foo()
}
}
}