Fix subtyping to match DOT rule TDECL-<:

[smarter]

This is based on my understanding of the DOT rules but could be completely wrong/not what we want, feedback welcome.

Review by @odersky @DarkDimius @namin .

[samuelgruetter]

I'm a bit confused, do you really mean this rule?

 G |- S' <: S    G |- T <: T'
------------------------------- (TDECL-<:)
 G |- (L: S..T) <: (L: S'..T')

I can't relate it to the proposed changes, could you please elaborate a bit?

[smarter]

Maybe I'm misinterpreting that rule or the DOT calculus in general, but to me it implies that if:

val a = new Top { z => type T : S'..T' } {};
val b = new Top { z => type T : S..T } {};

Then if S' <: S and T <: T':

(b.T: S..T) <: (a.T: S'..T')

Which I translate in dotty as test_tdecl_lt_colon: https://github.com/lampepfl/dotty/pull/181/files#diff-15bd40012c5ac4213ccb9b567dc3957eR20

[samuelgruetter]

I think you're misinterpreting that rule. Here's my attempt to clarity: L stands only for a type label, something like a string, i.e. just a name, and you cannot substitute b.T for it. Moreover, when we write (L: S..T), the : has nothing to do with the : in type assignment judgments G |- t : T. (L: S..T) is just a way of expressing a "data structure" which contains a type declaration. In Scala, the equivalent would be type L >: S <: T.
Does that make sense?

[smarter]

Alright, I think I get it, the fact that A <: B and a: A, b: B does not imply that a.T <: b.T even if the declaration of T in A subsumes the declaration of T in B, and I now understand why Martin had reservations about A#T <: B#T in #179 .

[samuelgruetter]

Yes, exactly.