Promotion based on a non-null test: Implementation more flexible than specification

[eernstg]

Consider the following declaration:

void f<X>(X x) {
  if (x is int?) {
    // `x` has been promoted to `X & int?`.
    X x1 = x;
    x?.isEven;
    if (x != null) {
      // `x` has been promoted to `X & int`.
      X x2 = x;
      x.isEven;
    }
  }
}

This program is accepted by the analyzer as well as the CFE (DartPad, 'Based on Flutter 3.0.1 Dart SDK 2.17.1'), and it illustrates that the test x != null can promote a variable from X & int? to X & int.

The specification language for this case would be the following:

A check of the form e != null or of the form e is T where e has static type T? promotes the type of e to T in the true continuation, and to Null in the false continuation.

However, that rule only handles the case where the variable has a type of the form T?, and X & int? is not such a type. Do we need to generalize the specification a little bit in order to describe what the tools are currently doing?

@leafpetersen, WDYT?

[leafpetersen]

@stereotype441 @johnniwinther might be useful to start with a short explanation of what the implementation is doing?

[stereotype441]

Yeah, that spec language doesn't adequately capture what the implementations are doing. The key implementation methods are the tryPromoteToType methods (which handle is and as promotions), and the promoteToNonNull methods (which handle null checks). These are in pkg/front_end/lib/src/fasta/type_inference/type_inference_engine.dart for the front end, and pkg/analyzer/lib/src/dart/resolver/flow_analysis_visitor.dart.

The front end implementation of promoteToNonNull is particularly instructive for this example. If you follow the thread, you'll see that it winds up in _NonNullVisitor.visitTypeParameterType, which has this comment:

    // NonNull(X) = X & NonNull(B), where B is the bound of X.
    //
    // NonNull(X & T) = X & NonNull(T)
    //
    // NonNull(T?) = NonNull(T)
    //
    // NonNull(T*) = NonNull(T)

So, for the example above, the test if (x != null) promotes from X & int? to NonNull(X & int?), which evaluates to X & NonNull(int?), which is X & int.

I think the NonNull function is described in the spec somewhere. So maybe all we have to do is update the spec to say something like:

A check of the form e != null where e has static type T promotes the type of e to NonNull(T).

This change would also address two other problems with that spec text you quoted:

• The spec text you quoted implies that we use the same rule for handling e != null and e is T where e has static type T?.
  We don't--it's handled in an entirely separate code path (tryPromoteToType). Although the effect is largely the same in simple cases, it's not obvious to me that they're equivalent in all cases, and it seems bad to spec it in a way that's so different from how it's implemented.
• The spec text you quoted says that we promote to Null in the false continuation. We don't. Initially we intended to do so, and it was an oversight that we forgot to. But later I did an investigation of how it would affect users' code if we did promote to Null in the false continuation, and decided that the drawbacks outweigh the benefits. See the discusison here: 'null' isn't promoted to 'Null'. #1505

[eernstg]

@leafpetersen and @stereotype441, here's the proposed updated text in the specification (a PR that introduces new sections about null safety):

\LMHash{}%
\BlindDefineSymbol{\ell, v}%
Let $\ell$ be a location,
and let $v$ be a local variable which is in scope at $\ell$.
Assume that $\ell$ occurs after the declaration of $v$.
The expressions that give rise to promotion or demotion
of the type of $v$ at $\ell$
are the following:

\begin{itemize}
\item A type test of the form \code{$v$\,\,\IS\,\,$T$}.
\item A type check of the form \code{$v$\,\,\AS\,\,$T$}.
\item An assignment of the form \code{$v$\,\,=\,\,$e$}
  where the static type of $e$ is a type of interest for $v$ at $\ell$,
  and similarly for compound assignments
  (\ref{compoundAssignment})
  including \lit{??=}.
\item An equality test of the form \code{$v$\,\,==\,\,$e$} or
  \code{$e$\,\,==\,\,$v$}, where $e$ is \NULL,
  optionally wrapped in one or more parentheses,
  and similarly for \lit{!=}.
\end{itemize}

\LMHash{}%
In particular,
an expression of the form \code{$v$\,\,==\,\,\NULL} or
\code{\NULL\,\,==\,\,$v$}
where $v$ has type $T$ at $\ell$
promotes the type of $v$
to \NonNullType{$T$} in the \FALSE{} continuation;
and an expression of the form \code{$v$\,\,!=\,\,\NULL} or
\code{\NULL\,\,!=\,\,$v$}
where $v$ has static type $T$ at $\ell$
promotes the type of $v$
to \NonNullType{$T$} in the \TRUE{} continuation.

\LMHash{}%
Similarly, a type test of the form \code{$v$\,\,\IS\,\,$T$}
promotes the type of $v$
to $T$ in the \TRUE{} continuation,
and a type check of the form \code{$v$\,\,\AS\,\,$T$}
promotes the type of $v$
to $T$ in the continuation where the expression evaluated to an object
(\commentary{that is, it did not throw}).

Note that this section is just a placeholder which is intended to give a brief, informal overview of the type promotion mechanism in Dart. It is needed because we used to have a short section on type promotion, and that section is being removed as part of the null safety updates, and it is useful to have a place for the references to point to (and it seems fair to give the reader just an informal section rather than nothing). So it's not fully formal, and it only covers a couple of special cases. In any case, comments about things to improve would be welcome, of course!