Type projection proposal

projection-proposal.md

NOTE: This is a sketch of the proposal, many details need to be filled out and the scheme hasn't been implemented yet.

G |- T <: S
--------------------
G |- T#L <: S#L

------------------------------
G |- {L: X..Y, ...}#L <: Y

------------------------------
G |- Y <: {L: X..Y, ...}#L

The original motivation for these rules is that given this:

trait C {
  type Elem <: AnyRef
}
trait D extends C {
  type Elem = String
}

In dotty we currently have:

String <:< D#Elem
D#Elem <:< C#Elem

but we don't have:

String <:< C#Elem

but this is incoherent if we assume transitivity as we do in DOT. With my scheme we have:

C#Elem =:= AnyRef
D#Elem =:= String

so we don't have any issue with transitivity. In this scheme, the intuitive interpretation of C#Elem is "The set of all types that can be passed as a parameter to a method accepting a parameter Elem in all possible subclasses of C".

The secondary motivation for this scheme is that it simplifies the implementation of type-lambdas in Dotty, from https://gist.github.com/odersky/92a0c9bcbdb8ff39c93d :

 1. `$Apply` refinements are covariant. If `T <: U` then

        S { type $Apply = T }  <:  S { type $Apply = U }

    This subtyping relationship does not hold for ordinary type refinements.
    It would hold for upper bound refinements, of course. But we cannot
    model `$Apply` refinements as upper bound refinements because that would
    lose beta reduction.

$Apply is a covariant type alias, I believe that this is unsound, though I haven't been able to prove it, but with my scheme we could simply write:

S { type $Apply <: U }

and beta-reduction still works.

I explored a system that included these subtyping rules

Hi @adriaanm! I'll be sure to take a closer look at Scalina, however the rules you describe seem different from what I propose: in my system, T#L is both a subtype and a supertype of the upper bound of the abstract type L, I believe that this simplify the type system, and has no significant impact on practical uses of type projections.

@smarter -- in your proposal, how would you prevent the compiler from accepting id1 implemented as the identity function:

object hk extends App {
  def id1[M1[_], M2[_]](x: M1[Any]): M2[Any] = ??? // x
  type M1[T] = Any
  type M2[T] = Nothing
  def id2(x: Any): Nothing = id1[M1,M2](x)
}

It seems to me that we need to use the lower bound of M2[Any] (Nothing) to prevent casting from an arbitrary M1[Any] to M2[Any] or am I missing something?