Test recheck in CompilationTests

Author: odersky

compiler/src/dotty/tools/dotc/Compiler.scala

@@ -99,6 +99,8 @@ class Compiler {
          new TupleOptimizations,     // Optimize generic operations on tuples
          new LetOverApply,           // Lift blocks from receivers of applications
          new ArrayConstructors) ::   // Intercept creation of (non-generic) arrays and intrinsify.
+    List(new PreRecheck) ::
+    List(new TestRecheck) ::
     List(new Erasure) ::             // Rewrite types to JVM model, erasing all type parameters, abstract types and refinements.
     List(new ElimErasedValueType,    // Expand erased value types to their underlying implmementation types
          new PureStats,              // Remove pure stats from blocks

compiler/src/dotty/tools/dotc/config/ScalaSettings.scala

@@ -238,6 +238,7 @@ private sealed trait YSettings:
   val YexplicitNulls: Setting[Boolean] = BooleanSetting("-Yexplicit-nulls", "Make reference types non-nullable. Nullable types can be expressed with unions: e.g. String|Null.")
   val YcheckInit: Setting[Boolean] = BooleanSetting("-Ysafe-init", "Ensure safe initialization of objects")
   val YrequireTargetName: Setting[Boolean] = BooleanSetting("-Yrequire-targetName", "Warn if an operator is defined without a @targetName annotation")
+  val Yrecheck: Setting[Boolean] = BooleanSetting("-Yrecheck", "Run type rechecks (test only)")
 
   /** Area-specific debug output */
   val YexplainLowlevel: Setting[Boolean] = BooleanSetting("-Yexplain-lowlevel", "When explaining type errors, show types at a lower level.")

compiler/src/dotty/tools/dotc/transform/Recheck.scala

@@ -24,7 +24,7 @@ abstract class Recheck extends Phase, IdentityDenotTransformer:
 
   def preRecheckPhase = this.prev.asInstanceOf[PreRecheck]
 
-  //override def isTyper = true
+  override def isEnabled(using Context) = ctx.settings.Yrecheck.value
 
   def run(using Context): Unit =
     val unit = ctx.compilationUnit

compiler/test/dotc/pos-test-recheck.exludes

@@ -0,0 +1,10 @@
+# Cannot compensate dealiasing due to false result dependency
+i6635a.scala
+
+# Cannot handle closures with skolem types
+i6199b.scala
+i6199c.scala
+
+# Skolemized type fails -Ycheck after recheck (NamedType caching problem?)
+i583.scala
+

compiler/test/dotc/run-test-recheck.exludes

@@ -11,17 +11,21 @@ object TestSources {
 
   def posFromTastyBlacklistFile: String = "compiler/test/dotc/pos-from-tasty.blacklist"
   def posTestPicklingBlacklistFile: String = "compiler/test/dotc/pos-test-pickling.blacklist"
+  def posTestRecheckExcludesFile = "compiler/test/dotc/pos-test-recheck.exludes"
 
   def posFromTastyBlacklisted: List[String] = loadList(posFromTastyBlacklistFile)
   def posTestPicklingBlacklisted: List[String] = loadList(posTestPicklingBlacklistFile)
+  def posTestRecheckExcluded = loadList(posTestRecheckExcludesFile)
 
   // run tests lists
 
   def runFromTastyBlacklistFile: String = "compiler/test/dotc/run-from-tasty.blacklist"
   def runTestPicklingBlacklistFile: String = "compiler/test/dotc/run-test-pickling.blacklist"
+  def runTestRecheckExcludesFile = "compiler/test/dotc/run-test-recheck.exludes"
 
   def runFromTastyBlacklisted: List[String] = loadList(runFromTastyBlacklistFile)
   def runTestPicklingBlacklisted: List[String] = loadList(runTestPicklingBlacklistFile)
+  def runTestRecheckExcluded = loadList(runTestRecheckExcludesFile)
 
   // load lists
 

compiler/test/dotty/tools/TestSources.scala

@@ -218,6 +218,15 @@ class CompilationTests {
     ).checkCompile()
   }
 
+  @Test def recheck: Unit =
+    given TestGroup = TestGroup("recheck")
+    aggregateTests(
+      compileFilesInDir("tests/new", recheckOptions),
+      compileFilesInDir("tests/pos", recheckOptions, FileFilter.exclude(TestSources.posTestRecheckExcluded)),
+      compileFilesInDir("tests/run", recheckOptions, FileFilter.exclude(TestSources.runTestRecheckExcluded))
+    ).checkCompile()
+
+
   /** The purpose of this test is three-fold, being able to compile dotty
    *  bootstrapped, and making sure that TASTY can link against a compiled
    *  version of Dotty, and compiling the compiler using the SemanticDB generation

compiler/test/dotty/tools/dotc/CompilationTests.scala

@@ -78,6 +78,7 @@ object TestConfiguration {
   )
   val picklingWithCompilerOptions =
     picklingOptions.withClasspath(withCompilerClasspath).withRunClasspath(withCompilerClasspath)
+  val recheckOptions = defaultOptions.and("-Yrecheck")
   val scala2CompatMode = defaultOptions.and("-source", "3.0-migration")
   val explicitUTF8 = defaultOptions and ("-encoding", "UTF8")
   val explicitUTF16 = defaultOptions and ("-encoding", "UTF16")

compiler/test/dotty/tools/vulpix/TestConfiguration.scala

@@ -0,0 +1,19 @@
+object Test {
+  abstract class ExprBase { s =>
+    type A
+  }
+
+  abstract class Lit extends ExprBase { s =>
+    type A = Int
+    val n: A
+  }
+
+  // It would be nice if the following could typecheck. We'd need to apply
+  // a reasoning like this:
+  //
+  //    Since there is an argument `e2` of type `Lit & e1.type`, it follows that
+  //    e1.type == e2.type Hence, e1.A == e2.A == Int. This looks similar
+  //    to techniques used in GADTs.
+  //
+  def castTestFail2a(e1: ExprBase)(e2: Lit & e1.type)(x: e1.A): Int = x // error: Found: (x : e1.A) Required: Int
+}

tests/neg/i6635a.scala

@@ -27,11 +27,12 @@ object Test {
   def castTest5a(e1: ExprBase)(e2: LitU with e1.type)(x: e2.A): e1.A = x
   def castTest5b(e1: ExprBase)(e2: LitL with e1.type)(x: e2.A): e1.A = x
 
-  //fail:
   def castTestFail1(e1: ExprBase)(e2: Lit with e1.type)(x: e2.A): e1.A = x // this is like castTest5a/b, but with Lit instead of LitU/LitL
-  // the other direction never works:
-  def castTestFail2a(e1: ExprBase)(e2: Lit with e1.type)(x: e1.A): e2.A = x
+
+  // The next example fails rechecking. It is repeated in i6635a.scala
+  // def castTestFail2a(e1: ExprBase)(e2: Lit with e1.type)(x: e1.A): e2.A = x
   def castTestFail2b(e1: ExprBase)(e2: LitL with e1.type)(x: e1.A): e2.A = x
+
   def castTestFail2c(e1: ExprBase)(e2: LitU with e1.type)(x: e1.A): e2.A = x
 
   // the problem isn't about order of intersections.

tests/pos/i6635.scala

@@ -0,0 +1,14 @@
+object Test {
+  abstract class ExprBase { s =>
+    type A
+  }
+
+  abstract class Lit extends ExprBase { s =>
+    type A = Int
+    val n: A
+  }
+
+  // Fails recheck since the result type e2.A is converted to Int to avoid
+  // a false dependency on e2.
+  def castTestFail2a(e1: ExprBase)(e2: Lit with e1.type)(x: e1.A): e2.A = x
+}