From 585dda9587bc95afb936eb18751fbf850cf3209c 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 1/8] Refactor NotNullInfo to record every reference which is
 retracted once.

---
 .../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 3f071dad2d03..74623ed7b4e9 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -52,15 +52,19 @@ object Nullables:
     val hiTree = if(hiTpe eq hi.typeOpt) hi else TypeTree(hiTpe)
     TypeBoundsTree(lo, hiTree, 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 =
@@ -68,19 +72,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 6bb5d1ee70ff..588e4188c7bc 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1552,8 +1552,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
@@ -2350,10 +2352,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 f86a5638e4c8..de3cd5bafd6b 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 bcc9e68c778da3faa4dcb8b6c0258a48befff819 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 2/8] Use a different rule for NotNullInfo

---
 .../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 74623ed7b4e9..62d2ccfb7200 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -53,48 +53,35 @@ object Nullables:
     TypeBoundsTree(lo, hiTree, 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` */
@@ -247,16 +234,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 588e4188c7bc..8a72076527b9 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1553,9 +1553,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
@@ -2150,9 +2150,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, wideSelType0: Type, pt: Type)(using Context): List[CaseDef] =
@@ -2334,7 +2334,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.
@@ -2346,25 +2347,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 05c630acf9dd8b2ecb98f34b1f40bfc8ddb55ce8 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 3/8] Consider cases with Nothing type

---
 .../src/dotty/tools/dotc/typer/Typer.scala    | 24 ++++++++++++-------
 tests/explicit-nulls/neg/i21380b.scala        | 18 ++++++++++++++
 2 files changed, 34 insertions(+), 8 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 8a72076527b9..5731b44368e6 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1552,9 +1552,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)
     )
@@ -2141,20 +2141,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, wideSelType0: Type, pt: Type)(using Context): List[CaseDef] =
     var caseCtx = ctx
     var wideSelType = wideSelType0
diff --git a/tests/explicit-nulls/neg/i21380b.scala b/tests/explicit-nulls/neg/i21380b.scala
index 83e23053547c..e4d0caa9e32f 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() // ok
+
+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
   x.trim() // ok
\ No newline at end of file

From d44147bc6ff5496dab9cc1569274dfb4b673ee09 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 4/8] 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>
---
 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 62d2ccfb7200..e6d764dc1be4 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -52,8 +52,11 @@ object Nullables:
     val hiTree = if(hiTpe eq hi.typeOpt) hi else TypeTree(hiTpe)
     TypeBoundsTree(lo, hiTree, 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 5731b44368e6..392a4e18c454 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -2367,7 +2367,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 de3cd5bafd6b..9b7a721fbdf0 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 f859afe8e4ace35e026600bb784664dcbcdbda98 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 5/8] Add terminated info

---
 .../dotty/tools/dotc/typer/Nullables.scala    | 43 ++++++++++++-------
 .../src/dotty/tools/dotc/typer/Typer.scala    | 27 ++++--------
 2 files changed, 36 insertions(+), 34 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index e6d764dc1be4..30c65771d9c2 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -53,37 +53,45 @@ object Nullables:
     TypeBoundsTree(lo, hiTree, 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
 
@@ -227,7 +235,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 _ =>
@@ -243,7 +251,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
@@ -516,7 +526,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 392a4e18c454..5ec9dbbe28b9 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1551,13 +1551,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
@@ -2154,14 +2148,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, wideSelType0: Type, pt: Type)(using Context): List[CaseDef] =
     var caseCtx = ctx
@@ -2251,7 +2240,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 */
@@ -2301,7 +2290,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 =
@@ -2388,15 +2377,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` annotation.
-      Typed(res,
+      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 {

From 158af7deed473826b5d16ade6b9472fd89948b6d 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 6/8] 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 -
 tests/explicit-nulls/neg/i21619.scala         | 15 +++++-
 4 files changed, 57 insertions(+), 20 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index 41e48f7595dc..96c38bcc80af 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -1134,7 +1134,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 {
@@ -1208,6 +1208,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 30c65771d9c2..2193866893f6 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -319,11 +319,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 =
@@ -404,21 +422,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 5ec9dbbe28b9..1e461a5e1cb7 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1201,7 +1201,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/i21619.scala b/tests/explicit-nulls/neg/i21619.scala
index 244f993fd4e1..d7af27e3fe64 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("", "")
\ No newline at end of file
+  val z2: String = y.replace("", "")
+
+def test6 = {
+  var x: String | Null = ""
+  var y: String = ""
+  x = ""
+  y = if (false) x else 1 match {
+    case _ => {
+      x = null
+      y
+    }
+  }
+  x.replace("", "") // error
+}
\ No newline at end of file

From 00430c042a9031059aefe638caba7c7e2e8c49f5 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 7/8] Treat asserted set of terminated NotNullInfo as universal
 set; fix test

---
 .../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 d69c7408d0b1..7f5779bb6127 100644
--- a/compiler/src/dotty/tools/dotc/core/Contexts.scala
+++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala
@@ -777,13 +777,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 2193866893f6..310ca999f4c5 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -235,7 +235,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 _ =>
@@ -315,8 +315,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` */
@@ -335,13 +335,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 1e461a5e1cb7..cea47817bb88 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -2849,6 +2849,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 200c038a818ed41d8a07a18b540abd0748a99f12 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 8/8] Comment on the empty cases in notNullInfoFromCases.

---
 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 cea47817bb88..2c513a41a039 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -2147,9 +2147,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, wideSelType0: Type, pt: Type)(using Context): List[CaseDef] =
     var caseCtx = ctx