From be022bb27853b0520f091b8112b7348b38a9bacb Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Sat, 21 Sep 2024 19:54:39 +0200
Subject: [PATCH 01/11] Refactor NotNullInfo to record every reference which is
 retracted once.

[Cherry-picked 585dda9587bc95afb936eb18751fbf850cf3209c]
---
 .../dotty/tools/dotc/typer/Nullables.scala    | 32 +++++++---
 .../src/dotty/tools/dotc/typer/Typer.scala    | 15 ++++-
 tests/explicit-nulls/neg/i21380c.scala        |  6 +-
 tests/explicit-nulls/neg/i21619.scala         | 62 +++++++++++++++++++
 4 files changed, 100 insertions(+), 15 deletions(-)
 create mode 100644 tests/explicit-nulls/neg/i21619.scala

diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index d47cfc0bf17e..96b71d2e8390 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -48,15 +48,19 @@ object Nullables:
     val newHi = if needNullifyHi(lo.typeOpt, hiTpe) then TypeTree(OrType(hiTpe, defn.NullType, soft = false)) else hi
     TypeBoundsTree(lo, newHi, alias)
 
-  /** A set of val or var references that are known to be not null, plus a set of
-   *  variable references that are not known (anymore) to be not null
+  /** A set of val or var references that are known to be not null,
+   *  a set of variable references that are not known (anymore) to be not null,
+   *  plus a set of variables that are known to be not null at any point.
    */
-  case class NotNullInfo(asserted: Set[TermRef], retracted: Set[TermRef]):
+  case class NotNullInfo(asserted: Set[TermRef], retracted: Set[TermRef], onceRetracted: Set[TermRef]):
     assert((asserted & retracted).isEmpty)
+    assert(retracted.subsetOf(onceRetracted))
 
     def isEmpty = this eq NotNullInfo.empty
 
-    def retractedInfo = NotNullInfo(Set(), retracted)
+    def retractedInfo = NotNullInfo(Set(), retracted, onceRetracted)
+
+    def onceRetractedInfo = NotNullInfo(Set(), onceRetracted, onceRetracted)
 
     /** The sequential combination with another not-null info */
     def seq(that: NotNullInfo): NotNullInfo =
@@ -64,19 +68,29 @@ object Nullables:
       else if that.isEmpty then this
       else NotNullInfo(
         this.asserted.union(that.asserted).diff(that.retracted),
-        this.retracted.union(that.retracted).diff(that.asserted))
+        this.retracted.union(that.retracted).diff(that.asserted),
+        this.onceRetracted.union(that.onceRetracted))
 
     /** The alternative path combination with another not-null info. Used to merge
      *  the nullability info of the two branches of an if.
      */
     def alt(that: NotNullInfo): NotNullInfo =
-      NotNullInfo(this.asserted.intersect(that.asserted), this.retracted.union(that.retracted))
+      NotNullInfo(
+        this.asserted.intersect(that.asserted),
+        this.retracted.union(that.retracted),
+        this.onceRetracted.union(that.onceRetracted))
+
+    def withOnceRetracted(that: NotNullInfo): NotNullInfo =
+      if that.isEmpty then this
+      else NotNullInfo(this.asserted, this.retracted, this.onceRetracted.union(that.onceRetracted))
 
   object NotNullInfo:
-    val empty = new NotNullInfo(Set(), Set())
+    val empty = new NotNullInfo(Set(), Set(), Set())
     def apply(asserted: Set[TermRef], retracted: Set[TermRef]): NotNullInfo =
-      if asserted.isEmpty && retracted.isEmpty then empty
-      else new NotNullInfo(asserted, retracted)
+      apply(asserted, retracted, retracted)
+    def apply(asserted: Set[TermRef], retracted: Set[TermRef], onceRetracted: Set[TermRef]): NotNullInfo =
+      if asserted.isEmpty && onceRetracted.isEmpty then empty
+      else new NotNullInfo(asserted, retracted, onceRetracted)
   end NotNullInfo
 
   /** A pair of not-null sets, depending on whether a condition is `true` or `false` */
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index d0a6272d390c..0e8cd8be3a1f 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1334,8 +1334,10 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
     def thenPathInfo = cond1.notNullInfoIf(true).seq(result.thenp.notNullInfo)
     def elsePathInfo = cond1.notNullInfoIf(false).seq(result.elsep.notNullInfo)
     result.withNotNullInfo(
-      if result.thenp.tpe.isRef(defn.NothingClass) then elsePathInfo
-      else if result.elsep.tpe.isRef(defn.NothingClass) then thenPathInfo
+      if result.thenp.tpe.isRef(defn.NothingClass) then
+        elsePathInfo.withOnceRetracted(thenPathInfo)
+      else if result.elsep.tpe.isRef(defn.NothingClass) then
+        thenPathInfo.withOnceRetracted(elsePathInfo)
       else thenPathInfo.alt(elsePathInfo)
     )
   end typedIf
@@ -2069,10 +2071,17 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
     }: @unchecked
     val cases2 = cases2x.asInstanceOf[List[CaseDef]]
 
-    var nni = expr2.notNullInfo.retractedInfo
+    // Since we don't know at which point the the exception is thrown in the body,
+    // we have to collect any reference that is once retracted.
+    var nni = expr2.notNullInfo.onceRetractedInfo
+    // It is possible to have non-exhaustive cases, and some exceptions are thrown and not caught.
+    // Therefore, the code in the finallizer and after the try block can only rely on the retracted
+    // info from the cases' body.
     if cases2.nonEmpty then nni = nni.seq(cases2.map(_.notNullInfo.retractedInfo).reduce(_.alt(_)))
+
     val finalizer1 = typed(tree.finalizer, defn.UnitType)(using ctx.addNotNullInfo(nni))
     nni = nni.seq(finalizer1.notNullInfo)
+
     assignType(cpy.Try(tree)(expr2, cases2, finalizer1), expr2, cases2).withNotNullInfo(nni)
   }
 
diff --git a/tests/explicit-nulls/neg/i21380c.scala b/tests/explicit-nulls/neg/i21380c.scala
index c5758743d784..af40b19318f4 100644
--- a/tests/explicit-nulls/neg/i21380c.scala
+++ b/tests/explicit-nulls/neg/i21380c.scala
@@ -32,9 +32,9 @@ def test4: Int =
     case npe: NullPointerException => x = ""
     case _ => x = ""
   x.length // error
-  // Although the catch block here is exhaustive,
-  // it is possible that the exception is thrown and not caught.
-  // Therefore, the code after the try block can only rely on the retracted info.
+  // Although the catch block here is exhaustive, it is possible to have non-exhaustive cases,
+  // and some exceptions are thrown and not caught. Therefore, the code in the finallizer and
+  // after the try block can only rely on the retracted info from the cases' body.
 
 def test5: Int =
   var x: String | Null = null
diff --git a/tests/explicit-nulls/neg/i21619.scala b/tests/explicit-nulls/neg/i21619.scala
new file mode 100644
index 000000000000..1c93af707b73
--- /dev/null
+++ b/tests/explicit-nulls/neg/i21619.scala
@@ -0,0 +1,62 @@
+def test1: String =
+  var x: String | Null = null
+  x = ""
+  var i: Int = 1
+  try
+    i match
+      case _ =>
+        x = null
+        throw new Exception()
+    x = ""
+  catch
+    case e: Exception =>
+  x.replace("", "") // error
+
+def test2: String =
+  var x: String | Null = null
+  x = ""
+  var i: Int = 1
+  try
+    i match
+      case _ =>
+        x = null
+        throw new Exception()
+    x = ""
+  catch
+    case e: Exception =>
+      x = "e"
+  x.replace("", "") // error
+
+def test3: String =
+  var x: String | Null = null
+  x = ""
+  var i: Int = 1
+  try
+    i match
+      case _ =>
+        x = null
+        throw new Exception()
+    x = ""
+  catch
+    case e: Exception =>
+  finally
+    x = "f"
+  x.replace("", "") // ok
+
+def test4: String =
+  var x: String | Null = null
+  x = ""
+  var i: Int = 1
+  try
+    try
+      if i == 1 then
+        x = null
+        throw new Exception()
+      else
+        x = ""
+    catch
+      case _ =>
+    x = ""
+  catch
+    case _ =>
+  x.replace("", "") // error
\ No newline at end of file

From cc6c7830ae85e7ff599d3f73ecfa7f141e1c1fd1 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Sun, 22 Sep 2024 17:03:39 +0200
Subject: [PATCH 02/11] Use a different rule for NotNullInfo

[Cherry-picked bcc9e68c778da3faa4dcb8b6c0258a48befff819]
---
 .../dotty/tools/dotc/typer/Nullables.scala    | 44 ++++++-------------
 .../src/dotty/tools/dotc/typer/Typer.scala    | 34 +++++++-------
 tests/explicit-nulls/neg/i21619.scala         | 19 +++++++-
 3 files changed, 50 insertions(+), 47 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 96b71d2e8390..68916a021d5e 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -49,48 +49,35 @@ object Nullables:
     TypeBoundsTree(lo, newHi, alias)
 
   /** A set of val or var references that are known to be not null,
-   *  a set of variable references that are not known (anymore) to be not null,
-   *  plus a set of variables that are known to be not null at any point.
+   *  plus a set of variable references that are once assigned to null.
    */
-  case class NotNullInfo(asserted: Set[TermRef], retracted: Set[TermRef], onceRetracted: Set[TermRef]):
-    assert((asserted & retracted).isEmpty)
-    assert(retracted.subsetOf(onceRetracted))
-
+  case class NotNullInfo(asserted: Set[TermRef], retracted: Set[TermRef]):
     def isEmpty = this eq NotNullInfo.empty
 
-    def retractedInfo = NotNullInfo(Set(), retracted, onceRetracted)
-
-    def onceRetractedInfo = NotNullInfo(Set(), onceRetracted, onceRetracted)
+    def retractedInfo = NotNullInfo(Set(), retracted)
 
     /** The sequential combination with another not-null info */
     def seq(that: NotNullInfo): NotNullInfo =
       if this.isEmpty then that
       else if that.isEmpty then this
       else NotNullInfo(
-        this.asserted.union(that.asserted).diff(that.retracted),
-        this.retracted.union(that.retracted).diff(that.asserted),
-        this.onceRetracted.union(that.onceRetracted))
+        this.asserted.diff(that.retracted).union(that.asserted),
+        this.retracted.union(that.retracted))
 
     /** The alternative path combination with another not-null info. Used to merge
      *  the nullability info of the two branches of an if.
      */
     def alt(that: NotNullInfo): NotNullInfo =
-      NotNullInfo(
-        this.asserted.intersect(that.asserted),
-        this.retracted.union(that.retracted),
-        this.onceRetracted.union(that.onceRetracted))
+      NotNullInfo(this.asserted.intersect(that.asserted), this.retracted.union(that.retracted))
 
-    def withOnceRetracted(that: NotNullInfo): NotNullInfo =
-      if that.isEmpty then this
-      else NotNullInfo(this.asserted, this.retracted, this.onceRetracted.union(that.onceRetracted))
+    def withRetracted(that: NotNullInfo): NotNullInfo =
+      NotNullInfo(this.asserted, this.retracted.union(that.retracted))
 
   object NotNullInfo:
-    val empty = new NotNullInfo(Set(), Set(), Set())
+    val empty = new NotNullInfo(Set(), Set())
     def apply(asserted: Set[TermRef], retracted: Set[TermRef]): NotNullInfo =
-      apply(asserted, retracted, retracted)
-    def apply(asserted: Set[TermRef], retracted: Set[TermRef], onceRetracted: Set[TermRef]): NotNullInfo =
-      if asserted.isEmpty && onceRetracted.isEmpty then empty
-      else new NotNullInfo(asserted, retracted, onceRetracted)
+      if asserted.isEmpty && retracted.isEmpty then empty
+      else new NotNullInfo(asserted, retracted)
   end NotNullInfo
 
   /** A pair of not-null sets, depending on whether a condition is `true` or `false` */
@@ -222,16 +209,13 @@ object Nullables:
     *  or retractions in `info` supersede infos in existing entries of `infos`.
     */
     def extendWith(info: NotNullInfo) =
-      if info.isEmpty
-        || info.asserted.forall(infos.impliesNotNull(_))
-            && !info.retracted.exists(infos.impliesNotNull(_))
-      then infos
+      if info.isEmpty then infos
       else info :: infos
 
     /** Retract all references to mutable variables */
     def retractMutables(using Context) =
-      val mutables = infos.foldLeft(Set[TermRef]())((ms, info) =>
-        ms.union(info.asserted.filter(_.symbol.is(Mutable))))
+      val mutables = infos.foldLeft(Set[TermRef]()):
+        (ms, info) => ms.union(info.asserted.filter(_.symbol.is(Mutable)))
       infos.extendWith(NotNullInfo(Set(), mutables))
 
   end extension
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 0e8cd8be3a1f..ec79be24ac3a 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1335,9 +1335,9 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
     def elsePathInfo = cond1.notNullInfoIf(false).seq(result.elsep.notNullInfo)
     result.withNotNullInfo(
       if result.thenp.tpe.isRef(defn.NothingClass) then
-        elsePathInfo.withOnceRetracted(thenPathInfo)
+        elsePathInfo.withRetracted(thenPathInfo)
       else if result.elsep.tpe.isRef(defn.NothingClass) then
-        thenPathInfo.withOnceRetracted(elsePathInfo)
+        thenPathInfo.withRetracted(elsePathInfo)
       else thenPathInfo.alt(elsePathInfo)
     )
   end typedIf
@@ -1871,9 +1871,9 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
   def typedMatchFinish(tree: untpd.Match, sel: Tree, wideSelType: Type, cases: List[untpd.CaseDef], pt: Type)(using Context): Tree = {
     val cases1 = harmonic(harmonize, pt)(typedCases(cases, sel, wideSelType, pt.dropIfProto))
       .asInstanceOf[List[CaseDef]]
-    var nni = sel.notNullInfo
-    if cases1.nonEmpty then nni = nni.seq(cases1.map(_.notNullInfo).reduce(_.alt(_)))
-    assignType(cpy.Match(tree)(sel, cases1), sel, cases1).withNotNullInfo(nni)
+    var nnInfo = sel.notNullInfo
+    if cases1.nonEmpty then nnInfo = nnInfo.seq(cases1.map(_.notNullInfo).reduce(_.alt(_)))
+    assignType(cpy.Match(tree)(sel, cases1), sel, cases1).withNotNullInfo(nnInfo)
   }
 
   def typedCases(cases: List[untpd.CaseDef], sel: Tree, wideSelType: Type, pt: Type)(using Context): List[CaseDef] =
@@ -2053,7 +2053,8 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
       val capabilityProof = caughtExceptions.reduce(OrType(_, _, true))
       untpd.Block(makeCanThrow(capabilityProof), expr)
 
-  def typedTry(tree: untpd.Try, pt: Type)(using Context): Try = {
+  def typedTry(tree: untpd.Try, pt: Type)(using Context): Try =
+    var nnInfo = NotNullInfo.empty
     val expr2 :: cases2x = harmonic(harmonize, pt) {
       // We want to type check tree.expr first to comput NotNullInfo, but `addCanThrowCapabilities`
       // uses the types of patterns in `tree.cases` to determine the capabilities.
@@ -2065,25 +2066,26 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
       val casesEmptyBody1 = tree.cases.mapconserve(cpy.CaseDef(_)(body = EmptyTree))
       val casesEmptyBody2 = typedCases(casesEmptyBody1, EmptyTree, defn.ThrowableType, WildcardType)
       val expr1 = typed(addCanThrowCapabilities(tree.expr, casesEmptyBody2), pt.dropIfProto)
-      val casesCtx = ctx.addNotNullInfo(expr1.notNullInfo.retractedInfo)
+
+      // Since we don't know at which point the the exception is thrown in the body,
+      // we have to collect any reference that is once retracted.
+      nnInfo = expr1.notNullInfo.retractedInfo
+
+      val casesCtx = ctx.addNotNullInfo(nnInfo)
       val cases1 = typedCases(tree.cases, EmptyTree, defn.ThrowableType, pt.dropIfProto)(using casesCtx)
       expr1 :: cases1
     }: @unchecked
     val cases2 = cases2x.asInstanceOf[List[CaseDef]]
 
-    // Since we don't know at which point the the exception is thrown in the body,
-    // we have to collect any reference that is once retracted.
-    var nni = expr2.notNullInfo.onceRetractedInfo
     // It is possible to have non-exhaustive cases, and some exceptions are thrown and not caught.
     // Therefore, the code in the finallizer and after the try block can only rely on the retracted
     // info from the cases' body.
-    if cases2.nonEmpty then nni = nni.seq(cases2.map(_.notNullInfo.retractedInfo).reduce(_.alt(_)))
-
-    val finalizer1 = typed(tree.finalizer, defn.UnitType)(using ctx.addNotNullInfo(nni))
-    nni = nni.seq(finalizer1.notNullInfo)
+    if cases2.nonEmpty then
+      nnInfo = nnInfo.seq(cases2.map(_.notNullInfo.retractedInfo).reduce(_.alt(_)))
 
-    assignType(cpy.Try(tree)(expr2, cases2, finalizer1), expr2, cases2).withNotNullInfo(nni)
-  }
+    val finalizer1 = typed(tree.finalizer, defn.UnitType)(using ctx.addNotNullInfo(nnInfo))
+    nnInfo = nnInfo.seq(finalizer1.notNullInfo)
+    assignType(cpy.Try(tree)(expr2, cases2, finalizer1), expr2, cases2).withNotNullInfo(nnInfo)
 
   def typedTry(tree: untpd.ParsedTry, pt: Type)(using Context): Try =
     val cases: List[untpd.CaseDef] = tree.handler match
diff --git a/tests/explicit-nulls/neg/i21619.scala b/tests/explicit-nulls/neg/i21619.scala
index 1c93af707b73..244f993fd4e1 100644
--- a/tests/explicit-nulls/neg/i21619.scala
+++ b/tests/explicit-nulls/neg/i21619.scala
@@ -59,4 +59,21 @@ def test4: String =
     x = ""
   catch
     case _ =>
-  x.replace("", "") // error
\ No newline at end of file
+  x.replace("", "") // error
+
+def test5: Unit =
+  var x: String | Null = null
+  var y: String | Null = null
+  x = ""
+  y = ""
+  var i: Int = 1
+  try
+    i match
+      case _ =>
+        x = null
+        throw new Exception()
+    x = ""
+  catch
+    case _ =>
+  val z1: String = x.replace("", "") // error
+  val z2: String = y.replace("", "")
\ No newline at end of file

From aa14cd8a321bd21d4f88ef744f8d9c82e677de89 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Fri, 11 Oct 2024 06:24:24 +0200
Subject: [PATCH 03/11] Consider cases with Nothing type

---
 .../src/dotty/tools/dotc/typer/Typer.scala    | 24 ++++++++++++-------
 tests/explicit-nulls/neg/i21380b.scala        | 20 +++++++++++++++-
 tests/explicit-nulls/neg/i21619.scala         |  4 ++--
 3 files changed, 37 insertions(+), 11 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index ec79be24ac3a..8d089527b2da 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1334,9 +1334,9 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
     def thenPathInfo = cond1.notNullInfoIf(true).seq(result.thenp.notNullInfo)
     def elsePathInfo = cond1.notNullInfoIf(false).seq(result.elsep.notNullInfo)
     result.withNotNullInfo(
-      if result.thenp.tpe.isRef(defn.NothingClass) then
+      if result.thenp.tpe.isNothingType then
         elsePathInfo.withRetracted(thenPathInfo)
-      else if result.elsep.tpe.isRef(defn.NothingClass) then
+      else if result.elsep.tpe.isNothingType then
         thenPathInfo.withRetracted(elsePathInfo)
       else thenPathInfo.alt(elsePathInfo)
     )
@@ -1862,20 +1862,28 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
         case1
       }
       .asInstanceOf[List[CaseDef]]
-    var nni = sel.notNullInfo
-    if cases1.nonEmpty then nni = nni.seq(cases1.map(_.notNullInfo).reduce(_.alt(_)))
-    assignType(cpy.Match(tree)(sel, cases1), sel, cases1).cast(pt).withNotNullInfo(nni)
+    assignType(cpy.Match(tree)(sel, cases1), sel, cases1).cast(pt)
+      .withNotNullInfo(notNullInfoFromCases(sel.notNullInfo, cases1))
   }
 
   // Overridden in InlineTyper for inline matches
   def typedMatchFinish(tree: untpd.Match, sel: Tree, wideSelType: Type, cases: List[untpd.CaseDef], pt: Type)(using Context): Tree = {
     val cases1 = harmonic(harmonize, pt)(typedCases(cases, sel, wideSelType, pt.dropIfProto))
       .asInstanceOf[List[CaseDef]]
-    var nnInfo = sel.notNullInfo
-    if cases1.nonEmpty then nnInfo = nnInfo.seq(cases1.map(_.notNullInfo).reduce(_.alt(_)))
-    assignType(cpy.Match(tree)(sel, cases1), sel, cases1).withNotNullInfo(nnInfo)
+    assignType(cpy.Match(tree)(sel, cases1), sel, cases1)
+      .withNotNullInfo(notNullInfoFromCases(sel.notNullInfo, cases1))
   }
 
+  private def notNullInfoFromCases(initInfo: NotNullInfo, cases: List[CaseDef])(using Context): NotNullInfo =
+    var nnInfo = initInfo
+    if cases.nonEmpty then
+      val (nothingCases, normalCases) = cases.partition(_.body.tpe.isNothingType)
+      nnInfo = nothingCases.foldLeft(nnInfo):
+        (nni, c) => nni.withRetracted(c.notNullInfo)
+      if normalCases.nonEmpty then
+        nnInfo = nnInfo.seq(normalCases.map(_.notNullInfo).reduce(_.alt(_)))
+    nnInfo
+
   def typedCases(cases: List[untpd.CaseDef], sel: Tree, wideSelType: Type, pt: Type)(using Context): List[CaseDef] =
     var caseCtx = ctx
     cases.mapconserve { cas =>
diff --git a/tests/explicit-nulls/neg/i21380b.scala b/tests/explicit-nulls/neg/i21380b.scala
index bd28bc63bd26..ea02f3731a29 100644
--- a/tests/explicit-nulls/neg/i21380b.scala
+++ b/tests/explicit-nulls/neg/i21380b.scala
@@ -18,4 +18,22 @@ def test3(i: Int) =
   i match
     case 1 if x != null => ()
     case _ => x = " "
-  x.trim() // error // LTS specific
\ No newline at end of file
+  x.trim() // error // LTS specific
+
+def test4(i: Int) =
+  var x: String | Null = null
+  var y: String | Null = null
+  i match
+    case 1 => x = "1"
+    case _ => y = " "
+  x.trim() // error
+
+def test5(i: Int): String =
+  var x: String | Null = null
+  var y: String | Null = null
+  i match
+    case 1 => x = "1"
+    case _ =>
+      y = " "
+      return y // error // LTS specific
+  x.trim() // error // LTS specific
diff --git a/tests/explicit-nulls/neg/i21619.scala b/tests/explicit-nulls/neg/i21619.scala
index 244f993fd4e1..bfc03b61e1b7 100644
--- a/tests/explicit-nulls/neg/i21619.scala
+++ b/tests/explicit-nulls/neg/i21619.scala
@@ -41,7 +41,7 @@ def test3: String =
     case e: Exception =>
   finally
     x = "f"
-  x.replace("", "") // ok
+  x.replace("", "") // error // LTS specific
 
 def test4: String =
   var x: String | Null = null
@@ -76,4 +76,4 @@ def test5: Unit =
   catch
     case _ =>
   val z1: String = x.replace("", "") // error
-  val z2: String = y.replace("", "")
\ No newline at end of file
+  val z2: String = y.replace("", "") // error // LTS specific
\ No newline at end of file

From 141424147192ff7a87b21757eca989047bcf0448 Mon Sep 17 00:00:00 2001
From: Tomasz Godzik <tgodzik@virtuslab.com>
Date: Wed, 12 Mar 2025 18:16:50 +0100
Subject: [PATCH 04/11] Consider cases with Nothing type

[Cherry-picked 05c630acf9dd8b2ecb98f34b1f40bfc8ddb55ce8][modified]

From eda874902f030a4257703e9ec2ed73ecf18b4032 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Mon, 14 Oct 2024 15:21:03 +0200
Subject: [PATCH 05/11] Apply suggestions from code review
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Ondřej Lhoták <olhotak@uwaterloo.ca>
[Cherry-picked d44147bc6ff5496dab9cc1569274dfb4b673ee09]
---
 compiler/src/dotty/tools/dotc/typer/Nullables.scala | 7 +++++--
 compiler/src/dotty/tools/dotc/typer/Typer.scala     | 2 +-
 tests/explicit-nulls/neg/i21380c.scala              | 2 +-
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 68916a021d5e..a61ef3ccfc3c 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -48,8 +48,11 @@ object Nullables:
     val newHi = if needNullifyHi(lo.typeOpt, hiTpe) then TypeTree(OrType(hiTpe, defn.NullType, soft = false)) else hi
     TypeBoundsTree(lo, newHi, alias)
 
-  /** A set of val or var references that are known to be not null,
-   *  plus a set of variable references that are once assigned to null.
+  /** A set of val or var references that are known to be not null
+  * after the tree finishes executing normally (non-exceptionally),
+   *  plus a set of variable references that are ever assigned to null,
+   *  and may therefore be null if execution of the tree is interrupted
+   *  by an exception.
    */
   case class NotNullInfo(asserted: Set[TermRef], retracted: Set[TermRef]):
     def isEmpty = this eq NotNullInfo.empty
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 8d089527b2da..eab185278ff7 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -2086,7 +2086,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
     val cases2 = cases2x.asInstanceOf[List[CaseDef]]
 
     // It is possible to have non-exhaustive cases, and some exceptions are thrown and not caught.
-    // Therefore, the code in the finallizer and after the try block can only rely on the retracted
+    // Therefore, the code in the finalizer and after the try block can only rely on the retracted
     // info from the cases' body.
     if cases2.nonEmpty then
       nnInfo = nnInfo.seq(cases2.map(_.notNullInfo.retractedInfo).reduce(_.alt(_)))
diff --git a/tests/explicit-nulls/neg/i21380c.scala b/tests/explicit-nulls/neg/i21380c.scala
index af40b19318f4..78914efaa939 100644
--- a/tests/explicit-nulls/neg/i21380c.scala
+++ b/tests/explicit-nulls/neg/i21380c.scala
@@ -33,7 +33,7 @@ def test4: Int =
     case _ => x = ""
   x.length // error
   // Although the catch block here is exhaustive, it is possible to have non-exhaustive cases,
-  // and some exceptions are thrown and not caught. Therefore, the code in the finallizer and
+  // and some exceptions are thrown and not caught. Therefore, the code in the finalizer and
   // after the try block can only rely on the retracted info from the cases' body.
 
 def test5: Int =

From 3be381323323bf27adcf0f5cc8011e4b7b72d4ee Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Fri, 1 Nov 2024 09:07:18 +0100
Subject: [PATCH 06/11] Add terminated info

---
 .../dotty/tools/dotc/typer/Nullables.scala    | 43 ++++++++++++-------
 .../src/dotty/tools/dotc/typer/Typer.scala    | 29 ++++---------
 .../explicit-nulls/neg/flow-early-exit.scala  |  2 +-
 .../explicit-nulls/neg/flow-simple-var.scala  |  2 +-
 4 files changed, 39 insertions(+), 37 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index a61ef3ccfc3c..723564cc52b8 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -49,37 +49,45 @@ object Nullables:
     TypeBoundsTree(lo, newHi, alias)
 
   /** A set of val or var references that are known to be not null
-  * after the tree finishes executing normally (non-exceptionally),
+   *  after the tree finishes executing normally (non-exceptionally),
    *  plus a set of variable references that are ever assigned to null,
    *  and may therefore be null if execution of the tree is interrupted
    *  by an exception.
    */
-  case class NotNullInfo(asserted: Set[TermRef], retracted: Set[TermRef]):
+  case class NotNullInfo(asserted: Set[TermRef] | Null, retracted: Set[TermRef]):
     def isEmpty = this eq NotNullInfo.empty
 
     def retractedInfo = NotNullInfo(Set(), retracted)
 
+    def terminatedInfo = NotNullInfo(null, retracted)
+
     /** The sequential combination with another not-null info */
     def seq(that: NotNullInfo): NotNullInfo =
       if this.isEmpty then that
       else if that.isEmpty then this
-      else NotNullInfo(
-        this.asserted.diff(that.retracted).union(that.asserted),
-        this.retracted.union(that.retracted))
+      else
+        val newAsserted =
+          if this.asserted == null || that.asserted == null then null
+          else this.asserted.diff(that.retracted).union(that.asserted)
+        val newRetracted = this.retracted.union(that.retracted)
+        NotNullInfo(newAsserted, newRetracted)
 
     /** The alternative path combination with another not-null info. Used to merge
-     *  the nullability info of the two branches of an if.
+     *  the nullability info of the branches of an if or match.
      */
     def alt(that: NotNullInfo): NotNullInfo =
-      NotNullInfo(this.asserted.intersect(that.asserted), this.retracted.union(that.retracted))
-
-    def withRetracted(that: NotNullInfo): NotNullInfo =
-      NotNullInfo(this.asserted, this.retracted.union(that.retracted))
+      val newAsserted =
+        if this.asserted == null then that.asserted
+        else if that.asserted == null then this.asserted
+        else this.asserted.intersect(that.asserted)
+      val newRetracted = this.retracted.union(that.retracted)
+      NotNullInfo(newAsserted, newRetracted)
+  end NotNullInfo
 
   object NotNullInfo:
     val empty = new NotNullInfo(Set(), Set())
-    def apply(asserted: Set[TermRef], retracted: Set[TermRef]): NotNullInfo =
-      if asserted.isEmpty && retracted.isEmpty then empty
+    def apply(asserted: Set[TermRef] | Null, retracted: Set[TermRef]): NotNullInfo =
+      if asserted != null && asserted.isEmpty && retracted.isEmpty then empty
       else new NotNullInfo(asserted, retracted)
   end NotNullInfo
 
@@ -202,7 +210,7 @@ object Nullables:
     */
     @tailrec def impliesNotNull(ref: TermRef): Boolean = infos match
       case info :: infos1 =>
-        if info.asserted.contains(ref) then true
+        if info.asserted != null && info.asserted.contains(ref) then true
         else if info.retracted.contains(ref) then false
         else infos1.impliesNotNull(ref)
       case _ =>
@@ -218,7 +226,9 @@ object Nullables:
     /** Retract all references to mutable variables */
     def retractMutables(using Context) =
       val mutables = infos.foldLeft(Set[TermRef]()):
-        (ms, info) => ms.union(info.asserted.filter(_.symbol.is(Mutable)))
+        (ms, info) => ms.union(
+                        if info.asserted == null then Set.empty
+                        else info.asserted.filter(_.symbol.is(Mutable)))
       infos.extendWith(NotNullInfo(Set(), mutables))
 
   end extension
@@ -491,7 +501,10 @@ object Nullables:
       && assignmentSpans.getOrElse(sym.span.start, Nil).exists(whileSpan.contains(_))
       && ctx.notNullInfos.impliesNotNull(ref)
 
-    val retractedVars = ctx.notNullInfos.flatMap(_.asserted.filter(isRetracted)).toSet
+    val retractedVars = ctx.notNullInfos.flatMap(info =>
+      if info.asserted == null then Set.empty
+      else info.asserted.filter(isRetracted)
+    ).toSet
     ctx.addNotNullInfo(NotNullInfo(Set(), retractedVars))
   end whileContext
 
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index eab185278ff7..6539c2c5513e 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1333,13 +1333,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
 
     def thenPathInfo = cond1.notNullInfoIf(true).seq(result.thenp.notNullInfo)
     def elsePathInfo = cond1.notNullInfoIf(false).seq(result.elsep.notNullInfo)
-    result.withNotNullInfo(
-      if result.thenp.tpe.isNothingType then
-        elsePathInfo.withRetracted(thenPathInfo)
-      else if result.elsep.tpe.isNothingType then
-        thenPathInfo.withRetracted(elsePathInfo)
-      else thenPathInfo.alt(elsePathInfo)
-    )
+    result.withNotNullInfo(thenPathInfo.alt(elsePathInfo))
   end typedIf
 
   /** Decompose function prototype into a list of parameter prototypes and a result
@@ -1875,14 +1869,9 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
   }
 
   private def notNullInfoFromCases(initInfo: NotNullInfo, cases: List[CaseDef])(using Context): NotNullInfo =
-    var nnInfo = initInfo
     if cases.nonEmpty then
-      val (nothingCases, normalCases) = cases.partition(_.body.tpe.isNothingType)
-      nnInfo = nothingCases.foldLeft(nnInfo):
-        (nni, c) => nni.withRetracted(c.notNullInfo)
-      if normalCases.nonEmpty then
-        nnInfo = nnInfo.seq(normalCases.map(_.notNullInfo).reduce(_.alt(_)))
-    nnInfo
+      initInfo.seq(cases.map(_.notNullInfo).reduce(_.alt(_)))
+    else initInfo
 
   def typedCases(cases: List[untpd.CaseDef], sel: Tree, wideSelType: Type, pt: Type)(using Context): List[CaseDef] =
     var caseCtx = ctx
@@ -1970,7 +1959,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
   def typedLabeled(tree: untpd.Labeled)(using Context): Labeled = {
     val bind1 = typedBind(tree.bind, WildcardType).asInstanceOf[Bind]
     val expr1 = typed(tree.expr, bind1.symbol.info)
-    assignType(cpy.Labeled(tree)(bind1, expr1))
+    assignType(cpy.Labeled(tree)(bind1, expr1)).withNotNullInfo(expr1.notNullInfo.retractedInfo)
   }
 
   /** Type a case of a type match */
@@ -2020,7 +2009,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
                             // Hence no adaptation is possible, and we assume WildcardType as prototype.
         (from, proto)
     val expr1 = typedExpr(tree.expr orElse untpd.syntheticUnitLiteral.withSpan(tree.span), proto)
-    assignType(cpy.Return(tree)(expr1, from))
+    assignType(cpy.Return(tree)(expr1, from)).withNotNullInfo(expr1.notNullInfo.terminatedInfo)
   end typedReturn
 
   def typedWhileDo(tree: untpd.WhileDo)(using Context): Tree =
@@ -2107,15 +2096,15 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
   def typedThrow(tree: untpd.Throw)(using Context): Tree =
     val expr1 = typed(tree.expr, defn.ThrowableType)
     val cap = checkCanThrow(expr1.tpe.widen, tree.span)
-    val res = Throw(expr1).withSpan(tree.span)
+    var res = Throw(expr1).withSpan(tree.span)
     if Feature.ccEnabled && !cap.isEmpty && !ctx.isAfterTyper then
       // Record access to the CanThrow capabulity recovered in `cap` by wrapping
-      // the type of the `throw` (i.e. Nothing) in a `@requiresCapability` annotatoon.
-      Typed(res,
+      // the type of the `throw` (i.e. Nothing) in a `@requiresCapability` annotation.
+      res = Typed(res,
         TypeTree(
           AnnotatedType(res.tpe,
             Annotation(defn.RequiresCapabilityAnnot, cap, tree.span))))
-    else res
+    res.withNotNullInfo(expr1.notNullInfo.terminatedInfo)
 
   def typedSeqLiteral(tree: untpd.SeqLiteral, pt: Type)(using Context): SeqLiteral = {
     val elemProto = pt.stripNull.elemType match {
diff --git a/tests/explicit-nulls/neg/flow-early-exit.scala b/tests/explicit-nulls/neg/flow-early-exit.scala
index 9b7e5fe628dc..77f17e470881 100644
--- a/tests/explicit-nulls/neg/flow-early-exit.scala
+++ b/tests/explicit-nulls/neg/flow-early-exit.scala
@@ -49,7 +49,7 @@ class Foo(x: String|Null) {
   def retTypeNothing(): String = {
     val y: String|Null = ???
     if (y == null) err("y is null!")
-    y
+    y // error
   }
 
   def errRetUnit(msg: String): Unit = {
diff --git a/tests/explicit-nulls/neg/flow-simple-var.scala b/tests/explicit-nulls/neg/flow-simple-var.scala
index 5ef50f8e8c6a..7dd81a3eb2fc 100644
--- a/tests/explicit-nulls/neg/flow-simple-var.scala
+++ b/tests/explicit-nulls/neg/flow-simple-var.scala
@@ -19,7 +19,7 @@ class SimpleVar {
     }
 
     assert(x != null)
-    val a: String = x
+    val a: String = x // error
     x = nullable(x)
     val b: String = x // error: x might be null
   }

From 252f4e38e7b4c2f385ec01499160d7bc405e03fd Mon Sep 17 00:00:00 2001
From: Tomasz Godzik <tgodzik@virtuslab.com>
Date: Wed, 12 Mar 2025 18:21:37 +0100
Subject: [PATCH 07/11] Add terminated info

[Cherry-picked f859afe8e4ace35e026600bb784664dcbcdbda98][modified]

From 4f53b9b1cd13d8d307d085bd9f902797109b4451 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Fri, 6 Dec 2024 16:59:32 +0100
Subject: [PATCH 08/11] Fix deep NotNullInfo

---
 .../dotty/tools/dotc/typer/Applications.scala |  7 ++-
 .../dotty/tools/dotc/typer/Nullables.scala    | 54 +++++++++++++------
 .../src/dotty/tools/dotc/typer/Typer.scala    |  1 -
 .../explicit-nulls/neg/flow-early-exit.scala  |  2 +-
 .../explicit-nulls/neg/flow-simple-var.scala  |  2 +-
 tests/explicit-nulls/neg/i21619.scala         | 15 +++++-
 6 files changed, 59 insertions(+), 22 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index f8594e1460a8..864c98dd475a 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -1058,7 +1058,7 @@ trait Applications extends Compatibility {
             case _ => ()
         else ()
 
-      fun1.tpe match {
+      val result = fun1.tpe match {
         case err: ErrorType => cpy.Apply(tree)(fun1, proto.typedArgs()).withType(err)
         case TryDynamicCallType =>
           val isInsertedApply = fun1 match {
@@ -1132,6 +1132,11 @@ trait Applications extends Compatibility {
                   else tryWithImplicitOnQualifier(fun1, proto).getOrElse(fail))
             }
       }
+
+      if result.tpe.isNothingType then
+        val nnInfo = result.notNullInfo
+        result.withNotNullInfo(nnInfo.terminatedInfo)
+      else result
     }
 
     /** Convert expression like
diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 723564cc52b8..d00137e4db3d 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -294,11 +294,29 @@ object Nullables:
       if !info.isEmpty then tree.putAttachment(NNInfo, info)
       tree
 
+    /* Collect the nullability info from parts of `tree` */
+    def collectNotNullInfo(using Context): NotNullInfo = tree match
+      case Typed(expr, _) =>
+        expr.notNullInfo
+      case Apply(fn, args) =>
+        val argsInfo = args.map(_.notNullInfo)
+        val fnInfo = fn.notNullInfo
+        argsInfo.foldLeft(fnInfo)(_ seq _)
+      case TypeApply(fn, _) =>
+        fn.notNullInfo
+      case _ =>
+        // Other cases are handled specially in typer.
+        NotNullInfo.empty
+
     /* The nullability info of `tree` */
     def notNullInfo(using Context): NotNullInfo =
-      stripInlined(tree).getAttachment(NNInfo) match
+      val tree1 = stripInlined(tree)
+      tree1.getAttachment(NNInfo) match
         case Some(info) if !ctx.erasedTypes => info
-        case _ => NotNullInfo.empty
+        case _ =>
+          val nnInfo = tree1.collectNotNullInfo
+          tree1.withNotNullInfo(nnInfo)
+          nnInfo
 
     /* The nullability info of `tree`, assuming it is a condition that evaluates to `c` */
     def notNullInfoIf(c: Boolean)(using Context): NotNullInfo =
@@ -379,21 +397,23 @@ object Nullables:
   end extension
 
   extension (tree: Assign)
-    def computeAssignNullable()(using Context): tree.type = tree.lhs match
-      case TrackedRef(ref) =>
-        val rhstp = tree.rhs.typeOpt
-        if ctx.explicitNulls && ref.isNullableUnion then
-          if rhstp.isNullType || rhstp.isNullableUnion then
-            // If the type of rhs is nullable (`T|Null` or `Null`), then the nullability of the
-            // lhs variable is no longer trackable. We don't need to check whether the type `T`
-            // is correct here, as typer will check it.
-            tree.withNotNullInfo(NotNullInfo(Set(), Set(ref)))
-          else
-            // If the initial type is nullable and the assigned value is non-null,
-            // we add it to the NotNull.
-            tree.withNotNullInfo(NotNullInfo(Set(ref), Set()))
-        else tree
-      case _ => tree
+    def computeAssignNullable()(using Context): tree.type =
+      var nnInfo = tree.rhs.notNullInfo
+      tree.lhs match
+        case TrackedRef(ref) if ctx.explicitNulls && ref.isNullableUnion =>
+          nnInfo = nnInfo.seq:
+            val rhstp = tree.rhs.typeOpt
+            if rhstp.isNullType || rhstp.isNullableUnion then
+              // If the type of rhs is nullable (`T|Null` or `Null`), then the nullability of the
+              // lhs variable is no longer trackable. We don't need to check whether the type `T`
+              // is correct here, as typer will check it.
+              NotNullInfo(Set(), Set(ref))
+            else
+              // If the initial type is nullable and the assigned value is non-null,
+              // we add it to the NotNull.
+              NotNullInfo(Set(ref), Set())
+        case _ =>
+      tree.withNotNullInfo(nnInfo)
   end extension
 
   private val analyzedOps = Set(nme.EQ, nme.NE, nme.eq, nme.ne, nme.ZAND, nme.ZOR, nme.UNARY_!)
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 6539c2c5513e..df7037e9f0f4 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1000,7 +1000,6 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
             untpd.unsplice(tree.expr).putAttachment(AscribedToUnit, ())
           typed(tree.expr, underlyingTreeTpe.tpe.widenSkolem)
       assignType(cpy.Typed(tree)(expr1, tpt), underlyingTreeTpe)
-        .withNotNullInfo(expr1.notNullInfo)
     }
 
     if (untpd.isWildcardStarArg(tree)) {
diff --git a/tests/explicit-nulls/neg/flow-early-exit.scala b/tests/explicit-nulls/neg/flow-early-exit.scala
index 77f17e470881..9b7e5fe628dc 100644
--- a/tests/explicit-nulls/neg/flow-early-exit.scala
+++ b/tests/explicit-nulls/neg/flow-early-exit.scala
@@ -49,7 +49,7 @@ class Foo(x: String|Null) {
   def retTypeNothing(): String = {
     val y: String|Null = ???
     if (y == null) err("y is null!")
-    y // error
+    y
   }
 
   def errRetUnit(msg: String): Unit = {
diff --git a/tests/explicit-nulls/neg/flow-simple-var.scala b/tests/explicit-nulls/neg/flow-simple-var.scala
index 7dd81a3eb2fc..5ef50f8e8c6a 100644
--- a/tests/explicit-nulls/neg/flow-simple-var.scala
+++ b/tests/explicit-nulls/neg/flow-simple-var.scala
@@ -19,7 +19,7 @@ class SimpleVar {
     }
 
     assert(x != null)
-    val a: String = x // error
+    val a: String = x
     x = nullable(x)
     val b: String = x // error: x might be null
   }
diff --git a/tests/explicit-nulls/neg/i21619.scala b/tests/explicit-nulls/neg/i21619.scala
index bfc03b61e1b7..2b89dfef7755 100644
--- a/tests/explicit-nulls/neg/i21619.scala
+++ b/tests/explicit-nulls/neg/i21619.scala
@@ -76,4 +76,17 @@ def test5: Unit =
   catch
     case _ =>
   val z1: String = x.replace("", "") // error
-  val z2: String = y.replace("", "") // error // LTS specific
\ No newline at end of file
+  val z2: String = y.replace("", "") // error // LTS specific
+
+def test6 = {
+  var x: String | Null = ""
+  var y: String = ""
+  x = ""
+  y = if (false) x else 1 match { // error
+    case _ => {
+      x = null
+      y
+    }
+  }
+  x.replace("", "") // error
+}

From 578c18b34698a3c2102da345720f31781a22d213 Mon Sep 17 00:00:00 2001
From: Tomasz Godzik <tgodzik@virtuslab.com>
Date: Wed, 12 Mar 2025 18:25:01 +0100
Subject: [PATCH 09/11] Fix deep NotNullInfo

[Cherry-picked 158af7deed473826b5d16ade6b9472fd89948b6d][modified]

From 5710a74129d205a123d92c300ef68f437bfa417b Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Sat, 7 Dec 2024 04:28:02 +0100
Subject: [PATCH 10/11] Treat asserted set of terminated NotNullInfo as
 universal set; fix test

[Cherry-picked 00430c042a9031059aefe638caba7c7e2e8c49f5]
---
 .../src/dotty/tools/dotc/core/Contexts.scala  |  6 ++---
 .../dotty/tools/dotc/typer/Nullables.scala    | 22 ++++++++++---------
 .../src/dotty/tools/dotc/typer/Typer.scala    |  2 ++
 .../pos/after-termination.scala               | 17 ++++++++++++++
 .../unsafe-common/unsafe-overload.scala       | 12 +++++-----
 5 files changed, 40 insertions(+), 19 deletions(-)
 create mode 100644 tests/explicit-nulls/pos/after-termination.scala

diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala
index 32790a647e2a..1a2764497e21 100644
--- a/compiler/src/dotty/tools/dotc/core/Contexts.scala
+++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala
@@ -755,13 +755,13 @@ object Contexts {
 
   extension (c: Context)
     def addNotNullInfo(info: NotNullInfo) =
-      c.withNotNullInfos(c.notNullInfos.extendWith(info))
+      if c.explicitNulls then c.withNotNullInfos(c.notNullInfos.extendWith(info)) else c
 
     def addNotNullRefs(refs: Set[TermRef]) =
-      c.addNotNullInfo(NotNullInfo(refs, Set()))
+      if c.explicitNulls then c.addNotNullInfo(NotNullInfo(refs, Set())) else c
 
     def withNotNullInfos(infos: List[NotNullInfo]): Context =
-      if c.notNullInfos eq infos then c else c.fresh.setNotNullInfos(infos)
+      if !c.explicitNulls || (c.notNullInfos eq infos) then c else c.fresh.setNotNullInfos(infos)
 
     def relaxedOverrideContext: Context =
       c.withModeBits(c.mode &~ Mode.SafeNulls | Mode.RelaxedOverriding)
diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index d00137e4db3d..53d32be7b3f3 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -210,7 +210,7 @@ object Nullables:
     */
     @tailrec def impliesNotNull(ref: TermRef): Boolean = infos match
       case info :: infos1 =>
-        if info.asserted != null && info.asserted.contains(ref) then true
+        if info.asserted == null || info.asserted.contains(ref) then true
         else if info.retracted.contains(ref) then false
         else infos1.impliesNotNull(ref)
       case _ =>
@@ -290,8 +290,8 @@ object Nullables:
   extension (tree: Tree)
 
     /* The `tree` with added nullability attachment */
-    def withNotNullInfo(info: NotNullInfo): tree.type =
-      if !info.isEmpty then tree.putAttachment(NNInfo, info)
+    def withNotNullInfo(info: NotNullInfo)(using Context): tree.type =
+      if ctx.explicitNulls && !info.isEmpty then tree.putAttachment(NNInfo, info)
       tree
 
     /* Collect the nullability info from parts of `tree` */
@@ -310,13 +310,15 @@ object Nullables:
 
     /* The nullability info of `tree` */
     def notNullInfo(using Context): NotNullInfo =
-      val tree1 = stripInlined(tree)
-      tree1.getAttachment(NNInfo) match
-        case Some(info) if !ctx.erasedTypes => info
-        case _ =>
-          val nnInfo = tree1.collectNotNullInfo
-          tree1.withNotNullInfo(nnInfo)
-          nnInfo
+      if !ctx.explicitNulls then NotNullInfo.empty
+      else
+        val tree1 = stripInlined(tree)
+        tree1.getAttachment(NNInfo) match
+          case Some(info) if !ctx.erasedTypes => info
+          case _ =>
+            val nnInfo = tree1.collectNotNullInfo
+            tree1.withNotNullInfo(nnInfo)
+            nnInfo
 
     /* The nullability info of `tree`, assuming it is a condition that evaluates to `c` */
     def notNullInfoIf(c: Boolean)(using Context): NotNullInfo =
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index df7037e9f0f4..3c3b0ceead7e 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -2514,6 +2514,8 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
     val vdef1 = assignType(cpy.ValDef(vdef)(name, tpt1, rhs1), sym)
     postProcessInfo(vdef1, sym)
     vdef1.setDefTree
+    val nnInfo = rhs1.notNullInfo
+    vdef1.withNotNullInfo(if sym.is(Lazy) then nnInfo.retractedInfo else nnInfo)
   }
 
   private def retractDefDef(sym: Symbol)(using Context): Tree =
diff --git a/tests/explicit-nulls/pos/after-termination.scala b/tests/explicit-nulls/pos/after-termination.scala
new file mode 100644
index 000000000000..00a57e371281
--- /dev/null
+++ b/tests/explicit-nulls/pos/after-termination.scala
@@ -0,0 +1,17 @@
+class C(val x: Int, val next: C | Null)
+
+def test1(x: String | Null, c: C | Null): Int =
+  return 0
+  // We know that the following code is unreachable,
+  // so we can treat `x`, `c`, and any variable/path non-nullable.
+  x.length + c.next.x
+
+def test2(x: String | Null, c: C | Null): Int =
+  throw new Exception()
+  x.length + c.next.x
+
+def fail(): Nothing = ???
+
+def test3(x: String | Null, c: C | Null): Int =
+  fail()
+  x.length + c.next.x
diff --git a/tests/explicit-nulls/unsafe-common/unsafe-overload.scala b/tests/explicit-nulls/unsafe-common/unsafe-overload.scala
index e7e551f1bda1..21af320806d8 100644
--- a/tests/explicit-nulls/unsafe-common/unsafe-overload.scala
+++ b/tests/explicit-nulls/unsafe-common/unsafe-overload.scala
@@ -16,8 +16,8 @@ class S {
   val o: O = ???
 
   locally {
-    def h1(hh: String => String) = ???
-    def h2(hh: Array[String] => Array[String]) = ???
+    def h1(hh: String => String): Unit = ???
+    def h2(hh: Array[String] => Array[String]): Unit = ???
     def f1(x: String | Null): String | Null = ???
     def f2(x: Array[String | Null]):  Array[String | Null] = ???
 
@@ -29,10 +29,10 @@ class S {
   }
 
   locally {
-    def h1(hh: String | Null => String | Null) = ???
-    def h2(hh: Array[String | Null] => Array[String | Null]) = ???
+    def h1(hh: String | Null => String | Null): Unit = ???
+    def h2(hh: Array[String | Null] => Array[String | Null]): Unit = ???
     def g1(x: String): String = ???
-    def g2(x: Array[String]):  Array[String] = ???
+    def g2(x: Array[String]): Array[String] = ???
 
     h1(g1) // error
     h1(o.g) // error
@@ -51,7 +51,7 @@ class S {
 
   locally {
     def g1(x: String): String = ???
-    def g2(x: Array[String]):  Array[String] = ???
+    def g2(x: Array[String]): Array[String] = ???
 
     o.i(g1) // error
     o.i(g2) // error

From 00f09acda0d5faa368d69864ae07f96e7190c4e1 Mon Sep 17 00:00:00 2001
From: noti0na1 <noti0na1@users.noreply.github.com>
Date: Tue, 10 Dec 2024 12:24:34 +0100
Subject: [PATCH 11/11] Comment on the empty cases in notNullInfoFromCases.

[Cherry-picked 200c038a818ed41d8a07a18b540abd0748a99f12]
---
 compiler/src/dotty/tools/dotc/typer/Typer.scala | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 3c3b0ceead7e..cad729da7e55 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1868,9 +1868,11 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
   }
 
   private def notNullInfoFromCases(initInfo: NotNullInfo, cases: List[CaseDef])(using Context): NotNullInfo =
-    if cases.nonEmpty then
-      initInfo.seq(cases.map(_.notNullInfo).reduce(_.alt(_)))
-    else initInfo
+    if cases.isEmpty then
+      // Empty cases is not allowed for match tree in the source code,
+      // but it can be generated by inlining: `tests/pos/i19198.scala`.
+      initInfo
+    else cases.map(_.notNullInfo).reduce(_.alt(_))
 
   def typedCases(cases: List[untpd.CaseDef], sel: Tree, wideSelType: Type, pt: Type)(using Context): List[CaseDef] =
     var caseCtx = ctx