Subtype checking of type lambdas with bounds is too restrictive

[sstucki]

This issue was previously reported in a comment to #1252. I'm re-reporting this as requested by @smarter. (The original issue was fixed, but the issue reported in the comment was not).

Given the code

trait A                  { type L[Y <: Int]    >: Int    }
trait B                  { type L[Y <: String] >: String }
trait C extends A with B { type L[Y <: Any]    >: Any    }

The compiler reports

-- Error: ... -------
3 |trait C extends A with B { type L[Y <: Any]    >: Any    }
  |                                ^
  |error overriding type L in trait B with bounds >: [Y <: String] => String <: [Y <: String] => Any;
  |  type L with bounds >: [Y] => Any <: [Y] => Any has incompatible type

The problem is that, when the compiler checks that the bounds of L declared in C conform to those declared in B, it compares the bound annotations of the type-lambdas that form those bounds. But when checking whether two lambdas are subtypes, their bounds need not be compared, as long as both lambdas have a common kind.

Concretely, here we want all the lambdas to have the (wider) kind (Y <: String) -> * which is the declared kind of L in the parent trait B:

[Y <: String] => String  has kind  (Y <: String) -> *
[Y <: String] => Any     has kind  (Y <: String) -> *
[Y] => Any               has kind  (Y <: Any) -> *   sub-kind of  (Y <: String) -> *
[Y] => Any               has kind  (Y <: Any) -> *   sub-kind of  (Y <: String) -> *

so all the bounds are well-kinded and their kinds conform to the signature in the parent class. Then we need to check that the definitions of the lambdas agree in this kind, which they do:

/* Lower bounds are checked contravariantly: */
  String <: Any  forall  Y <: String,  so  [Y <: String] => String <: [Y <: Any   ] => Any
/* Upper bounds are checked covariantly: */
  Any    <: Any  forall  Y <: String,  so  [Y <: Any   ] => Any    <: [Y <: String] => Any

With @smarter and @Blaisorblade, we have discussed two possible fixes:

1. Make subtype checking kind driven: when comparing two lambdas, use the expected bounds from the kind when comparing the bodies. This can be summed up in the following kinded subtyping rule.

   G, X >: L <: U |- T1  <:  T2  ::  K
   G |- [X >: L1 <: U1] => T1  ::  (X >: L <: U) -> K
   G |- [X >: L2 <: U2] => T2  ::  (X >: L <: U) -> K
   -----------------------------------------------------------------------------
   G |- [X >: L1 <: U1] => T1  <:  [X >: L2 <: U2] => T2  ::  (X >: L <: U) -> K
   

   The advantage of this solution is that it's known to be sound (it has been verified at least for a subset of the type system in my thesis). The drawback is that subtype checking would have to be rewritten to take an additional input: expected kind of the types being compared. That would be a major change.

2. Find a compatible, common bound by computing the intersection/union of the bounds in the individual lambdas. As a subtyping rule, this would look as follows.

   G, X >: (L1 | L2) <: (U1 & U2) |- T1  <:  T2
   -----------------------------------------------------
   G |- [X >: L1 <: U1] => T1  <:  [X >: L2 <: U2] => T2
   

   The advantage of this solution is that subtype checking does not have to be redesigned completely, while the drawback is that it requires computing the intersections/unions of higher-kinded types. That can probably be done point-wise (i.e. by pushing intersections/unions into lambdas) but I have not worked out the details nor have I got any sort of soundness proof.

[smarter]

Concretely, here we want all the lambdas to have the (wider) kind (Y <: String) -> * which is the declared kind of L in the parent trait B:

Can you extend this to the case where the upper and lower bounds of L have different kinds ? e.g.:

trait A {
  type L >: [Y <: Any] => Any <: [Y <: String] => Any
}

[sstucki]

Yes, you can. But the two bounds need to have at least the same simple kind, i.e. the same number of arguments. It doesn't work if one bound is, say, Int and the other is a type lambda.

In your example, the common kind could be

[Y <: Any] => Any     :: (Y <: String) -> *
[Y <: String] => Any  :: (Y <: String) -> *

But that's not the only option, e.g. (Y <: Nothing) -> * would work as well.

Whether or not there's always a comon kind depends on how liberal you allow bounds to be. For example, the type lambdas [X >: Nothing <: Nothing] => Any and [X >: Any <: Any] => Any only have a common kind if you allow absurd/empty bounds: (X >: Any <: Nothing) -> *.

Does that answer your question.

[smarter]

Yes, makes sense.

[Blaisorblade]

Concretely, here we want all the lambdas to have the (wider) kind (Y <: String) -> * which is the declared kind of L in the parent trait B:

But in A, L takes Y <: Int. Is that a typo? How should A look like I have further questions related to how A fits in the rest... Should I just remove A everywhere to read your post?

[smarter]

Then we need to check that the definitions of the lambdas agree in this kind

What if the body of one of the lambda is not well-formed under the widened kind ? e.g. given:

class Foo[X >: String]

I may want to check:

[X >: Any] => Nothing <: [X >: String] => Foo[X]

Which according to the second typing rule you give means checking:

G, X >: Any |- Nothing <: Foo[X]

Which doesn't type-check. Given that the compiler only fully check bounds of applications after typechecking is done (I think mostly to avoid completion cycles), that seems problematic.

[smarter]

Wait no, my example is wrong and does type-check, nevermind, it's too late for me to think about this properly :). But maybe you can tell me if the body of the lambdas are always guaranteed to typecheck with the widened kind.

[smarter]

Here's a better example of what I have in mind, given:

trait A {
  type L >: [X] => Nothing <: [X] => Any
  def foo: L[Int]
}

I think your rules allow me to write:

trait B extends A {
  type L = [X <: String] => Any
}

But then the type of foo in B is L[Int] which reduces to ([X <: String] => Any)[Int] which doesn't typecheck, that seems bad to me.

[Blaisorblade]

@smarter

What if the body of one of the lambda is not well-formed under the widened kind ?

That can't happen: a wider lambda-kind gives narrower bounds, which makes more things typecheck (by Liskov substitution principle). So your example would be a problem, but the rules should allow contravariant bound refinement (just like for methods).

So, IIUC, this issue is about allowing the "reverse" of your example, as follows:

trait A {
  type L >: [X <: String] => Nothing <: [X <: String] => Any
  def foo: L[String]
}

trait B extends A {
  type L = [X] => Any // this has kind `(Y <: Any) -> *`, which can be widened to the expected `(Y <: String) -> *`, so this is a valid definition
}

==

In Sandro's example, kind (Y <: String) -> * is wider than (Y <: Any) -> *, because Any is wider than String and function kinds are contravariant (just like function types).
And any lambda body that typechecks in Y <: Any also typechecks in Y <: String (that's part of the LSP — in particular, that should be the narrowing lemma).

To be clear, \forall is contravariant and \lambda isn't. Function types/kinds are contravariant \forall (x: S). T is contravariant, and the kind-level \forall (x <: T) -> K is as well.

[smarter]

I don't get it. The original post says:

G, X >: (L1 | L2) <: (U1 & U2) |- T1  <:  T2
-----------------------------------------------------
G |- [X >: L1 <: U1] => T1  <:  [X >: L2 <: U2] => T2

From this I get [X] => Nothing <: [X <: String] => Any and [X <: String] => Any <: [X] => Any, so #6320 (comment) should compile. What's the step I'm missing exactly ?

[sstucki]

But in A, L takes Y <: Int. Is that a typo? How should A look like I have further questions related to how A fits in the rest... Should I just remove A everywhere to read your post?

No, it's not a typo. But I had the same reaction as @Blaisorblade when copy-pasting the code from the old issue. What follows really only addresses the error reported by the compiler about incompatibility with B.

At first I thought, once the error w.r.t. B is resolved, there should be a similar check for A, which, following the same reasoning, should pass as well. But the common kind for that check would be different. So I'm actually not sure whether the whole example should pass or not. I guess it depends on how mixins work. For example, is it OK to find a common kind for all three declarations of L that isn't the declared kind of L in either A or B? The kind (Y <: Int & String) -> * would work, but it's an upper bound, rather than a lower bound of the kinds of L in A and B, respectively. That's probably not safe. We probably have to "fix" the kind of L in both A and B before performing the check. If we fix it to (Y <: Int & String) -> * in both traits, then everything works out, but if we fix different, incompatible kinds in A and B the code should not pass the typer. Does that make sense?

In fact, I think this is related to @smarter's comment:

From this I get [X] => Nothing <: [X <: String] => Any and [X <: String] => Any <: [X] => Any, so #6320 (comment) should compile. What's the step I'm missing exactly ?

This is very interesting! You may just have found a counter example to the second approach. You're right, the bounds check out, but what is happening is that they only do so in the wider kind that L has in B rather than the kind L has in A. It all makes sense once we make kinds explicit (essentially following the first approach).

In A, the type L has kind (X >: Nothing <: Any) -> * (or * -> * for short). In principle, it could also have kind (X >: Nothing <: String) -> * but then the application L[Int] would be ill-kinded, so we really want it to have the narrower kind * -> * for the entire trait definition to work.

Now in B, the type L suddenly acquires a wider kind (X >: Nothing <: String) -> *. It cannot have kind * -> * because that doesn't fit the upper bound String on X. But then there is a problem: a type member does not get to widen it's kind in a refinement!

So how come solution 2 did not show this? Well, because it automatically finds the narrowest kind that fits both lambdas being compared rather than taking an expected kind as an input. Here, this kind is (X >: Nothing <: String) -> *. The comparison [X <: String] => Any <: [X] => Any only makes sense in (X >: Nothing <: String) -> *, which means the bounds only check if we assume L already had kind (X >: Nothing <: String) -> * in A, which contradicts well-kindedness of L[Int].

I have no clue how this issue with solution 2 could be fixed without passing an expected kind. Any ideas?

[smarter]

I guess it depends on how mixins work.

After typechecking, we'll check that the type definition is within bounds of the definitions in each mixin, one by one.

I have no clue how this issue with solution 2 could be fixed without passing an expected kind. Any ideas?

Nope, I was hoping you'd have some magic solution :)

[smarter]

Going back to solution 1, I'm not sure how being kind-directed would work in practice. How do you decide which kind to use in the first place ?

[sstucki]

I guess it depends on how mixins work.

After typechecking, we'll check that the type definition is within bounds of the definitions in each mixin, one by one.

OK, so there is no linearization order of something? If these checks should be driven by some expected kind from the parent traits, then a common one would have to be found first. For example, one could pick the first one (here A?) and check the second one against it (here, check that the kind of L in B conforms to the kind of L in A). Alternatively try to find the GLB of the kinds of L form both A and B and use that as an upper bound to check the kind of L in C.

What would you do if L was an abstract method rather than an abstract type constructor? I'm sure there's some way to determine the expected type of a method in a mixin composition, no?

I have no clue how this issue with solution 2 could be fixed without passing an expected kind. Any ideas?

Nope, I was hoping you'd have some magic solution :)

One possibility I see is to have a flag in the subtype checker to indicate whether you want to check from above or below. When checking A <: B, the "above" version would assume the common kind to be the kind of the RHS B and the "below" version would use the LHS A to drive checking. This would result in two versions of the rule from solution 2 above: one using the bounds of the LHS when extending the context, and one using the bounds of the RHS. But I'm not sure this could be made to work consistently for the entire subtype checker. E.g. any "rules" that make use of some form of transitivity would result in some sort of narrowing of the implicit expected kind. So this probably wouldn't work.

Going back to solution 1, I'm not sure how being kind-directed would work in practice. How do you decide which kind to use in the first place ?

Well, it depends on where you are performing the subtype check, and it may not be obvious in all situations. But a good rule of thumb would be that you do something similar to what you do when you're using expected types (e.g. for checking definitions). For example, in the above case, you somehow manage to figure out the right type to use when you compare refinements of method signatures. If you have traits

trait A { def foo(x: Int): Any }
trait B { def foo(x: String): Any }
trait C extends A with B { def foo(x: Nothing): Any }

this somehow works out, so you have to find a common "expected type" for foo to check against in C, no?

[sstucki]

this somehow works out, (...)

Whoops, this does not do what I thought it would. I thought that foo in C would be considered a refinement of the abstract methods foo in A and B but apparently they are just overloaded. So type members are treated differently from methods after all, it seems.