Dotty: Ycheck failure in pattern matching against a value of type `Nothing`

[abeln]

Given test.scala

object Foo {
  val Some(y) = ???
}

dotc -Ycheck:patternMatcher test.scala fails with

[warn] Multiple main classes detected. Run 'show discoveredMainClasses' to see the list [info] Running (fork) dotty.tools.dotc.Main -classpath /Users/abeln/.sbt/boot/scala-2.12.6/lib/scala-library.jar:/Users/abeln/src/dotty2/dotty/library/../out/bootstrap/dotty-library-bootstrapped/scala-0.10/dotty-library_0.10-0.10.0-bin-SNAPSHOT.jar -Ycheck:patternMatcher kk.scala checking kk.scala after phase MegaPhase{tryCatchPatterns, patternMatcher, explicitOuter, explicitSelf, stringInterpolatorOpt, crossCast, splitter} exception while typing x1.ne of class class dotty.tools.dotc.ast.Trees$Select # 636 exception while typing x1.ne(null) of class class dotty.tools.dotc.ast.Trees$Apply # 638 exception while typing if x1.ne(null) then { case val y: Nothing = x1.value.asInstanceOf[Nothing] return[matchResult1] y: Nothing } else () of class class dotty.tools.dotc.ast.Trees$If # 648 exception while typing { case val x1: Nothing @unchecked = ???: Nothing @unchecked if x1.ne(null) then { case val y: Nothing = x1.value.asInstanceOf[Nothing] return[matchResult1] y: Nothing } else () return[matchResult1] throw new MatchError(x1) } of class class dotty.tools.dotc.ast.Trees$Block # 652 exception while typing matchResult1[Nothing]: { case val x1: Nothing @unchecked = ???: Nothing @unchecked if x1.ne(null) then { case val y: Nothing = x1.value.asInstanceOf[Nothing] return[matchResult1] y: Nothing } else () return[matchResult1] throw new MatchError(x1) } of class class dotty.tools.dotc.ast.Trees$Labeled # 654 exception while typing val y: Nothing = matchResult1[Nothing]: { case val x1: Nothing @unchecked = ???: Nothing @unchecked if x1.ne(null) then { case val y: Nothing = x1.value.asInstanceOf[Nothing] return[matchResult1] y: Nothing } else () return[matchResult1] throw new MatchError(x1) } of class class dotty.tools.dotc.ast.Trees$ValDef # 655 exception while typing @scala.annotation.internal.SourceFile("kk.scala") final module class Foo() extends Object() { val y: Nothing = matchResult1[Nothing]: { case val x1: Nothing @unchecked = ???: Nothing @unchecked if x1.ne(null) then { case val y: Nothing = x1.value.asInstanceOf[Nothing] return[matchResult1] y: Nothing } else () return[matchResult1] throw new MatchError(x1) } } of class class dotty.tools.dotc.ast.Trees$TypeDef # 657 exception while typing package <empty> { final lazy module val Foo: Foo = new Foo() @scala.annotation.internal.SourceFile("kk.scala") final module class Foo() extends Object() { val y: Nothing = matchResult1[Nothing]: { case val x1: Nothing @unchecked = ???: Nothing @unchecked if x1.ne(null) then { case val y: Nothing = x1.value.asInstanceOf[Nothing] return[matchResult1] y: Nothing } else () return[matchResult1] throw new MatchError(x1) } } } of class class dotty.tools.dotc.ast.Trees$PackageDef # 658 *** error while checking kk.scala after phase splitter *** exception occurred while compiling kk.scala Exception in thread "main" java.lang.AssertionError: assertion failed: symbols differ for x1.ne was : method ne alternatives by type: of types qualifier type : Nothing @unchecked(x1) tree type : ((x$0: Object): Boolean)(x1.ne) of class class dotty.tools.dotc.core.Types$CachedTermRef at scala.Predef$.assert(Predef.scala:219) at dotty.tools.dotc.transform.TreeChecker$Checker.typedSelect(TreeChecker.scala:350) at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:1806) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1876) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:112) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:282) at dotty.tools.dotc.typer.Typer.$anonfun$typed$2(Typer.scala:1908) at dotty.tools.dotc.reporting.trace$.apply(trace.scala:40) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1904) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1920) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:270) at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:1977) at dotty.tools.dotc.typer.Applications.$anonfun$typedApply$1(Applications.scala:695) at dotty.tools.dotc.util.Stats$.track(Stats.scala:37) at dotty.tools.dotc.typer.Applications.realApply$1(Applications.scala:693) at dotty.tools.dotc.typer.Applications.typedApply(Applications.scala:794) at dotty.tools.dotc.typer.Applications.typedApply$(Applications.scala:691) at dotty.tools.dotc.typer.Typer.typedApply(Typer.scala:82) at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:1826) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1877) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:112) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:282) at dotty.tools.dotc.typer.Typer.$anonfun$typed$2(Typer.scala:1908) at dotty.tools.dotc.reporting.trace$.apply(trace.scala:40) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1904) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1920) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:270) at dotty.tools.dotc.typer.Typer.$anonfun$typedIf$1(Typer.scala:713) at dotty.tools.dotc.util.Stats$.track(Stats.scala:37) at dotty.tools.dotc.typer.Typer.typedIf(Typer.scala:711) at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:1834) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1877) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:112) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:282) at dotty.tools.dotc.typer.Typer.$anonfun$typed$2(Typer.scala:1908) at dotty.tools.dotc.reporting.trace$.apply(trace.scala:40) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1904) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1920) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:270) at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:1960) at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:1973) at dotty.tools.dotc.transform.TreeChecker$Checker.typedStats(TreeChecker.scala:446) at dotty.tools.dotc.typer.Typer.typedBlockStats(Typer.scala:664) at dotty.tools.dotc.typer.Typer.$anonfun$typedBlock$1(Typer.scala:667) at dotty.tools.dotc.util.Stats$.track(Stats.scala:37) at dotty.tools.dotc.typer.Typer.typedBlock(Typer.scala:666) at dotty.tools.dotc.transform.TreeChecker$Checker.super$typedBlock(TreeChecker.scala:428) at dotty.tools.dotc.transform.TreeChecker$Checker.$anonfun$typedBlock$1(TreeChecker.scala:428) at dotty.tools.dotc.transform.TreeChecker$Checker.withDefinedSyms(TreeChecker.scala:179) at dotty.tools.dotc.transform.TreeChecker$Checker.typedBlock(TreeChecker.scala:428) at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:1833) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1877) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:112) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:282) at dotty.tools.dotc.typer.Typer.$anonfun$typed$2(Typer.scala:1908) at dotty.tools.dotc.reporting.trace$.apply(trace.scala:40) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1904) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1920) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:270) at dotty.tools.dotc.typer.Typer.$anonfun$typedLabeled$1(Typer.scala:1075) at dotty.tools.dotc.util.Stats$.track(Stats.scala:37) at dotty.tools.dotc.typer.Typer.typedLabeled(Typer.scala:1073) at dotty.tools.dotc.transform.TreeChecker$Checker.super$typedLabeled(TreeChecker.scala:451) at dotty.tools.dotc.transform.TreeChecker$Checker.$anonfun$typedLabeled$1(TreeChecker.scala:451) at dotty.tools.dotc.transform.TreeChecker$Checker.withDefinedSyms(TreeChecker.scala:179) at dotty.tools.dotc.transform.TreeChecker$Checker.typedLabeled(TreeChecker.scala:451) at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:1819) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1876) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:112) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:282) at dotty.tools.dotc.typer.Typer.$anonfun$typed$2(Typer.scala:1908) at dotty.tools.dotc.reporting.trace$.apply(trace.scala:40) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1904) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1920) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:270) at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:1977) at dotty.tools.dotc.typer.Typer.$anonfun$typedValDef$1(Typer.scala:1402) at dotty.tools.dotc.util.Stats$.track(Stats.scala:37) at dotty.tools.dotc.typer.Typer.typedValDef(Typer.scala:1396) at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:1810) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1876) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:112) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:282) at dotty.tools.dotc.typer.Typer.$anonfun$typed$2(Typer.scala:1908) at dotty.tools.dotc.reporting.trace$.apply(trace.scala:40) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1904) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1920) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:270) at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:1939) at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:1973) at dotty.tools.dotc.transform.TreeChecker$Checker.typedStats(TreeChecker.scala:446) at dotty.tools.dotc.typer.Typer.$anonfun$typedClassDef$1(Typer.scala:1569) at dotty.tools.dotc.util.Stats$.track(Stats.scala:37) at dotty.tools.dotc.typer.Typer.typedClassDef(Typer.scala:1492) at dotty.tools.dotc.transform.TreeChecker$Checker.typedClassDef(TreeChecker.scala:399) at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:1816) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1876) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:112) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:282) at dotty.tools.dotc.typer.Typer.$anonfun$typed$2(Typer.scala:1908) at dotty.tools.dotc.reporting.trace$.apply(trace.scala:40) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1904) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1920) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:270) at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:1939) at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:1973) at dotty.tools.dotc.transform.TreeChecker$Checker.typedStats(TreeChecker.scala:446) at dotty.tools.dotc.typer.Typer.$anonfun$typedPackageDef$1(Typer.scala:1682) at dotty.tools.dotc.util.Stats$.track(Stats.scala:37) at dotty.tools.dotc.typer.Typer.typedPackageDef(Typer.scala:1675) at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:1856) at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:1877) at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:112) at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:282) at dotty.tools.dotc.typer.Typer.$anonfun$typed$2(Typer.scala:1908) at dotty.tools.dotc.reporting.trace$.apply(trace.scala:40) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1904) at dotty.tools.dotc.typer.Typer.typed(Typer.scala:1920) at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:270) at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:1977) at dotty.tools.dotc.transform.TreeChecker.check(TreeChecker.scala:132) at dotty.tools.dotc.transform.TreeChecker.run(TreeChecker.scala:104) at dotty.tools.dotc.core.Phases$Phase.$anonfun$runOn$1(Phases.scala:299) at scala.collection.immutable.List.map(List.scala:283) at dotty.tools.dotc.core.Phases$Phase.runOn(Phases.scala:297) at dotty.tools.dotc.core.Phases$Phase.runOn$(Phases.scala:296) at dotty.tools.dotc.transform.TreeChecker.runOn(TreeChecker.scala:48) at dotty.tools.dotc.Run.$anonfun$compileUnits$3(Run.scala:175) at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12) at dotty.tools.dotc.util.Stats$.trackTime(Stats.scala:49) at dotty.tools.dotc.Run.$anonfun$compileUnits$2(Run.scala:172) at dotty.tools.dotc.Run.$anonfun$compileUnits$2$adapted(Run.scala:170) at scala.collection.IndexedSeqOptimized.foreach(IndexedSeqOptimized.scala:32) at scala.collection.IndexedSeqOptimized.foreach$(IndexedSeqOptimized.scala:29) at scala.collection.mutable.ArrayOps$ofRef.foreach(ArrayOps.scala:194) at dotty.tools.dotc.Run.runPhases$1(Run.scala:170) at dotty.tools.dotc.Run.$anonfun$compileUnits$1(Run.scala:195) at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:12) at dotty.tools.dotc.util.Stats$.maybeMonitored(Stats.scala:90) at dotty.tools.dotc.Run.compileUnits(Run.scala:150) at dotty.tools.dotc.Run.compileSources(Run.scala:137) at dotty.tools.dotc.Run.compile(Run.scala:121) at dotty.tools.dotc.Driver.doCompile(Driver.scala:31) at dotty.tools.dotc.Driver.process(Driver.scala:134) at dotty.tools.dotc.Driver.process(Driver.scala:103) at dotty.tools.dotc.Driver.process(Driver.scala:115) at dotty.tools.dotc.Driver.main(Driver.scala:142) at dotty.tools.dotc.Main.main(Main.scala)

[abeln]

The problem is in the desugaring of the unapply method. Tree after patternMatcher:

package <empty> {
  final lazy module val Foo: Foo$ = new Foo$()
  @scala.annotation.internal.SourceFile("kk.scala") final module class Foo$()
     extends
   Object() { 
    val y: Nothing = 
      matchResult1[Nothing]: 
        {
          case val x1: Nothing @unchecked = ???: Nothing @unchecked
          if x1.ne(null) then 
            {
              case val y: Nothing = x1.value.asInstanceOf[Nothing]
              return[matchResult1] y: Nothing
            }
           else ()
          return[matchResult1] throw new MatchError(x1)
        }
  }
}

x1.ne(null) fails because x1 has type Nothing.

[abeln]

Here's another one that fails with -Ycheck:

object Foo {
  val Some(x) = null
}

After desugaring:

  final lazy module val Foo: Foo = new Foo()
  @scala.annotation.internal.SourceFile("kk.scala") final module class Foo()
     extends
   Object() { 
    val x: Nothing = 
      matchResult1[Nothing]: 
        {
          case val x1: Null @unchecked = null: Null @unchecked
          if x1.ne(null) then 
            {
              case val x: Nothing = x1.value.asInstanceOf[Nothing]
              return[matchResult1] x: Nothing
            }
           else ()
          return[matchResult1] throw new MatchError(x1)
        }
  }

In this case because of x1.value.asInstanceOf[Nothing], since x1: Null.

[abeln]

If we decide to accept matching against Null or Nothing as type-correct, then https://github.com/lampepfl/dotty/pull/5075 changes how we desugar unapply so that Ycheck works.

[allanrenucci]

Note that scalac rejects matches against both Null and Nothing:

class Test {
  def test = {
    val Some(x) = null
    val Some(y) = ???
  }
}

Test.scala:3: error: constructor cannot be instantiated to expected type;
 found   : Some[A]
 required: Null
    val Some(x) = null
        ^
Test.scala:4: error: constructor cannot be instantiated to expected type;
 found   : Some[A]
 required: Nothing
    val Some(y) = ???

I don't see a good reason to allow it

[abeln]

I don't have a strong opinion either way. Allowing it does seems to remove a special case.
For example, this typechecks in scalac:

def test[T](x: T): Unit = {
  val Some(y) = x
}
test[Null](null)
test[Nothing](???)

https://scastie.scala-lang.org/igmBh2RJTt23TEeRN5uF1g

[sjrd]

IMO this should be accepted by -Ycheck. In fact calling any method of any class should be accepted on a receiver of type Nothing or Null (for the latter, possibly only methods of classes that are not AnyVals). This is necessary for LSP. Let's say I have

val x: Null = null
val y: String = x
println(y.substring(1))

which is obviously valid. Now let's assume I have some phase that makes types more precise, and hence produces:

val x: Null = null
val y: Null = x
println(y.substring(1))

it should still be valid. Yes, the code is guaranteed to throw an NPE when it gets there, but it is still a valid type-safe tree.

We had a similar issue in the IR checker of Scala.js at some point, which was discovered by the optimizer specializing some types. We relaxed the IR checker to consider any method call on Null and Nothing to be valid. https://github.com/scala-js/scala-js/issues/1123

[Blaisorblade]

@abeln I agree with @sjrd for the same reason (LSP); the current behavior also violates type preservation/subject reduction. But fixing it seems tricky enough to warrant a special issue.

The change doesn't break existing code but removes compiler errors some people might expect (tho I don't know any valid usecases, I can imagine people exploiting this); nevertheless we should try this change.
Both (null: Null).foo(args) and ???.foo(args) should return type Nothing, and I guess they should compile to code throwing exceptions (because we don't know what JVM signature to emit). It's unclear what Denotation we should get by method lookup on Null or Nothing. I thought foo(args: Any*): Nothing might work but isn't quite right, since LSP mandates methods with all signatures. Not sure if we can observe this mismatch.
If we can, to get this right we need to obtain the argument types from the arguments, so I suspect we'd need a special sort of MultiDenotation, probably with special cases handling it (in fact, quite a bit of MultiDenotation couldn't be implemented in this case).