The current rule for when an is-expression 'shows a type' uses subtyping to ensure that we always promote to a type that holds atleast the same information as the current type (in order to hold all type information through a single type).

This breaks down due the fact that subtyping is not a partial order. For instance:

class A { aMethod() {} }
class B { bMethod() {} }

List<A> list = ...
if (list is List) { // ok since List <: List<A>
  if (list is List<B>) { // ok since List<B> <: List
    list[0].aMethod(); // warning, since operator[] on List<B> returns a B
  }
}

We need to use the more specific relation (<< defined in §15.4) as the criterion for showing the type of an is-expression. In the example this will make the promotion from List<A> to List invalid and thus retain the information that 'list[0]' returns an A.

Currently the more specific relation is not defined on function types and void, so this needs to be added.

I propose that a function type T is more specific that Function, and more specific than another function type S if T is a subtype S, the return type of T is more specific than the return type of S (covariance), and that all parameter types of T are less specific that the corresponding parameter types of S, if any, (contravariance).

For void, I propose that we only have void << void to avoid any promotion that changes the known return type of a function to or from void.