This problem manifest when a RULE calls method f.foo(a,b) where f is know to be of type Foo extends Bar. The problem is that when type checking the call to foo the type checker may use the parameter types of Foo.foo to infer a type for expression a and b. This can lead to type errors when the call matches a signature for an inherite dversion of foo.

Assume Foo declares X Foo.foo(A, C) while Bar declares Y Bar.foo(A, B) where B anc C are unrelated types i.e. not C < B and not B < C. The type checker identifes that there is only one cadidate implementation for foo on Foo, i.e. foo(A,C). So, it tries to type check a as an A and b as a C and gets a type check error from b.typeCheck(C). What it should do is collect all candidates first so it can identify the potential ambiguity of foo(A, B) and foo(A, C). It should then typecheck a against A and b against UNDEFINED. If b can be unambiguously be resolved as a B then this will rule out the subclass implementation foo(A, C) as a candidate leaving the parent method foo(A,B) as the only candidate.

The tricky part is to deal with overriding i.e. the type checker must ensure that when we have X Foo.foo(A, B) and X Bar.foo(A, B) it selects Foo.foo(A, B) as the unique candidate.