Fix #4880: always instantiate prefix tvar

[liufengyun]

Fix #4880: always instantiate prefix tvar

[Blaisorblade]

Why a backquoted eq here (or elsewhere for that matter)?

[liufengyun]

I should use it in both cases, just following a coding style experimented by Martin in Dotty.

[Blaisorblade]

So I've pushed a couple of examples, and a patch for them I'm not happy about. Below's why.

Enabling Printers.exhaustivity reveals that ZipArchive#Entry decomposes to [], which is not correct. Varying the example a bit demonstrates an incorrect warning:

sealed abstract class AbstractFile
class PlainFile(path: String) extends AbstractFile
class VirtualFile(name: String) extends AbstractFile
abstract class ZipArchive(path: String) extends AbstractFile {
  sealed abstract class Entry(name: String) extends VirtualFile(name)
  class DirEntry(path: String) extends Entry(path)
}

object Test {
  def foo(file: AbstractFile) =  file match {
    case a: PlainFile =>
    case b: ZipArchive =>
    case c1: ZipArchive#Entry => // marked as unreachable, incorrectly!
    case c1: ZipArchive#DirEntry => // accepted, correctly, even tho this is the instance of ZipArchive#Entry
    case c: VirtualFile =>
  }
}

Analysis

Once instantiate finds that ?X#DirEntry can be an instance of ZipArchive#Entry, it must pick ?X. The new code maximizes it to Nothing, but then we get Nothing#DirEntry inhabited? false. The old code turns ?X#DirEntry into WildcardType. Neither's correct.

I can add a special case for inhabited(TypeRef(Nothing, member)) = true, and that passes tests, but I'm not very happy with it — we'd risk running again into 3574 if, say, intersections were smarter.

I suspect we should produce something else instead of Nothing#DirEntry: I'll look into that next.

Space.instantiate: protoTp1((param)9#DirEntry) <:< tp2(ZipArchive#Entry) = true
Space.instantiate: isFullyDefined((param)9#DirEntry) = false
`Nothing#DirEntry inhabited?  false`

[Blaisorblade]

A better way of handling the new examples is needed.

[Blaisorblade]

Also, have you already tried using asSeenFrom on the parents instead of RemoveThisMap? Because I'm taking a look at that.

EDIT: forcing isFullyDefined to maximize rather than minimize indeterminate type variables was enough. I gave up on asSeenFrom, for me this is sensible but too hard, and the intersection/type inference seems to be taking care of that.

Why is maximizing correct?

The difference between this testcase and others seems the following. We're replacing ThisType(tref) with a new prefix type, because tref is only valid at the child class definition site. Elsewhere, we can infer that prefix type from the scrutinee, while here the only prefix is tref, which we use as the type variable upper bound. So we should default to the upper bound, that is maximize. Since we always use the upper bound (and we should), we must maximize irrespective of variance.

EDIT2: looking into the failure, I suspect I should only maximize the prefix type variable, and not even force the other ones. I'll give this a try.

[liufengyun]

@Blaisorblade The following change works for me locally:

+++ b/compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
@@ -292,7 +292,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
   private val nullType             = ConstantType(Constant(null))
   private val nullSpace            = Typ(nullType)

   override def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type) = {
     val and = AndType(tp1, tp2)
     // Precondition: !(tp1 <:< tp2) && !(tp2 <:< tp1)
     // Then, no leaf of the and-type tree `and` is a subtype of `and`.
@@ -689,7 +689,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
       tvar =>
         !(ctx.typerState.constraint.entry(tvar.origin) `eq` tvar.origin.underlying) ||
         (tvar `eq` removeThisType.prefixTVar),
-      minimizeAll = false
+      minimizeAll = false,
+      allowBottom = false
     )
--- a/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inferencing.scala
@@ -115,7 +115,7 @@ object Inferencing {
             val minimize =
               force.minimizeAll ||
               variance >= 0 && !(
-                force == ForceDegree.noBottom &&
+                !force.allowBottom &&
                 defn.isBottomType(ctx.typeComparer.approximation(tvar.origin, fromBelow = true)))
             if (minimize) instantiate(tvar, fromBelow = true)
             else toMaximize = true
@@ -466,9 +466,9 @@ trait Inferencing { this: Typer =>

 /** An enumeration controlling the degree of forcing in "is-dully-defined" checks. */
 @sharable object ForceDegree {
-  class Value(val appliesTo: TypeVar => Boolean, val minimizeAll: Boolean)
+  class Value(val appliesTo: TypeVar => Boolean, val minimizeAll: Boolean, val allowBottom: Boolean = true)
   val none = new Value(_ => false, minimizeAll = false)
   val all = new Value(_ => true, minimizeAll = false)
-  val noBottom = new Value(_ => true, minimizeAll = false)
+  val noBottom = new Value(_ => true, minimizeAll = false, allowBottom = false)
 }

If you play with reachability, you may want to incorperate the changes in #4869.

[Blaisorblade]

Feel free to push your change.
Meanwhile, WIP idea: what I wanted to do with asSeenFrom is to actually use the notion of base types as defined here (and I think implemented in the compiler somewhere):
https://www.scala-lang.org/files/archive/spec/2.13/03-types.html#base-types-and-member-definitions. But that should be a separate change, if it works at all.

[Blaisorblade]

LGTM! This looks reasonable to me, and I'm pretty confident the changes to Inferencing are just a refactor for all other users, so they're safe.

Plus, my idea about baseTypes doesn't work as-is for two reasons: first, we need to find children and not parents, and second because (as @liufengyun pointed out) there might be no prefix (just like when GADT pattern match uses unification, it might find no solution).