From 6e271a7798a233e95f3de0867b07bddcd968a861 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 14:06:45 +0100
Subject: [PATCH 01/37] Thread context through typedStats

---
 .../dotty/tools/dotc/transform/Erasure.scala  |  5 ++--
 .../tools/dotc/transform/TreeChecker.scala    |  2 +-
 .../dotty/tools/dotc/typer/Docstrings.scala   |  2 +-
 .../src/dotty/tools/dotc/typer/Namer.scala    |  4 ++-
 .../src/dotty/tools/dotc/typer/Typer.scala    | 28 ++++++++++---------
 5 files changed, 23 insertions(+), 18 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/Erasure.scala b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
index df8a3f8ca449..5f72f9214584 100644
--- a/compiler/src/dotty/tools/dotc/transform/Erasure.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
@@ -740,11 +740,12 @@ object Erasure {
     override def typedAnnotated(tree: untpd.Annotated, pt: Type)(implicit ctx: Context): Tree =
       typed(tree.arg, pt)
 
-    override def typedStats(stats: List[untpd.Tree], exprOwner: Symbol)(implicit ctx: Context): List[Tree] = {
+    override def typedStats(stats: List[untpd.Tree], exprOwner: Symbol)(implicit ctx: Context): (List[Tree], Context) = {
       val stats1 =
         if (takesBridges(ctx.owner)) new Bridges(ctx.owner.asClass, erasurePhase).add(stats)
         else stats
-      super.typedStats(stats1, exprOwner).filter(!_.isEmpty)
+      val (stats2, finalCtx) = super.typedStats(stats1, exprOwner)
+      (stats2.filter(!_.isEmpty), finalCtx)
     }
 
     override def adapt(tree: Tree, pt: Type, locked: TypeVars)(implicit ctx: Context): Tree =
diff --git a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
index d20105ae2586..3433be335086 100644
--- a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
@@ -466,7 +466,7 @@ class TreeChecker extends Phase with SymTransformer {
      *  is that we should be able to pull out an expression as an initializer
      *  of a helper value without having to do a change owner traversal of the expression.
      */
-    override def typedStats(trees: List[untpd.Tree], exprOwner: Symbol)(implicit ctx: Context): List[Tree] = {
+    override def typedStats(trees: List[untpd.Tree], exprOwner: Symbol)(implicit ctx: Context): (List[Tree], Context) = {
       for (tree <- trees) tree match {
         case tree: untpd.DefTree => checkOwner(tree)
         case _: untpd.Thicket => assert(false, i"unexpanded thicket $tree in statement sequence $trees%\n%")
diff --git a/compiler/src/dotty/tools/dotc/typer/Docstrings.scala b/compiler/src/dotty/tools/dotc/typer/Docstrings.scala
index a7fe1ac69b9c..7bedf6033b45 100644
--- a/compiler/src/dotty/tools/dotc/typer/Docstrings.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Docstrings.scala
@@ -33,7 +33,7 @@ object Docstrings {
         expandComment(sym).map { expanded =>
           val typedUsecases = expanded.usecases.map { usecase =>
             ctx.typer.enterSymbol(ctx.typer.createSymbol(usecase.untpdCode))
-            ctx.typer.typedStats(usecase.untpdCode :: Nil, owner) match {
+            ctx.typer.typedStats(usecase.untpdCode :: Nil, owner)._1 match {
               case List(df: tpd.DefDef) =>
                 usecase.typed(df)
               case _ =>
diff --git a/compiler/src/dotty/tools/dotc/typer/Namer.scala b/compiler/src/dotty/tools/dotc/typer/Namer.scala
index 3d8583b78c6e..0228d7dc8ba5 100644
--- a/compiler/src/dotty/tools/dotc/typer/Namer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala
@@ -559,7 +559,9 @@ class Namer { typer: Typer =>
     case _ => ()
   }
 
-  /** Create top-level symbols for statements and enter them into symbol table */
+  /** Create top-level symbols for statements and enter them into symbol table
+   *  @return A context that reflects all imports in `stats`.
+   */
   def index(stats: List[Tree])(implicit ctx: Context): Context = {
 
     // module name -> (stat, moduleCls | moduleVal)
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 505da8883248..5808660d9964 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -754,13 +754,14 @@ class Typer extends Namer
         }
     }
 
-  def typedBlockStats(stats: List[untpd.Tree])(implicit ctx: Context): (Context, List[tpd.Tree]) =
-    (index(stats), typedStats(stats, ctx.owner))
+  def typedBlockStats(stats: List[untpd.Tree])(implicit ctx: Context): (List[tpd.Tree], Context) =
+    index(stats)
+    typedStats(stats, ctx.owner)
 
   def typedBlock(tree: untpd.Block, pt: Type)(implicit ctx: Context): Tree = {
     val localCtx = ctx.retractMode(Mode.Pattern)
-    val (exprCtx, stats1) = typedBlockStats(tree.stats)(given localCtx)
-    val expr1 = typedExpr(tree.expr, pt.dropIfProto)(exprCtx)
+    val (stats1, exprCtx) = typedBlockStats(tree.stats)(given localCtx)
+    val expr1 = typedExpr(tree.expr, pt.dropIfProto)(given exprCtx)
     ensureNoLocalRefs(
       cpy.Block(tree)(stats1, expr1).withType(expr1.tpe), pt, localSyms(stats1))
   }
@@ -1291,7 +1292,7 @@ class Typer extends Namer
   }
 
   def typedInlined(tree: untpd.Inlined, pt: Type)(implicit ctx: Context): Tree = {
-    val (exprCtx, bindings1) = typedBlockStats(tree.bindings)
+    val (bindings1, exprCtx) = typedBlockStats(tree.bindings)
     val expansion1 = typed(tree.expansion, pt)(inlineContext(tree.call)(exprCtx))
     assignType(cpy.Inlined(tree)(tree.call, bindings1.asInstanceOf[List[MemberDef]], expansion1),
         bindings1, expansion1)
@@ -1728,7 +1729,7 @@ class Typer extends Namer
     else {
       val dummy = localDummy(cls, impl)
       val body1 = addAccessorDefs(cls,
-        typedStats(impl.body, dummy)(ctx.inClassContext(self1.symbol)))
+        typedStats(impl.body, dummy)(ctx.inClassContext(self1.symbol))._1)
 
       checkNoDoubleDeclaration(cls)
       val impl1 = cpy.Template(impl)(constr1, parents1, Nil, self1, body1)
@@ -1848,9 +1849,9 @@ class Typer extends Namer
       case pid1: RefTree if pkg.exists =>
         if (!pkg.is(Package)) ctx.error(PackageNameAlreadyDefined(pkg), tree.sourcePos)
         val packageCtx = ctx.packageContext(tree, pkg)
-        var stats1 = typedStats(tree.stats, pkg.moduleClass)(packageCtx)
+        var stats1 = typedStats(tree.stats, pkg.moduleClass)(packageCtx)._1
         if (!ctx.isAfterTyper)
-          stats1 = stats1 ++ typedBlockStats(MainProxies.mainProxies(stats1))(packageCtx)._2
+          stats1 = stats1 ++ typedBlockStats(MainProxies.mainProxies(stats1))(packageCtx)._1
         cpy.PackageDef(tree)(pid1, stats1).withType(pkg.termRef)
       case _ =>
         // Package will not exist if a duplicate type has already been entered, see `tests/neg/1708.scala`
@@ -2167,11 +2168,11 @@ class Typer extends Namer
   def typedTrees(trees: List[untpd.Tree])(implicit ctx: Context): List[Tree] =
     trees mapconserve (typed(_))
 
-  def typedStats(stats: List[untpd.Tree], exprOwner: Symbol)(implicit ctx: Context): List[Tree] = {
+  def typedStats(stats: List[untpd.Tree], exprOwner: Symbol)(implicit ctx: Context): (List[Tree], Context) = {
     val buf = new mutable.ListBuffer[Tree]
     val enumContexts = new mutable.HashMap[Symbol, Context]
       // A map from `enum` symbols to the contexts enclosing their definitions
-    @tailrec def traverse(stats: List[untpd.Tree])(implicit ctx: Context): List[Tree] = stats match {
+    @tailrec def traverse(stats: List[untpd.Tree])(implicit ctx: Context): (List[Tree], Context) = stats match {
       case (imp: untpd.Import) :: rest =>
         val imp1 = typed(imp)
         buf += imp1
@@ -2208,7 +2209,7 @@ class Typer extends Namer
         buf += stat1
         traverse(rest)
       case nil =>
-        buf.toList
+        (buf.toList, ctx)
     }
     val localCtx = {
       val exprOwnerOpt = if (exprOwner == ctx.owner) None else Some(exprOwner)
@@ -2225,9 +2226,10 @@ class Typer extends Namer
       case _ =>
         stat
     }
-    val stats1 = traverse(stats)(localCtx).mapConserve(finalize)
+    val (stats0, finalCtx) = traverse(stats)(localCtx)
+    val stats1 = stats0.mapConserve(finalize)
     if (ctx.owner == exprOwner) checkNoAlphaConflict(stats1)
-    stats1
+    (stats1, finalCtx)
   }
 
   /** Given an inline method `mdef`, the method rewritten so that its body

From 435024a83a03975a60100007dbc30c17f14f7112 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 14:35:40 +0100
Subject: [PATCH 02/37] Nullability prototype

---
 .../src/dotty/tools/dotc/ast/TreeInfo.scala   | 27 +++++-
 .../src/dotty/tools/dotc/core/Contexts.scala  | 26 ++++-
 .../dotty/tools/dotc/typer/Applications.scala |  6 +-
 .../dotty/tools/dotc/typer/Nullables.scala    | 94 +++++++++++++++++++
 .../src/dotty/tools/dotc/typer/Typer.scala    | 69 ++++++++++----
 5 files changed, 197 insertions(+), 25 deletions(-)
 create mode 100644 compiler/src/dotty/tools/dotc/typer/Nullables.scala

diff --git a/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala b/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
index 8cdb7ce38e85..0557c8aa6a3c 100644
--- a/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
+++ b/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
@@ -4,7 +4,7 @@ package ast
 
 import core._
 import Flags._, Trees._, Types._, Contexts._
-import Names._, StdNames._, NameOps._, Symbols._
+import Names._, StdNames._, NameOps._, Symbols._, Constants._
 import typer.ConstFold
 import reporting.trace
 import dotty.tools.dotc.transform.SymUtils._
@@ -648,6 +648,31 @@ trait TypedTreeInfo extends TreeInfo[Type] { self: Trees.Instance[Type] =>
     acc(Nil, tree)
   }
 
+  /** An extractor for null comparisons */
+  object CompareNull with
+
+    /** Matches one of
+     *
+     *    tree == null, tree eq null, null == tree, null eq tree
+     *    tree != null, tree ne null, null != tree, null ne tree
+     *
+     *  The second boolean result is true for equality tests, false for inequality tests
+     */
+    def unapply(tree: Tree)(given Context): Option[(Tree, Boolean)] = tree match
+      case Apply(Select(l, _), Literal(Constant(null)) :: Nil) =>
+        testSym(tree.symbol, l)
+      case Apply(Select(Literal(Constant(null)), _), r :: Nil) =>
+        testSym(tree.symbol, r)
+      case _ =>
+        None
+
+    private def testSym(sym: Symbol, operand: Tree)(given Context) =
+      if sym == defn.Any_== || sym == defn.Object_eq then Some((operand, true))
+      else if sym == defn.Any_!= || sym == defn.Object_ne then Some((operand, false))
+      else None
+
+  end CompareNull
+
   /** Is this pattern node a catch-all or type-test pattern? */
   def isCatchCase(cdef: CaseDef)(implicit ctx: Context): Boolean = cdef match {
     case CaseDef(Typed(Ident(nme.WILDCARD), tpt), EmptyTree, _) =>
diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala
index 679c43f76a36..fce4834feb4c 100644
--- a/compiler/src/dotty/tools/dotc/core/Contexts.scala
+++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala
@@ -15,7 +15,8 @@ import ast.Trees._
 import ast.untpd
 import Flags.GivenOrImplicit
 import util.{FreshNameCreator, NoSource, SimpleIdentityMap, SourceFile}
-import typer.{Implicits, ImportInfo, Inliner, NamerContextOps, SearchHistory, SearchRoot, TypeAssigner, Typer}
+import typer.{Implicits, ImportInfo, Inliner, NamerContextOps, SearchHistory, SearchRoot, TypeAssigner, Typer, Nullables}
+import Nullables.given
 import Implicits.ContextualImplicits
 import config.Settings._
 import config.Config
@@ -47,7 +48,11 @@ object Contexts {
   private val (compilationUnitLoc,  store6) = store5.newLocation[CompilationUnit]()
   private val (runLoc,              store7) = store6.newLocation[Run]()
   private val (profilerLoc,         store8) = store7.newLocation[Profiler]()
-  private val initialStore = store8
+  private val (notNullRefsLoc,      store9) = store8.newLocation[List[Nullables.Excluded]]()
+  private val initialStore = store9
+
+  /** The current context */
+  def curCtx(given ctx: Context): Context = ctx
 
   /** A context is passed basically everywhere in dotc.
    *  This is convenient but carries the risk of captured contexts in
@@ -207,6 +212,9 @@ object Contexts {
     /**  The current compiler-run profiler */
     def profiler: Profiler = store(profilerLoc)
 
+    /** The paths currently known to be not null */
+    def notNullRefs = store(notNullRefsLoc)
+
     /** The new implicit references that are introduced by this scope */
     protected var implicitsCache: ContextualImplicits = null
     def implicits: ContextualImplicits = {
@@ -556,6 +564,7 @@ object Contexts {
     def setRun(run: Run): this.type = updateStore(runLoc, run)
     def setProfiler(profiler: Profiler): this.type = updateStore(profilerLoc, profiler)
     def setFreshNames(freshNames: FreshNameCreator): this.type = updateStore(freshNamesLoc, freshNames)
+    def setNotNullRefs(notNullRefs: List[Nullables.Excluded]): this.type = updateStore(notNullRefsLoc, notNullRefs)
 
     def setProperty[T](key: Key[T], value: T): this.type =
       setMoreProperties(moreProperties.updated(key, value))
@@ -587,6 +596,15 @@ object Contexts {
     def setDebug: this.type = setSetting(base.settings.Ydebug, true)
   }
 
+  given (c: Context)
+    def addExcluded(refs: Nullables.Excluded) =
+      if c.notNullRefs.containsAll(refs) then c
+      else c.fresh.setNotNullRefs(refs :: c.notNullRefs)
+
+    def withNotNullRefs(nnrefs: List[Nullables.Excluded]): Context =
+      if c.notNullRefs eq nnrefs then c else c.fresh.setNotNullRefs(nnrefs)
+
+  // TODO: Fix issue when converting ModeChanges and FreshModeChanges to extension givens
   implicit class ModeChanges(val c: Context) extends AnyVal {
     final def withModeBits(mode: Mode): Context =
       if (mode != c.mode) c.fresh.setMode(mode) else c
@@ -615,7 +633,9 @@ object Contexts {
     typeAssigner = TypeAssigner
     moreProperties = Map.empty
     source = NoSource
-    store = initialStore.updated(settingsStateLoc, settingsGroup.defaultState)
+    store = initialStore
+      .updated(settingsStateLoc, settingsGroup.defaultState)
+      .updated(notNullRefsLoc, Nil)
     typeComparer = new TypeComparer(this)
     searchHistory = new SearchRoot
     gadt = EmptyGadtConstraint
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index cc3641f1c94f..f3811862a8ad 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -22,6 +22,7 @@ import NameKinds.DefaultGetterName
 import ProtoTypes._
 import Inferencing._
 import transform.TypeUtils._
+import Nullables.given
 
 import collection.mutable
 import config.Printers.{overload, typr, unapp}
@@ -864,8 +865,9 @@ trait Applications extends Compatibility {
               if (proto.allArgTypesAreCurrent())
                 new ApplyToTyped(tree, fun1, funRef, proto.unforcedTypedArgs, pt)
               else
-                new ApplyToUntyped(tree, fun1, funRef, proto, pt)(argCtx(tree))
-            convertNewGenericArray(app.result)
+                new ApplyToUntyped(tree, fun1, funRef, proto, pt)(
+                  fun1.nullableInArgContext(given argCtx(tree)))
+            convertNewGenericArray(app.result).computeNullable
           case _ =>
             handleUnexpectedFunType(tree, fun1)
         }
diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
new file mode 100644
index 000000000000..cee6f657d8c5
--- /dev/null
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -0,0 +1,94 @@
+package dotty.tools
+package dotc
+package typer
+
+import core._
+import Types._, Contexts._, Symbols._, Decorators._
+import annotation.tailrec
+import util.Property
+
+/** Operations for implementing a flow analysis for nullability */
+object Nullables with
+  import ast.tpd._
+
+  type Excluded = Set[TermRef]
+
+  case class EitherExcluded(ifTrue: Excluded, ifFalse: Excluded) with
+    def isEmpty = ifTrue.isEmpty && ifFalse.isEmpty
+
+  val NoneExcluded = EitherExcluded(Set(), Set())
+
+  /** An attachment that represents conditional flow facts established
+   *  by this tree, which represents a condition.
+   */
+  private[typer] val CondExcluded = Property.Key[Nullables.EitherExcluded]
+
+   /** An attachment that represents unconditional flow facts established
+    *  by this tree.
+    */
+  private[typer] val AlwaysExcluded = Property.Key[Nullables.Excluded]
+
+  given (excluded: List[Excluded])
+    def containsRef(ref: TermRef): Boolean =
+      excluded.exists(_.contains(ref))
+
+    def containsAll(refs: Set[TermRef]): Boolean =
+      refs.forall(excluded.containsRef(_))
+
+  given (tree: Tree)
+    def withNotNullRefs(refs: Excluded): tree.type =
+      if refs.nonEmpty then tree.putAttachment(AlwaysExcluded, refs)
+      tree
+
+    def notNullRefs(given Context): Excluded =
+      tree.getAttachment(AlwaysExcluded) match
+        case Some(cond) if !curCtx.isAfterTyper => cond
+        case _ => Set.empty
+
+    def condNotNullRefs(given Context): EitherExcluded =
+      stripBlock(tree).getAttachment(CondExcluded) match
+        case Some(cond) if !curCtx.isAfterTyper => cond
+        case _ => NoneExcluded
+
+    def nullableContext(given Context): Context =
+      val excl = tree.notNullRefs
+      if excl.isEmpty then curCtx else curCtx.addExcluded(excl)
+
+    def nullableContext(tru: Boolean)(given Context): Context =
+      val excl = tree.condNotNullRefs
+      if excl.isEmpty then curCtx
+      else curCtx.addExcluded(if tru then excl.ifTrue else excl.ifFalse)
+
+    def nullableInArgContext(given Context): Context = tree match
+      case Select(x, _) if !curCtx.isAfterTyper =>
+        if tree.symbol == defn.Boolean_&& then x.nullableContext(true)
+        else if tree.symbol == defn.Boolean_|| then x.nullableContext(false)
+        else curCtx
+      case _ => curCtx
+
+    def computeNullable(given Context): tree.type =
+      def setExcluded(ifTrue: Excluded, ifFalse: Excluded) =
+        tree.putAttachment(CondExcluded, EitherExcluded(ifTrue, ifFalse))
+      if !curCtx.isAfterTyper then tree match
+        case CompareNull(x, isEqual) =>
+          x.tpe match
+            case ref: TermRef if ref.isStable =>
+              if isEqual then setExcluded(Set(), Set(ref))
+              else setExcluded(Set(ref), Set())
+            case _ =>
+        case Apply(Select(x, _), y :: Nil) =>
+          val xc = x.condNotNullRefs
+          val yc = y.condNotNullRefs
+          if !(xc.isEmpty && yc.isEmpty) then
+            if tree.symbol == defn.Boolean_&& then
+              setExcluded(xc.ifTrue | yc.ifTrue, xc.ifFalse & yc.ifFalse)
+            else if tree.symbol == defn.Boolean_|| then
+              setExcluded(xc.ifTrue & yc.ifTrue, xc.ifFalse | yc.ifFalse)
+        case Apply(Select(x, _), Nil) if tree.symbol == defn.Boolean_! =>
+          val xc = x.condNotNullRefs
+          if !xc.isEmpty then
+            setExcluded(xc.ifFalse, xc.ifTrue)
+        case _ =>
+      tree
+
+end Nullables
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 5808660d9964..d60034ff47ac 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -40,6 +40,7 @@ import dotty.tools.dotc.transform.{PCPCheckAndHeal, Staging, TreeMapWithStages}
 import transform.SymUtils._
 import transform.TypeUtils._
 import reporting.trace
+import Nullables.given
 
 object Typer {
 
@@ -78,8 +79,6 @@ object Typer {
    */
   private[typer] val HiddenSearchFailure = new Property.Key[SearchFailure]
 }
-
-
 class Typer extends Namer
                with TypeAssigner
                with Applications
@@ -634,6 +633,7 @@ class Typer extends Namer
         else if (isWildcard) tree.expr.withType(tpt.tpe)
         else typed(tree.expr, tpt.tpe.widenSkolem)
       assignType(cpy.Typed(tree)(expr1, tpt), underlyingTreeTpe)
+        .withNotNullRefs(expr1.notNullRefs)
     }
 
     if (untpd.isWildcardStarArg(tree)) {
@@ -763,7 +763,10 @@ class Typer extends Namer
     val (stats1, exprCtx) = typedBlockStats(tree.stats)(given localCtx)
     val expr1 = typedExpr(tree.expr, pt.dropIfProto)(given exprCtx)
     ensureNoLocalRefs(
-      cpy.Block(tree)(stats1, expr1).withType(expr1.tpe), pt, localSyms(stats1))
+      cpy.Block(tree)(stats1, expr1)
+        .withType(expr1.tpe)
+        .withNotNullRefs(stats1.foldLeft(expr1.notNullRefs)(_ | _.notNullRefs)),
+      pt, localSyms(stats1))
   }
 
   def escapingRefs(block: Tree, localSyms: => List[Symbol])(implicit ctx: Context): collection.Set[NamedType] = {
@@ -804,21 +807,30 @@ class Typer extends Namer
     }
   }
 
-  def typedIf(tree: untpd.If, pt: Type)(implicit ctx: Context): Tree = {
-    if (tree.isInline) checkInInlineContext("inline if", tree.posd)
+  def typedIf(tree: untpd.If, pt: Type)(implicit ctx: Context): Tree =
+    if tree.isInline then checkInInlineContext("inline if", tree.posd)
     val cond1 = typed(tree.cond, defn.BooleanType)
 
-    if (tree.elsep.isEmpty) {
-      val thenp1 = typed(tree.thenp, defn.UnitType)
-      val elsep1 = tpd.unitLiteral.withSpan(tree.span.endPos)
-      cpy.If(tree)(cond1, thenp1, elsep1).withType(defn.UnitType)
-    }
-    else {
-      val thenp1 :: elsep1 :: Nil = harmonic(harmonize, pt)(
-        (tree.thenp :: tree.elsep :: Nil).map(typed(_, pt.dropIfProto)))
-      assignType(cpy.If(tree)(cond1, thenp1, elsep1), thenp1, elsep1)
-    }
-  }
+    val result =
+      if tree.elsep.isEmpty then
+        val thenp1 = typed(tree.thenp, defn.UnitType)(given cond1.nullableContext(true))
+        val elsep1 = tpd.unitLiteral.withSpan(tree.span.endPos)
+        cpy.If(tree)(cond1, thenp1, elsep1).withType(defn.UnitType)
+      else
+        val thenp1 :: elsep1 :: Nil = harmonic(harmonize, pt) {
+          val thenp0 = typed(tree.thenp, pt.dropIfProto)(given cond1.nullableContext(true))
+          val elsep0 = typed(tree.elsep, pt.dropIfProto)(given cond1.nullableContext(false))
+          thenp0 :: elsep0 :: Nil
+        }
+        assignType(cpy.If(tree)(cond1, thenp1, elsep1), thenp1, elsep1)
+
+    if result.thenp.tpe.isRef(defn.NothingClass) then
+      result.withNotNullRefs(cond1.condNotNullRefs.ifFalse)
+    else if result.elsep.tpe.isRef(defn.NothingClass) then
+      result.withNotNullRefs(cond1.condNotNullRefs.ifTrue)
+    else
+      result
+  end typedIf
 
   /** Decompose function prototype into a list of parameter prototypes and a result prototype
    *  tree, using WildcardTypes where a type is not known.
@@ -1242,8 +1254,9 @@ class Typer extends Namer
     val cond1 =
       if (tree.cond eq EmptyTree) EmptyTree
       else typed(tree.cond, defn.BooleanType)
-    val body1 = typed(tree.body, defn.UnitType)
+    val body1 = typed(tree.body, defn.UnitType)(given cond1.nullableContext(true))
     assignType(cpy.WhileDo(tree)(cond1, body1))
+      .withNotNullRefs(cond1.condNotNullRefs.ifFalse)
   }
 
   def typedTry(tree: untpd.Try, pt: Type)(implicit ctx: Context): Try = {
@@ -1531,6 +1544,16 @@ class Typer extends Namer
     typed(annot, defn.AnnotationClass.typeRef)
 
   def typedValDef(vdef: untpd.ValDef, sym: Symbol)(implicit ctx: Context): Tree = {
+    sym.infoOrCompleter match
+      case completer: Namer#Completer
+      if completer.creationContext.notNullRefs ne ctx.notNullRefs =>
+        // The RHS of a val def should know about not null facts established
+        // in preceding statements (unless the ValDef is completed ahead of time,
+        // then it is impossible).
+        vdef.symbol.info = Completer(completer.original)(
+          given completer.creationContext.withNotNullRefs(ctx.notNullRefs))
+      case _ =>
+
     val ValDef(name, tpt, _) = vdef
     completeAnnotations(vdef, sym)
     if (sym.isOneOf(GivenOrImplicit)) checkImplicitConversionDefOK(sym)
@@ -2171,6 +2194,7 @@ class Typer extends Namer
   def typedStats(stats: List[untpd.Tree], exprOwner: Symbol)(implicit ctx: Context): (List[Tree], Context) = {
     val buf = new mutable.ListBuffer[Tree]
     val enumContexts = new mutable.HashMap[Symbol, Context]
+    val initialNotNullRefs = ctx.notNullRefs
       // A map from `enum` symbols to the contexts enclosing their definitions
     @tailrec def traverse(stats: List[untpd.Tree])(implicit ctx: Context): (List[Tree], Context) = stats match {
       case (imp: untpd.Import) :: rest =>
@@ -2182,7 +2206,14 @@ class Typer extends Namer
           case Some(xtree) =>
             traverse(xtree :: rest)
           case none =>
-            typed(mdef) match {
+            val defCtx = mdef match
+              // Keep preceding not null facts in the current context only if `mdef`
+              // cannot be executed out-of-sequence.
+              case _: ValDef if !mdef.mods.is(Lazy) && ctx.owner.isTerm =>
+                ctx // all preceding statements will have been executed in this case
+              case _ =>
+                ctx.withNotNullRefs(initialNotNullRefs)
+            typed(mdef)(given defCtx) match {
               case mdef1: DefDef if !Inliner.bodyToInline(mdef1.symbol).isEmpty =>
                 buf += inlineExpansion(mdef1)
                   // replace body with expansion, because it will be used as inlined body
@@ -2207,7 +2238,7 @@ class Typer extends Namer
         val stat1 = typed(stat)(ctx.exprContext(stat, exprOwner))
         checkStatementPurity(stat1)(stat, exprOwner)
         buf += stat1
-        traverse(rest)
+        traverse(rest)(given stat1.nullableContext)
       case nil =>
         (buf.toList, ctx)
     }

From 06f72db7158b9e96f2332e72cff61281a99d1f93 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 17:44:42 +0100
Subject: [PATCH 03/37] Add extractor for comparisons of null and a path

Also, doc comments for Nullables.scala
---
 .../src/dotty/tools/dotc/ast/TreeInfo.scala   | 11 +++++
 .../dotty/tools/dotc/typer/Nullables.scala    | 43 ++++++++++++++-----
 2 files changed, 43 insertions(+), 11 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala b/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
index 0557c8aa6a3c..47343cabd498 100644
--- a/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
+++ b/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
@@ -673,6 +673,17 @@ trait TypedTreeInfo extends TreeInfo[Type] { self: Trees.Instance[Type] =>
 
   end CompareNull
 
+  /** An extractor for comparisons between a path and null. */
+  object ComparePathNull with
+    def unapply(tree: Tree)(given Context): Option[(TermRef, Boolean)] =
+      CompareNull.unapply(tree) match
+        case some @ Some((x, testEqual)) =>
+          x.tpe match
+            case ref: TermRef if ref.isStable => Some((ref, testEqual))
+            case _ => None
+        case none => None
+  end ComparePathNull
+
   /** Is this pattern node a catch-all or type-test pattern? */
   def isCatchCase(cdef: CaseDef)(implicit ctx: Context): Boolean = cdef match {
     case CaseDef(Typed(Ident(nme.WILDCARD), tpt), EmptyTree, _) =>
diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index cee6f657d8c5..427a723e4c09 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -11,8 +11,10 @@ import util.Property
 object Nullables with
   import ast.tpd._
 
+  /** A set of paths that are known to be not null */
   type Excluded = Set[TermRef]
 
+  /** A pair of not-null sets, depending on whether a condition is `true` or `false` */
   case class EitherExcluded(ifTrue: Excluded, ifFalse: Excluded) with
     def isEmpty = ifTrue.isEmpty && ifFalse.isEmpty
 
@@ -21,12 +23,12 @@ object Nullables with
   /** An attachment that represents conditional flow facts established
    *  by this tree, which represents a condition.
    */
-  private[typer] val CondExcluded = Property.Key[Nullables.EitherExcluded]
+  private[typer] val CondExcluded = Property.StickyKey[Nullables.EitherExcluded]
 
    /** An attachment that represents unconditional flow facts established
     *  by this tree.
     */
-  private[typer] val AlwaysExcluded = Property.Key[Nullables.Excluded]
+  private[typer] val AlwaysExcluded = Property.StickyKey[Nullables.Excluded]
 
   given (excluded: List[Excluded])
     def containsRef(ref: TermRef): Boolean =
@@ -36,29 +38,45 @@ object Nullables with
       refs.forall(excluded.containsRef(_))
 
   given (tree: Tree)
+
+    /* The `tree` with added attachment stating that all paths in `refs` are not-null */
     def withNotNullRefs(refs: Excluded): tree.type =
       if refs.nonEmpty then tree.putAttachment(AlwaysExcluded, refs)
       tree
 
+    /* The paths that are known to be not null after execution of `tree` terminates normally */
     def notNullRefs(given Context): Excluded =
       tree.getAttachment(AlwaysExcluded) match
-        case Some(cond) if !curCtx.isAfterTyper => cond
+        case Some(excl) if !curCtx.isAfterTyper => excl
         case _ => Set.empty
 
+    /** The paths that are known to be not null if the condition represented
+     *  by `tree` yields `true` or `false`. Two empty sets if `tree` is not
+     *  a condition.
+     */
     def condNotNullRefs(given Context): EitherExcluded =
       stripBlock(tree).getAttachment(CondExcluded) match
-        case Some(cond) if !curCtx.isAfterTyper => cond
+        case Some(excl) if !curCtx.isAfterTyper => excl
         case _ => NoneExcluded
 
+    /** The current context augmented with nullability information of `tree` */
     def nullableContext(given Context): Context =
       val excl = tree.notNullRefs
       if excl.isEmpty then curCtx else curCtx.addExcluded(excl)
 
+    /** The current context augmented with nullability information,
+     *  assuming the result of the condition represented by `tree` is the same as
+     *  the value of `tru`. The current context if `tree` is not a condition.
+     */
     def nullableContext(tru: Boolean)(given Context): Context =
       val excl = tree.condNotNullRefs
       if excl.isEmpty then curCtx
       else curCtx.addExcluded(if tru then excl.ifTrue else excl.ifFalse)
 
+    /** The context to use for the arguments of the function represented by `tree`.
+     *  This is the current context, augmented with nullability information
+     *  of the left argument, if the application is a boolean `&&` or `||`.
+     */
     def nullableInArgContext(given Context): Context = tree match
       case Select(x, _) if !curCtx.isAfterTyper =>
         if tree.symbol == defn.Boolean_&& then x.nullableContext(true)
@@ -66,16 +84,20 @@ object Nullables with
         else curCtx
       case _ => curCtx
 
+    /** The `tree` augmented with nullability information in an attachment.
+     *  The following operations lead to nullability info being recorded:
+     *
+     *  1. Null tests using `==`, `!=`, `eq`, `ne`, if the compared entity is
+     *     a path (i.e. a stable TermRef)
+     *  2. Boolean &&, ||, !
+     */
     def computeNullable(given Context): tree.type =
       def setExcluded(ifTrue: Excluded, ifFalse: Excluded) =
         tree.putAttachment(CondExcluded, EitherExcluded(ifTrue, ifFalse))
       if !curCtx.isAfterTyper then tree match
-        case CompareNull(x, isEqual) =>
-          x.tpe match
-            case ref: TermRef if ref.isStable =>
-              if isEqual then setExcluded(Set(), Set(ref))
-              else setExcluded(Set(ref), Set())
-            case _ =>
+        case ComparePathNull(ref, testEqual) =>
+          if testEqual then setExcluded(Set(), Set(ref))
+          else setExcluded(Set(ref), Set())
         case Apply(Select(x, _), y :: Nil) =>
           val xc = x.condNotNullRefs
           val yc = y.condNotNullRefs
@@ -90,5 +112,4 @@ object Nullables with
             setExcluded(xc.ifFalse, xc.ifTrue)
         case _ =>
       tree
-
 end Nullables

From d904a3c78f8bb01c53b99fd9330c0ca827a4733c Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 17:48:33 +0100
Subject: [PATCH 04/37] Generalize expression purity

Also recognize pure operations in Any and Object
---
 compiler/src/dotty/tools/dotc/ast/TreeInfo.scala     | 4 +++-
 compiler/src/dotty/tools/dotc/core/Definitions.scala | 6 +++++-
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala b/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
index 47343cabd498..787ec5c8c242 100644
--- a/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
+++ b/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
@@ -391,7 +391,9 @@ trait TypedTreeInfo extends TreeInfo[Type] { self: Trees.Instance[Type] =>
       if (fn.symbol.is(Erased) || fn.symbol == defn.InternalQuoted_typeQuote) Pure else exprPurity(fn)
     case Apply(fn, args) =>
       def isKnownPureOp(sym: Symbol) =
-        sym.owner.isPrimitiveValueClass || sym.owner == defn.StringClass
+        sym.owner.isPrimitiveValueClass
+        || sym.owner == defn.StringClass
+        || defn.pureMethods.contains(sym)
       if (tree.tpe.isInstanceOf[ConstantType] && isKnownPureOp(tree.symbol) // A constant expression with pure arguments is pure.
           || (fn.symbol.isStableMember && !fn.symbol.is(Lazy))
           || fn.symbol.isPrimaryConstructor && fn.symbol.owner.isNoInitsClass) // TODO: include in isStable?
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index df5f6194d8ed..b3d136d61811 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -272,7 +272,7 @@ class Definitions {
           Final,
           bounds = TypeBounds.lower(AnyClass.thisType))
 
-    def AnyMethods: List[TermSymbol] = List(Any_==, Any_!=, Any_equals, Any_hashCode,
+    private def AnyMethods: List[TermSymbol] = List(Any_==, Any_!=, Any_equals, Any_hashCode,
       Any_toString, Any_##, Any_getClass, Any_isInstanceOf, Any_asInstanceOf, Any_typeTest, Any_typeCast)
 
   @tu lazy val ObjectClass: ClassSymbol = {
@@ -310,6 +310,10 @@ class Definitions {
     def ObjectMethods: List[TermSymbol] = List(Object_eq, Object_ne, Object_synchronized, Object_clone,
         Object_finalize, Object_notify, Object_notifyAll, Object_wait, Object_waitL, Object_waitLI)
 
+  /** Methods in Object and Any that do not have a side effect */
+  @tu lazy val pureMethods: List[TermSymbol] = List(Any_==, Any_!=, Any_equals, Any_hashCode,
+    Any_toString, Any_##, Any_getClass, Any_isInstanceOf, Any_typeTest, Object_eq, Object_ne)
+
   @tu lazy val AnyKindClass: ClassSymbol = {
     val cls = ctx.newCompleteClassSymbol(ScalaPackageClass, tpnme.AnyKind, AbstractFinal | Permanent, Nil)
     if (!ctx.settings.YnoKindPolymorphism.value)

From 6a7c740e942745caacdbd29670193fdbee044016 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 17:52:55 +0100
Subject: [PATCH 05/37] Simplify more if-expressions in FirstTransform

Previously we simplified an `if c then a else b`
to `a` or `b` only if `c` is literally `true` or `false`.
We now do the same if `c` is a pure Boolean constant expression.
---
 compiler/src/dotty/tools/dotc/transform/FirstTransform.scala | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/FirstTransform.scala b/compiler/src/dotty/tools/dotc/transform/FirstTransform.scala
index 18a31b12cbf2..8050581ed544 100644
--- a/compiler/src/dotty/tools/dotc/transform/FirstTransform.scala
+++ b/compiler/src/dotty/tools/dotc/transform/FirstTransform.scala
@@ -160,8 +160,9 @@ class FirstTransform extends MiniPhase with InfoTransformer { thisPhase =>
     constToLiteral(tree)
 
   override def transformIf(tree: If)(implicit ctx: Context): Tree =
-    tree.cond match {
-      case Literal(Constant(c: Boolean)) => if (c) tree.thenp else tree.elsep
+    tree.cond.tpe match {
+      case ConstantType(Constant(c: Boolean)) if isPureExpr(tree.cond) =>
+        if (c) tree.thenp else tree.elsep
       case _ => tree
     }
 

From e96e0275c509583453b989a6f100f3447b08b468 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 17:56:05 +0100
Subject: [PATCH 06/37] Maintain constant types of applications in
 TimeTravellingTreeCopier

We keep the type (instead of retyping it) if

 - the function and argumens of an application are the same,
 - the application is a pure constant expression.

It's a shame to lose the type in this case. This does constrain what can
be done in transforms: It's forbidden to change a pure function with a constant
type so that the application no longer has that type.
---
 compiler/src/dotty/tools/dotc/ast/tpd.scala | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/ast/tpd.scala b/compiler/src/dotty/tools/dotc/ast/tpd.scala
index 1827638ba9ad..117f4f1b8697 100644
--- a/compiler/src/dotty/tools/dotc/ast/tpd.scala
+++ b/compiler/src/dotty/tools/dotc/ast/tpd.scala
@@ -711,11 +711,19 @@ object tpd extends Trees.Instance[Type] with TypedTreeInfo {
 
   class TimeTravellingTreeCopier extends TypedTreeCopier {
     override def Apply(tree: Tree)(fun: Tree, args: List[Tree])(implicit ctx: Context): Apply =
-      ta.assignType(untpdCpy.Apply(tree)(fun, args), fun, args)
+      tree match
+        case tree: Apply
+        if (tree.fun eq fun) && (tree.args eq args)
+           && tree.tpe.isInstanceOf[ConstantType]
+           && isPureExpr(tree) => tree
+        case _ =>
+          ta.assignType(untpdCpy.Apply(tree)(fun, args), fun, args)
       // Note: Reassigning the original type if `fun` and `args` have the same types as before
-      // does not work here: The computed type depends on the widened function type, not
-      // the function type itself. A treetransform may keep the function type the
+      // does not work here in general: The computed type depends on the widened function type, not
+      // the function type itself. A tree transform may keep the function type the
       // same but its widened type might change.
+      // However, we keep constant types of pure expressions. This uses the underlying assumptions
+      // that pure functions yielding a constant will not change in later phases.
 
     override def TypeApply(tree: Tree)(fun: Tree, args: List[Tree])(implicit ctx: Context): TypeApply =
       ta.assignType(untpdCpy.TypeApply(tree)(fun, args), fun, args)

From d1981f82665b53278c882c9e43f0c2f7f0bdc0d1 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 18:00:21 +0100
Subject: [PATCH 07/37] Constant fold null tests

This is a temporary commit so that we can test the nullability analysis without
having the full implementation of explicit nulls.

Once we have explicit nulls, we could consider dropping this, as the benefits
seem smallish.
---
 compiler/src/dotty/tools/dotc/typer/ConstFold.scala | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/ConstFold.scala b/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
index 9b4eef28369a..a49608c6260e 100644
--- a/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
@@ -19,15 +19,16 @@ object ConstFold {
   /** If tree is a constant operation, replace with result. */
   def apply[T <: Tree](tree: T)(implicit ctx: Context): T = finish(tree) {
     tree match {
+      case ComparePathNull(ref, testEqual) if ctx.notNullRefs.containsRef(ref) =>
+        // TODO maybe drop once we have general Nullability?
+        Constant(!testEqual)
       case Apply(Select(xt, op), yt :: Nil) =>
-        xt.tpe.widenTermRefExpr.normalized match {
+        xt.tpe.widenTermRefExpr.normalized match
           case ConstantType(x) =>
-            yt.tpe.widenTermRefExpr match {
+            yt.tpe.widenTermRefExpr match
               case ConstantType(y) => foldBinop(op, x, y)
               case _ => null
-            }
           case _ => null
-        }
       case Select(xt, op) =>
         xt.tpe.widenTermRefExpr match {
           case ConstantType(x) => foldUnop(op, x)

From 16cc0665bae2a81d0017541d6111e22034389b5a Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 18:25:07 +0100
Subject: [PATCH 08/37] Fix handling of negation for nullability

---
 .../dotty/tools/dotc/typer/Nullables.scala    |  2 +-
 .../src/dotty/tools/dotc/typer/Typer.scala    |  1 +
 tests/pos/nullable.scala                      | 43 +++++++++++++++++++
 3 files changed, 45 insertions(+), 1 deletion(-)
 create mode 100644 tests/pos/nullable.scala

diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 427a723e4c09..85492b74c913 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -106,7 +106,7 @@ object Nullables with
               setExcluded(xc.ifTrue | yc.ifTrue, xc.ifFalse & yc.ifFalse)
             else if tree.symbol == defn.Boolean_|| then
               setExcluded(xc.ifTrue & yc.ifTrue, xc.ifFalse | yc.ifFalse)
-        case Apply(Select(x, _), Nil) if tree.symbol == defn.Boolean_! =>
+        case Select(x, _) if tree.symbol == defn.Boolean_! =>
           val xc = x.condNotNullRefs
           if !xc.isEmpty then
             setExcluded(xc.ifFalse, xc.ifTrue)
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index d60034ff47ac..deadb8314508 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -452,6 +452,7 @@ class Typer extends Namer
 
     def typeSelectOnTerm(implicit ctx: Context): Tree =
       typedSelect(tree, pt, typedExpr(tree.qualifier, selectionProto(tree.name, pt, this)))
+        .computeNullable
 
     def typeSelectOnType(qual: untpd.Tree)(implicit ctx: Context) =
       typedSelect(untpd.cpy.Select(tree)(qual, tree.name.toTypeName), pt)
diff --git a/tests/pos/nullable.scala b/tests/pos/nullable.scala
new file mode 100644
index 000000000000..e4d903b7ef26
--- /dev/null
+++ b/tests/pos/nullable.scala
@@ -0,0 +1,43 @@
+trait T { def f: Int }
+def impossible(x: Any): Unit =
+  val y = x
+
+def test: Unit =
+  val x, x2, x3, x4 = ""
+
+  if x != null then
+    if x == null then impossible(new T{})
+
+    if x == null then ()
+    else
+      if x == null then impossible(new T{})
+
+  if x == null || {
+    if x == null then impossible(new T{})
+    true
+  }
+  then ()
+
+  if x != null && {
+    if x == null then impossible(new T{})
+    true
+  }
+  then ()
+
+  if !(x == null) && {
+    if x == null then impossible(new T{})
+    true
+  }
+  then ()
+
+  if x == null then return
+  if x == null then impossible(new T{})
+
+  if x2 == null then throw AssertionError()
+  if x2 == null then impossible(new T{})
+
+  if !(x3 != null) then throw AssertionError()
+  if x3 == null then impossible(new T{})
+
+  //assert(x4 != null)
+  //if x4 == null then impossible(new T{})

From a38574cc7c6f200e67858932222d8bd4d68c5db9 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 21:53:11 +0100
Subject: [PATCH 09/37] Skip also Inlined nodes with skipBlock

---
 compiler/src/dotty/tools/dotc/ast/TreeInfo.scala | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala b/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
index 787ec5c8c242..a39d409dacf6 100644
--- a/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
+++ b/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
@@ -88,6 +88,12 @@ trait TreeInfo[T >: Untyped <: Type] { self: Trees.Instance[T] =>
   /** If this is a block, its expression part */
   def stripBlock(tree: Tree): Tree = unsplice(tree) match {
     case Block(_, expr) => stripBlock(expr)
+    case Inlined(_, _, expr) => stripBlock(expr)
+    case _ => tree
+  }
+
+  def stripInlined(tree: Tree): Tree = unsplice(tree) match {
+    case Inlined(_, _, expr) => stripInlined(expr)
     case _ => tree
   }
 

From 1910c871d0270e46cc953dcc5751bc04d9493511 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 21:54:14 +0100
Subject: [PATCH 10/37] Always compute nullable info unless ersedTypes

Not computing it after typer (as was done before) fails Ycheck.
---
 compiler/src/dotty/tools/dotc/typer/Nullables.scala | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 85492b74c913..40e97e20ab8a 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -46,8 +46,8 @@ object Nullables with
 
     /* The paths that are known to be not null after execution of `tree` terminates normally */
     def notNullRefs(given Context): Excluded =
-      tree.getAttachment(AlwaysExcluded) match
-        case Some(excl) if !curCtx.isAfterTyper => excl
+      stripInlined(tree).getAttachment(AlwaysExcluded) match
+        case Some(excl) if !curCtx.erasedTypes => excl
         case _ => Set.empty
 
     /** The paths that are known to be not null if the condition represented
@@ -56,7 +56,7 @@ object Nullables with
      */
     def condNotNullRefs(given Context): EitherExcluded =
       stripBlock(tree).getAttachment(CondExcluded) match
-        case Some(excl) if !curCtx.isAfterTyper => excl
+        case Some(excl) if !curCtx.erasedTypes => excl
         case _ => NoneExcluded
 
     /** The current context augmented with nullability information of `tree` */
@@ -78,7 +78,7 @@ object Nullables with
      *  of the left argument, if the application is a boolean `&&` or `||`.
      */
     def nullableInArgContext(given Context): Context = tree match
-      case Select(x, _) if !curCtx.isAfterTyper =>
+      case Select(x, _) if !curCtx.erasedTypes =>
         if tree.symbol == defn.Boolean_&& then x.nullableContext(true)
         else if tree.symbol == defn.Boolean_|| then x.nullableContext(false)
         else curCtx
@@ -94,7 +94,7 @@ object Nullables with
     def computeNullable(given Context): tree.type =
       def setExcluded(ifTrue: Excluded, ifFalse: Excluded) =
         tree.putAttachment(CondExcluded, EitherExcluded(ifTrue, ifFalse))
-      if !curCtx.isAfterTyper then tree match
+      if !curCtx.erasedTypes then tree match
         case ComparePathNull(ref, testEqual) =>
           if testEqual then setExcluded(Set(), Set(ref))
           else setExcluded(Set(ref), Set())

From a691e96b7d253e647e5186ea9ca2231f71710072 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 21:57:27 +0100
Subject: [PATCH 11/37] Recompute nullability info when inlining

---
 compiler/src/dotty/tools/dotc/typer/Inliner.scala | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Inliner.scala b/compiler/src/dotty/tools/dotc/typer/Inliner.scala
index 632b5be4ae53..51bca3f3a765 100644
--- a/compiler/src/dotty/tools/dotc/typer/Inliner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inliner.scala
@@ -24,6 +24,7 @@ import ErrorReporting.errorTree
 import dotty.tools.dotc.tastyreflect.ReflectionImpl
 import dotty.tools.dotc.util.{SimpleIdentityMap, SimpleIdentitySet, SourceFile, SourcePosition}
 import dotty.tools.dotc.parsing.Parsers.Parser
+import Nullables.given
 
 import collection.mutable
 import reporting.trace
@@ -1064,10 +1065,18 @@ class Inliner(call: tpd.Tree, rhsToInline: tpd.Tree)(implicit ctx: Context) {
             errorTree(tree, em"""cannot reduce inline if
                                 | its condition   ${tree.cond}
                                 | is not a constant value""")
-          else {
+          else
+            // Recompute nullablity info. This is needed because inlined code could have come
+            // from Tasty where no nullability info is kept.
+            val addNullable = new TreeTraverser {
+              def traverse(tree: Tree)(implicit ctx: Context) =
+                traverseChildren(tree)
+                tree.computeNullable
+            }
+            addNullable.traverse(cond1)
+            
             val if1 = untpd.cpy.If(tree)(cond = untpd.TypedSplice(cond1))
             super.typedIf(if1, pt)
-          }
       }
 
     override def typedApply(tree: untpd.Apply, pt: Type)(implicit ctx: Context): Tree =

From 691996ade7609e4a41d977bf6f95e714dc7725c6 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 21:58:37 +0100
Subject: [PATCH 12/37] Tweak assert so that nullability info is propagated
 correctly

---
 library/src/dotty/DottyPredef.scala | 6 +++---
 tests/pos/nullable.scala            | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/library/src/dotty/DottyPredef.scala b/library/src/dotty/DottyPredef.scala
index 529266cb3922..c934bf0ddd67 100644
--- a/library/src/dotty/DottyPredef.scala
+++ b/library/src/dotty/DottyPredef.scala
@@ -8,13 +8,13 @@ object DottyPredef {
       assertFail(message)
   }
 
-  inline final def assert(assertion: => Boolean): Unit = {
+  inline final def assert(assertion: => Boolean) <: Unit = {
     if (!assertion)
       assertFail()
   }
 
-  def assertFail(): Unit = throw new java.lang.AssertionError("assertion failed")
-  def assertFail(message: => Any): Unit = throw new java.lang.AssertionError("assertion failed: " + message)
+  def assertFail(): Nothing = throw new java.lang.AssertionError("assertion failed")
+  def assertFail(message: => Any): Nothing = throw new java.lang.AssertionError("assertion failed: " + message)
 
   inline final def implicitly[T](implicit ev: T): T = ev
 
diff --git a/tests/pos/nullable.scala b/tests/pos/nullable.scala
index e4d903b7ef26..9a24c8f494b4 100644
--- a/tests/pos/nullable.scala
+++ b/tests/pos/nullable.scala
@@ -39,5 +39,5 @@ def test: Unit =
   if !(x3 != null) then throw AssertionError()
   if x3 == null then impossible(new T{})
 
-  //assert(x4 != null)
-  //if x4 == null then impossible(new T{})
+  assert(x4 != null)
+  if x4 == null then impossible(new T{})

From 94d05a4e5eb19123be8d8669691b90d924efba5d Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 22:29:00 +0100
Subject: [PATCH 13/37] Exclude nullable.scala from pickling and fromTasy tests

Constant folding null comparisons cannot be reproduced after pickling
since notNullRefs are not maintained top-down.

We should drop constant folding null comparisons once full explicit nulls are
in. for full explicit nulles, we need to wrap references in "assert not null"
calls to keep a record of what was inferred.
---
 compiler/test/dotc/pos-from-tasty.blacklist    | 5 ++++-
 compiler/test/dotc/pos-test-pickling.blacklist | 3 +++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/compiler/test/dotc/pos-from-tasty.blacklist b/compiler/test/dotc/pos-from-tasty.blacklist
index f3a7568dcf01..4afb169cc85d 100644
--- a/compiler/test/dotc/pos-from-tasty.blacklist
+++ b/compiler/test/dotc/pos-from-tasty.blacklist
@@ -8,4 +8,7 @@ t3612.scala
 t802.scala
 
 # Matchtype
-i7087.scala
\ No newline at end of file
+i7087.scala
+
+# Nullability
+nullable.scala
diff --git a/compiler/test/dotc/pos-test-pickling.blacklist b/compiler/test/dotc/pos-test-pickling.blacklist
index 740ff1108fad..59a9b8498080 100644
--- a/compiler/test/dotc/pos-test-pickling.blacklist
+++ b/compiler/test/dotc/pos-test-pickling.blacklist
@@ -28,3 +28,6 @@ i5720.scala
 
 # Tuples
 toexproftuple.scala
+
+# Nullability
+nullable.scala

From 27c92a9a5958ba88bdc0809763b46d73125a7204 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Fri, 8 Nov 2019 23:11:07 +0100
Subject: [PATCH 14/37] Disable sjsJUnitTests

They don't link if assertFail() has Nothing as result type.
---
 .drone.yml | 2 +-
 build.sbt  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/.drone.yml b/.drone.yml
index 839cbb9a1aae..303e2fdebc36 100644
--- a/.drone.yml
+++ b/.drone.yml
@@ -40,7 +40,7 @@ steps:
   depends_on: [ clone ]
   commands:
   - cp -R . /tmp/2/ && cd /tmp/2/
-  - ./project/scripts/sbt ";dotty-bootstrapped/compile ;dotty-bootstrapped/test ;dotty-staging/test ;sjsSandbox/run;sjsSandbox/test;sjsJUnitTests/test"
+  - ./project/scripts/sbt ";dotty-bootstrapped/compile ;dotty-bootstrapped/test ;dotty-staging/test"
   - ./project/scripts/bootstrapCmdTests
 
 - name: community_build
diff --git a/build.sbt b/build.sbt
index e4f27b72a3ad..a613eadf4a4c 100644
--- a/build.sbt
+++ b/build.sbt
@@ -23,7 +23,7 @@ val `dist-bootstrapped` = Build.`dist-bootstrapped`
 val `community-build` = Build.`community-build`
 
 val sjsSandbox = Build.sjsSandbox
-val sjsJUnitTests = Build.sjsJUnitTests
+//val sjsJUnitTests = Build.sjsJUnitTests
 
 val `sbt-dotty` = Build.`sbt-dotty`
 val `vscode-dotty` = Build.`vscode-dotty`

From cb6ff0c584e57bbb2465f9e6af5bc69971dbccfe Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sat, 9 Nov 2019 14:28:37 +0100
Subject: [PATCH 15/37] Move null comparison extractors into Nullables

---
 .../src/dotty/tools/dotc/ast/TreeInfo.scala   | 36 -----------------
 .../dotty/tools/dotc/typer/ConstFold.scala    |  3 +-
 .../dotty/tools/dotc/typer/Nullables.scala    | 39 ++++++++++++++++++-
 3 files changed, 39 insertions(+), 39 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala b/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
index a39d409dacf6..a6aab75558e1 100644
--- a/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
+++ b/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
@@ -656,42 +656,6 @@ trait TypedTreeInfo extends TreeInfo[Type] { self: Trees.Instance[Type] =>
     acc(Nil, tree)
   }
 
-  /** An extractor for null comparisons */
-  object CompareNull with
-
-    /** Matches one of
-     *
-     *    tree == null, tree eq null, null == tree, null eq tree
-     *    tree != null, tree ne null, null != tree, null ne tree
-     *
-     *  The second boolean result is true for equality tests, false for inequality tests
-     */
-    def unapply(tree: Tree)(given Context): Option[(Tree, Boolean)] = tree match
-      case Apply(Select(l, _), Literal(Constant(null)) :: Nil) =>
-        testSym(tree.symbol, l)
-      case Apply(Select(Literal(Constant(null)), _), r :: Nil) =>
-        testSym(tree.symbol, r)
-      case _ =>
-        None
-
-    private def testSym(sym: Symbol, operand: Tree)(given Context) =
-      if sym == defn.Any_== || sym == defn.Object_eq then Some((operand, true))
-      else if sym == defn.Any_!= || sym == defn.Object_ne then Some((operand, false))
-      else None
-
-  end CompareNull
-
-  /** An extractor for comparisons between a path and null. */
-  object ComparePathNull with
-    def unapply(tree: Tree)(given Context): Option[(TermRef, Boolean)] =
-      CompareNull.unapply(tree) match
-        case some @ Some((x, testEqual)) =>
-          x.tpe match
-            case ref: TermRef if ref.isStable => Some((ref, testEqual))
-            case _ => None
-        case none => None
-  end ComparePathNull
-
   /** Is this pattern node a catch-all or type-test pattern? */
   def isCatchCase(cdef: CaseDef)(implicit ctx: Context): Boolean = cdef match {
     case CaseDef(Typed(Ident(nme.WILDCARD), tpt), EmptyTree, _) =>
diff --git a/compiler/src/dotty/tools/dotc/typer/ConstFold.scala b/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
index a49608c6260e..c5cf647c8d19 100644
--- a/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
@@ -11,6 +11,7 @@ import Constants._
 import Names._
 import StdNames._
 import Contexts._
+import Nullables.{CompareNull, TrackedRef}
 
 object ConstFold {
 
@@ -19,7 +20,7 @@ object ConstFold {
   /** If tree is a constant operation, replace with result. */
   def apply[T <: Tree](tree: T)(implicit ctx: Context): T = finish(tree) {
     tree match {
-      case ComparePathNull(ref, testEqual) if ctx.notNullRefs.containsRef(ref) =>
+      case CompareNull(TrackedRef(ref), testEqual) if ctx.notNullRefs.containsRef(ref) =>
         // TODO maybe drop once we have general Nullability?
         Constant(!testEqual)
       case Apply(Select(xt, op), yt :: Nil) =>
diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 40e97e20ab8a..8bcf72b8b43a 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -3,7 +3,7 @@ package dotc
 package typer
 
 import core._
-import Types._, Contexts._, Symbols._, Decorators._
+import Types._, Contexts._, Symbols._, Decorators._, Constants._
 import annotation.tailrec
 import util.Property
 
@@ -30,6 +30,41 @@ object Nullables with
     */
   private[typer] val AlwaysExcluded = Property.StickyKey[Nullables.Excluded]
 
+  /** An extractor for null comparisons */
+  object CompareNull with
+
+    /** Matches one of
+     *
+     *    tree == null, tree eq null, null == tree, null eq tree
+     *    tree != null, tree ne null, null != tree, null ne tree
+     *
+     *  The second boolean result is true for equality tests, false for inequality tests
+     */
+    def unapply(tree: Tree)(given Context): Option[(Tree, Boolean)] = tree match
+      case Apply(Select(l, _), Literal(Constant(null)) :: Nil) =>
+        testSym(tree.symbol, l)
+      case Apply(Select(Literal(Constant(null)), _), r :: Nil) =>
+        testSym(tree.symbol, r)
+      case _ =>
+        None
+
+    private def testSym(sym: Symbol, operand: Tree)(given Context) =
+      if sym == defn.Any_== || sym == defn.Object_eq then Some((operand, true))
+      else if sym == defn.Any_!= || sym == defn.Object_ne then Some((operand, false))
+      else None
+
+  end CompareNull
+
+  /** An extractor for null-trackable references */
+  object TrackedRef
+    def unapply(tree: Tree)(given Context): Option[TermRef] = tree.typeOpt match
+      case ref: TermRef if isTracked(ref) => Some(ref)
+      case _ => None
+  end TrackedRef
+
+  /** Is given reference tracked for nullability? */
+  def isTracked(ref: TermRef)(given Context) = ref.isStable
+
   given (excluded: List[Excluded])
     def containsRef(ref: TermRef): Boolean =
       excluded.exists(_.contains(ref))
@@ -95,7 +130,7 @@ object Nullables with
       def setExcluded(ifTrue: Excluded, ifFalse: Excluded) =
         tree.putAttachment(CondExcluded, EitherExcluded(ifTrue, ifFalse))
       if !curCtx.erasedTypes then tree match
-        case ComparePathNull(ref, testEqual) =>
+        case CompareNull(TrackedRef(ref), testEqual) =>
           if testEqual then setExcluded(Set(), Set(ref))
           else setExcluded(Set(ref), Set())
         case Apply(Select(x, _), y :: Nil) =>

From 0d2a0f0ba5c4f3df29e702fa9e0f4c3ec18e3128 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sat, 9 Nov 2019 15:03:30 +0100
Subject: [PATCH 16/37] Track nullability in pattern matches

---
 .../tools/dotc/transform/TreeChecker.scala    |  4 ++--
 .../dotty/tools/dotc/typer/Nullables.scala    | 14 ++++++++++++
 .../src/dotty/tools/dotc/typer/Typer.scala    | 22 ++++++++++++-------
 tests/pos/nullable.scala                      | 13 +++++++++++
 4 files changed, 43 insertions(+), 10 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
index 3433be335086..73af47c275bb 100644
--- a/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
+++ b/compiler/src/dotty/tools/dotc/transform/TreeChecker.scala
@@ -434,9 +434,9 @@ class TreeChecker extends Phase with SymTransformer {
         }
       }
 
-    override def typedCase(tree: untpd.CaseDef, selType: Type, pt: Type)(implicit ctx: Context): CaseDef =
+    override def typedCase(tree: untpd.CaseDef, sel: Tree, selType: Type, pt: Type)(implicit ctx: Context): CaseDef =
       withPatSyms(tpd.patVars(tree.pat.asInstanceOf[tpd.Tree])) {
-        super.typedCase(tree, selType, pt)
+        super.typedCase(tree, sel, selType, pt)
       }
 
     override def typedClosure(tree: untpd.Closure, pt: Type)(implicit ctx: Context): Tree = {
diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 8bcf72b8b43a..710cda9576a4 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -65,6 +65,20 @@ object Nullables with
   /** Is given reference tracked for nullability? */
   def isTracked(ref: TermRef)(given Context) = ref.isStable
 
+  def afterPatternContext(sel: Tree, pat: Tree)(given ctx: Context) = (sel, pat) match
+    case (TrackedRef(ref), Literal(Constant(null))) => ctx.addExcluded(Set(ref))
+    case _ => ctx
+
+  def caseContext(sel: Tree, pat: Tree)(given ctx: Context): Context = sel match
+    case TrackedRef(ref) if matchesNotNull(pat) => ctx.addExcluded(Set(ref))
+    case _ => ctx
+
+  private def matchesNotNull(pat: Tree)(given Context): Boolean = pat match
+    case _: Typed | _: UnApply => true
+    case Alternative(pats) => pats.forall(matchesNotNull)
+    // TODO: Add constant pattern if the constant type is not nullable
+    case _ => false
+
   given (excluded: List[Excluded])
     def containsRef(ref: TermRef): Boolean =
       excluded.exists(_.contains(ref))
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index deadb8314508..3f10e71db385 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1138,13 +1138,18 @@ class Typer extends Namer
 
   // Overridden in InlineTyper for inline matches
   def typedMatchFinish(tree: untpd.Match, sel: Tree, wideSelType: Type, cases: List[untpd.CaseDef], pt: Type)(implicit ctx: Context): Tree = {
-    val cases1 = harmonic(harmonize, pt)(typedCases(cases, wideSelType, pt.dropIfProto))
+    val cases1 = harmonic(harmonize, pt)(typedCases(cases, sel, wideSelType, pt.dropIfProto))
       .asInstanceOf[List[CaseDef]]
     assignType(cpy.Match(tree)(sel, cases1), sel, cases1)
   }
 
-  def typedCases(cases: List[untpd.CaseDef], selType: Type, pt: Type)(implicit ctx: Context): List[CaseDef] =
-    cases.mapconserve(typedCase(_, selType, pt))
+  def typedCases(cases: List[untpd.CaseDef], sel: Tree, wideSelType: Type, pt: Type)(implicit ctx: Context): List[CaseDef] =
+    var caseCtx = ctx
+    cases.mapconserve { cas =>
+      val case1 = typedCase(cas, sel, wideSelType, pt)(given caseCtx)
+      caseCtx = Nullables.afterPatternContext(sel, case1.pat)
+      case1
+    }
 
   /** - strip all instantiated TypeVars from pattern types.
     *    run/reducable.scala is a test case that shows stripping typevars is necessary.
@@ -1171,7 +1176,7 @@ class Typer extends Namer
   }
 
   /** Type a case. */
-  def typedCase(tree: untpd.CaseDef, selType: Type, pt: Type)(implicit ctx: Context): CaseDef = {
+  def typedCase(tree: untpd.CaseDef, sel: Tree, wideSelType: Type, pt: Type)(implicit ctx: Context): CaseDef = {
     val originalCtx = ctx
     val gadtCtx: Context = ctx.fresh.setFreshGADTBounds
 
@@ -1184,8 +1189,10 @@ class Typer extends Namer
       assignType(cpy.CaseDef(tree)(pat1, guard1, body1), pat1, body1)
     }
 
-    val pat1 = typedPattern(tree.pat, selType)(gadtCtx)
-    caseRest(pat1)(gadtCtx.fresh.setNewScope)
+    val pat1 = typedPattern(tree.pat, wideSelType)(gadtCtx)
+    caseRest(pat1)(
+      given Nullables.caseContext(sel, pat1)(
+        given gadtCtx.fresh.setNewScope))
   }
 
   def typedLabeled(tree: untpd.Labeled)(implicit ctx: Context): Labeled = {
@@ -1205,7 +1212,6 @@ class Typer extends Namer
     caseRest(ctx.fresh.setFreshGADTBounds.setNewScope)
   }
 
-
   def typedReturn(tree: untpd.Return)(implicit ctx: Context): Return = {
     def returnProto(owner: Symbol, locals: Scope): Type =
       if (owner.isConstructor) defn.UnitType
@@ -1263,7 +1269,7 @@ class Typer extends Namer
   def typedTry(tree: untpd.Try, pt: Type)(implicit ctx: Context): Try = {
     val expr2 :: cases2x = harmonic(harmonize, pt) {
       val expr1 = typed(tree.expr, pt.dropIfProto)
-      val cases1 = typedCases(tree.cases, defn.ThrowableType, pt.dropIfProto)
+      val cases1 = typedCases(tree.cases, EmptyTree, defn.ThrowableType, pt.dropIfProto)
       expr1 :: cases1
     }
     val finalizer1 = typed(tree.finalizer, defn.UnitType)
diff --git a/tests/pos/nullable.scala b/tests/pos/nullable.scala
index 9a24c8f494b4..4fda55af6f15 100644
--- a/tests/pos/nullable.scala
+++ b/tests/pos/nullable.scala
@@ -30,6 +30,19 @@ def test: Unit =
   }
   then ()
 
+  x match
+    case _: String =>
+      if x == null then impossible(new T{})
+
+  val y: Any = List(x)
+  y match
+    case y1 :: ys => if y == null then impossible(new T{})
+    case Some(_) | Seq(_: _*) => if y == null then impossible(new T{})
+
+  x match
+    case null =>
+    case _ => if x == null then impossible(new T{})
+
   if x == null then return
   if x == null then impossible(new T{})
 

From b20cae81d20cdef239269d7db975b98a1b91460e Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sat, 9 Nov 2019 15:41:32 +0100
Subject: [PATCH 17/37] Polishings

---
 compiler/src/dotty/tools/dotc/ast/TreeInfo.scala      |  2 +-
 .../src/dotty/tools/dotc/typer/Applications.scala     |  2 +-
 compiler/src/dotty/tools/dotc/typer/Inliner.scala     | 10 +---------
 compiler/src/dotty/tools/dotc/typer/Nullables.scala   | 11 ++++++++++-
 compiler/src/dotty/tools/dotc/typer/Typer.scala       |  2 +-
 5 files changed, 14 insertions(+), 13 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala b/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
index a6aab75558e1..7352139ea0e9 100644
--- a/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
+++ b/compiler/src/dotty/tools/dotc/ast/TreeInfo.scala
@@ -4,7 +4,7 @@ package ast
 
 import core._
 import Flags._, Trees._, Types._, Contexts._
-import Names._, StdNames._, NameOps._, Symbols._, Constants._
+import Names._, StdNames._, NameOps._, Symbols._
 import typer.ConstFold
 import reporting.trace
 import dotty.tools.dotc.transform.SymUtils._
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index f3811862a8ad..e0876632c2e6 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -867,7 +867,7 @@ trait Applications extends Compatibility {
               else
                 new ApplyToUntyped(tree, fun1, funRef, proto, pt)(
                   fun1.nullableInArgContext(given argCtx(tree)))
-            convertNewGenericArray(app.result).computeNullable
+            convertNewGenericArray(app.result).computeNullable()
           case _ =>
             handleUnexpectedFunType(tree, fun1)
         }
diff --git a/compiler/src/dotty/tools/dotc/typer/Inliner.scala b/compiler/src/dotty/tools/dotc/typer/Inliner.scala
index 51bca3f3a765..9b04ce1e8b78 100644
--- a/compiler/src/dotty/tools/dotc/typer/Inliner.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Inliner.scala
@@ -1066,15 +1066,7 @@ class Inliner(call: tpd.Tree, rhsToInline: tpd.Tree)(implicit ctx: Context) {
                                 | its condition   ${tree.cond}
                                 | is not a constant value""")
           else
-            // Recompute nullablity info. This is needed because inlined code could have come
-            // from Tasty where no nullability info is kept.
-            val addNullable = new TreeTraverser {
-              def traverse(tree: Tree)(implicit ctx: Context) =
-                traverseChildren(tree)
-                tree.computeNullable
-            }
-            addNullable.traverse(cond1)
-            
+            cond1.computeNullableDeeply()
             val if1 = untpd.cpy.If(tree)(cond = untpd.TypedSplice(cond1))
             super.typedIf(if1, pt)
       }
diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 710cda9576a4..6c56fc324890 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -140,7 +140,7 @@ object Nullables with
      *     a path (i.e. a stable TermRef)
      *  2. Boolean &&, ||, !
      */
-    def computeNullable(given Context): tree.type =
+    def computeNullable()(given Context): tree.type =
       def setExcluded(ifTrue: Excluded, ifFalse: Excluded) =
         tree.putAttachment(CondExcluded, EitherExcluded(ifTrue, ifFalse))
       if !curCtx.erasedTypes then tree match
@@ -161,4 +161,13 @@ object Nullables with
             setExcluded(xc.ifFalse, xc.ifTrue)
         case _ =>
       tree
+
+    /** Compute nullability information for this tree and all its subtrees */
+    def computeNullableDeeply()(given Context): Unit =
+      new TreeTraverser {
+        def traverse(tree: Tree)(implicit ctx: Context) =
+          traverseChildren(tree)
+          tree.computeNullable()
+      }.traverse(tree)
+
 end Nullables
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 3f10e71db385..66c96c148f8a 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -452,7 +452,7 @@ class Typer extends Namer
 
     def typeSelectOnTerm(implicit ctx: Context): Tree =
       typedSelect(tree, pt, typedExpr(tree.qualifier, selectionProto(tree.name, pt, this)))
-        .computeNullable
+        .computeNullable()
 
     def typeSelectOnType(qual: untpd.Tree)(implicit ctx: Context) =
       typedSelect(untpd.cpy.Select(tree)(qual, tree.name.toTypeName), pt)

From 2d5007cd6f95ec67550d4c99b3e031c3a25d57a7 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 10 Nov 2019 12:23:50 +0100
Subject: [PATCH 18/37] Allow retracting a not null status

This is needed to support mutable variables. It required a fundamental
change in data structures. Now, we keep two sets where before we kept one:
The set of references known to be not null, and the set of references
that are retracted, so that they can be null again.
---
 .../src/dotty/tools/dotc/core/Contexts.scala  |  22 +--
 .../dotty/tools/dotc/typer/Applications.scala |   2 +-
 .../dotty/tools/dotc/typer/ConstFold.scala    |   2 +-
 .../dotty/tools/dotc/typer/Nullables.scala    | 137 +++++++++++-------
 .../src/dotty/tools/dotc/typer/Typer.scala    |  20 +--
 5 files changed, 112 insertions(+), 71 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Contexts.scala b/compiler/src/dotty/tools/dotc/core/Contexts.scala
index fce4834feb4c..11ef4ef2a778 100644
--- a/compiler/src/dotty/tools/dotc/core/Contexts.scala
+++ b/compiler/src/dotty/tools/dotc/core/Contexts.scala
@@ -16,7 +16,7 @@ import ast.untpd
 import Flags.GivenOrImplicit
 import util.{FreshNameCreator, NoSource, SimpleIdentityMap, SourceFile}
 import typer.{Implicits, ImportInfo, Inliner, NamerContextOps, SearchHistory, SearchRoot, TypeAssigner, Typer, Nullables}
-import Nullables.given
+import Nullables.{NotNullInfo, given}
 import Implicits.ContextualImplicits
 import config.Settings._
 import config.Config
@@ -48,7 +48,7 @@ object Contexts {
   private val (compilationUnitLoc,  store6) = store5.newLocation[CompilationUnit]()
   private val (runLoc,              store7) = store6.newLocation[Run]()
   private val (profilerLoc,         store8) = store7.newLocation[Profiler]()
-  private val (notNullRefsLoc,      store9) = store8.newLocation[List[Nullables.Excluded]]()
+  private val (notNullInfosLoc,     store9) = store8.newLocation[List[NotNullInfo]]()
   private val initialStore = store9
 
   /** The current context */
@@ -213,7 +213,7 @@ object Contexts {
     def profiler: Profiler = store(profilerLoc)
 
     /** The paths currently known to be not null */
-    def notNullRefs = store(notNullRefsLoc)
+    def notNullInfos = store(notNullInfosLoc)
 
     /** The new implicit references that are introduced by this scope */
     protected var implicitsCache: ContextualImplicits = null
@@ -564,7 +564,7 @@ object Contexts {
     def setRun(run: Run): this.type = updateStore(runLoc, run)
     def setProfiler(profiler: Profiler): this.type = updateStore(profilerLoc, profiler)
     def setFreshNames(freshNames: FreshNameCreator): this.type = updateStore(freshNamesLoc, freshNames)
-    def setNotNullRefs(notNullRefs: List[Nullables.Excluded]): this.type = updateStore(notNullRefsLoc, notNullRefs)
+    def setNotNullInfos(notNullInfos: List[NotNullInfo]): this.type = updateStore(notNullInfosLoc, notNullInfos)
 
     def setProperty[T](key: Key[T], value: T): this.type =
       setMoreProperties(moreProperties.updated(key, value))
@@ -597,12 +597,14 @@ object Contexts {
   }
 
   given (c: Context)
-    def addExcluded(refs: Nullables.Excluded) =
-      if c.notNullRefs.containsAll(refs) then c
-      else c.fresh.setNotNullRefs(refs :: c.notNullRefs)
+    def addNotNullInfo(info: NotNullInfo) =
+      c.withNotNullInfos(c.notNullInfos.extendWith(info))
 
-    def withNotNullRefs(nnrefs: List[Nullables.Excluded]): Context =
-      if c.notNullRefs eq nnrefs then c else c.fresh.setNotNullRefs(nnrefs)
+    def addNotNullRefs(refs: Set[TermRef]) =
+      c.addNotNullInfo(NotNullInfo(refs, Set()))
+
+    def withNotNullInfos(infos: List[NotNullInfo]): Context =
+      if c.notNullInfos eq infos then c else c.fresh.setNotNullInfos(infos)
 
   // TODO: Fix issue when converting ModeChanges and FreshModeChanges to extension givens
   implicit class ModeChanges(val c: Context) extends AnyVal {
@@ -635,7 +637,7 @@ object Contexts {
     source = NoSource
     store = initialStore
       .updated(settingsStateLoc, settingsGroup.defaultState)
-      .updated(notNullRefsLoc, Nil)
+      .updated(notNullInfosLoc, Nil)
     typeComparer = new TypeComparer(this)
     searchHistory = new SearchRoot
     gadt = EmptyGadtConstraint
diff --git a/compiler/src/dotty/tools/dotc/typer/Applications.scala b/compiler/src/dotty/tools/dotc/typer/Applications.scala
index e0876632c2e6..2f04f7f17a8f 100644
--- a/compiler/src/dotty/tools/dotc/typer/Applications.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Applications.scala
@@ -866,7 +866,7 @@ trait Applications extends Compatibility {
                 new ApplyToTyped(tree, fun1, funRef, proto.unforcedTypedArgs, pt)
               else
                 new ApplyToUntyped(tree, fun1, funRef, proto, pt)(
-                  fun1.nullableInArgContext(given argCtx(tree)))
+                  given fun1.nullableInArgContext(given argCtx(tree)))
             convertNewGenericArray(app.result).computeNullable()
           case _ =>
             handleUnexpectedFunType(tree, fun1)
diff --git a/compiler/src/dotty/tools/dotc/typer/ConstFold.scala b/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
index c5cf647c8d19..352f279a59d1 100644
--- a/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
@@ -20,7 +20,7 @@ object ConstFold {
   /** If tree is a constant operation, replace with result. */
   def apply[T <: Tree](tree: T)(implicit ctx: Context): T = finish(tree) {
     tree match {
-      case CompareNull(TrackedRef(ref), testEqual) if ctx.notNullRefs.containsRef(ref) =>
+      case CompareNull(TrackedRef(ref), testEqual) if ctx.notNullInfos.containsRef(ref) =>
         // TODO maybe drop once we have general Nullability?
         Constant(!testEqual)
       case Apply(Select(xt, op), yt :: Nil) =>
diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 6c56fc324890..f0eb22cf6e50 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -4,31 +4,58 @@ package typer
 
 import core._
 import Types._, Contexts._, Symbols._, Decorators._, Constants._
-import annotation.tailrec
+import annotation.{tailrec, infix}
 import util.Property
 
 /** Operations for implementing a flow analysis for nullability */
 object Nullables with
   import ast.tpd._
 
-  /** A set of paths that are known to be not null */
-  type Excluded = Set[TermRef]
+  /** 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 null
+   */
+  case class NotNullInfo(asserted: Set[TermRef], retracted: Set[TermRef])
+    assert((asserted & retracted).isEmpty)
+
+    def isEmpty = this eq noNotNulls
+
+    /** The sequential combination with another not-null info */
+    @infix 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))
+
+  object NotNullInfo with
+    def apply(asserted: Set[TermRef], retracted: Set[TermRef]): NotNullInfo =
+      if asserted.isEmpty && retracted.isEmpty then noNotNulls
+      else new NotNullInfo(asserted, retracted)
+  end NotNullInfo
+
+  val noNotNulls = new NotNullInfo(Set(), Set())
 
   /** A pair of not-null sets, depending on whether a condition is `true` or `false` */
-  case class EitherExcluded(ifTrue: Excluded, ifFalse: Excluded) with
-    def isEmpty = ifTrue.isEmpty && ifFalse.isEmpty
+  case class NotNullConditional(ifTrue: Set[TermRef], ifFalse: Set[TermRef]) with
+    def isEmpty = this eq neitherNotNull
+
+  object NotNullConditional with
+    def apply(ifTrue: Set[TermRef], ifFalse: Set[TermRef]): NotNullConditional =
+      if ifTrue.isEmpty && ifFalse.isEmpty then neitherNotNull
+      else new NotNullConditional(ifTrue, ifFalse)
+  end NotNullConditional
 
-  val NoneExcluded = EitherExcluded(Set(), Set())
+  val neitherNotNull = new NotNullConditional(Set(), Set())
 
   /** An attachment that represents conditional flow facts established
    *  by this tree, which represents a condition.
    */
-  private[typer] val CondExcluded = Property.StickyKey[Nullables.EitherExcluded]
+  private[typer] val NNConditional = Property.StickyKey[NotNullConditional]
 
    /** An attachment that represents unconditional flow facts established
     *  by this tree.
     */
-  private[typer] val AlwaysExcluded = Property.StickyKey[Nullables.Excluded]
+  private[typer] val NNInfo = Property.StickyKey[NotNullInfo]
 
   /** An extractor for null comparisons */
   object CompareNull with
@@ -66,11 +93,11 @@ object Nullables with
   def isTracked(ref: TermRef)(given Context) = ref.isStable
 
   def afterPatternContext(sel: Tree, pat: Tree)(given ctx: Context) = (sel, pat) match
-    case (TrackedRef(ref), Literal(Constant(null))) => ctx.addExcluded(Set(ref))
+    case (TrackedRef(ref), Literal(Constant(null))) => ctx.addNotNullRefs(Set(ref))
     case _ => ctx
 
   def caseContext(sel: Tree, pat: Tree)(given ctx: Context): Context = sel match
-    case TrackedRef(ref) if matchesNotNull(pat) => ctx.addExcluded(Set(ref))
+    case TrackedRef(ref) if matchesNotNull(pat) => ctx.addNotNullRefs(Set(ref))
     case _ => ctx
 
   private def matchesNotNull(pat: Tree)(given Context): Boolean = pat match
@@ -79,48 +106,59 @@ object Nullables with
     // TODO: Add constant pattern if the constant type is not nullable
     case _ => false
 
-  given (excluded: List[Excluded])
-    def containsRef(ref: TermRef): Boolean =
-      excluded.exists(_.contains(ref))
+  given (infos: List[NotNullInfo])
+    @tailRec
+    def containsRef(ref: TermRef): Boolean = infos match
+      case info :: infos1 =>
+        if info.asserted.contains(ref) then true
+        else if info.retracted.contains(ref) then false
+        else containsRef(infos1)(ref)
+      case _ =>
+        false
 
-    def containsAll(refs: Set[TermRef]): Boolean =
-      refs.forall(excluded.containsRef(_))
+    def extendWith(info: NotNullInfo) =
+      if info.asserted.forall(infos.containsRef(_))
+         && !info.retracted.exists(infos.containsRef(_))
+      then infos
+      else info :: infos
 
   given (tree: Tree)
 
     /* The `tree` with added attachment stating that all paths in `refs` are not-null */
-    def withNotNullRefs(refs: Excluded): tree.type =
-      if refs.nonEmpty then tree.putAttachment(AlwaysExcluded, refs)
+    def withNotNullInfo(info: NotNullInfo): tree.type =
+      if !info.isEmpty then tree.putAttachment(NNInfo, info)
       tree
 
+    def withNotNullRefs(refs: Set[TermRef]) = tree.withNotNullInfo(NotNullInfo(refs, Set()))
+
     /* The paths that are known to be not null after execution of `tree` terminates normally */
-    def notNullRefs(given Context): Excluded =
-      stripInlined(tree).getAttachment(AlwaysExcluded) match
-        case Some(excl) if !curCtx.erasedTypes => excl
-        case _ => Set.empty
+    def notNullInfo(given Context): NotNullInfo =
+      stripInlined(tree).getAttachment(NNInfo) match
+        case Some(info) if !curCtx.erasedTypes => info
+        case _ => noNotNulls
 
     /** The paths that are known to be not null if the condition represented
      *  by `tree` yields `true` or `false`. Two empty sets if `tree` is not
      *  a condition.
      */
-    def condNotNullRefs(given Context): EitherExcluded =
-      stripBlock(tree).getAttachment(CondExcluded) match
-        case Some(excl) if !curCtx.erasedTypes => excl
-        case _ => NoneExcluded
+    def notNullConditional(given Context): NotNullConditional =
+      stripBlock(tree).getAttachment(NNConditional) match
+        case Some(cond) if !curCtx.erasedTypes => cond
+        case _ => neitherNotNull
 
     /** The current context augmented with nullability information of `tree` */
     def nullableContext(given Context): Context =
-      val excl = tree.notNullRefs
-      if excl.isEmpty then curCtx else curCtx.addExcluded(excl)
+      val info = tree.notNullInfo
+      if info.isEmpty then curCtx else curCtx.addNotNullInfo(info)
 
     /** The current context augmented with nullability information,
      *  assuming the result of the condition represented by `tree` is the same as
      *  the value of `tru`. The current context if `tree` is not a condition.
      */
     def nullableContext(tru: Boolean)(given Context): Context =
-      val excl = tree.condNotNullRefs
-      if excl.isEmpty then curCtx
-      else curCtx.addExcluded(if tru then excl.ifTrue else excl.ifFalse)
+      val cond = tree.notNullConditional
+      if cond.isEmpty then curCtx
+      else curCtx.addNotNullRefs(if tru then cond.ifTrue else cond.ifFalse)
 
     /** The context to use for the arguments of the function represented by `tree`.
      *  This is the current context, augmented with nullability information
@@ -141,25 +179,26 @@ object Nullables with
      *  2. Boolean &&, ||, !
      */
     def computeNullable()(given Context): tree.type =
-      def setExcluded(ifTrue: Excluded, ifFalse: Excluded) =
-        tree.putAttachment(CondExcluded, EitherExcluded(ifTrue, ifFalse))
-      if !curCtx.erasedTypes then tree match
-        case CompareNull(TrackedRef(ref), testEqual) =>
-          if testEqual then setExcluded(Set(), Set(ref))
-          else setExcluded(Set(ref), Set())
-        case Apply(Select(x, _), y :: Nil) =>
-          val xc = x.condNotNullRefs
-          val yc = y.condNotNullRefs
-          if !(xc.isEmpty && yc.isEmpty) then
-            if tree.symbol == defn.Boolean_&& then
-              setExcluded(xc.ifTrue | yc.ifTrue, xc.ifFalse & yc.ifFalse)
-            else if tree.symbol == defn.Boolean_|| then
-              setExcluded(xc.ifTrue & yc.ifTrue, xc.ifFalse | yc.ifFalse)
-        case Select(x, _) if tree.symbol == defn.Boolean_! =>
-          val xc = x.condNotNullRefs
-          if !xc.isEmpty then
-            setExcluded(xc.ifFalse, xc.ifTrue)
-        case _ =>
+      def setConditional(ifTrue: Set[TermRef], ifFalse: Set[TermRef]) =
+        tree.putAttachment(NNConditional, NotNullConditional(ifTrue, ifFalse))
+      if !curCtx.erasedTypes then
+        tree match
+          case CompareNull(TrackedRef(ref), testEqual) =>
+            if testEqual then setConditional(Set(), Set(ref))
+            else setConditional(Set(ref), Set())
+          case Apply(Select(x, _), y :: Nil) =>
+            val xc = x.notNullConditional
+            val yc = y.notNullConditional
+            if !(xc.isEmpty && yc.isEmpty) then
+              if tree.symbol == defn.Boolean_&& then
+                setConditional(xc.ifTrue | yc.ifTrue, xc.ifFalse & yc.ifFalse)
+              else if tree.symbol == defn.Boolean_|| then
+                setConditional(xc.ifTrue & yc.ifTrue, xc.ifFalse | yc.ifFalse)
+          case Select(x, _) if tree.symbol == defn.Boolean_! =>
+            val xc = x.notNullConditional
+            if !xc.isEmpty then
+              setConditional(xc.ifFalse, xc.ifTrue)
+          case _ =>
       tree
 
     /** Compute nullability information for this tree and all its subtrees */
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 66c96c148f8a..f3b0b679e621 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -40,7 +40,7 @@ import dotty.tools.dotc.transform.{PCPCheckAndHeal, Staging, TreeMapWithStages}
 import transform.SymUtils._
 import transform.TypeUtils._
 import reporting.trace
-import Nullables.given
+import Nullables.{NotNullInfo, given}
 
 object Typer {
 
@@ -634,7 +634,7 @@ class Typer extends Namer
         else if (isWildcard) tree.expr.withType(tpt.tpe)
         else typed(tree.expr, tpt.tpe.widenSkolem)
       assignType(cpy.Typed(tree)(expr1, tpt), underlyingTreeTpe)
-        .withNotNullRefs(expr1.notNullRefs)
+        .withNotNullInfo(expr1.notNullInfo)
     }
 
     if (untpd.isWildcardStarArg(tree)) {
@@ -766,7 +766,7 @@ class Typer extends Namer
     ensureNoLocalRefs(
       cpy.Block(tree)(stats1, expr1)
         .withType(expr1.tpe)
-        .withNotNullRefs(stats1.foldLeft(expr1.notNullRefs)(_ | _.notNullRefs)),
+        .withNotNullInfo(stats1.foldRight(expr1.notNullInfo)(_.notNullInfo.seq(_))),
       pt, localSyms(stats1))
   }
 
@@ -826,9 +826,9 @@ class Typer extends Namer
         assignType(cpy.If(tree)(cond1, thenp1, elsep1), thenp1, elsep1)
 
     if result.thenp.tpe.isRef(defn.NothingClass) then
-      result.withNotNullRefs(cond1.condNotNullRefs.ifFalse)
+      result.withNotNullRefs(cond1.notNullConditional.ifFalse)
     else if result.elsep.tpe.isRef(defn.NothingClass) then
-      result.withNotNullRefs(cond1.condNotNullRefs.ifTrue)
+      result.withNotNullRefs(cond1.notNullConditional.ifTrue)
     else
       result
   end typedIf
@@ -1263,7 +1263,7 @@ class Typer extends Namer
       else typed(tree.cond, defn.BooleanType)
     val body1 = typed(tree.body, defn.UnitType)(given cond1.nullableContext(true))
     assignType(cpy.WhileDo(tree)(cond1, body1))
-      .withNotNullRefs(cond1.condNotNullRefs.ifFalse)
+      .withNotNullRefs(cond1.notNullConditional.ifFalse)
   }
 
   def typedTry(tree: untpd.Try, pt: Type)(implicit ctx: Context): Try = {
@@ -1553,12 +1553,12 @@ class Typer extends Namer
   def typedValDef(vdef: untpd.ValDef, sym: Symbol)(implicit ctx: Context): Tree = {
     sym.infoOrCompleter match
       case completer: Namer#Completer
-      if completer.creationContext.notNullRefs ne ctx.notNullRefs =>
+      if completer.creationContext.notNullInfos ne ctx.notNullInfos =>
         // The RHS of a val def should know about not null facts established
         // in preceding statements (unless the ValDef is completed ahead of time,
         // then it is impossible).
         vdef.symbol.info = Completer(completer.original)(
-          given completer.creationContext.withNotNullRefs(ctx.notNullRefs))
+          given completer.creationContext.withNotNullInfos(ctx.notNullInfos))
       case _ =>
 
     val ValDef(name, tpt, _) = vdef
@@ -2201,7 +2201,7 @@ class Typer extends Namer
   def typedStats(stats: List[untpd.Tree], exprOwner: Symbol)(implicit ctx: Context): (List[Tree], Context) = {
     val buf = new mutable.ListBuffer[Tree]
     val enumContexts = new mutable.HashMap[Symbol, Context]
-    val initialNotNullRefs = ctx.notNullRefs
+    val initialNotNullInfos = ctx.notNullInfos
       // A map from `enum` symbols to the contexts enclosing their definitions
     @tailrec def traverse(stats: List[untpd.Tree])(implicit ctx: Context): (List[Tree], Context) = stats match {
       case (imp: untpd.Import) :: rest =>
@@ -2219,7 +2219,7 @@ class Typer extends Namer
               case _: ValDef if !mdef.mods.is(Lazy) && ctx.owner.isTerm =>
                 ctx // all preceding statements will have been executed in this case
               case _ =>
-                ctx.withNotNullRefs(initialNotNullRefs)
+                ctx.withNotNullInfos(initialNotNullInfos)
             typed(mdef)(given defCtx) match {
               case mdef1: DefDef if !Inliner.bodyToInline(mdef1.symbol).isEmpty =>
                 buf += inlineExpansion(mdef1)

From 10896a101aa3e3e58c4e24be6c94a2c7cf3a050d Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 10 Nov 2019 12:40:18 +0100
Subject: [PATCH 19/37] Nullables refactorings

---
 .../dotty/tools/dotc/typer/Nullables.scala    | 28 ++++++++++---------
 1 file changed, 15 insertions(+), 13 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index f0eb22cf6e50..67c676aadb74 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -5,6 +5,7 @@ package typer
 import core._
 import Types._, Contexts._, Symbols._, Decorators._, Constants._
 import annotation.{tailrec, infix}
+import StdNames.nme
 import util.Property
 
 /** Operations for implementing a flow analysis for nullability */
@@ -17,7 +18,7 @@ object Nullables with
   case class NotNullInfo(asserted: Set[TermRef], retracted: Set[TermRef])
     assert((asserted & retracted).isEmpty)
 
-    def isEmpty = this eq noNotNulls
+    def isEmpty = this eq NotNullInfo.empty
 
     /** The sequential combination with another not-null info */
     @infix def seq(that: NotNullInfo): NotNullInfo =
@@ -28,25 +29,23 @@ object Nullables with
         this.retracted.union(that.retracted).diff(that.asserted))
 
   object NotNullInfo with
+    val empty = new NotNullInfo(Set(), Set())
     def apply(asserted: Set[TermRef], retracted: Set[TermRef]): NotNullInfo =
-      if asserted.isEmpty && retracted.isEmpty then noNotNulls
+      if asserted.isEmpty && retracted.isEmpty then empty
       else new NotNullInfo(asserted, retracted)
   end NotNullInfo
 
-  val noNotNulls = new NotNullInfo(Set(), Set())
-
   /** A pair of not-null sets, depending on whether a condition is `true` or `false` */
   case class NotNullConditional(ifTrue: Set[TermRef], ifFalse: Set[TermRef]) with
-    def isEmpty = this eq neitherNotNull
+    def isEmpty = this eq NotNullConditional.empty
 
   object NotNullConditional with
+    val empty = new NotNullConditional(Set(), Set())
     def apply(ifTrue: Set[TermRef], ifFalse: Set[TermRef]): NotNullConditional =
-      if ifTrue.isEmpty && ifFalse.isEmpty then neitherNotNull
+      if ifTrue.isEmpty && ifFalse.isEmpty then empty
       else new NotNullConditional(ifTrue, ifFalse)
   end NotNullConditional
 
-  val neitherNotNull = new NotNullConditional(Set(), Set())
-
   /** An attachment that represents conditional flow facts established
    *  by this tree, which represents a condition.
    */
@@ -117,8 +116,9 @@ object Nullables with
         false
 
     def extendWith(info: NotNullInfo) =
-      if info.asserted.forall(infos.containsRef(_))
-         && !info.retracted.exists(infos.containsRef(_))
+      if info.isEmpty
+         || info.asserted.forall(infos.containsRef(_))
+            && !info.retracted.exists(infos.containsRef(_))
       then infos
       else info :: infos
 
@@ -135,7 +135,7 @@ object Nullables with
     def notNullInfo(given Context): NotNullInfo =
       stripInlined(tree).getAttachment(NNInfo) match
         case Some(info) if !curCtx.erasedTypes => info
-        case _ => noNotNulls
+        case _ => NotNullInfo.empty
 
     /** The paths that are known to be not null if the condition represented
      *  by `tree` yields `true` or `false`. Two empty sets if `tree` is not
@@ -144,7 +144,7 @@ object Nullables with
     def notNullConditional(given Context): NotNullConditional =
       stripBlock(tree).getAttachment(NNConditional) match
         case Some(cond) if !curCtx.erasedTypes => cond
-        case _ => neitherNotNull
+        case _ => NotNullConditional.empty
 
     /** The current context augmented with nullability information of `tree` */
     def nullableContext(given Context): Context =
@@ -181,7 +181,7 @@ object Nullables with
     def computeNullable()(given Context): tree.type =
       def setConditional(ifTrue: Set[TermRef], ifFalse: Set[TermRef]) =
         tree.putAttachment(NNConditional, NotNullConditional(ifTrue, ifFalse))
-      if !curCtx.erasedTypes then
+      if !curCtx.erasedTypes && analyzedOps.contains(tree.symbol.name.toTermName) then
         tree match
           case CompareNull(TrackedRef(ref), testEqual) =>
             if testEqual then setConditional(Set(), Set(ref))
@@ -209,4 +209,6 @@ object Nullables with
           tree.computeNullable()
       }.traverse(tree)
 
+  private val analyzedOps = Set(nme.EQ, nme.NE, nme.eq, nme.ne, nme.ZAND, nme.ZOR, nme.UNARY_!)
+
 end Nullables

From 5b46483814eb2c47c1f4aeba108a1e25182c73cf Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 10 Nov 2019 13:42:36 +0100
Subject: [PATCH 20/37] Account for side effects in conditions

Generalize not null computations so that any side effects in conditions
if if and while expressions are accounted for.
---
 .../dotty/tools/dotc/typer/Nullables.scala    | 37 ++++++++++++-------
 .../src/dotty/tools/dotc/typer/Typer.scala    | 23 ++++++------
 2 files changed, 35 insertions(+), 25 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 67c676aadb74..6b34c57982a6 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -4,7 +4,7 @@ package typer
 
 import core._
 import Types._, Contexts._, Symbols._, Decorators._, Constants._
-import annotation.{tailrec, infix}
+import annotation.tailrec
 import StdNames.nme
 import util.Property
 
@@ -20,14 +20,20 @@ object Nullables with
 
     def isEmpty = this eq NotNullInfo.empty
 
+    def retractedInfo = NotNullInfo(Set(), retracted)
+
     /** The sequential combination with another not-null info */
-    @infix def seq(that: NotNullInfo): NotNullInfo =
+    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))
 
+    /** The alternative path combination with another not-null info */
+    def alt(that: NotNullInfo): NotNullInfo =
+      NotNullInfo(this.asserted.intersect(that.asserted), this.retracted.union(that.retracted))
+
   object NotNullInfo with
     val empty = new NotNullInfo(Set(), Set())
     def apply(asserted: Set[TermRef], retracted: Set[TermRef]): NotNullInfo =
@@ -124,24 +130,28 @@ object Nullables with
 
   given (tree: Tree)
 
-    /* The `tree` with added attachment stating that all paths in `refs` are not-null */
+    /* The `tree` with added nullability attachment */
     def withNotNullInfo(info: NotNullInfo): tree.type =
       if !info.isEmpty then tree.putAttachment(NNInfo, info)
       tree
 
-    def withNotNullRefs(refs: Set[TermRef]) = tree.withNotNullInfo(NotNullInfo(refs, Set()))
-
-    /* The paths that are known to be not null after execution of `tree` terminates normally */
+    /* The nullability info of `tree` */
     def notNullInfo(given Context): NotNullInfo =
       stripInlined(tree).getAttachment(NNInfo) match
         case Some(info) if !curCtx.erasedTypes => info
         case _ => NotNullInfo.empty
 
+    /* The nullability info of `tree`, assuming it is a condition that evaluates to `c` */
+    def notNullInfoIf(c: Boolean)(given Context): NotNullInfo =
+      val cond = tree.notNullConditional
+      if cond.isEmpty then tree.notNullInfo
+      else tree.notNullInfo.seq(NotNullInfo(if c then cond.ifTrue else cond.ifFalse, Set()))
+
     /** The paths that are known to be not null if the condition represented
      *  by `tree` yields `true` or `false`. Two empty sets if `tree` is not
      *  a condition.
      */
-    def notNullConditional(given Context): NotNullConditional =
+    private def notNullConditional(given Context): NotNullConditional =
       stripBlock(tree).getAttachment(NNConditional) match
         case Some(cond) if !curCtx.erasedTypes => cond
         case _ => NotNullConditional.empty
@@ -153,12 +163,11 @@ object Nullables with
 
     /** The current context augmented with nullability information,
      *  assuming the result of the condition represented by `tree` is the same as
-     *  the value of `tru`. The current context if `tree` is not a condition.
+     *  the value of `c`.
      */
-    def nullableContext(tru: Boolean)(given Context): Context =
-      val cond = tree.notNullConditional
-      if cond.isEmpty then curCtx
-      else curCtx.addNotNullRefs(if tru then cond.ifTrue else cond.ifFalse)
+    def nullableContextIf(c: Boolean)(given Context): Context =
+      val info = tree.notNullInfoIf(c)
+      if info.isEmpty then curCtx else curCtx.addNotNullInfo(info)
 
     /** The context to use for the arguments of the function represented by `tree`.
      *  This is the current context, augmented with nullability information
@@ -166,8 +175,8 @@ object Nullables with
      */
     def nullableInArgContext(given Context): Context = tree match
       case Select(x, _) if !curCtx.erasedTypes =>
-        if tree.symbol == defn.Boolean_&& then x.nullableContext(true)
-        else if tree.symbol == defn.Boolean_|| then x.nullableContext(false)
+        if tree.symbol == defn.Boolean_&& then x.nullableContextIf(true)
+        else if tree.symbol == defn.Boolean_|| then x.nullableContextIf(false)
         else curCtx
       case _ => curCtx
 
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index f3b0b679e621..a481767b1693 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -814,23 +814,24 @@ class Typer extends Namer
 
     val result =
       if tree.elsep.isEmpty then
-        val thenp1 = typed(tree.thenp, defn.UnitType)(given cond1.nullableContext(true))
+        val thenp1 = typed(tree.thenp, defn.UnitType)(given cond1.nullableContextIf(true))
         val elsep1 = tpd.unitLiteral.withSpan(tree.span.endPos)
         cpy.If(tree)(cond1, thenp1, elsep1).withType(defn.UnitType)
       else
         val thenp1 :: elsep1 :: Nil = harmonic(harmonize, pt) {
-          val thenp0 = typed(tree.thenp, pt.dropIfProto)(given cond1.nullableContext(true))
-          val elsep0 = typed(tree.elsep, pt.dropIfProto)(given cond1.nullableContext(false))
+          val thenp0 = typed(tree.thenp, pt.dropIfProto)(given cond1.nullableContextIf(true))
+          val elsep0 = typed(tree.elsep, pt.dropIfProto)(given cond1.nullableContextIf(false))
           thenp0 :: elsep0 :: Nil
         }
         assignType(cpy.If(tree)(cond1, thenp1, elsep1), thenp1, elsep1)
 
-    if result.thenp.tpe.isRef(defn.NothingClass) then
-      result.withNotNullRefs(cond1.notNullConditional.ifFalse)
-    else if result.elsep.tpe.isRef(defn.NothingClass) then
-      result.withNotNullRefs(cond1.notNullConditional.ifTrue)
-    else
-      result
+    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
+      else thenPathInfo.alt(elsePathInfo)
+    )
   end typedIf
 
   /** Decompose function prototype into a list of parameter prototypes and a result prototype
@@ -1261,9 +1262,9 @@ class Typer extends Namer
     val cond1 =
       if (tree.cond eq EmptyTree) EmptyTree
       else typed(tree.cond, defn.BooleanType)
-    val body1 = typed(tree.body, defn.UnitType)(given cond1.nullableContext(true))
+    val body1 = typed(tree.body, defn.UnitType)(given cond1.nullableContextIf(true))
     assignType(cpy.WhileDo(tree)(cond1, body1))
-      .withNotNullRefs(cond1.notNullConditional.ifFalse)
+      .withNotNullInfo(body1.notNullInfo.retractedInfo.seq(cond1.notNullInfoIf(false)))
   }
 
   def typedTry(tree: untpd.Try, pt: Type)(implicit ctx: Context): Try = {

From 5cb0873cd77bc99991a37c65b1fd2f21bf16efc9 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 10 Nov 2019 13:59:18 +0100
Subject: [PATCH 21/37] Track assignments for nullability

---
 compiler/src/dotty/tools/dotc/typer/Nullables.scala | 6 ++++++
 compiler/src/dotty/tools/dotc/typer/Typer.scala     | 1 +
 2 files changed, 7 insertions(+)

diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 6b34c57982a6..6705f2381bb5 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -218,6 +218,12 @@ object Nullables with
           tree.computeNullable()
       }.traverse(tree)
 
+  given (tree: Assign)
+    def computeAssignNullable()(given Context): tree.type = tree.lhs match
+      case TrackedRef(ref) =>
+        tree.withNotNullInfo(NotNullInfo(Set(), Set(ref))) // TODO: refine with nullability type info
+      case _ => tree
+
   private val analyzedOps = Set(nme.EQ, nme.NE, nme.eq, nme.ne, nme.ZAND, nme.ZOR, nme.UNARY_!)
 
 end Nullables
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index a481767b1693..1ca2410b0edd 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -733,6 +733,7 @@ class Typer extends Namer
               val lhsBounds =
                 TypeBounds.lower(lhsVal.symbol.info).asSeenFrom(ref.prefix, lhsVal.symbol.owner)
               assignType(cpy.Assign(tree)(lhs1, typed(tree.rhs, lhsBounds.loBound)))
+                .computeAssignNullable()
             }
             else {
               val pre = ref.prefix

From 6d5ed25c1ff7d6110ebd4b85e5a865eeca2c768d Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 10 Nov 2019 17:20:43 +0100
Subject: [PATCH 22/37] Allow local variables to be tracked for nullability

---
 .../dotty/tools/dotc/CompilationUnit.scala    | 11 +++
 .../dotty/tools/dotc/typer/Nullables.scala    | 70 ++++++++++++++++++-
 tests/pos/nullable.scala                      | 10 +++
 3 files changed, 88 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/CompilationUnit.scala b/compiler/src/dotty/tools/dotc/CompilationUnit.scala
index ea0faa19ce6d..70d5c8dee20a 100644
--- a/compiler/src/dotty/tools/dotc/CompilationUnit.scala
+++ b/compiler/src/dotty/tools/dotc/CompilationUnit.scala
@@ -5,11 +5,13 @@ import util.SourceFile
 import ast.{tpd, untpd}
 import tpd.{Tree, TreeTraverser}
 import typer.PrepareInlineable.InlineAccessors
+import typer.Nullables
 import dotty.tools.dotc.core.Contexts.Context
 import dotty.tools.dotc.core.SymDenotations.ClassDenotation
 import dotty.tools.dotc.core.Symbols._
 import dotty.tools.dotc.transform.SymUtils._
 import util.{NoSource, SourceFile}
+import util.Spans.Span
 import core.Decorators._
 
 class CompilationUnit protected (val source: SourceFile) {
@@ -42,6 +44,15 @@ class CompilationUnit protected (val source: SourceFile) {
       suspended = true
       ctx.run.suspendedUnits += this
     throw CompilationUnit.SuspendException()
+
+  private var myTrackedVarSpans: Set[Int] = null
+
+  /** The (name-) offsets of all local variables in this compilation unit
+   *  that can be tracked for being not null.
+   */
+  def trackedVarSpans(given Context): Set[Int] =
+    if myTrackedVarSpans == null then myTrackedVarSpans = Nullables.trackedVarSpans
+    myTrackedVarSpans
 }
 
 object CompilationUnit {
diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 6705f2381bb5..1fa9629cc653 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -7,6 +7,9 @@ import Types._, Contexts._, Symbols._, Decorators._, Constants._
 import annotation.tailrec
 import StdNames.nme
 import util.Property
+import Names.Name
+import util.Spans.Span
+import Flags.Mutable
 
 /** Operations for implementing a flow analysis for nullability */
 object Nullables with
@@ -94,8 +97,21 @@ object Nullables with
       case _ => None
   end TrackedRef
 
-  /** Is given reference tracked for nullability? */
-  def isTracked(ref: TermRef)(given Context) = ref.isStable
+  /** Is given reference tracked for nullability?
+   *  This is the case if the reference is a path to an immutable val,
+   *  or if it refers to a local mutable variable where all assignments
+   *  to the variable are reachable.
+   */
+  def isTracked(ref: TermRef)(given Context) =
+    ref.isStable
+    || { val sym = ref.symbol
+         sym.is(Mutable)
+         && sym.owner.isTerm
+         && sym.owner.enclosingMethod == curCtx.owner.enclosingMethod
+         && sym.span.exists
+         && curCtx.compilationUnit.trackedVarSpans.contains(sym.span.start)
+//           .reporting(i"tracked? $sym ${sym.span} = $result")
+       }
 
   def afterPatternContext(sel: Tree, pat: Tree)(given ctx: Context) = (sel, pat) match
     case (TrackedRef(ref), Literal(Constant(null))) => ctx.addNotNullRefs(Set(ref))
@@ -151,7 +167,7 @@ object Nullables with
      *  by `tree` yields `true` or `false`. Two empty sets if `tree` is not
      *  a condition.
      */
-    private def notNullConditional(given Context): NotNullConditional =
+    def notNullConditional(given Context): NotNullConditional =
       stripBlock(tree).getAttachment(NNConditional) match
         case Some(cond) if !curCtx.erasedTypes => cond
         case _ => NotNullConditional.empty
@@ -226,4 +242,52 @@ object Nullables with
 
   private val analyzedOps = Set(nme.EQ, nme.NE, nme.eq, nme.ne, nme.ZAND, nme.ZOR, nme.UNARY_!)
 
+  /** The name offsets of all local mutable variables in the current compilation unit
+   *  that have only reachable assignments. An assignment is reachable if the
+   *  path of tree nodes between the block enclosing the variable declaration to
+   *  the assignment consists only of if-expressions, while-expressions, block-expressions
+   *  and type-ascriptions. Only reachable assignments are handled correctly in the
+   *  nullability analysis. Therefore, variables with unreachable assignments can
+   *  be assumed to be not-null only if their type asserts it.
+   */
+  def trackedVarSpans(given Context): Set[Int] =
+    import ast.untpd._
+    object populate extends UntypedTreeTraverser with
+
+      /** The name offsets of variables that are tracked */
+      var tracked: Set[Int] = Set.empty
+      /** The names of candidate variables in scope that might be tracked */
+      var candidates: Set[Name] = Set.empty
+      /** An assignment to a variable that's not in reachable makes the variable ineligible for tracking */
+      var reachable: Set[Name] = Set.empty
+
+      def traverse(tree: Tree)(implicit ctx: Context) =
+        val savedReachable = reachable
+        tree match
+          case Block(stats, expr) =>
+            var shadowed: Set[Name] = Set.empty
+            for case (stat: ValDef) <- stats if stat.mods.is(Mutable) do
+              if candidates.contains(stat.name) then shadowed += stat.name
+              else candidates += stat.name
+              reachable += stat.name
+            traverseChildren(tree)
+            for case (stat: ValDef) <- stats if stat.mods.is(Mutable) do
+              if candidates.contains(stat.name) then
+                tracked += stat.nameSpan.start // candidates that survive until here are tracked
+                candidates -= stat.name
+            candidates ++= shadowed
+          case Assign(Ident(name), rhs) =>
+            if !reachable.contains(name) then candidates -= name // variable cannot be tracked
+            traverseChildren(tree)
+          case _: (If | WhileDo | Typed) =>
+            traverseChildren(tree)      // assignments to candidate variables are OK here ...
+          case _ =>
+            reachable = Set.empty       // ... but not here
+            traverseChildren(tree)
+        reachable = savedReachable
+
+    populate.traverse(curCtx.compilationUnit.untpdTree)
+    populate.tracked
+      .reporting(i"tracked vars: ${result.toList}%, %")
+  end trackedVarSpans
 end Nullables
diff --git a/tests/pos/nullable.scala b/tests/pos/nullable.scala
index 4fda55af6f15..d2d68f0dcfd1 100644
--- a/tests/pos/nullable.scala
+++ b/tests/pos/nullable.scala
@@ -54,3 +54,13 @@ def test: Unit =
 
   assert(x4 != null)
   if x4 == null then impossible(new T{})
+
+  class C(val x: Int, val next: C)
+  var xs: C = C(1, C(2, null))
+  while xs != null do
+    if xs == null then println("?")
+      // looking at this with -Xprint-frontend -Xprint-types shows that the
+      // type of `xs == null` is indeed `false`. We cannot currently use this in a test
+      // since `xs == null` is not technically a pure expression since `xs` is not a path.
+      // We should test variable tracking once this is integrated with explicit not null types.
+    xs = xs.next

From 74d5b1ef3580b058ed3628e3291da39f8ce47138 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 10 Nov 2019 17:58:40 +0100
Subject: [PATCH 23/37] Drop debug output

---
 compiler/src/dotty/tools/dotc/typer/Nullables.scala | 2 --
 1 file changed, 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 1fa9629cc653..892533c3c96e 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -110,7 +110,6 @@ object Nullables with
          && sym.owner.enclosingMethod == curCtx.owner.enclosingMethod
          && sym.span.exists
          && curCtx.compilationUnit.trackedVarSpans.contains(sym.span.start)
-//           .reporting(i"tracked? $sym ${sym.span} = $result")
        }
 
   def afterPatternContext(sel: Tree, pat: Tree)(given ctx: Context) = (sel, pat) match
@@ -288,6 +287,5 @@ object Nullables with
 
     populate.traverse(curCtx.compilationUnit.untpdTree)
     populate.tracked
-      .reporting(i"tracked vars: ${result.toList}%, %")
   end trackedVarSpans
 end Nullables

From f1e2863c632a60a9295350f451fd7fcd6d2ed2c8 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Sun, 10 Nov 2019 19:25:34 +0100
Subject: [PATCH 24/37] Constant fold null comparisons only under
 -Yexplicit-nulls

---
 compiler/src/dotty/tools/dotc/config/ScalaSettings.scala | 1 +
 compiler/src/dotty/tools/dotc/typer/ConstFold.scala      | 3 ++-
 compiler/src/dotty/tools/dotc/typer/Nullables.scala      | 3 ++-
 compiler/test/dotty/tools/dotc/CompilationTests.scala    | 1 +
 tests/{pos => pos-special}/nullable.scala                | 0
 5 files changed, 6 insertions(+), 2 deletions(-)
 rename tests/{pos => pos-special}/nullable.scala (100%)

diff --git a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala b/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
index 8b053263ed00..d78f1cbd8b3d 100644
--- a/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
+++ b/compiler/src/dotty/tools/dotc/config/ScalaSettings.scala
@@ -162,6 +162,7 @@ class ScalaSettings extends Settings.SettingGroup {
 
   // Extremely experimental language features
   val YnoKindPolymorphism: Setting[Boolean] = BooleanSetting("-Yno-kind-polymorphism", "Enable kind polymorphism (see https://dotty.epfl.ch/docs/reference/kind-polymorphism.html). Potentially unsound.")
+  val YexplicitNulls: Setting[Boolean] = BooleanSetting("-Yexplicit-nulls", "Make reference types non-nullable. Nullable types can be expressed with unions: e.g. String|Null.")
 
   /** Area-specific debug output */
   val YexplainLowlevel: Setting[Boolean] = BooleanSetting("-Yexplain-lowlevel", "When explaining type errors, show types at a lower level.")
diff --git a/compiler/src/dotty/tools/dotc/typer/ConstFold.scala b/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
index 352f279a59d1..b715825f006a 100644
--- a/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
@@ -20,7 +20,8 @@ object ConstFold {
   /** If tree is a constant operation, replace with result. */
   def apply[T <: Tree](tree: T)(implicit ctx: Context): T = finish(tree) {
     tree match {
-      case CompareNull(TrackedRef(ref), testEqual) if ctx.notNullInfos.containsRef(ref) =>
+      case CompareNull(TrackedRef(ref), testEqual)
+      if ctx.settings.YexplicitNulls.value && ctx.notNullInfos.containsRef(ref) =>
         // TODO maybe drop once we have general Nullability?
         Constant(!testEqual)
       case Apply(Select(xt, op), yt :: Nil) =>
diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 892533c3c96e..47e5f93fb341 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -109,8 +109,9 @@ object Nullables with
          && sym.owner.isTerm
          && sym.owner.enclosingMethod == curCtx.owner.enclosingMethod
          && sym.span.exists
+         && curCtx.compilationUnit != null // could be null under -Ytest-pickler
          && curCtx.compilationUnit.trackedVarSpans.contains(sym.span.start)
-       }
+      }
 
   def afterPatternContext(sel: Tree, pat: Tree)(given ctx: Context) = (sel, pat) match
     case (TrackedRef(ref), Literal(Constant(null))) => ctx.addNotNullRefs(Set(ref))
diff --git a/compiler/test/dotty/tools/dotc/CompilationTests.scala b/compiler/test/dotty/tools/dotc/CompilationTests.scala
index 78915d3ce2f8..aefcb8b90d6e 100644
--- a/compiler/test/dotty/tools/dotc/CompilationTests.scala
+++ b/compiler/test/dotty/tools/dotc/CompilationTests.scala
@@ -59,6 +59,7 @@ class CompilationTests extends ParallelTesting {
       compileFile("tests/pos-special/typeclass-scaling.scala", defaultOptions.and("-Xmax-inlines", "40")),
       compileFile("tests/pos-special/indent-colons.scala", defaultOptions.and("-Yindent-colons")),
       compileFile("tests/pos-special/i7296.scala", defaultOptions.and("-strict", "-deprecation", "-Xfatal-warnings")),
+      compileFile("tests/pos-special/nullable.scala", defaultOptions.and("-Yexplicit-nulls")),
       compileDir("tests/pos-special/adhoc-extension", defaultOptions.and("-strict", "-feature", "-Xfatal-warnings"))
     ).checkCompile()
   }
diff --git a/tests/pos/nullable.scala b/tests/pos-special/nullable.scala
similarity index 100%
rename from tests/pos/nullable.scala
rename to tests/pos-special/nullable.scala

From ed00d961945e694a24140a4699ba267a4a9a5961 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 11 Nov 2019 10:52:01 +0100
Subject: [PATCH 25/37] Handle while expressions correctly for nullability

---
 .../dotty/tools/dotc/CompilationUnit.scala    | 13 +--
 .../dotty/tools/dotc/typer/Nullables.scala    | 91 ++++++++++++++-----
 .../src/dotty/tools/dotc/typer/Typer.scala    |  1 +
 3 files changed, 78 insertions(+), 27 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/CompilationUnit.scala b/compiler/src/dotty/tools/dotc/CompilationUnit.scala
index 70d5c8dee20a..0682d171b1b2 100644
--- a/compiler/src/dotty/tools/dotc/CompilationUnit.scala
+++ b/compiler/src/dotty/tools/dotc/CompilationUnit.scala
@@ -45,14 +45,15 @@ class CompilationUnit protected (val source: SourceFile) {
       ctx.run.suspendedUnits += this
     throw CompilationUnit.SuspendException()
 
-  private var myTrackedVarSpans: Set[Int] = null
+  private var myAssignmentSpans: Map[Int, List[Span]] = null
 
-  /** The (name-) offsets of all local variables in this compilation unit
-   *  that can be tracked for being not null.
+  /** A map from (name-) offsets of all local variables in this compilation unit
+   *  that can be tracked for being not null to the list of spans of assignments
+   *  to these variables.
    */
-  def trackedVarSpans(given Context): Set[Int] =
-    if myTrackedVarSpans == null then myTrackedVarSpans = Nullables.trackedVarSpans
-    myTrackedVarSpans
+  def assignmentSpans(given Context): Map[Int, List[Span]] =
+    if myAssignmentSpans == null then myAssignmentSpans = Nullables.assignmentSpans
+    myAssignmentSpans
 }
 
 object CompilationUnit {
diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 47e5f93fb341..2d9da99708ad 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -10,6 +10,7 @@ import util.Property
 import Names.Name
 import util.Spans.Span
 import Flags.Mutable
+import collection.mutable
 
 /** Operations for implementing a flow analysis for nullability */
 object Nullables with
@@ -110,7 +111,7 @@ object Nullables with
          && sym.owner.enclosingMethod == curCtx.owner.enclosingMethod
          && sym.span.exists
          && curCtx.compilationUnit != null // could be null under -Ytest-pickler
-         && curCtx.compilationUnit.trackedVarSpans.contains(sym.span.start)
+         && curCtx.compilationUnit.assignmentSpans.contains(sym.span.start)
       }
 
   def afterPatternContext(sel: Tree, pat: Tree)(given ctx: Context) = (sel, pat) match
@@ -242,42 +243,54 @@ object Nullables with
 
   private val analyzedOps = Set(nme.EQ, nme.NE, nme.eq, nme.ne, nme.ZAND, nme.ZOR, nme.UNARY_!)
 
-  /** The name offsets of all local mutable variables in the current compilation unit
-   *  that have only reachable assignments. An assignment is reachable if the
-   *  path of tree nodes between the block enclosing the variable declaration to
-   *  the assignment consists only of if-expressions, while-expressions, block-expressions
-   *  and type-ascriptions. Only reachable assignments are handled correctly in the
-   *  nullability analysis. Therefore, variables with unreachable assignments can
-   *  be assumed to be not-null only if their type asserts it.
+  /** A map from (name-) offsets of all local variables in this compilation unit
+   *  that can be tracked for being not null to the list of spans of assignments
+   *  to these variables. A variable can be tracked if it has only reachable assignments.
+   *  An assignment is reachable if the path of tree nodes between the block enclosing
+   *  the variable declaration to the assignment consists only of if-expressions,
+   *  while-expressions, block-expressions and type-ascriptions.
+   *  Only reachable assignments are handled correctly in the nullability analysis.
+   *  Therefore, variables with unreachable assignments can be assumed to be not-null
+   *  only if their type asserts it.
    */
-  def trackedVarSpans(given Context): Set[Int] =
+  def assignmentSpans(given Context): Map[Int, List[Span]] =
     import ast.untpd._
+
     object populate extends UntypedTreeTraverser with
 
       /** The name offsets of variables that are tracked */
-      var tracked: Set[Int] = Set.empty
-      /** The names of candidate variables in scope that might be tracked */
-      var candidates: Set[Name] = Set.empty
-      /** An assignment to a variable that's not in reachable makes the variable ineligible for tracking */
+      var tracked: Map[Int, List[Span]] = Map.empty
+
+      /** Map the names of potentially trackable candidate variables in scope to the spans
+       *  of their reachable assignments
+       */
+      val candidates = mutable.Map[Name, List[Span]]()
+
+      /** An assignment to a variable that's not in reachable makes the variable
+       *  ineligible for tracking
+       */
       var reachable: Set[Name] = Set.empty
 
       def traverse(tree: Tree)(implicit ctx: Context) =
         val savedReachable = reachable
         tree match
           case Block(stats, expr) =>
-            var shadowed: Set[Name] = Set.empty
+            var shadowed: Set[(Name, List[Span])] = Set.empty
             for case (stat: ValDef) <- stats if stat.mods.is(Mutable) do
-              if candidates.contains(stat.name) then shadowed += stat.name
-              else candidates += stat.name
+              for prevSpans <- candidates.put(stat.name, Nil) do
+                shadowed += (stat.name -> prevSpans)
               reachable += stat.name
             traverseChildren(tree)
             for case (stat: ValDef) <- stats if stat.mods.is(Mutable) do
-              if candidates.contains(stat.name) then
-                tracked += stat.nameSpan.start // candidates that survive until here are tracked
-                candidates -= stat.name
+              for spans <- candidates.remove(stat.name) do
+                tracked += (stat.nameSpan.start -> spans) // candidates that survive until here are tracked
             candidates ++= shadowed
           case Assign(Ident(name), rhs) =>
-            if !reachable.contains(name) then candidates -= name // variable cannot be tracked
+            candidates.get(name) match
+              case Some(spans) =>
+                if reachable.contains(name) then candidates(name) = tree.span :: spans
+                else candidates -= name
+              case None =>
             traverseChildren(tree)
           case _: (If | WhileDo | Typed) =>
             traverseChildren(tree)      // assignments to candidate variables are OK here ...
@@ -288,5 +301,41 @@ object Nullables with
 
     populate.traverse(curCtx.compilationUnit.untpdTree)
     populate.tracked
-  end trackedVarSpans
+  end assignmentSpans
+
+  /** The initial context to be used for a while expression with given span.
+   *  In this context, all variables that are assigned within the while expression
+   *  have their nullability status retracted, i.e. are not known to be null.
+   *  While necessary for soundness, this scheme loses precision: Even if
+   *  the initial state of the variable is not null and all assignments to the variable
+   *  in the while expression are also known to be not null, the variable is still
+   *  assumed to be potentially null. The loss of precision is unavoidable during
+   *  normal typing, since we can only do a linear traversal which does not allow
+   *  a fixpoint computation. But it could be mitigated as follows:
+   *
+   *   - initially, use `whileContext` as computed here
+   *   - when typechecking the while, delay all errors due to a variable being potentially null
+   *   - afterwards, if there are such delayed errors, run the analysis again with
+   *     as a fixpoint computation, reporting all previously delayed errors that remain.
+   *
+   *  The following code would produce an error in the current analysis, but not in the
+   *  refined analysis:
+   *
+   *     class Links(val elem: T, val next: Links | Null)
+   *
+   *     var ys: Links | Null = Links(1, null)
+   *     var xs: Links | Null = xs
+   *     while xs != null
+   *       ys = Links(xs.elem, ys.next)  // error in unrefined: ys is potentially null here
+   *       xs = xs.next
+   */
+  def whileContext(whileSpan: Span)(given Context): Context =
+    def isRetracted(ref: TermRef): Boolean =
+      val sym = ref.symbol
+      sym.span.exists
+      && assignmentSpans.getOrElse(sym.span.start, Nil).exists(whileSpan.contains(_))
+      && curCtx.notNullInfos.containsRef(ref)
+    val retractedVars = curCtx.notNullInfos.flatMap(_.asserted.filter(isRetracted)).toSet
+    curCtx.addNotNullInfo(NotNullInfo(Set(), retractedVars))
+
 end Nullables
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
index 1ca2410b0edd..55b44bd18f54 100644
--- a/compiler/src/dotty/tools/dotc/typer/Typer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -1260,6 +1260,7 @@ class Typer extends Namer
   }
 
   def typedWhileDo(tree: untpd.WhileDo)(implicit ctx: Context): Tree = {
+    given whileCtx: Context = Nullables.whileContext(tree.span)(given ctx)
     val cond1 =
       if (tree.cond eq EmptyTree) EmptyTree
       else typed(tree.cond, defn.BooleanType)

From 926b08ea4c0a0c66c05ffe43980f1448966cbf15 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Mon, 11 Nov 2019 13:11:24 +0100
Subject: [PATCH 26/37] Don't widen T | Null in widenUnion

---
 .../src/dotty/tools/dotc/core/Types.scala     | 28 +++++++++++++++++--
 1 file changed, 25 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index fb0f712a3e8f..22513ae4d03a 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -1068,8 +1068,9 @@ object Types {
      *  instead of `ArrayBuffer[? >: Int | A <: Int & A]`
      */
     def widenUnion(implicit ctx: Context): Type = widen match {
-      case OrType(tp1, tp2) =>
-        ctx.typeComparer.lub(tp1.widenUnion, tp2.widenUnion, canConstrain = true) match {
+      case tp @ OrType(tp1, tp2) =>
+        if tp1.isNull || tp2.isNull then tp
+        else ctx.typeComparer.lub(tp1.widenUnion, tp2.widenUnion, canConstrain = true) match {
           case union: OrType => union.join
           case res => res
         }
@@ -1399,6 +1400,10 @@ object Types {
       case _ => true
     }
 
+    /** Is this (an alias of) the `scala.Null` type? */
+    final def isNull(given Context) =
+      isRef(defn.NullClass)
+
     /** The resultType of a LambdaType, or ExprType, the type itself for others */
     def resultType(implicit ctx: Context): Type = this
 
@@ -2293,7 +2298,7 @@ object Types {
   }
 
   /** The singleton type for path prefix#myDesignator.
-    */
+   */
   abstract case class TermRef(override val prefix: Type,
                               private var myDesignator: Designator)
     extends NamedType with SingletonType with ImplicitRef {
@@ -2886,6 +2891,23 @@ object Types {
       else apply(tp1, tp2)
   }
 
+  object OrNull with
+    private def stripNull(tp: Type)(given Context): Type = tp match
+      case tp @ OrType(tp1, tp2) =>
+        if tp1.isNull then tp2
+        else if tp2.isNull then tp1
+        else tp.derivedOrType(stripNull(tp1), stripNull(tp2))
+      case tp @ AndType(tp1, tp2) =>
+        tp.derivedAndType(stripNull(tp1), stripNull(tp2))
+      case _ =>
+        tp
+    def apply(tp: Type)(given Context) =
+      OrType(tp, defn.NullType)
+    def unapply(tp: Type)(given Context): Option[Type] =
+      val tp1 = stripNull(tp)
+      if tp1 ne tp then Some(tp1) else None
+  end OrNull
+
   // ----- ExprType and LambdaTypes -----------------------------------
 
   // Note: method types are cached whereas poly types are not. The reason

From 947c49e688543c543152ec5cb5a512432f1fac53 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Tue, 12 Nov 2019 10:59:21 +0100
Subject: [PATCH 27/37] Introduce NotNull type

NotNull is a common supertype of AnyRef and AnyVal. It will be interpreted specially
in type comparisons.
---
 .../src/dotty/tools/dotc/core/Definitions.scala    | 14 ++++++++++++--
 compiler/src/dotty/tools/dotc/core/StdNames.scala  |  1 +
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index b3d136d61811..e304fe701b2e 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -249,7 +249,9 @@ class Definitions {
    */
   @tu lazy val AnyClass: ClassSymbol = completeClass(enterCompleteClassSymbol(ScalaPackageClass, tpnme.Any, Abstract, Nil), ensureCtor = false)
   def AnyType: TypeRef = AnyClass.typeRef
-  @tu lazy val AnyValClass: ClassSymbol = completeClass(enterCompleteClassSymbol(ScalaPackageClass, tpnme.AnyVal, Abstract, List(AnyClass.typeRef)))
+  @tu lazy val AnyValClass: ClassSymbol = completeClass(
+    enterCompleteClassSymbol(ScalaPackageClass, tpnme.AnyVal, Abstract,
+      List(AnyClass.typeRef, NotNullClass.typeRef)))
   def AnyValType: TypeRef = AnyValClass.typeRef
 
     @tu lazy val Any_== : TermSymbol           = enterMethod(AnyClass, nme.EQ, methOfAny(BooleanType), Final)
@@ -278,7 +280,8 @@ class Definitions {
   @tu lazy val ObjectClass: ClassSymbol = {
     val cls = ctx.requiredClass("java.lang.Object")
     assert(!cls.isCompleted, "race for completing java.lang.Object")
-    cls.info = ClassInfo(cls.owner.thisType, cls, AnyClass.typeRef :: Nil, newScope)
+    cls.info = ClassInfo(cls.owner.thisType, cls,
+      List(AnyClass.typeRef, NotNullClass.typeRef), newScope)
     cls.setFlag(NoInits | JavaDefined)
 
     // The companion object doesn't really exist, so it needs to be marked as
@@ -403,6 +406,11 @@ class Definitions {
       List(AnyClass.typeRef), EmptyScope)
   @tu lazy val SingletonType: TypeRef = SingletonClass.typeRef
 
+  @tu lazy val NotNullClass: ClassSymbol =
+    enterCompleteClassSymbol(
+      ScalaPackageClass, tpnme.NotNull, PureInterfaceCreationFlags,
+      List(AnyClass.typeRef), EmptyScope)
+
   @tu lazy val CollectionSeqType: TypeRef = ctx.requiredClassRef("scala.collection.Seq")
   @tu lazy val SeqType: TypeRef = ctx.requiredClassRef("scala.collection.immutable.Seq")
   def SeqClass(given Context): ClassSymbol = SeqType.symbol.asClass
@@ -1290,6 +1298,7 @@ class Definitions {
       .updated(AnyClass, ObjectClass)
       .updated(AnyValClass, ObjectClass)
       .updated(SingletonClass, ObjectClass)
+      .updated(NotNullClass, ObjectClass)
       .updated(TupleClass, ObjectClass)
       .updated(NonEmptyTupleClass, ProductClass)
 
@@ -1306,6 +1315,7 @@ class Definitions {
     ByNameParamClass2x,
     AnyValClass,
     NullClass,
+    NotNullClass,
     NothingClass,
     SingletonClass)
 
diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala
index 58fdc137e6bf..e2171a3bbf0d 100644
--- a/compiler/src/dotty/tools/dotc/core/StdNames.scala
+++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala
@@ -195,6 +195,7 @@ object StdNames {
     final val ExprApi: N             = "ExprApi"
     final val Mirror: N              = "Mirror"
     final val Nothing: N             = "Nothing"
+    final val NotNull: N             = "NotNull"
     final val Null: N                = "Null"
     final val Object: N              = "Object"
     final val Product: N             = "Product"

From 62b756bac7f34807a70250a6395a20ed7351e315 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Tue, 12 Nov 2019 13:32:38 +0100
Subject: [PATCH 28/37] Simplify in widenRHS

When computing the type for local type inferennce, use a simplify
transformation.
---
 compiler/src/dotty/tools/dotc/core/Types.scala  | 1 +
 compiler/src/dotty/tools/dotc/typer/Namer.scala | 5 ++---
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 22513ae4d03a..90420ea420b2 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -2891,6 +2891,7 @@ object Types {
       else apply(tp1, tp2)
   }
 
+  /** An extractor for `T | Null` or `Null | T`, returning the `T` */
   object OrNull with
     private def stripNull(tp: Type)(given Context): Type = tp match
       case tp @ OrType(tp1, tp2) =>
diff --git a/compiler/src/dotty/tools/dotc/typer/Namer.scala b/compiler/src/dotty/tools/dotc/typer/Namer.scala
index 0228d7dc8ba5..e45205a4457a 100644
--- a/compiler/src/dotty/tools/dotc/typer/Namer.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala
@@ -1347,11 +1347,10 @@ class Namer { typer: Typer =>
       // We also drop the @Repeated annotation here to avoid leaking it in method result types
       // (see run/inferred-repeated-result).
       def widenRhs(tp: Type): Type = {
-        val tp1 = tp.widenTermRefExpr match {
+        val tp1 = tp.widenTermRefExpr.simplified match
           case ctp: ConstantType if isInlineVal => ctp
           case ref: TypeRef if ref.symbol.is(ModuleClass) => tp
-          case _ => tp.widenUnion
-        }
+          case tp => tp.widenUnion
         tp1.dropRepeatedAnnot
       }
 

From e6746e56cfee87383eea9bb961d12d0cc4f48e09 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Tue, 12 Nov 2019 13:36:31 +0100
Subject: [PATCH 29/37] Special treatment of NotNull in TypeComparer

Makes use of the fact that `Null & NotNull = Nothing`. This fact is
used in both type comparisons and glb operations.
---
 .../dotty/tools/dotc/core/TypeComparer.scala  | 67 ++++++++++++-------
 .../tools/dotc/interactive/Completion.scala   |  2 +-
 2 files changed, 43 insertions(+), 26 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index a881b361d553..715ef0f6c7ee 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -62,6 +62,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
   private var myAnyKindClass: ClassSymbol = null
   private var myNothingClass: ClassSymbol = null
   private var myNullClass: ClassSymbol = null
+  private var myNotNullClass: ClassSymbol = null
   private var myObjectClass: ClassSymbol = null
   private var myAnyType: TypeRef = null
   private var myAnyKindType: TypeRef = null
@@ -83,6 +84,10 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
     if (myNullClass == null) myNullClass = defn.NullClass
     myNullClass
   }
+  def NotNullClass: ClassSymbol =
+    if myNotNullClass == null then myNotNullClass = defn.NotNullClass
+    myNotNullClass
+
   def ObjectClass: ClassSymbol = {
     if (myObjectClass == null) myObjectClass = defn.ObjectClass
     myObjectClass
@@ -770,6 +775,15 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
         if (tp2a ne tp2) // Follow the alias; this might avoid truncating the search space in the either below
           return recur(tp1, tp2a)
 
+        if tp11.isRef(NotNullClass)
+          tp12.widen match
+            case OrNull(tp12a) if recur(tp12a, tp2) => return true
+            case _ =>
+        if tp12.isRef(NotNullClass)
+          tp11.widen match
+            case OrNull(tp11a) if recur(tp11a, tp2) => return true
+            case _ =>
+
         // Rewrite (T111 | T112) & T12 <: T2 to (T111 & T12) <: T2 and (T112 | T12) <: T2
         // and analogously for T11 & (T121 | T122) & T12 <: T2
         // `&' types to the left of <: are problematic, because
@@ -1042,7 +1056,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
      */
     def isNewSubType(tp1: Type): Boolean =
       if (isCovered(tp1) && isCovered(tp2))
-        //println(s"useless subtype: $tp1 <:< $tp2")
+        //println(i"useless subtype: $tp1 <:< $tp2")
         false
       else isSubType(tp1, tp2, approx.addLow)
 
@@ -1533,7 +1547,11 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    *  combiners are AppliedTypes, RefinedTypes, RecTypes, And/Or-Types or AnnotatedTypes.
    */
   private def isCovered(tp: Type): Boolean = tp.dealiasKeepRefiningAnnots.stripTypeVar match {
-    case tp: TypeRef => tp.symbol.isClass && tp.symbol != NothingClass && tp.symbol != NullClass
+    case tp: TypeRef =>
+      tp.symbol.isClass
+      && tp.symbol != NothingClass
+      && tp.symbol != NullClass
+      && tp.symbol != NotNullClass
     case tp: AppliedType => isCovered(tp.tycon)
     case tp: RefinedOrRecType => isCovered(tp.parent)
     case tp: AndType => isCovered(tp.tp1) && isCovered(tp.tp2)
@@ -1701,28 +1719,27 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
             tp11 & tp2 | tp12 & tp2
           case _ =>
             val tp1a = dropIfSuper(tp1, tp2)
-            if (tp1a ne tp1) glb(tp1a, tp2)
-            else {
-              val tp2a = dropIfSuper(tp2, tp1)
-              if (tp2a ne tp2) glb(tp1, tp2a)
-              else tp1 match {
-                case tp1: ConstantType =>
-                  tp2 match {
-                    case tp2: ConstantType =>
-                      // Make use of the fact that the intersection of two constant types
-                      // types which are not subtypes of each other is known to be empty.
-                      // Note: The same does not apply to singleton types in general.
-                      // E.g. we could have a pattern match against `x.type & y.type`
-                      // which might succeed if `x` and `y` happen to be the same ref
-                      // at run time. It would not work to replace that with `Nothing`.
-                      // However, maybe we can still apply the replacement to
-                      // types which are not explicitly written.
-                      NothingType
-                    case _ => andType(tp1, tp2)
-                  }
-                case _ => andType(tp1, tp2)
-              }
-            }
+            if (tp1a ne tp1) return glb(tp1a, tp2)
+            val tp2a = dropIfSuper(tp2, tp1)
+            if (tp2a ne tp2) return glb(tp1, tp2a)
+            tp1 match
+              case tp1: ConstantType =>
+                tp2 match
+                  case tp2: ConstantType =>
+                    // Make use of the fact that the intersection of two constant types
+                    // types which are not subtypes of each other is known to be empty.
+                    // Note: The same does not apply to singleton types in general.
+                    // E.g. we could have a pattern match against `x.type & y.type`
+                    // which might succeed if `x` and `y` happen to be the same ref
+                    // at run time. It would not work to replace that with `Nothing`.
+                    // However, maybe we can still apply the replacement to
+                    // types which are not explicitly written.
+                    return NothingType
+                  case _ =>
+              case _ =>
+            if tp1.isRef(NotNullClass) && tp2.isNull then return NothingType
+            if tp2.isRef(NotNullClass) && tp1.isNull then return NothingType
+            andType(tp1, tp2)
         }
     }
   }
@@ -1838,7 +1855,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
     else if (!tp2.exists) tp1
     else tp.derivedAndType(tp1, tp2)
 
-  /** If some (&-operand of) this type is a supertype of `sub` replace it with `NoType`.
+  /** If some (&-operand of) `tp` is a supertype of `sub` replace it with `NoType`.
    */
   private def dropIfSuper(tp: Type, sub: Type): Type =
     if (isSubTypeWhenFrozen(sub, tp)) NoType
diff --git a/compiler/src/dotty/tools/dotc/interactive/Completion.scala b/compiler/src/dotty/tools/dotc/interactive/Completion.scala
index d3178ba2bbca..ef573fb7a1df 100644
--- a/compiler/src/dotty/tools/dotc/interactive/Completion.scala
+++ b/compiler/src/dotty/tools/dotc/interactive/Completion.scala
@@ -207,7 +207,7 @@ object Completion {
     def addMemberCompletions(qual: Tree)(implicit ctx: Context): Unit =
       if (!qual.tpe.widenDealias.isBottomType) {
         addAccessibleMembers(qual.tpe)
-        if (!mode.is(Mode.Import) && !qual.tpe.isRef(defn.NullClass))
+        if (!mode.is(Mode.Import) && !qual.tpe.isNull)
           // Implicit conversions do not kick in when importing
           // and for `NullClass` they produce unapplicable completions (for unclear reasons)
           implicitConversionTargets(qual)(ctx.fresh.setExploreTyperState())

From f32f22a2cdfe2c5a6badf2ad5d8f9c4fba74d4ee Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Tue, 12 Nov 2019 13:39:36 +0100
Subject: [PATCH 30/37] Temporary hack to support testing

For now, we treat _every_ type spelled "Null" as the Null type. That way
we can introduce a user-level Null that sits next to AnyVal and AnyRef, like
the real Null will once explicit nulls are in. This hack should be reverted
once we have the changes for Null implemented.
---
 compiler/src/dotty/tools/dotc/core/Types.scala | 1 +
 1 file changed, 1 insertion(+)

diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala
index 90420ea420b2..b5edc3e59dd8 100644
--- a/compiler/src/dotty/tools/dotc/core/Types.scala
+++ b/compiler/src/dotty/tools/dotc/core/Types.scala
@@ -1403,6 +1403,7 @@ object Types {
     /** Is this (an alias of) the `scala.Null` type? */
     final def isNull(given Context) =
       isRef(defn.NullClass)
+      || classSymbol.name == tpnme.Null // !!! temporary kludge for being able to test without the explicit nulls PR
 
     /** The resultType of a LambdaType, or ExprType, the type itself for others */
     def resultType(implicit ctx: Context): Type = this

From e79dc4970c8ca3bc5e6bc78a23d0febe125d3b20 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Tue, 12 Nov 2019 13:40:17 +0100
Subject: [PATCH 31/37] Test case

This test implements a notNull operation and demonstrates that it works
as required.

Also: Fix repltest
---
 compiler/test-resources/repl/i5218 |  2 +-
 tests/pos/notNull.scala            | 21 +++++++++++++++++++++
 2 files changed, 22 insertions(+), 1 deletion(-)
 create mode 100644 tests/pos/notNull.scala

diff --git a/compiler/test-resources/repl/i5218 b/compiler/test-resources/repl/i5218
index 3402ed98e286..abe63009ef74 100644
--- a/compiler/test-resources/repl/i5218
+++ b/compiler/test-resources/repl/i5218
@@ -3,4 +3,4 @@ val tuple: (Int, String, Long) = (1,2,3)
 scala> 0.0 *: tuple
 val res0: (Double, Int, String, Long) = (0.0,1,2,3)
 scala> tuple ++ tuple
-val res1: Int *: String *: Long *: scala.Tuple.Concat[Unit, tuple.type] = (1,2,3,1,2,3)
\ No newline at end of file
+val res1: Int *: String *: Long *: tuple.type = (1,2,3,1,2,3)
diff --git a/tests/pos/notNull.scala b/tests/pos/notNull.scala
new file mode 100644
index 000000000000..2e043a042bf5
--- /dev/null
+++ b/tests/pos/notNull.scala
@@ -0,0 +1,21 @@
+trait Null extends Any
+object Test with
+  def notNull(x: Any): x.type & NotNull =
+    assert(x != null)
+    x.asInstanceOf  // TODO: drop the .asInstanceOf when explicit nulls are implemented
+
+  locally {
+    val x: (Int | Null) = ???
+    val y = x; val _: Int | Null = y
+  }
+  locally {
+    val x: (Int | Null) & NotNull = ???
+    val y = identity(x); val yc: Int = y
+    val z = x; val zc: Int = z
+  }
+  locally {
+    val x: Int | Null = ???
+    val y = notNull(identity(x)); val yc: Int = y
+    val z = notNull(x); val zc: Int = z
+  }
+

From e56743b30a69485ed1fd7212ec52de803456f8a6 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Tue, 12 Nov 2019 16:26:23 +0100
Subject: [PATCH 32/37] Blacklist notNull as from Tasty test

There seems to be a missing simplification when compiling from Tasty.
Here is the error message:

```
*** error while checking out/posTestFromTasty/pos/notNull/Test.class after phase readTasty ***
java.lang.AssertionError: assertion failed: Types differ
Original type : (x: Int): Int
After checking: (x: (Int | Null) & NotNull): (Int | Null) & NotNull
Original tree : identity[(Int | Null) & NotNull]
After checking: identity[(Int | Null) & NotNull]
```
---
 compiler/test/dotc/pos-from-tasty.blacklist | 1 +
 1 file changed, 1 insertion(+)

diff --git a/compiler/test/dotc/pos-from-tasty.blacklist b/compiler/test/dotc/pos-from-tasty.blacklist
index 4afb169cc85d..1fac00b403ab 100644
--- a/compiler/test/dotc/pos-from-tasty.blacklist
+++ b/compiler/test/dotc/pos-from-tasty.blacklist
@@ -12,3 +12,4 @@ i7087.scala
 
 # Nullability
 nullable.scala
+notNull.scala

From 84c0fdf108e3715e7e615c276d78194722ba4bcf Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Wed, 13 Nov 2019 12:53:53 +0100
Subject: [PATCH 33/37] Revert "Disable sjsJUnitTests"

This reverts commit 27c92a9a5958ba88bdc0809763b46d73125a7204.
---
 .drone.yml | 2 +-
 build.sbt  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/.drone.yml b/.drone.yml
index 303e2fdebc36..839cbb9a1aae 100644
--- a/.drone.yml
+++ b/.drone.yml
@@ -40,7 +40,7 @@ steps:
   depends_on: [ clone ]
   commands:
   - cp -R . /tmp/2/ && cd /tmp/2/
-  - ./project/scripts/sbt ";dotty-bootstrapped/compile ;dotty-bootstrapped/test ;dotty-staging/test"
+  - ./project/scripts/sbt ";dotty-bootstrapped/compile ;dotty-bootstrapped/test ;dotty-staging/test ;sjsSandbox/run;sjsSandbox/test;sjsJUnitTests/test"
   - ./project/scripts/bootstrapCmdTests
 
 - name: community_build
diff --git a/build.sbt b/build.sbt
index a613eadf4a4c..e4f27b72a3ad 100644
--- a/build.sbt
+++ b/build.sbt
@@ -23,7 +23,7 @@ val `dist-bootstrapped` = Build.`dist-bootstrapped`
 val `community-build` = Build.`community-build`
 
 val sjsSandbox = Build.sjsSandbox
-//val sjsJUnitTests = Build.sjsJUnitTests
+val sjsJUnitTests = Build.sjsJUnitTests
 
 val `sbt-dotty` = Build.`sbt-dotty`
 val `vscode-dotty` = Build.`vscode-dotty`

From b32e30ab9077b6c613f3d4cd7f1c9dad6e887453 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Wed, 13 Nov 2019 15:20:58 +0100
Subject: [PATCH 34/37] Address review suggestions

Better document Nullables.scala. Also, rename containsRef to impliesNotNull.
---
 .../dotty/tools/dotc/typer/ConstFold.scala    |  2 +-
 .../dotty/tools/dotc/typer/Nullables.scala    | 49 +++++++++++++------
 2 files changed, 35 insertions(+), 16 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/typer/ConstFold.scala b/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
index b715825f006a..0fd7174dc774 100644
--- a/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
+++ b/compiler/src/dotty/tools/dotc/typer/ConstFold.scala
@@ -21,7 +21,7 @@ object ConstFold {
   def apply[T <: Tree](tree: T)(implicit ctx: Context): T = finish(tree) {
     tree match {
       case CompareNull(TrackedRef(ref), testEqual)
-      if ctx.settings.YexplicitNulls.value && ctx.notNullInfos.containsRef(ref) =>
+      if ctx.settings.YexplicitNulls.value && ctx.notNullInfos.impliesNotNull(ref) =>
         // TODO maybe drop once we have general Nullability?
         Constant(!testEqual)
       case Apply(Select(xt, op), yt :: Nil) =>
diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index 2d9da99708ad..bb1ab9e75365 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -17,7 +17,7 @@ object Nullables with
   import ast.tpd._
 
   /** 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 null
+   *  variable references that are not known (anymore) to be not null
    */
   case class NotNullInfo(asserted: Set[TermRef], retracted: Set[TermRef])
     assert((asserted & retracted).isEmpty)
@@ -34,7 +34,9 @@ object Nullables with
         this.asserted.union(that.asserted).diff(that.retracted),
         this.retracted.union(that.retracted).diff(that.asserted))
 
-    /** The alternative path combination with another not-null info */
+    /** 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))
 
@@ -99,9 +101,9 @@ object Nullables with
   end TrackedRef
 
   /** Is given reference tracked for nullability?
-   *  This is the case if the reference is a path to an immutable val,
-   *  or if it refers to a local mutable variable where all assignments
-   *  to the variable are reachable.
+   *  This is the case if the reference is a path to an immutable val, or if it refers
+   *  to a local mutable variable where all assignments to the variable are _reachable_
+   *  (in the sense of how it is defined in assignmentSpans).
    */
   def isTracked(ref: TermRef)(given Context) =
     ref.isStable
@@ -114,10 +116,17 @@ object Nullables with
          && curCtx.compilationUnit.assignmentSpans.contains(sym.span.start)
       }
 
+  /** The nullability context to be used after a case that matches pattern `pat`.
+   *  If `pat` is `null`, this will assert that the selector `sel` is not null afterwards.
+   */
   def afterPatternContext(sel: Tree, pat: Tree)(given ctx: Context) = (sel, pat) match
     case (TrackedRef(ref), Literal(Constant(null))) => ctx.addNotNullRefs(Set(ref))
     case _ => ctx
 
+  /** The nullability context to be used for the guard and rhs of a case with
+   *  given pattern `pat`. If the pattern can only match non-null values, this
+   *  will assert that the selector `sel` is not null in these regions.
+   */
   def caseContext(sel: Tree, pat: Tree)(given ctx: Context): Context = sel match
     case TrackedRef(ref) if matchesNotNull(pat) => ctx.addNotNullRefs(Set(ref))
     case _ => ctx
@@ -129,19 +138,26 @@ object Nullables with
     case _ => false
 
   given (infos: List[NotNullInfo])
-    @tailRec
-    def containsRef(ref: TermRef): Boolean = infos match
+
+    /** Do the current not-null infos imply that `ref` is not null?
+     *  Not-null infos are as a history where earlier assertions and retractions replace
+     *  later ones (i.e. it records the assignment history in reverse, with most recent first)
+     */
+    @tailrec def impliesNotNull(ref: TermRef): Boolean = infos match
       case info :: infos1 =>
         if info.asserted.contains(ref) then true
         else if info.retracted.contains(ref) then false
-        else containsRef(infos1)(ref)
+        else impliesNotNull(infos1)(ref)
       case _ =>
         false
 
+    /** Add `info` as the most recent entry to the list of null infos. Assertions
+     *  or retractions in `info` supersede infos in existing entries of `infos`.
+     */
     def extendWith(info: NotNullInfo) =
       if info.isEmpty
-         || info.asserted.forall(infos.containsRef(_))
-            && !info.retracted.exists(infos.containsRef(_))
+         || info.asserted.forall(infos.impliesNotNull(_))
+            && !info.retracted.exists(infos.impliesNotNull(_))
       then infos
       else info :: infos
 
@@ -245,13 +261,16 @@ object Nullables with
 
   /** A map from (name-) offsets of all local variables in this compilation unit
    *  that can be tracked for being not null to the list of spans of assignments
-   *  to these variables. A variable can be tracked if it has only reachable assignments.
+   *  to these variables. A variable can be tracked if it has only reachable assignments
    *  An assignment is reachable if the path of tree nodes between the block enclosing
    *  the variable declaration to the assignment consists only of if-expressions,
    *  while-expressions, block-expressions and type-ascriptions.
    *  Only reachable assignments are handled correctly in the nullability analysis.
    *  Therefore, variables with unreachable assignments can be assumed to be not-null
    *  only if their type asserts it.
+   *
+   *  Note: we the local variables through their offset and not through their name
+   *  because of shadowing.
    */
   def assignmentSpans(given Context): Map[Int, List[Span]] =
     import ast.untpd._
@@ -305,7 +324,7 @@ object Nullables with
 
   /** The initial context to be used for a while expression with given span.
    *  In this context, all variables that are assigned within the while expression
-   *  have their nullability status retracted, i.e. are not known to be null.
+   *  have their nullability status retracted, i.e. are not known to be not null.
    *  While necessary for soundness, this scheme loses precision: Even if
    *  the initial state of the variable is not null and all assignments to the variable
    *  in the while expression are also known to be not null, the variable is still
@@ -323,8 +342,8 @@ object Nullables with
    *
    *     class Links(val elem: T, val next: Links | Null)
    *
-   *     var ys: Links | Null = Links(1, null)
-   *     var xs: Links | Null = xs
+   *     var xs: Links | Null = Links(1, null)
+   *     var ys: Links | Null = xs
    *     while xs != null
    *       ys = Links(xs.elem, ys.next)  // error in unrefined: ys is potentially null here
    *       xs = xs.next
@@ -334,7 +353,7 @@ object Nullables with
       val sym = ref.symbol
       sym.span.exists
       && assignmentSpans.getOrElse(sym.span.start, Nil).exists(whileSpan.contains(_))
-      && curCtx.notNullInfos.containsRef(ref)
+      && curCtx.notNullInfos.impliesNotNull(ref)
     val retractedVars = curCtx.notNullInfos.flatMap(_.asserted.filter(isRetracted)).toSet
     curCtx.addNotNullInfo(NotNullInfo(Set(), retractedVars))
 

From 1726660547de72fdab6eef80322a6a812378dfb1 Mon Sep 17 00:00:00 2001
From: Martin Odersky <odersky@gmail.com>
Date: Thu, 14 Nov 2019 09:09:09 +0100
Subject: [PATCH 35/37] Add notNull member to Any

Add a method $nn to Any that has type

    def $nn: this.type & NotNull

The method is marked as stable & realizable, which means it can appear in paths.
Special handling is required in asSeenFrom, to reflect the fact that $nn are not
real selections, i.e. the selected item has the same owner as the one in the prefix.

N.B. I tried to make $nn a field instead, but this caused AbstractMethod errors
for reasons I cannot quite track down.
---
 compiler/src/dotty/tools/dotc/core/Definitions.scala |  8 ++++++--
 compiler/src/dotty/tools/dotc/core/StdNames.scala    |  1 +
 compiler/src/dotty/tools/dotc/core/TypeErasure.scala |  1 +
 compiler/src/dotty/tools/dotc/core/TypeOps.scala     |  2 +-
 .../src/dotty/tools/dotc/transform/Erasure.scala     |  2 ++
 compiler/src/dotty/tools/dotc/typer/Nullables.scala  |  2 +-
 compiler/src/dotty/tools/repl/ReplDriver.scala       |  2 +-
 tests/pos/notNull.scala                              | 12 ++++++++++++
 tests/run-macros/i6518.check                         |  1 +
 9 files changed, 26 insertions(+), 5 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index e304fe701b2e..cd5b19c054be 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -254,7 +254,7 @@ class Definitions {
       List(AnyClass.typeRef, NotNullClass.typeRef)))
   def AnyValType: TypeRef = AnyValClass.typeRef
 
-    @tu lazy val Any_== : TermSymbol           = enterMethod(AnyClass, nme.EQ, methOfAny(BooleanType), Final)
+    @tu lazy val Any_== : TermSymbol          = enterMethod(AnyClass, nme.EQ, methOfAny(BooleanType), Final)
     @tu lazy val Any_!= : TermSymbol          = enterMethod(AnyClass, nme.NE, methOfAny(BooleanType), Final)
     @tu lazy val Any_equals: TermSymbol       = enterMethod(AnyClass, nme.equals_, methOfAny(BooleanType))
     @tu lazy val Any_hashCode: TermSymbol     = enterMethod(AnyClass, nme.hashCode_, MethodType(Nil, IntType))
@@ -263,6 +263,8 @@ class Definitions {
     @tu lazy val Any_isInstanceOf: TermSymbol = enterT1ParameterlessMethod(AnyClass, nme.isInstanceOf_, _ => BooleanType, Final)
     @tu lazy val Any_asInstanceOf: TermSymbol = enterT1ParameterlessMethod(AnyClass, nme.asInstanceOf_, _.paramRefs(0), Final)
     @tu lazy val Any_typeTest: TermSymbol     = enterT1ParameterlessMethod(AnyClass, nme.isInstanceOfPM, _ => BooleanType, Final | Synthetic | Artifact)
+    @tu lazy val Any_notNull: TermSymbol      = newSymbol(AnyClass, nme.NOT_NULL, Method | Final | Erased | Artifact| StableRealizable,
+                                                          AndType(AnyClass.thisType, NotNullClass.typeRef)).entered
     @tu lazy val Any_typeCast: TermSymbol     = enterT1ParameterlessMethod(AnyClass, nme.asInstanceOfPM, _.paramRefs(0), Final | Synthetic | Artifact | StableRealizable)
       // generated by pattern matcher, eliminated by erasure
 
@@ -275,7 +277,9 @@ class Definitions {
           bounds = TypeBounds.lower(AnyClass.thisType))
 
     private def AnyMethods: List[TermSymbol] = List(Any_==, Any_!=, Any_equals, Any_hashCode,
-      Any_toString, Any_##, Any_getClass, Any_isInstanceOf, Any_asInstanceOf, Any_typeTest, Any_typeCast)
+      Any_toString, Any_##, Any_getClass, Any_isInstanceOf, Any_asInstanceOf, Any_typeTest, Any_typeCast, Any_notNull)
+
+    def isAny_notNull(sym: Symbol)(given Context) = sym.name == nme.NOT_NULL && sym == Any_notNull
 
   @tu lazy val ObjectClass: ClassSymbol = {
     val cls = ctx.requiredClass("java.lang.Object")
diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala
index e2171a3bbf0d..fa6a32d775a8 100644
--- a/compiler/src/dotty/tools/dotc/core/StdNames.scala
+++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala
@@ -262,6 +262,7 @@ object StdNames {
     val MIRROR_PREFIX: N            = "$m."
     val MIRROR_SHORT: N             = "$m"
     val MIRROR_UNTYPED: N           = "$m$untyped"
+    val NOT_NULL: N                 = "$nn"
     val REIFY_FREE_PREFIX: N        = "free$"
     val REIFY_FREE_THIS_SUFFIX: N   = "$this"
     val REIFY_FREE_VALUE_SUFFIX: N  = "$value"
diff --git a/compiler/src/dotty/tools/dotc/core/TypeErasure.scala b/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
index 700fe6134940..5fa150d5ce6b 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
@@ -197,6 +197,7 @@ object TypeErasure {
     else if (sym.isAbstractType) TypeAlias(WildcardType)
     else if (sym.isConstructor) outer.addParam(sym.owner.asClass, erase(tp)(erasureCtx))
     else if (sym.is(Label)) erase.eraseResult(sym.info)(erasureCtx)
+    else if sym.is(Erased) && defn.isAny_notNull(sym) then NoType // Q: Should we delete all erased symbols that way?
     else erase.eraseInfo(tp, sym)(erasureCtx) match {
       case einfo: MethodType =>
         if (sym.isGetter && einfo.resultType.isRef(defn.UnitClass))
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
index f0a710ea8b17..dd0467c1ef35 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeOps.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -81,7 +81,7 @@ trait TypeOps { this: Context => // TODO: Make standalone object.
                   // called which we override to set the `approximated` flag.
                   range(defn.NothingType, pre)
               else pre
-            else if ((pre.termSymbol is Package) && !(thiscls is Package))
+            else if (pre.termSymbol.is(Package) && !thiscls.is(Package))
               toPrefix(pre.select(nme.PACKAGE), cls, thiscls)
             else
               toPrefix(pre.baseType(cls).normalizedPrefix, cls.owner, thiscls)
diff --git a/compiler/src/dotty/tools/dotc/transform/Erasure.scala b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
index 5f72f9214584..3f0083d4fd1a 100644
--- a/compiler/src/dotty/tools/dotc/transform/Erasure.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
@@ -426,6 +426,8 @@ object Erasure {
      *      e.m -> e.[]m                if `m` is an array operation other than `clone`.
      */
     override def typedSelect(tree: untpd.Select, pt: Type)(implicit ctx: Context): Tree = {
+      if defn.isAny_notNull(tree.symbol) then return typed(tree.qualifier, pt)
+
       val qual1 = typed(tree.qualifier, AnySelectionProto)
 
       def mapOwner(sym: Symbol): Symbol = {
diff --git a/compiler/src/dotty/tools/dotc/typer/Nullables.scala b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
index bb1ab9e75365..d3b2d146d9c1 100644
--- a/compiler/src/dotty/tools/dotc/typer/Nullables.scala
+++ b/compiler/src/dotty/tools/dotc/typer/Nullables.scala
@@ -269,7 +269,7 @@ object Nullables with
    *  Therefore, variables with unreachable assignments can be assumed to be not-null
    *  only if their type asserts it.
    *
-   *  Note: we the local variables through their offset and not through their name
+   *  Note: we track the local variables through their offset and not through their name
    *  because of shadowing.
    */
   def assignmentSpans(given Context): Map[Int, List[Span]] =
diff --git a/compiler/src/dotty/tools/repl/ReplDriver.scala b/compiler/src/dotty/tools/repl/ReplDriver.scala
index acfa33f02765..e181ff042c72 100644
--- a/compiler/src/dotty/tools/repl/ReplDriver.scala
+++ b/compiler/src/dotty/tools/repl/ReplDriver.scala
@@ -272,7 +272,7 @@ class ReplDriver(settings: Array[String],
 
       val vals =
         info.fields
-          .filterNot(_.symbol.isOneOf(ParamAccessor | Private | Synthetic | Module))
+          .filterNot(_.symbol.isOneOf(ParamAccessor | Private | Synthetic | Artifact | Module))
           .filter(_.symbol.name.is(SimpleNameKind))
           .sortBy(_.name)
 
diff --git a/tests/pos/notNull.scala b/tests/pos/notNull.scala
index 2e043a042bf5..7af610c70a42 100644
--- a/tests/pos/notNull.scala
+++ b/tests/pos/notNull.scala
@@ -18,4 +18,16 @@ object Test with
     val y = notNull(identity(x)); val yc: Int = y
     val z = notNull(x); val zc: Int = z
   }
+  locally {
+    val x: Int | Null = ???
+    val y = identity(x).$nn; val yc: Int = y
+    val z = x.$nn; val zc: Int = z
+  }
+  class C { type T }
+  locally {
+    val x: C { type T = Int } = new C { type T = Int }
+    val y: x.$nn.T = 33
+    val z = y; val zc: Int = z
+  }
+
 
diff --git a/tests/run-macros/i6518.check b/tests/run-macros/i6518.check
index 388ef88a5170..2038e177254f 100644
--- a/tests/run-macros/i6518.check
+++ b/tests/run-macros/i6518.check
@@ -2,6 +2,7 @@
 ##
 $asInstanceOf$
 $isInstanceOf$
+$nn
 ==
 andThen
 apply

From 434204f5890d3f43ce778fb20b5d1be8150f07ea Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= <sjrdoeraene@gmail.com>
Date: Thu, 14 Nov 2019 16:27:55 +0100
Subject: [PATCH 36/37] Use a definition of `def notNull` that does not require
 `NotNull`.

---
 tests/pos/notNull.scala | 17 +++--------------
 1 file changed, 3 insertions(+), 14 deletions(-)

diff --git a/tests/pos/notNull.scala b/tests/pos/notNull.scala
index 7af610c70a42..3d46fe658948 100644
--- a/tests/pos/notNull.scala
+++ b/tests/pos/notNull.scala
@@ -1,6 +1,6 @@
 trait Null extends Any
 object Test with
-  def notNull(x: Any): x.type & NotNull =
+  def notNull[A](x: A | Null): x.type & A =
     assert(x != null)
     x.asInstanceOf  // TODO: drop the .asInstanceOf when explicit nulls are implemented
 
@@ -8,26 +8,15 @@ object Test with
     val x: (Int | Null) = ???
     val y = x; val _: Int | Null = y
   }
-  locally {
-    val x: (Int | Null) & NotNull = ???
-    val y = identity(x); val yc: Int = y
-    val z = x; val zc: Int = z
-  }
   locally {
     val x: Int | Null = ???
     val y = notNull(identity(x)); val yc: Int = y
     val z = notNull(x); val zc: Int = z
   }
-  locally {
-    val x: Int | Null = ???
-    val y = identity(x).$nn; val yc: Int = y
-    val z = x.$nn; val zc: Int = z
-  }
   class C { type T }
   locally {
     val x: C { type T = Int } = new C { type T = Int }
-    val y: x.$nn.T = 33
+    val xnn: x.type & C { type T = Int } = notNull(x)
+    val y: xnn.T = 33
     val z = y; val zc: Int = z
   }
-
-

From 016f47191c75c386f0af1cbfba041506ce9e5830 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Doeraene?= <sjrdoeraene@gmail.com>
Date: Thu, 14 Nov 2019 16:28:17 +0100
Subject: [PATCH 37/37] Revert all the changes that added NonNull.

---
 .../dotty/tools/dotc/core/Definitions.scala   | 24 ++-----
 .../dotty/tools/dotc/core/TypeComparer.scala  | 65 +++++++------------
 .../dotty/tools/dotc/core/TypeErasure.scala   |  1 -
 .../dotty/tools/dotc/transform/Erasure.scala  |  2 -
 tests/run-macros/i6518.check                  |  1 -
 5 files changed, 29 insertions(+), 64 deletions(-)

diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
index cd5b19c054be..d4f78f93155e 100644
--- a/compiler/src/dotty/tools/dotc/core/Definitions.scala
+++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -249,12 +249,10 @@ class Definitions {
    */
   @tu lazy val AnyClass: ClassSymbol = completeClass(enterCompleteClassSymbol(ScalaPackageClass, tpnme.Any, Abstract, Nil), ensureCtor = false)
   def AnyType: TypeRef = AnyClass.typeRef
-  @tu lazy val AnyValClass: ClassSymbol = completeClass(
-    enterCompleteClassSymbol(ScalaPackageClass, tpnme.AnyVal, Abstract,
-      List(AnyClass.typeRef, NotNullClass.typeRef)))
+  @tu lazy val AnyValClass: ClassSymbol = completeClass(enterCompleteClassSymbol(ScalaPackageClass, tpnme.AnyVal, Abstract, List(AnyClass.typeRef)))
   def AnyValType: TypeRef = AnyValClass.typeRef
 
-    @tu lazy val Any_== : TermSymbol          = enterMethod(AnyClass, nme.EQ, methOfAny(BooleanType), Final)
+    @tu lazy val Any_== : TermSymbol           = enterMethod(AnyClass, nme.EQ, methOfAny(BooleanType), Final)
     @tu lazy val Any_!= : TermSymbol          = enterMethod(AnyClass, nme.NE, methOfAny(BooleanType), Final)
     @tu lazy val Any_equals: TermSymbol       = enterMethod(AnyClass, nme.equals_, methOfAny(BooleanType))
     @tu lazy val Any_hashCode: TermSymbol     = enterMethod(AnyClass, nme.hashCode_, MethodType(Nil, IntType))
@@ -263,8 +261,6 @@ class Definitions {
     @tu lazy val Any_isInstanceOf: TermSymbol = enterT1ParameterlessMethod(AnyClass, nme.isInstanceOf_, _ => BooleanType, Final)
     @tu lazy val Any_asInstanceOf: TermSymbol = enterT1ParameterlessMethod(AnyClass, nme.asInstanceOf_, _.paramRefs(0), Final)
     @tu lazy val Any_typeTest: TermSymbol     = enterT1ParameterlessMethod(AnyClass, nme.isInstanceOfPM, _ => BooleanType, Final | Synthetic | Artifact)
-    @tu lazy val Any_notNull: TermSymbol      = newSymbol(AnyClass, nme.NOT_NULL, Method | Final | Erased | Artifact| StableRealizable,
-                                                          AndType(AnyClass.thisType, NotNullClass.typeRef)).entered
     @tu lazy val Any_typeCast: TermSymbol     = enterT1ParameterlessMethod(AnyClass, nme.asInstanceOfPM, _.paramRefs(0), Final | Synthetic | Artifact | StableRealizable)
       // generated by pattern matcher, eliminated by erasure
 
@@ -276,16 +272,13 @@ class Definitions {
           Final,
           bounds = TypeBounds.lower(AnyClass.thisType))
 
-    private def AnyMethods: List[TermSymbol] = List(Any_==, Any_!=, Any_equals, Any_hashCode,
-      Any_toString, Any_##, Any_getClass, Any_isInstanceOf, Any_asInstanceOf, Any_typeTest, Any_typeCast, Any_notNull)
-
-    def isAny_notNull(sym: Symbol)(given Context) = sym.name == nme.NOT_NULL && sym == Any_notNull
+    def AnyMethods: List[TermSymbol] = List(Any_==, Any_!=, Any_equals, Any_hashCode,
+      Any_toString, Any_##, Any_getClass, Any_isInstanceOf, Any_asInstanceOf, Any_typeTest, Any_typeCast)
 
   @tu lazy val ObjectClass: ClassSymbol = {
     val cls = ctx.requiredClass("java.lang.Object")
     assert(!cls.isCompleted, "race for completing java.lang.Object")
-    cls.info = ClassInfo(cls.owner.thisType, cls,
-      List(AnyClass.typeRef, NotNullClass.typeRef), newScope)
+    cls.info = ClassInfo(cls.owner.thisType, cls, AnyClass.typeRef :: Nil, newScope)
     cls.setFlag(NoInits | JavaDefined)
 
     // The companion object doesn't really exist, so it needs to be marked as
@@ -410,11 +403,6 @@ class Definitions {
       List(AnyClass.typeRef), EmptyScope)
   @tu lazy val SingletonType: TypeRef = SingletonClass.typeRef
 
-  @tu lazy val NotNullClass: ClassSymbol =
-    enterCompleteClassSymbol(
-      ScalaPackageClass, tpnme.NotNull, PureInterfaceCreationFlags,
-      List(AnyClass.typeRef), EmptyScope)
-
   @tu lazy val CollectionSeqType: TypeRef = ctx.requiredClassRef("scala.collection.Seq")
   @tu lazy val SeqType: TypeRef = ctx.requiredClassRef("scala.collection.immutable.Seq")
   def SeqClass(given Context): ClassSymbol = SeqType.symbol.asClass
@@ -1302,7 +1290,6 @@ class Definitions {
       .updated(AnyClass, ObjectClass)
       .updated(AnyValClass, ObjectClass)
       .updated(SingletonClass, ObjectClass)
-      .updated(NotNullClass, ObjectClass)
       .updated(TupleClass, ObjectClass)
       .updated(NonEmptyTupleClass, ProductClass)
 
@@ -1319,7 +1306,6 @@ class Definitions {
     ByNameParamClass2x,
     AnyValClass,
     NullClass,
-    NotNullClass,
     NothingClass,
     SingletonClass)
 
diff --git a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
index 715ef0f6c7ee..1b902d20e016 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeComparer.scala
@@ -62,7 +62,6 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
   private var myAnyKindClass: ClassSymbol = null
   private var myNothingClass: ClassSymbol = null
   private var myNullClass: ClassSymbol = null
-  private var myNotNullClass: ClassSymbol = null
   private var myObjectClass: ClassSymbol = null
   private var myAnyType: TypeRef = null
   private var myAnyKindType: TypeRef = null
@@ -84,10 +83,6 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
     if (myNullClass == null) myNullClass = defn.NullClass
     myNullClass
   }
-  def NotNullClass: ClassSymbol =
-    if myNotNullClass == null then myNotNullClass = defn.NotNullClass
-    myNotNullClass
-
   def ObjectClass: ClassSymbol = {
     if (myObjectClass == null) myObjectClass = defn.ObjectClass
     myObjectClass
@@ -775,15 +770,6 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
         if (tp2a ne tp2) // Follow the alias; this might avoid truncating the search space in the either below
           return recur(tp1, tp2a)
 
-        if tp11.isRef(NotNullClass)
-          tp12.widen match
-            case OrNull(tp12a) if recur(tp12a, tp2) => return true
-            case _ =>
-        if tp12.isRef(NotNullClass)
-          tp11.widen match
-            case OrNull(tp11a) if recur(tp11a, tp2) => return true
-            case _ =>
-
         // Rewrite (T111 | T112) & T12 <: T2 to (T111 & T12) <: T2 and (T112 | T12) <: T2
         // and analogously for T11 & (T121 | T122) & T12 <: T2
         // `&' types to the left of <: are problematic, because
@@ -1056,7 +1042,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
      */
     def isNewSubType(tp1: Type): Boolean =
       if (isCovered(tp1) && isCovered(tp2))
-        //println(i"useless subtype: $tp1 <:< $tp2")
+        //println(s"useless subtype: $tp1 <:< $tp2")
         false
       else isSubType(tp1, tp2, approx.addLow)
 
@@ -1547,11 +1533,7 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
    *  combiners are AppliedTypes, RefinedTypes, RecTypes, And/Or-Types or AnnotatedTypes.
    */
   private def isCovered(tp: Type): Boolean = tp.dealiasKeepRefiningAnnots.stripTypeVar match {
-    case tp: TypeRef =>
-      tp.symbol.isClass
-      && tp.symbol != NothingClass
-      && tp.symbol != NullClass
-      && tp.symbol != NotNullClass
+    case tp: TypeRef => tp.symbol.isClass && tp.symbol != NothingClass && tp.symbol != NullClass
     case tp: AppliedType => isCovered(tp.tycon)
     case tp: RefinedOrRecType => isCovered(tp.parent)
     case tp: AndType => isCovered(tp.tp1) && isCovered(tp.tp2)
@@ -1719,27 +1701,28 @@ class TypeComparer(initctx: Context) extends ConstraintHandling[AbsentContext] w
             tp11 & tp2 | tp12 & tp2
           case _ =>
             val tp1a = dropIfSuper(tp1, tp2)
-            if (tp1a ne tp1) return glb(tp1a, tp2)
-            val tp2a = dropIfSuper(tp2, tp1)
-            if (tp2a ne tp2) return glb(tp1, tp2a)
-            tp1 match
-              case tp1: ConstantType =>
-                tp2 match
-                  case tp2: ConstantType =>
-                    // Make use of the fact that the intersection of two constant types
-                    // types which are not subtypes of each other is known to be empty.
-                    // Note: The same does not apply to singleton types in general.
-                    // E.g. we could have a pattern match against `x.type & y.type`
-                    // which might succeed if `x` and `y` happen to be the same ref
-                    // at run time. It would not work to replace that with `Nothing`.
-                    // However, maybe we can still apply the replacement to
-                    // types which are not explicitly written.
-                    return NothingType
-                  case _ =>
-              case _ =>
-            if tp1.isRef(NotNullClass) && tp2.isNull then return NothingType
-            if tp2.isRef(NotNullClass) && tp1.isNull then return NothingType
-            andType(tp1, tp2)
+            if (tp1a ne tp1) glb(tp1a, tp2)
+            else {
+              val tp2a = dropIfSuper(tp2, tp1)
+              if (tp2a ne tp2) glb(tp1, tp2a)
+              else tp1 match {
+                case tp1: ConstantType =>
+                  tp2 match {
+                    case tp2: ConstantType =>
+                      // Make use of the fact that the intersection of two constant types
+                      // types which are not subtypes of each other is known to be empty.
+                      // Note: The same does not apply to singleton types in general.
+                      // E.g. we could have a pattern match against `x.type & y.type`
+                      // which might succeed if `x` and `y` happen to be the same ref
+                      // at run time. It would not work to replace that with `Nothing`.
+                      // However, maybe we can still apply the replacement to
+                      // types which are not explicitly written.
+                      NothingType
+                    case _ => andType(tp1, tp2)
+                  }
+                case _ => andType(tp1, tp2)
+              }
+            }
         }
     }
   }
diff --git a/compiler/src/dotty/tools/dotc/core/TypeErasure.scala b/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
index 5fa150d5ce6b..700fe6134940 100644
--- a/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
+++ b/compiler/src/dotty/tools/dotc/core/TypeErasure.scala
@@ -197,7 +197,6 @@ object TypeErasure {
     else if (sym.isAbstractType) TypeAlias(WildcardType)
     else if (sym.isConstructor) outer.addParam(sym.owner.asClass, erase(tp)(erasureCtx))
     else if (sym.is(Label)) erase.eraseResult(sym.info)(erasureCtx)
-    else if sym.is(Erased) && defn.isAny_notNull(sym) then NoType // Q: Should we delete all erased symbols that way?
     else erase.eraseInfo(tp, sym)(erasureCtx) match {
       case einfo: MethodType =>
         if (sym.isGetter && einfo.resultType.isRef(defn.UnitClass))
diff --git a/compiler/src/dotty/tools/dotc/transform/Erasure.scala b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
index 3f0083d4fd1a..5f72f9214584 100644
--- a/compiler/src/dotty/tools/dotc/transform/Erasure.scala
+++ b/compiler/src/dotty/tools/dotc/transform/Erasure.scala
@@ -426,8 +426,6 @@ object Erasure {
      *      e.m -> e.[]m                if `m` is an array operation other than `clone`.
      */
     override def typedSelect(tree: untpd.Select, pt: Type)(implicit ctx: Context): Tree = {
-      if defn.isAny_notNull(tree.symbol) then return typed(tree.qualifier, pt)
-
       val qual1 = typed(tree.qualifier, AnySelectionProto)
 
       def mapOwner(sym: Symbol): Symbol = {
diff --git a/tests/run-macros/i6518.check b/tests/run-macros/i6518.check
index 2038e177254f..388ef88a5170 100644
--- a/tests/run-macros/i6518.check
+++ b/tests/run-macros/i6518.check
@@ -2,7 +2,6 @@
 ##
 $asInstanceOf$
 $isInstanceOf$
-$nn
 ==
 andThen
 apply