Experiment: Replace type application encoding with native AppliedType

[odersky]

This is an experiment to replace the encoding of type applications in terms of type members by native AppliedTypes.

Arguments for keeping the existing encoding:

• It's close to DOT, giving a semantics of type applications in terms of proven foundations
• It gives a natural and simple meaning to wildcard arguments, e.g. List[_].

Arguments for changing to native applications:

• It's probably easier to understand in the compiler, since it is closer to source syntax.
• It's easier to give good error messages.
• It might avoid some cyclic reference errors.
• It might be faster, since types are smaller and there's less back-and-forth encoding.

I believe keeping the DOT scheme would be overall simpler if it was not for higher-kinded types. Higher-kinded types force us to introduce Application nodes anyway, so maybe the overall implementation effort is simpler if we just generalize this to all types. We have to figure out how to best represent wildcard arguments, though. The purpose of this experiment is to do this, and then to evaluate implementation complexity and compiler performance.

[liufengyun]

If I understand well, the difficulty with wildcard is the following, which type checks with current dotc but not in scalac nor java:

class Option[T](var t: T) {
  def foo = {
    val opt: Option[_] = new Option[String]("")
    opt.t = opt.t
  }
}

[liufengyun]

I was thinking about how native application can achieve the same for wildcards based on existential types. Here are some tentative thoughts:

Auto Packing. If the expected type has underscores, instantiate the underscores with fresh type variables with the bounds as check condition, type check the given term with the new expected type. Type checking succeeds only if the type variables are instantiated and the instantiation satisfies the check condition.

Auto Unpacking. When type checking a variable definition of a type with underscores, always define fresh type parameters in the same scope with the same bounds as the underscores, then type all references to the variable as the type instantiated by the type parameters.

Auto Instantiation. If the synthesized type of a term has underscores, introduce fresh type parameters for those underscores in the enclosing method and instantiate the type of the term with the type parameters.

By type parameters, I mean the abstract type T like the follows:

 def foo: Option[_ <: Int] = {
    type T <: Int                                       // <= inserted type parameter for `x`
    val x: Option[_ <: Int] = Some(5)
    x                                                   // usage of `x` gets the type: Option[T]
 }

The rule Auto Instantiation is inspired by Wild FJ[1, Section 3.1] which make the type parameters global instead of being in the enclosing method as an approximation.

There's also subtle interaction with mutable vars as in the encoding (#2928).

[1] Wild FJ, Torgersen et. al., 2005

Edited: updated Auto Instantiation to introduce type parameters in the enclosing method as an approximation.

[odersky]

@liufengyun Yes, this looks much like what we use skolemization for, and how scalac treats existential types. But details get very tricky. Happy to discuss over lunch/coffee.

[odersky]

Closed for the reasons given in #2947