Fixed #264 - failure to typecheck GADTs

[odersky]

The previous scheme derived the right bounds, but then failed to use them
because a TypeRef already has a set info (its bounds). Changing the bounds in
the symbol by a side effect does not affect that. This is good! But it showed
that the previous scheme was too fragile because it used a sneaky side effect
when updating the symbol info which failed to propgate into the cached
info in TypeRef.

We now keep GADT computed bounds separate form the symbol info
in a map gadt in the current context.

Closes #268. (Branch got wrong ticket number due to a typo).

[odersky]

Who would like to review this?

[retronym]

@Blaisorblade's investigations into the limitations of scalac's GADT support might be worth a look while you're thinking about this.

In the comments, I minimized the problem to:

package bugreport

object BugReport {
  trait Type {
    type DT <: Type
  }

  trait BaseInt extends Type {
    type DT = BaseInt
  }

  trait Exp[TP <: Type]

  class Num extends Exp[BaseInt]

  def derive[T <: Type](term: Exp[T]): Any = {

    val res1 = term match { case _: Num => (??? : Exp[T#DT]) }
    res1: Exp[T#DT] // fails, the prefix of the type projection in the case body underwent unwanted GADT refinement

    type X = T#DT
    val res2 = term match { case _: Num => (??? : Exp[X]) }
    res2: Exp[T#DT] // works
  }
}

That fails in scalac with:

% scalac-hash v2.11.4 sandbox/test.scala
sandbox/test.scala:37: error: type mismatch;
 found   : bugreport.BugReport.Exp[bugreport.BugReport.BaseInt]
 required: bugreport.BugReport.Exp[T#DT]
        a //fails
        ^
one error found

But is allowed in dotc as of this PR.

However, the main example in that Gist fails in both compilers (albeit with different error messages)

% scalac-hash v2.11.4 sandbox/test.scala
sandbox/test.scala:37: error: type mismatch;
 found   : bugreport.BugReport.Exp[bugreport.BugReport.BaseInt]
 required: bugreport.BugReport.Exp[T#DT]
        a //fails
        ^
one error found

% ./bin/dotc sandbox/test.scala
sandbox/test.scala:20: error: Exp.this.T is not a valid prefix for '# DT'
    def derive: Exp[T#DT]
                    ^
sandbox/test.scala:30: error: T is not a valid prefix for '# DT'
  def derive[T <: Type](term: Exp[T]): Exp[T#DT] =
                                           ^
sandbox/test.scala:33: error: T is not a valid prefix for '# DT'
        val a = Num(n): Exp[T#DT]
                            ^
sandbox/test.scala:33: error: type mismatch:
 found   : bugreport.BugReport.Num
 required: bugreport.BugReport.Exp[T#DT]
        val a = Num(n): Exp[T#DT]
                   ^
four errors found

[retronym]

In the process of playing around with that test case, I discovered a dotc crasher.

trait Type {
  type DT
}

trait Exp[type T <: Type] {
  def derive: Exp[T#DT]
}

Fails with:

findMember exception for  = ...:  = ... member DT
...
assertion failure for ... <:< ?{ DT: ? }, frozen = false
typeref ... found in trait Exp
?{ DT: ? } is a class dotty.tools.dotc.typer.ProtoTypes$CachedSelectionProto
exception occured while typechecking sandbox/test.scala
Exception in thread "main" java.lang.AssertionError: assertion failed
       ....
    at dotty.tools.dotc.core.Denotations$Denotation.findMember(Denotations.scala:164)
    at dotty.tools.dotc.core.Types$Type.go$1(Types.scala:417)
    at dotty.tools.dotc.core.Types$Type.findMember(Types.scala:465)
    at dotty.tools.dotc.core.Denotations$Denotation.findMember(Denotations.scala:164)
    at dotty.tools.dotc.core.Types$Type.go$1(Types.scala:417)
    at dotty.tools.dotc.core.Types$Type.findMember(Types.scala:465)
    at dotty.tools.dotc.core.Denotations$Denotation.findMember(Denotations.scala:164)
    at dotty.tools.dotc.core.Types$Type.go$1(Types.scala:417)
    at dotty.tools.dotc.core.Types$Type.findMember(Types.scala:465)
    at dotty.tools.dotc.core.Denotations$Denotation.findMember(Denotations.scala:164)
    at dotty.tools.dotc.core.Types$Type.go$1(Types.scala:417)
    at dotty.tools.dotc.core.Types$Type.findMember(Types.scala:465)
    at dotty.tools.dotc.core.Types$Type$$anonfun$member$1.apply(Types.scala:395)
    at dotty.tools.dotc.core.Types$Type$$anonfun$member$1.apply(Types.scala:395)
    at dotty.tools.dotc.util.Stats$.track(Stats.scala:35)
    at dotty.tools.dotc.core.Types$Type.member(Types.scala:394)
    at dotty.tools.dotc.typer.ProtoTypes$SelectionProto.isMatchedBy(ProtoTypes.scala:95)
    at dotty.tools.dotc.core.TypeComparer.isMatchedByProto(TypeComparer.scala:893)
    at dotty.tools.dotc.core.TypeComparer.firstTry(TypeComparer.scala:487)
        ...

[retronym]

This encaspulates the ability to assign a new map, but leaves the door open for anyone to mutate GADTMap#bounds.

I'd prefer to see something like:

class GADTMap {
  private var bounds = new SimpleMap
  def narrowBounds(sym: Symbol, bounds: TypeBounds): Unit = {
    bounds = bounds.updated(symbol, bounds)
  }
  def apply(sym: Symbol): TypeBounds = bounds(sym)
}

[odersky]

regarding @Blaisorblade's gist, I think the errors reported by dotc are intentional. We are stricter than scalac when checking legal projections. scalac converts them to existentials, which dotc does not have.

[Blaisorblade]

Hi, thanks for the mention!

We are stricter than scalac when checking legal projections.

Is the new criterion explained somewhere? That sentence makes vaguely sense to me, since ML modules are even more restrictive — though I don't fully remember why. Is that projection volatile without desugaring?

scalac converts them to existentials, which dotc does not have.

As in, T#DT used to become t.DT forSome { val t: T } which is now forbidden?
If that's the only problem, maybe passing a value would work:

  def derive(t: Type)(term: Exp[t.type]): Exp[t.DT] =
    term match {
      case Num(n) => Num(n)
        //val a = Num(n): Exp[v.DT]
        //a
    }
  object BaseInt extends BaseType[Int] { // this was a sealed trait with no children, but no more!
    type DT = BaseInt
  }

so we'd be able to wouldn't limit expressiveness much. As you probably remember, I'd like to make t implicit there:

  def derive[[t: Type]](term: Exp[t.type]): Exp[t.DT] =

so we wouldn't create boilerplate, but that's a separate issue. (BTW, in the Agda version one would have t inferred by unification rather than implicit search, with a different kind of implicit — I'm not sure if conflating the two would actually work).

[odersky]

The explanation of the restriction is in Typer.scala:

/** A type T is a legal prefix in a type selection T#A if
 *  T is stable or T contains no abstract types except possibly A.
 *  Todo: What about non-final vals that contain abstract types?
 */
final def isLegalPrefixFor(selector: Name)(implicit ctx: Context): Boolean =
  isStable || {
    val absTypeNames = memberNames(abstractTypeNameFilter)
    if (absTypeNames.nonEmpty) typr.println(s"abstract type members of ${this.showWithUnderlying()}: $absTypeNames")
    absTypeNames.isEmpty ||
      absTypeNames.head == selector && absTypeNames.tail.isEmpty
  }

It's one of the spots where I am not sure yet what to do because the theory is not worked out. Motivation: We definitely need to support A # B for classes A, B because that's what Java's inner classes are. We also need to support T # X for a single abstract type X because that's the encoding of an instantiated higher-kinded type.E.g.

Rep[String]

for abstract Rep gets encoded as something like:

type Rep = Lambda { type Apply; type hk$Arg$0 }
Rep { type hk$arg$0 = String } # Apply

The idea is to regard a type T # X as a skolem, similar to a path dependent type p.T. So the only info we have about the type are the bounds of X. But unlike an existential it is a first-class type, which does not need to be packed/unpacked.

It's easy to show that this is unsound if T contains abstract types besides X: Just mix two different implementations of these abstract types. But if X is the only abstract type member, nobody could shoot holes in this so far. Nevertheless it would be important to work out the theory of this, and if necessary revise. So the current status is just a snapshot.

[odersky]

The crasher exercises named type parameters, which are not really supported yet. I'll move a test into pending so that we remember to come back to it.