Refine comments

Author: noti0na1

compiler/src/dotty/tools/dotc/typer/Nullables.scala

@@ -105,17 +105,50 @@ object Nullables with
    *  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).
+   *
+   *  A mutable vriable is trackable with following restrictions:
+   *  1. All the assignment must be reachable by the definition.
+   *  2. We only analyze the comparisons and use the facts in the same closure as
+   *    the definition.
+   *
+   *  ```scala
+   *  var x: String|Null = ???
+   *  def y = {
+   *    x = null
+   *  }
+   *  if (x != null) {
+   *    // y can be called here
+   *    val a: String = x // error: x is captured and mutated by the closure, not tackable
+   *  }
+   *  ```
+   *
+   *  ```scala
+   *  var x: String|Null = ???
+   *  def y = {
+   *    if (x != null) {
+   *      // not safe to use the fact (x != null) here
+   *      // since y can be executed at the same time as the outer block
+   *      val _: String = x
+   *    }
+   *  }
+   *  if (x != null) {
+   *    val a: String = x // ok to use the fact here
+   *    x = null
+   *  }
+   *  ```
+   *
+   *  See more examples in `tests/explicit-nulls/neg/var-ref-in-closure.scala`.
    */
   def isTracked(ref: TermRef)(given Context) =
     ref.isStable
     || { val sym = ref.symbol
          sym.is(Mutable)
          && sym.owner.isTerm
-         && (if sym.owner != curCtx.owner then
-              // TODO: need to check by-name parameters
-              !curCtx.owner.is(Flags.Lazy) // not at the rhs of lazy ValDef
-              && sym.owner.enclosingMethod == curCtx.owner.enclosingMethod // not in different DefDef
-            else true)
+         && ( sym.owner == curCtx.owner
+          || !curCtx.owner.is(Flags.Lazy) // not at the rhs of lazy ValDef
+            && sym.owner.enclosingMethod == curCtx.owner.enclosingMethod // not in different methods
+            // TODO: need to check by-name paramter
+          )
          && sym.span.exists
          && curCtx.compilationUnit != null // could be null under -Ytest-pickler
          && curCtx.compilationUnit.assignmentSpans.contains(sym.span.start)

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -348,6 +348,8 @@ class Typer extends Namer
     findRefRecur(NoType, BindingPrec.NothingBound, NoContext)
   }
 
+  // If `tree`'s type is a `TermRef` identified by flow typing to be non-null, then
+  // cast away `tree`s nullability. Otherwise, `tree` remains unchanged.
   def toNotNullTermRef(tree: Tree, pt: Type)(implicit ctx: Context): Tree = tree.tpe match
     case ref @ OrNull(tpnn) : TermRef
     if pt != AssignProto && // Ensure it is not the lhs of Assign

docs/docs/internals/explicit-nulls.md

@@ -90,20 +90,51 @@ are methods of the `Type` class, so call them with `this` as a receiver:
 
 - `isNullableUnion` determines whether `this` is a nullable union.
 - `isJavaNullableUnion` determines whether `this` is syntactically a union of the form
-  `T|JavaNull`
+  `T|JavaNull`.
 - `stripNull` syntactically strips all `Null` types in the union:
   e.g. `String|Null => String`.
 - `stripAllJavaNull` is like `stripNull` but only removes `JavaNull` from the union.
   This is needed when we want to "revert" the Java nullification function.
 
 ## Flow Typing
 
-`NotNullInfo`s are collected as we typing each statements, see `Nullables.scala` for more
-details about how we compute `NotNullInfo`s.
+As typing happens, we accumulate a set of `NotNullInfo`s in the `Context` (see
+`Contexts.scala`). A `NotNullInfo` contains the set of `TermRef`s that are known to
+be non-null at the current program point.  See `Nullables.scala` for how `NotNullInfo`s
+are computed.
 
-When we type an identity or a select tree (in `typedIdent` and `typedSelect`), we will
-call `toNotNullTermRef` on the tree before reture the result. If the tree `x` has nullable
-type `T|Null` and it is known to be not null according to the `NotNullInfo` and it is not
-on the lhs of assignment, then we cast it to `x.type & T` using `defn.Any_typeCast`. The
-reason to have a `TermRef(x)` in the `AndType` is that we can track the new result as well and
-use it as a path.
+During type-checking, when we type an identity or a select tree (in `typedIdent` and
+`typedSelect`), we will call `toNotNullTermRef` on the tree before return the typed tree.
+If the tree `x` has nullable type `T|Null` and it is known to be not null according to
+the `NotNullInfo` and it is not on the lhs of assignment, then we cast it to `x.type & T`
+using `defn.Any_typeCast`.
+
+The reason for casting to `x.type & T`, as opposed to just `T`, is that it allows us to
+support flow typing for paths of length greater than one.
+
+```scala
+abstract class Node {
+  val x: String
+  val next: Node | Null
+}
+
+def f = {
+  val l: Node|Null = ???
+  if (l != null && l.next != null) {
+    val third: l.next.next.type = l.next.next
+  }
+}
+```
+
+After typing, `f` becomes:
+
+```scala
+def f = {
+  val l: Node|Null = ???
+  if (l != null && l.$asInstanceOf$[l.type & Node].next != null) {
+    val third:
+      l.$asInstanceOf$[l.type & Node].next.$asInstanceOf$[(l.type & Node).next.type & Node].next.type =
+      l.$asInstanceOf$[l.type & Node].next.$asInstanceOf$[(l.type & Node).next.type & Node].next
+  }
+}
+```