diff --git a/.dart_tool/package_config.json b/.dart_tool/package_config.json
index 429b915e380..70cfbb2a186 100644
--- a/.dart_tool/package_config.json
+++ b/.dart_tool/package_config.json
@@ -55,6 +55,11 @@
       "rootUri": "../pkg/_fe_analyzer_shared/test/flow_analysis/type_promotion",
       "packageUri": ".nonexisting/"
     },
+    {
+      "name": "_fe_analyzer_shared_why_not_promoted",
+      "rootUri": "../pkg/_fe_analyzer_shared/test/flow_analysis/why_not_promoted",
+      "packageUri": ".nonexisting/"
+    },
     {
       "name": "_js_interop_checks",
       "rootUri": "../pkg/_js_interop_checks",
diff --git a/pkg/_fe_analyzer_shared/analysis_options_no_lints.yaml b/pkg/_fe_analyzer_shared/analysis_options_no_lints.yaml
index bba3f74c829..467f3234a3e 100644
--- a/pkg/_fe_analyzer_shared/analysis_options_no_lints.yaml
+++ b/pkg/_fe_analyzer_shared/analysis_options_no_lints.yaml
@@ -15,4 +15,5 @@ analyzer:
     - test/flow_analysis/nullability/data/**
     - test/flow_analysis/reachability/data/**
     - test/flow_analysis/type_promotion/data/**
+    - test/flow_analysis/why_not_promoted/data/**
     - test/inheritance/data/**
diff --git a/pkg/_fe_analyzer_shared/lib/src/flow_analysis/flow_analysis.dart b/pkg/_fe_analyzer_shared/lib/src/flow_analysis/flow_analysis.dart
index 6809bbc0735..327b0038a4c 100644
--- a/pkg/_fe_analyzer_shared/lib/src/flow_analysis/flow_analysis.dart
+++ b/pkg/_fe_analyzer_shared/lib/src/flow_analysis/flow_analysis.dart
@@ -307,6 +307,61 @@ class AssignedVariablesNodeInfo<Variable extends Object> {
       '_declared=$_declared)';
 }
 
+/// Non-promotion reason describing the situation where a variable was not
+/// promoted due to an explicit write to the variable appearing somewhere in the
+/// source code.
+class DemoteViaExplicitWrite<Variable extends Object, Expression extends Object>
+    extends NonPromotionReason {
+  /// The local variable that was not promoted.
+  final Variable variable;
+
+  /// The expression that wrote to the variable; this corresponds to an
+  /// expression that was passed to [FlowAnalysis.write].
+  final Expression writeExpression;
+
+  DemoteViaExplicitWrite(this.variable, this.writeExpression);
+
+  @override
+  String get shortName => 'explicitWrite';
+
+  @override
+  R accept<R, Node extends Object, Expression extends Object,
+              Variable extends Object>(
+          NonPromotionReasonVisitor<R, Node, Expression, Variable> visitor) =>
+      visitor.visitDemoteViaExplicitWrite(
+          this as DemoteViaExplicitWrite<Variable, Expression>);
+
+  @override
+  String toString() => 'DemoteViaExplicitWrite($writeExpression)';
+}
+
+/// Non-promotion reason describing the situation where a variable was not
+/// promoted due to the variable appearing before the word `in` in a "for each"
+/// statement or a "for each" collection element.
+class DemoteViaForEachVariableWrite<Variable extends Object,
+    Node extends Object> extends NonPromotionReason {
+  /// The local variable that was not promoted.
+  final Variable variable;
+
+  /// The "for each" statement or collection element that wrote to the variable.
+  final Node node;
+
+  DemoteViaForEachVariableWrite(this.variable, this.node);
+
+  @override
+  String get shortName => 'explicitWrite';
+
+  @override
+  R accept<R, Node extends Object, Expression extends Object,
+              Variable extends Object>(
+          NonPromotionReasonVisitor<R, Node, Expression, Variable> visitor) =>
+      visitor.visitDemoteViaForEachVariableWrite(
+          this as DemoteViaForEachVariableWrite<Variable, Node>);
+
+  @override
+  String toString() => 'DemoteViaForEachVariableWrite($node)';
+}
+
 /// A collection of flow models representing the possible outcomes of evaluating
 /// an expression that are relevant to flow analysis.
 class ExpressionInfo<Variable extends Object, Type extends Object> {
@@ -338,6 +393,24 @@ class ExpressionInfo<Variable extends Object, Type extends Object> {
       'ExpressionInfo(after: $after, _ifTrue: $ifTrue, ifFalse: $ifFalse)';
 }
 
+/// Non-promotion reason describing the situation where an expression was not
+/// promoted due to the fact that it's a field (technically, a property get).
+class FieldNotPromoted extends NonPromotionReason {
+  /// The name of the property.
+  final String propertyName;
+
+  FieldNotPromoted(this.propertyName);
+
+  @override
+  String get shortName => 'fieldNotPromoted($propertyName)';
+
+  @override
+  R accept<R, Node extends Object, Expression extends Object,
+              Variable extends Object>(
+          NonPromotionReasonVisitor<R, Node, Expression, Variable> visitor) =>
+      visitor.visitFieldNotPromoted(this);
+}
+
 /// Implementation of flow analysis to be shared between the analyzer and the
 /// front end.
 ///
@@ -715,6 +788,13 @@ abstract class FlowAnalysis<Node extends Object, Statement extends Node,
   /// is currently promoted.  Otherwise returns `null`.
   Type? promotedType(Variable variable);
 
+  /// Call this method just after visiting a property get expression.
+  /// [wholeExpression] should be the whole property get, [target] should be the
+  /// expression to the left hand side of the `.`, and [propertyName] should be
+  /// the identifier to the right hand side of the `.`.
+  void propertyGet(
+      Expression wholeExpression, Expression target, String propertyName);
+
   /// Retrieves the SSA node associated with [variable], or `null` if [variable]
   /// is not associated with an SSA node because it is write captured.  For
   /// testing only.
@@ -750,6 +830,20 @@ abstract class FlowAnalysis<Node extends Object, Statement extends Node,
   /// - Call [switchStatement_end].
   void switchStatement_expressionEnd(Statement switchStatement);
 
+  /// Call this method just after visiting the expression `this` (or the
+  /// pseudo-expression `super`, in the case of the analyzer, which represents
+  /// `super.x` as a property get whose target is `super`).  [expression] should
+  /// be the `this` or `super` expression.
+  void thisOrSuper(Expression expression);
+
+  /// Call this method just after visiting an expression that represents a
+  /// property get on `this` or `super`.  This handles situations where there is
+  /// an implicit reference to `this`, or the case of the front end, where
+  /// `super.x` is represented by a single expression.  [expression] should be
+  /// the whole property get, and [propertyName] should be the name of the
+  /// property being read.
+  void thisOrSuperPropertyGet(Expression expression, String propertyName);
+
   /// Call this method just before visiting the body of a "try/catch" statement.
   ///
   /// The order of visiting a "try/catch" statement should be:
@@ -855,8 +949,23 @@ abstract class FlowAnalysis<Node extends Object, Statement extends Node,
   /// Call this method after visiting a "while" statement.
   void whileStatement_end();
 
+  /// Call this method when an error occurs that may be due to a lack of type
+  /// promotion, to retrieve information about why [target] was not promoted.
+  /// This call must be made right after visiting [target].
+  ///
+  /// The returned value is a map whose keys are types that the user might have
+  /// been expecting the target to be promoted to, and whose values are reasons
+  /// why the corresponding promotion did not occur.  The caller is expected to
+  /// select which non-promotion reason to report to the user by seeing which
+  /// promotion would have prevented the error.  (For example, if an error
+  /// occurs due to the target having a nullable type, the caller should report
+  /// a non-promotion reason associated with non-promotion to a non-nullable
+  /// type).
+  Map<Type, NonPromotionReason> whyNotPromoted(Expression target);
+
   /// Register write of the given [variable] in the current state.
   /// [writtenType] should be the type of the value that was written.
+  /// [expression] should be the whole expression performing the write.
   /// [writtenExpression] should be the expression that was written, or `null`
   /// if the expression that was written is not directly represented in the
   /// source code (this happens, for example, with compound assignments and with
@@ -865,8 +974,8 @@ abstract class FlowAnalysis<Node extends Object, Statement extends Node,
   /// This should also be used for the implicit write to a non-final variable in
   /// its initializer, to ensure that the type is promoted to non-nullable if
   /// necessary; in this case, [viaInitializer] should be `true`.
-  void write(
-      Variable variable, Type writtenType, Expression? writtenExpression);
+  void write(Expression expression, Variable variable, Type writtenType,
+      Expression? writtenExpression);
 
   /// Prints out a summary of the current state of flow analysis, intended for
   /// debugging use only.
@@ -1248,6 +1357,13 @@ class FlowAnalysisDebug<Node extends Object, Statement extends Node,
         isQuery: true);
   }
 
+  @override
+  void propertyGet(
+      Expression wholeExpression, Expression target, String propertyName) {
+    _wrap('propertyGet($wholeExpression, $target, $propertyName)',
+        () => _wrapped.propertyGet(wholeExpression, target, propertyName));
+  }
+
   @override
   SsaNode<Variable, Type>? ssaNodeForTesting(Variable variable) {
     return _wrap('ssaNodeForTesting($variable)',
@@ -1273,6 +1389,18 @@ class FlowAnalysisDebug<Node extends Object, Statement extends Node,
         () => _wrapped.switchStatement_expressionEnd(switchStatement));
   }
 
+  @override
+  void thisOrSuper(Expression expression) {
+    return _wrap(
+        'thisOrSuper($expression)', () => _wrapped.thisOrSuper(expression));
+  }
+
+  @override
+  void thisOrSuperPropertyGet(Expression expression, String propertyName) {
+    _wrap('thisOrSuperPropertyGet($expression, $propertyName)',
+        () => _wrapped.thisOrSuperPropertyGet(expression, propertyName));
+  }
+
   @override
   void tryCatchStatement_bodyBegin() {
     return _wrap('tryCatchStatement_bodyBegin()',
@@ -1350,10 +1478,19 @@ class FlowAnalysisDebug<Node extends Object, Statement extends Node,
   }
 
   @override
-  void write(
-      Variable variable, Type writtenType, Expression? writtenExpression) {
-    _wrap('write($variable, $writtenType, $writtenExpression)',
-        () => _wrapped.write(variable, writtenType, writtenExpression));
+  Map<Type, NonPromotionReason> whyNotPromoted(Expression target) {
+    return _wrap(
+        'whyNotPromoted($target)', () => _wrapped.whyNotPromoted(target),
+        isQuery: true);
+  }
+
+  @override
+  void write(Expression expression, Variable variable, Type writtenType,
+      Expression? writtenExpression) {
+    _wrap(
+        'write($expression, $variable, $writtenType, $writtenExpression)',
+        () => _wrapped.write(
+            expression, variable, writtenType, writtenExpression));
   }
 
   @override
@@ -1403,10 +1540,14 @@ class FlowModel<Variable extends Object, Type extends Object> {
   /// variable is not in scope anymore.  This should not have any effect on
   /// analysis results for error-free code, because it is an error to refer to a
   /// variable that is no longer in scope.
-  final Map<Variable, VariableModel<Variable, Type> /*!*/ > variableInfo;
+  ///
+  /// `null` is allowed as a special key; it represents the pseudo-variable
+  /// `this`.  (This is needed so that we can explain why `this` is not
+  /// promoted, and why properties of `this` are not promoted).
+  final Map<Variable?, VariableModel<Variable, Type> /*!*/ > variableInfo;
 
   /// The empty map, used to [join] variables.
-  final Map<Variable, VariableModel<Variable, Type>> _emptyVariableMap = {};
+  final Map<Variable?, VariableModel<Variable, Type>> _emptyVariableMap = {};
 
   /// Creates a state object with the given [reachable] status.  All variables
   /// are assumed to be unpromoted and already assigned, so joining another
@@ -1455,13 +1596,13 @@ class FlowModel<Variable extends Object, Type extends Object> {
     Reachability newReachable = afterFinally.reachable.rebaseForward(reachable);
 
     // Consider each variable that is common to all three models.
-    Map<Variable, VariableModel<Variable, Type>> newVariableInfo =
-        <Variable, VariableModel<Variable, Type>>{};
+    Map<Variable?, VariableModel<Variable, Type>> newVariableInfo =
+        <Variable?, VariableModel<Variable, Type>>{};
     bool variableInfoMatchesThis = true;
     bool variableInfoMatchesAfterFinally = true;
-    for (MapEntry<Variable, VariableModel<Variable, Type>> entry
+    for (MapEntry<Variable?, VariableModel<Variable, Type>> entry
         in variableInfo.entries) {
-      Variable variable = entry.key;
+      Variable? variable = entry.key;
       VariableModel<Variable, Type> thisModel = entry.value;
       VariableModel<Variable, Type>? beforeFinallyModel =
           beforeFinally.variableInfo[variable];
@@ -1524,7 +1665,7 @@ class FlowModel<Variable extends Object, Type extends Object> {
     // erroneously think that `newVariableInfo` matches `afterFinally`.  If so,
     // correct that.
     if (variableInfoMatchesAfterFinally) {
-      for (Variable variable in afterFinally.variableInfo.keys) {
+      for (Variable? variable in afterFinally.variableInfo.keys) {
         if (!variableInfo.containsKey(variable)) {
           variableInfoMatchesAfterFinally = false;
           break;
@@ -1567,7 +1708,7 @@ class FlowModel<Variable extends Object, Type extends Object> {
   FlowModel<Variable, Type> conservativeJoin(
       Iterable<Variable> writtenVariables,
       Iterable<Variable> capturedVariables) {
-    Map<Variable, VariableModel<Variable, Type>>? newVariableInfo;
+    Map<Variable?, VariableModel<Variable, Type>>? newVariableInfo;
 
     for (Variable variable in writtenVariables) {
       VariableModel<Variable, Type> info = infoFor(variable);
@@ -1575,7 +1716,7 @@ class FlowModel<Variable extends Object, Type extends Object> {
           info.discardPromotionsAndMarkNotUnassigned();
       if (!identical(info, newInfo)) {
         (newVariableInfo ??=
-            new Map<Variable, VariableModel<Variable, Type>>.from(
+            new Map<Variable?, VariableModel<Variable, Type>>.from(
                 variableInfo))[variable] = newInfo;
       }
     }
@@ -1630,14 +1771,14 @@ class FlowModel<Variable extends Object, Type extends Object> {
   FlowModel<Variable, Type> inheritTested(
       TypeOperations<Variable, Type> typeOperations,
       FlowModel<Variable, Type> other) {
-    Map<Variable, VariableModel<Variable, Type>> newVariableInfo =
-        <Variable, VariableModel<Variable, Type>>{};
-    Map<Variable, VariableModel<Variable, Type>> otherVariableInfo =
+    Map<Variable?, VariableModel<Variable, Type>> newVariableInfo =
+        <Variable?, VariableModel<Variable, Type>>{};
+    Map<Variable?, VariableModel<Variable, Type>> otherVariableInfo =
         other.variableInfo;
     bool changed = false;
-    for (MapEntry<Variable, VariableModel<Variable, Type>> entry
+    for (MapEntry<Variable?, VariableModel<Variable, Type>> entry
         in variableInfo.entries) {
-      Variable variable = entry.key;
+      Variable? variable = entry.key;
       VariableModel<Variable, Type> variableModel = entry.value;
       VariableModel<Variable, Type>? otherVariableModel =
           otherVariableInfo[variable];
@@ -1674,13 +1815,13 @@ class FlowModel<Variable extends Object, Type extends Object> {
     Reachability newReachable = reachable.rebaseForward(base.reachable);
 
     // Consider each variable in the new base model.
-    Map<Variable, VariableModel<Variable, Type>> newVariableInfo =
-        <Variable, VariableModel<Variable, Type>>{};
+    Map<Variable?, VariableModel<Variable, Type>> newVariableInfo =
+        <Variable?, VariableModel<Variable, Type>>{};
     bool variableInfoMatchesThis = true;
     bool variableInfoMatchesBase = true;
-    for (MapEntry<Variable, VariableModel<Variable, Type>> entry
+    for (MapEntry<Variable?, VariableModel<Variable, Type>> entry
         in base.variableInfo.entries) {
-      Variable variable = entry.key;
+      Variable? variable = entry.key;
       VariableModel<Variable, Type> baseModel = entry.value;
       VariableModel<Variable, Type>? thisModel = variableInfo[variable];
       if (thisModel == null) {
@@ -1736,7 +1877,7 @@ class FlowModel<Variable extends Object, Type extends Object> {
     // present in `this` that aren't present in `base`, we may erroneously think
     // that `newVariableInfo` matches `this`.  If so, correct that.
     if (variableInfoMatchesThis) {
-      for (Variable variable in variableInfo.keys) {
+      for (Variable? variable in variableInfo.keys) {
         if (!base.variableInfo.containsKey(variable)) {
           variableInfoMatchesThis = false;
           break;
@@ -1789,13 +1930,13 @@ class FlowModel<Variable extends Object, Type extends Object> {
     Reachability newReachable =
         Reachability.restrict(reachable, other.reachable);
 
-    Map<Variable, VariableModel<Variable, Type>> newVariableInfo =
-        <Variable, VariableModel<Variable, Type>>{};
+    Map<Variable?, VariableModel<Variable, Type>> newVariableInfo =
+        <Variable?, VariableModel<Variable, Type>>{};
     bool variableInfoMatchesThis = true;
     bool variableInfoMatchesOther = true;
-    for (MapEntry<Variable, VariableModel<Variable, Type>> entry
+    for (MapEntry<Variable?, VariableModel<Variable, Type>> entry
         in variableInfo.entries) {
-      Variable variable = entry.key;
+      Variable? variable = entry.key;
       VariableModel<Variable, Type> thisModel = entry.value;
       VariableModel<Variable, Type>? otherModel = other.variableInfo[variable];
       if (otherModel == null) {
@@ -1809,7 +1950,7 @@ class FlowModel<Variable extends Object, Type extends Object> {
       if (!identical(restricted, otherModel)) variableInfoMatchesOther = false;
     }
     if (variableInfoMatchesOther) {
-      for (Variable variable in other.variableInfo.keys) {
+      for (Variable? variable in other.variableInfo.keys) {
         if (!variableInfo.containsKey(variable)) {
           variableInfoMatchesOther = false;
           break;
@@ -1975,7 +2116,12 @@ class FlowModel<Variable extends Object, Type extends Object> {
   /// Updates the state to indicate that an assignment was made to the given
   /// [variable].  The variable is marked as definitely assigned, and any
   /// previous type promotion is removed.
+  ///
+  /// If there is any chance that the write will cause a demotion, the caller
+  /// must pass in a non-null value for [nonPromotionReason] describing the
+  /// reason for any potential demotion.
   FlowModel<Variable, Type> write(
+      NonPromotionReason? nonPromotionReason,
       Variable variable,
       Type writtenType,
       SsaNode<Variable, Type> newSsaNode,
@@ -1983,8 +2129,8 @@ class FlowModel<Variable extends Object, Type extends Object> {
     VariableModel<Variable, Type>? infoForVar = variableInfo[variable];
     if (infoForVar == null) return this;
 
-    VariableModel<Variable, Type> newInfoForVar =
-        infoForVar.write(variable, writtenType, typeOperations, newSsaNode);
+    VariableModel<Variable, Type> newInfoForVar = infoForVar.write(
+        nonPromotionReason, variable, writtenType, typeOperations, newSsaNode);
     if (identical(newInfoForVar, infoForVar)) return this;
 
     return _updateVariableInfo(new VariableReference(variable), newInfoForVar);
@@ -2019,7 +2165,8 @@ class FlowModel<Variable extends Object, Type extends Object> {
     if (promotedType != null) {
       newPromotedTypes =
           VariableModel._addToPromotedTypes(info.promotedTypes, promotedType);
-      if (typeOperations.isNever(promotedType)) {
+      if (reference is VariableReference<Object, Object> &&
+          typeOperations.isNever(promotedType)) {
         newReachable = reachable.setUnreachable();
       }
     }
@@ -2035,7 +2182,8 @@ class FlowModel<Variable extends Object, Type extends Object> {
                 tested: newTested,
                 assigned: info.assigned,
                 unassigned: info.unassigned,
-                ssaNode: info.ssaNode),
+                ssaNode: info.ssaNode,
+                nonPromotionHistory: info.nonPromotionHistory),
             reachable: newReachable);
   }
 
@@ -2045,8 +2193,8 @@ class FlowModel<Variable extends Object, Type extends Object> {
       Reference<Variable, Type> reference, VariableModel<Variable, Type> model,
       {Reachability? reachable}) {
     reachable ??= this.reachable;
-    Map<Variable, VariableModel<Variable, Type>> newVariableInfo =
-        new Map<Variable, VariableModel<Variable, Type>>.from(variableInfo);
+    Map<Variable?, VariableModel<Variable, Type>> newVariableInfo =
+        new Map<Variable?, VariableModel<Variable, Type>>.from(variableInfo);
     reference.storeInfo(newVariableInfo, model);
     return new FlowModel<Variable, Type>.withInfo(reachable, newVariableInfo);
   }
@@ -2065,7 +2213,7 @@ class FlowModel<Variable extends Object, Type extends Object> {
     TypeOperations<Variable, Type> typeOperations,
     FlowModel<Variable, Type>? first,
     FlowModel<Variable, Type>? second,
-    Map<Variable, VariableModel<Variable, Type>> emptyVariableMap,
+    Map<Variable?, VariableModel<Variable, Type>> emptyVariableMap,
   ) {
     if (first == null) return second!;
     if (second == null) return first;
@@ -2082,7 +2230,7 @@ class FlowModel<Variable extends Object, Type extends Object> {
 
     Reachability newReachable =
         Reachability.join(first.reachable, second.reachable);
-    Map<Variable, VariableModel<Variable, Type>> newVariableInfo =
+    Map<Variable?, VariableModel<Variable, Type>> newVariableInfo =
         FlowModel.joinVariableInfo(typeOperations, first.variableInfo,
             second.variableInfo, emptyVariableMap);
 
@@ -2092,25 +2240,25 @@ class FlowModel<Variable extends Object, Type extends Object> {
 
   /// Joins two "variable info" maps.  See [join] for details.
   @visibleForTesting
-  static Map<Variable, VariableModel<Variable, Type>>
+  static Map<Variable?, VariableModel<Variable, Type>>
       joinVariableInfo<Variable extends Object, Type extends Object>(
     TypeOperations<Variable, Type> typeOperations,
-    Map<Variable, VariableModel<Variable, Type>> first,
-    Map<Variable, VariableModel<Variable, Type>> second,
-    Map<Variable, VariableModel<Variable, Type>> emptyMap,
+    Map<Variable?, VariableModel<Variable, Type>> first,
+    Map<Variable?, VariableModel<Variable, Type>> second,
+    Map<Variable?, VariableModel<Variable, Type>> emptyMap,
   ) {
     if (identical(first, second)) return first;
     if (first.isEmpty || second.isEmpty) {
       return emptyMap;
     }
 
-    Map<Variable, VariableModel<Variable, Type>> result =
-        <Variable, VariableModel<Variable, Type>>{};
+    Map<Variable?, VariableModel<Variable, Type>> result =
+        <Variable?, VariableModel<Variable, Type>>{};
     bool alwaysFirst = true;
     bool alwaysSecond = true;
-    for (MapEntry<Variable, VariableModel<Variable, Type>> entry
+    for (MapEntry<Variable?, VariableModel<Variable, Type>> entry
         in first.entries) {
-      Variable variable = entry.key;
+      Variable? variable = entry.key;
       VariableModel<Variable, Type>? secondModel = second[variable];
       if (secondModel == null) {
         alwaysFirst = false;
@@ -2137,7 +2285,7 @@ class FlowModel<Variable extends Object, Type extends Object> {
     TypeOperations<Variable, Type> typeOperations,
     FlowModel<Variable, Type>? first,
     FlowModel<Variable, Type>? second,
-    Map<Variable, VariableModel<Variable, Type>> emptyVariableMap,
+    Map<Variable?, VariableModel<Variable, Type>> emptyVariableMap,
   ) {
     if (first == null) return second!.unsplit();
     if (second == null) return first.unsplit();
@@ -2154,7 +2302,7 @@ class FlowModel<Variable extends Object, Type extends Object> {
 
     Reachability newReachable =
         Reachability.join(first.reachable, second.reachable).unsplit();
-    Map<Variable, VariableModel<Variable, Type>> newVariableInfo =
+    Map<Variable?, VariableModel<Variable, Type>> newVariableInfo =
         FlowModel.joinVariableInfo(typeOperations, first.variableInfo,
             second.variableInfo, emptyVariableMap);
 
@@ -2169,7 +2317,7 @@ class FlowModel<Variable extends Object, Type extends Object> {
           FlowModel<Variable, Type> first,
           FlowModel<Variable, Type> second,
           Reachability newReachable,
-          Map<Variable, VariableModel<Variable, Type>> newVariableInfo) {
+          Map<Variable?, VariableModel<Variable, Type>> newVariableInfo) {
     if (first.reachable == newReachable &&
         identical(first.variableInfo, newVariableInfo)) {
       return first;
@@ -2188,11 +2336,11 @@ class FlowModel<Variable extends Object, Type extends Object> {
   /// The equivalence check is shallow; if two variables' models are not
   /// identical, we return `false`.
   static bool _variableInfosEqual<Variable extends Object, Type extends Object>(
-      Map<Variable, VariableModel<Variable, Type>> p1,
-      Map<Variable, VariableModel<Variable, Type>> p2) {
+      Map<Variable?, VariableModel<Variable, Type>> p1,
+      Map<Variable?, VariableModel<Variable, Type>> p2) {
     if (p1.length != p2.length) return false;
     if (!p1.keys.toSet().containsAll(p2.keys)) return false;
-    for (MapEntry<Variable, VariableModel<Variable, Type>> entry
+    for (MapEntry<Variable?, VariableModel<Variable, Type>> entry
         in p1.entries) {
       VariableModel<Variable, Type> p1Value = entry.value;
       VariableModel<Variable, Type>? p2Value = p2[entry.key];
@@ -2204,6 +2352,62 @@ class FlowModel<Variable extends Object, Type extends Object> {
   }
 }
 
+/// Linked list node representing a set of reasons why a given expression was
+/// not promoted.
+///
+/// We use a linked list representation because it is very efficient to build;
+/// this means that in the "happy path" where no error occurs (so non-promotion
+/// history is not needed) we do a minimal amount of work.
+class NonPromotionHistory<Type> {
+  /// The type that was not promoted to.
+  final Type type;
+
+  /// The reason why the promotion didn't occur.
+  final NonPromotionReason nonPromotionReason;
+
+  /// The previous link in the list.
+  final NonPromotionHistory<Type>? previous;
+
+  NonPromotionHistory(this.type, this.nonPromotionReason, this.previous);
+
+  @override
+  String toString() {
+    List<String> items = <String>[];
+    for (NonPromotionHistory<Type>? link = this;
+        link != null;
+        link = link.previous) {
+      items.add('${link.type}: ${link.nonPromotionReason}');
+    }
+    return items.toString();
+  }
+}
+
+/// Abstract class representing a reason why something was not promoted.
+abstract class NonPromotionReason {
+  /// Short text description of this non-promotion reason; intended for ID
+  /// testing.
+  String get shortName;
+
+  /// Implementation of the visitor pattern for non-promotion reasons.
+  R accept<R, Node extends Object, Expression extends Object,
+          Variable extends Object>(
+      NonPromotionReasonVisitor<R, Node, Expression, Variable> visitor);
+}
+
+/// Implementation of the visitor pattern for non-promotion reasons.
+abstract class NonPromotionReasonVisitor<R, Node extends Object,
+    Expression extends Object, Variable extends Object> {
+  NonPromotionReasonVisitor._() : assert(false, 'Do not extend this class');
+
+  R visitDemoteViaExplicitWrite(
+      DemoteViaExplicitWrite<Variable, Expression> reason);
+
+  R visitDemoteViaForEachVariableWrite(
+      DemoteViaForEachVariableWrite<Variable, Node> reason);
+
+  R visitFieldNotPromoted(FieldNotPromoted reason);
+}
+
 /// Immutable data structure modeling the reachability of the given point in the
 /// source code.  Reachability is tracked relative to checkpoints occurring
 /// previously along the control flow path leading up to the current point in
@@ -2359,16 +2563,27 @@ abstract class Reference<Variable extends Object, Type extends Object> {
 
   /// Gets the info for this reference, creating it if it doesn't exist.
   VariableModel<Variable, Type> getInfo(
-          Map<Variable, VariableModel<Variable, Type>> variableInfo) =>
+          Map<Variable?, VariableModel<Variable, Type>> variableInfo) =>
       _getInfo(variableInfo) ?? new VariableModel<Variable, Type>.fresh();
 
+  /// Gets a map of non-promotion reasons associated with this reference.  This
+  /// is the map that will be returned from [FlowAnalysis.whyNotPromoted].
+  Map<Type, NonPromotionReason> getNonPromotionReasons(
+      Map<Variable?, VariableModel<Variable, Type>> variableInfo,
+      TypeOperations<Variable, Type> typeOperations);
+
+  /// Creates a reference representing a get of a property called [propertyName]
+  /// on the reference represented by `this`.
+  Reference<Variable, Type> propertyGet(String propertyName) =>
+      new _PropertyGetReference<Variable, Type>(this, propertyName);
+
   /// Stores info for this reference in [variableInfo].
-  void storeInfo(Map<Variable, VariableModel<Variable, Type>> variableInfo,
+  void storeInfo(Map<Variable?, VariableModel<Variable, Type>> variableInfo,
       VariableModel<Variable, Type> variableModel);
 
   /// Gets the info for this reference, or `null` if it doesn't exist.
   VariableModel<Variable, Type>? _getInfo(
-      Map<Variable, VariableModel<Variable, Type>> variableInfo);
+      Map<Variable?, VariableModel<Variable, Type>> variableInfo);
 }
 
 /// Data structure representing a unique value that a variable might take on
@@ -2423,6 +2638,9 @@ enum TypeClassification {
 
 /// Operations on types, abstracted from concrete type interfaces.
 abstract class TypeOperations<Variable extends Object, Type extends Object> {
+  /// Gets the representation of the top type (`Object?`) in the type system.
+  Type get topType;
+
   /// Classifies the given type into one of the three categories defined by
   /// the [TypeClassification] enum.
   TypeClassification classifyType(Type type);
@@ -2510,12 +2728,22 @@ class VariableModel<Variable extends Object, Type extends Object> {
   /// `null` if the variable has been write captured.
   final SsaNode<Variable, Type>? ssaNode;
 
+  /// Non-promotion history of this variable.
+  final NonPromotionHistory<Type>? nonPromotionHistory;
+
+  /// Promotion information for properties of this variable.  We don't actually
+  /// promote properties, but we track the promotions that would occur if we
+  /// did, so that we can report those as non-promotion reasons.
+  final Map<String, VariableModel<Variable, Type>> properties;
+
   VariableModel(
       {required this.promotedTypes,
       required this.tested,
       required this.assigned,
       required this.unassigned,
-      required this.ssaNode}) {
+      required this.ssaNode,
+      this.nonPromotionHistory,
+      this.properties = const {}}) {
     assert(!(assigned && unassigned),
         "Can't be both definitely assigned and unassigned");
     assert(promotedTypes == null || promotedTypes!.isNotEmpty);
@@ -2533,7 +2761,9 @@ class VariableModel<Variable extends Object, Type extends Object> {
       : promotedTypes = null,
         tested = const [],
         unassigned = !assigned,
-        ssaNode = new SsaNode<Variable, Type>(null);
+        ssaNode = new SsaNode<Variable, Type>(null),
+        nonPromotionHistory = null,
+        properties = const {};
 
   /// Indicates whether the variable has been write captured.
   bool get writeCaptured => ssaNode == null;
@@ -2605,6 +2835,18 @@ class VariableModel<Variable extends Object, Type extends Object> {
         newAssigned, newUnassigned, newWriteCaptured ? null : ssaNode);
   }
 
+  /// Updates `this` with a new set of properties.
+  VariableModel<Variable, Type> setProperties(
+          Map<String, VariableModel<Variable, Type>> newProperties) =>
+      new VariableModel<Variable, Type>(
+          promotedTypes: promotedTypes,
+          tested: tested,
+          unassigned: unassigned,
+          assigned: assigned,
+          ssaNode: ssaNode,
+          nonPromotionHistory: nonPromotionHistory,
+          properties: newProperties);
+
   @override
   String toString() {
     List<String> parts = [ssaNode.toString()];
@@ -2623,12 +2865,20 @@ class VariableModel<Variable extends Object, Type extends Object> {
     if (writeCaptured) {
       parts.add('writeCaptured: true');
     }
+    if (nonPromotionHistory != null) {
+      parts.add('nonPromotionHistory: $nonPromotionHistory');
+    }
     return 'VariableModel(${parts.join(', ')})';
   }
 
   /// Returns a new [VariableModel] reflecting the fact that the variable was
   /// just written to.
+  ///
+  /// If there is any chance that the write will cause a demotion, the caller
+  /// must pass in a non-null value for [nonPromotionReason] describing the
+  /// reason for any potential demotion.
   VariableModel<Variable, Type> write(
+      NonPromotionReason? nonPromotionReason,
       Variable variable,
       Type writtenType,
       TypeOperations<Variable, Type> typeOperations,
@@ -2642,14 +2892,15 @@ class VariableModel<Variable extends Object, Type extends Object> {
           ssaNode: null);
     }
 
-    List<Type>? newPromotedTypes = _demoteViaAssignment(
-      writtenType,
-      typeOperations,
-    );
+    _DemotionResult<Type> demotionResult =
+        _demoteViaAssignment(writtenType, typeOperations, nonPromotionReason);
+    List<Type>? newPromotedTypes = demotionResult.promotedTypes;
 
     Type declaredType = typeOperations.variableType(variable);
     newPromotedTypes = _tryPromoteToTypeOfInterest(
         typeOperations, declaredType, newPromotedTypes, writtenType);
+    // TODO(paulberry): remove demotions from demotionResult.nonPromotionHistory
+    // that are no longer in effect due to re-promotion.
     if (identical(promotedTypes, newPromotedTypes) && assigned) {
       return new VariableModel<Variable, Type>(
           promotedTypes: promotedTypes,
@@ -2671,7 +2922,8 @@ class VariableModel<Variable extends Object, Type extends Object> {
         tested: newTested,
         assigned: true,
         unassigned: false,
-        ssaNode: newSsaNode);
+        ssaNode: newSsaNode,
+        nonPromotionHistory: demotionResult.nonPromotionHistory);
   }
 
   /// Returns a new [VariableModel] reflecting the fact that the variable has
@@ -2685,28 +2937,45 @@ class VariableModel<Variable extends Object, Type extends Object> {
         ssaNode: null);
   }
 
-  List<Type>? _demoteViaAssignment(
-    Type writtenType,
-    TypeOperations<Variable, Type> typeOperations,
-  ) {
+  /// Computes the result of demoting this variable due to writing a value of
+  /// type [writtenType].
+  ///
+  /// If there is any chance that the write will cause an actual demotion to
+  /// occur, the caller must pass in a non-null value for [nonPromotionReason]
+  /// describing the reason for the potential demotion.
+  _DemotionResult<Type> _demoteViaAssignment(
+      Type writtenType,
+      TypeOperations<Variable, Type> typeOperations,
+      NonPromotionReason? nonPromotionReason) {
     List<Type>? promotedTypes = this.promotedTypes;
     if (promotedTypes == null) {
-      return null;
+      return new _DemotionResult<Type>(null, nonPromotionHistory);
     }
 
     int numElementsToKeep = promotedTypes.length;
+    NonPromotionHistory<Type>? newNonPromotionHistory = nonPromotionHistory;
+    List<Type>? newPromotedTypes;
     for (;; numElementsToKeep--) {
       if (numElementsToKeep == 0) {
-        return null;
+        break;
       }
       Type promoted = promotedTypes[numElementsToKeep - 1];
       if (typeOperations.isSubtypeOf(writtenType, promoted)) {
         if (numElementsToKeep == promotedTypes.length) {
-          return promotedTypes;
+          newPromotedTypes = promotedTypes;
+          break;
         }
-        return promotedTypes.sublist(0, numElementsToKeep);
+        newPromotedTypes = promotedTypes.sublist(0, numElementsToKeep);
+        break;
+      }
+      if (nonPromotionReason == null) {
+        assert(false, 'Demotion occurred but nonPromotionReason is null');
+      } else {
+        newNonPromotionHistory = new NonPromotionHistory<Type>(
+            promoted, nonPromotionReason, newNonPromotionHistory);
       }
     }
+    return new _DemotionResult<Type>(newPromotedTypes, newNonPromotionHistory);
   }
 
   /// Determines whether a variable with the given [promotedTypes] should be
@@ -3067,14 +3336,36 @@ class VariableReference<Variable extends Object, Type extends Object>
       typeOperations.variableType(variable);
 
   @override
-  void storeInfo(Map<Variable, VariableModel<Variable, Type>> variableInfo,
+  Map<Type, NonPromotionReason> getNonPromotionReasons(
+      Map<Variable?, VariableModel<Variable, Type>> variableInfo,
+      TypeOperations<Variable, Type> typeOperations) {
+    Map<Type, NonPromotionReason> result = <Type, NonPromotionReason>{};
+    VariableModel<Variable, Type>? currentVariableInfo = variableInfo[variable];
+    if (currentVariableInfo != null) {
+      Type currentType = currentVariableInfo.promotedTypes?.last ??
+          typeOperations.variableType(variable);
+      NonPromotionHistory? nonPromotionHistory =
+          currentVariableInfo.nonPromotionHistory;
+      while (nonPromotionHistory != null) {
+        Type nonPromotedType = nonPromotionHistory.type;
+        if (!typeOperations.isSubtypeOf(currentType, nonPromotedType)) {
+          result[nonPromotedType] ??= nonPromotionHistory.nonPromotionReason;
+        }
+        nonPromotionHistory = nonPromotionHistory.previous;
+      }
+    }
+    return result;
+  }
+
+  @override
+  void storeInfo(Map<Variable?, VariableModel<Variable, Type>> variableInfo,
       VariableModel<Variable, Type> variableModel) {
     variableInfo[variable] = variableModel;
   }
 
   @override
   VariableModel<Variable, Type>? _getInfo(
-          Map<Variable, VariableModel<Variable, Type>> variableInfo) =>
+          Map<Variable?, VariableModel<Variable, Type>> variableInfo) =>
       variableInfo[variable];
 }
 
@@ -3145,6 +3436,19 @@ class _ConditionalContext<Variable extends Object, Type extends Object>
       'thenInfo: $_thenInfo)';
 }
 
+/// Data structure representing the result of demoting a variable from one type
+/// to another.
+class _DemotionResult<Type extends Object> {
+  /// The new set of promoted types.
+  final List<Type>? promotedTypes;
+
+  /// The new non-promotion history (including the types that the variable is
+  /// no longer promoted to).
+  final NonPromotionHistory<Type>? nonPromotionHistory;
+
+  _DemotionResult(this.promotedTypes, this.nonPromotionHistory);
+}
+
 /// [_FlowContext] representing an equality comparison using `==` or `!=`.
 class _EqualityOpContext<Variable extends Object, Type extends Object>
     extends _BranchContext<Variable, Type> {
@@ -3437,8 +3741,12 @@ class _FlowAnalysisImpl<Node extends Object, Statement extends Node,
             _current.reachable.parent!, _current);
     _stack.add(context);
     if (loopVariable != null) {
-      _current = _current.write(loopVariable, writtenType,
-          new SsaNode<Variable, Type>(null), typeOperations);
+      _current = _current.write(
+          new DemoteViaForEachVariableWrite<Variable, Node>(loopVariable, node),
+          loopVariable,
+          writtenType,
+          new SsaNode<Variable, Type>(null),
+          typeOperations);
     }
   }
 
@@ -3581,8 +3889,8 @@ class _FlowAnalysisImpl<Node extends Object, Statement extends Node,
       // written type is the variable's declared type.
       initializerType = typeOperations.variableType(variable);
     }
-    _current =
-        _current.write(variable, initializerType, newSsaNode, typeOperations);
+    _current = _current.write(
+        null, variable, initializerType, newSsaNode, typeOperations);
   }
 
   @override
@@ -3740,6 +4048,16 @@ class _FlowAnalysisImpl<Node extends Object, Statement extends Node,
     return _current.infoFor(variable).promotedTypes?.last;
   }
 
+  @override
+  void propertyGet(
+      Expression wholeExpression, Expression target, String propertyName) {
+    Reference<Variable, Type>? reference = _getExpressionReference(target);
+    if (reference != null) {
+      _storeExpressionReference(
+          wholeExpression, reference.propertyGet(propertyName));
+    }
+  }
+
   @override
   SsaNode<Variable, Type>? ssaNodeForTesting(Variable variable) =>
       _current.variableInfo[variable]?.ssaNode;
@@ -3784,6 +4102,17 @@ class _FlowAnalysisImpl<Node extends Object, Statement extends Node,
     _statementToContext[switchStatement] = context;
   }
 
+  @override
+  void thisOrSuper(Expression expression) {
+    _storeExpressionReference(expression, new _ThisReference<Variable, Type>());
+  }
+
+  @override
+  void thisOrSuperPropertyGet(Expression expression, String propertyName) {
+    _storeExpressionReference(expression,
+        new _ThisReference<Variable, Type>().propertyGet(propertyName));
+  }
+
   @override
   void tryCatchStatement_bodyBegin() {
     _current = _current.split();
@@ -3914,15 +4243,31 @@ class _FlowAnalysisImpl<Node extends Object, Statement extends Node,
   }
 
   @override
-  void write(
-      Variable variable, Type writtenType, Expression? writtenExpression) {
+  Map<Type, NonPromotionReason> whyNotPromoted(Expression target) {
+    if (identical(target, _expressionWithReference)) {
+      Reference<Variable, Type>? reference = _expressionReference;
+      if (reference != null) {
+        return reference.getNonPromotionReasons(
+            _current.variableInfo, typeOperations);
+      }
+    }
+    return {};
+  }
+
+  @override
+  void write(Expression expression, Variable variable, Type writtenType,
+      Expression? writtenExpression) {
     ExpressionInfo<Variable, Type>? expressionInfo = writtenExpression == null
         ? null
         : _getExpressionInfo(writtenExpression);
     SsaNode<Variable, Type> newSsaNode = new SsaNode<Variable, Type>(
         expressionInfo is _TrivialExpressionInfo ? null : expressionInfo);
-    _current =
-        _current.write(variable, writtenType, newSsaNode, typeOperations);
+    _current = _current.write(
+        new DemoteViaExplicitWrite<Variable, Expression>(variable, expression),
+        variable,
+        writtenType,
+        newSsaNode,
+        typeOperations);
   }
 
   @override
@@ -4424,6 +4769,10 @@ class _LegacyTypePromotion<Node extends Object, Statement extends Node,
     return _knownTypes[variable];
   }
 
+  @override
+  void propertyGet(
+      Expression wholeExpression, Expression target, String propertyName) {}
+
   @override
   SsaNode<Variable, Type>? ssaNodeForTesting(Variable variable) {
     throw new StateError('ssaNodeForTesting requires null-aware flow analysis');
@@ -4438,6 +4787,12 @@ class _LegacyTypePromotion<Node extends Object, Statement extends Node,
   @override
   void switchStatement_expressionEnd(Statement switchStatement) {}
 
+  @override
+  void thisOrSuper(Expression expression) {}
+
+  @override
+  void thisOrSuperPropertyGet(Expression expression, String propertyName) {}
+
   @override
   void tryCatchStatement_bodyBegin() {}
 
@@ -4481,8 +4836,13 @@ class _LegacyTypePromotion<Node extends Object, Statement extends Node,
   void whileStatement_end() {}
 
   @override
-  void write(
-      Variable variable, Type writtenType, Expression? writtenExpression) {
+  Map<Type, NonPromotionReason> whyNotPromoted(Expression target) {
+    return {};
+  }
+
+  @override
+  void write(Expression expression, Variable variable, Type writtenType,
+      Expression? writtenExpression) {
     assert(
         _assignedVariables._anywhere._written.contains(variable),
         "Variable is written to, but was not included in "
@@ -4615,6 +4975,57 @@ class _NullInfo<Variable extends Object, Type extends Object>
       null;
 }
 
+/// [Reference] object representing a property get applied to another reference.
+class _PropertyGetReference<Variable extends Object, Type extends Object>
+    extends Reference<Variable, Type> {
+  /// The target of the property get.  For example a property get of the form
+  /// `a.b`, where `a` is a local variable, has a target which is a reference to
+  /// `a`.
+  final Reference<Variable, Type> target;
+
+  /// The name of the property.
+  final String propertyName;
+
+  _PropertyGetReference(this.target, this.propertyName);
+
+  @override
+  Type getDeclaredType(TypeOperations<Variable, Type> typeOperations) {
+    return typeOperations.topType;
+  }
+
+  @override
+  Map<Type, NonPromotionReason> getNonPromotionReasons(
+      Map<Variable?, VariableModel<Variable, Type>> variableInfo,
+      TypeOperations<Variable, Type> typeOperations) {
+    Map<Type, NonPromotionReason> result = <Type, NonPromotionReason>{};
+    List<Type>? promotedTypes = _getInfo(variableInfo)?.promotedTypes;
+    if (promotedTypes != null) {
+      for (Type type in promotedTypes) {
+        result[type] = new FieldNotPromoted(propertyName);
+      }
+    }
+    return result;
+  }
+
+  @override
+  void storeInfo(Map<Variable?, VariableModel<Variable, Type>> variableInfo,
+      VariableModel<Variable, Type> variableModel) {
+    VariableModel<Variable, Type> targetInfo = target.getInfo(variableInfo);
+    Map<String, VariableModel<Variable, Type>> newProperties =
+        new Map<String, VariableModel<Variable, Type>>.from(
+            targetInfo.properties);
+    newProperties[propertyName] = variableModel;
+    target.storeInfo(variableInfo, targetInfo.setProperties(newProperties));
+  }
+
+  @override
+  VariableModel<Variable, Type>? _getInfo(
+      Map<Variable?, VariableModel<Variable, Type>> variableInfo) {
+    VariableModel<Variable, Type> targetInfo = target.getInfo(variableInfo);
+    return targetInfo.properties[propertyName];
+  }
+}
+
 /// [_FlowContext] representing a language construct for which flow analysis
 /// must store a flow model state to be retrieved later, such as a `try`
 /// statement, function expression, or "if-null" (`??`) expression.
@@ -4650,6 +5061,36 @@ class _SimpleStatementContext<Variable extends Object, Type extends Object>
       'checkpoint: $_checkpoint)';
 }
 
+/// [Reference] object representing an implicit or explicit reference to `this`.
+class _ThisReference<Variable extends Object, Type extends Object>
+    extends Reference<Variable, Type> {
+  @override
+  Type getDeclaredType(TypeOperations<Variable, Type> typeOperations) {
+    // TODO(paulberry): can we return the actual type?  Would that have a
+    // user-visible effect?
+    return typeOperations.topType;
+  }
+
+  @override
+  Map<Type, NonPromotionReason> getNonPromotionReasons(
+      Map<Variable?, VariableModel<Variable, Type>> variableInfo,
+      TypeOperations<Variable, Type> typeOperations) {
+    // TODO(paulberry): implement.
+    return {};
+  }
+
+  @override
+  void storeInfo(Map<Variable?, VariableModel<Variable, Type>> variableInfo,
+      VariableModel<Variable, Type> variableModel) {
+    variableInfo[null] = variableModel;
+  }
+
+  @override
+  VariableModel<Variable, Type>? _getInfo(
+          Map<Variable?, VariableModel<Variable, Type>> variableInfo) =>
+      variableInfo[null];
+}
+
 /// Specialization of [ExpressionInfo] for the case where the information we
 /// have about the expression is trivial (meaning we know by construction that
 /// the expression's [after], [ifTrue], and [ifFalse] models are all the same).
diff --git a/pkg/_fe_analyzer_shared/lib/src/messages/codes_generated.dart b/pkg/_fe_analyzer_shared/lib/src/messages/codes_generated.dart
index ba1e3a600fa..d053b4e065f 100644
--- a/pkg/_fe_analyzer_shared/lib/src/messages/codes_generated.dart
+++ b/pkg/_fe_analyzer_shared/lib/src/messages/codes_generated.dart
@@ -4032,6 +4032,29 @@ const MessageCode messageFieldInitializerOutsideConstructor = const MessageCode(
     message: r"""Field formal parameters can only be used in a constructor.""",
     tip: r"""Try removing 'this.'.""");
 
+// DO NOT EDIT. THIS FILE IS GENERATED. SEE TOP OF FILE.
+const Template<Message Function(String name)> templateFieldNotPromoted =
+    const Template<Message Function(String name)>(
+        messageTemplate:
+            r"""'#name' refers to a property so it could not be promoted.""",
+        withArguments: _withArgumentsFieldNotPromoted);
+
+// DO NOT EDIT. THIS FILE IS GENERATED. SEE TOP OF FILE.
+const Code<Message Function(String name)> codeFieldNotPromoted =
+    const Code<Message Function(String name)>(
+  "FieldNotPromoted",
+);
+
+// DO NOT EDIT. THIS FILE IS GENERATED. SEE TOP OF FILE.
+Message _withArgumentsFieldNotPromoted(String name) {
+  if (name.isEmpty) throw 'No name provided';
+  name = demangleMixinApplicationName(name);
+  return new Message(codeFieldNotPromoted,
+      message:
+          """'${name}' refers to a property so it could not be promoted.""",
+      arguments: {'name': name});
+}
+
 // DO NOT EDIT. THIS FILE IS GENERATED. SEE TOP OF FILE.
 const Code<Null> codeFinalAndCovariant = messageFinalAndCovariant;
 
@@ -9620,6 +9643,34 @@ const MessageCode messageVarReturnType = const MessageCode("VarReturnType",
     tip:
         r"""Try removing the keyword 'var', or replacing it with the name of the return type.""");
 
+// DO NOT EDIT. THIS FILE IS GENERATED. SEE TOP OF FILE.
+const Template<
+    Message Function(
+        String
+            name)> templateVariableCouldBeNullDueToWrite = const Template<
+        Message Function(String name)>(
+    messageTemplate:
+        r"""Variable '#name' could be null due to a write occurring here.""",
+    tipTemplate: r"""Try null checking the variable after the write.""",
+    withArguments: _withArgumentsVariableCouldBeNullDueToWrite);
+
+// DO NOT EDIT. THIS FILE IS GENERATED. SEE TOP OF FILE.
+const Code<Message Function(String name)> codeVariableCouldBeNullDueToWrite =
+    const Code<Message Function(String name)>(
+  "VariableCouldBeNullDueToWrite",
+);
+
+// DO NOT EDIT. THIS FILE IS GENERATED. SEE TOP OF FILE.
+Message _withArgumentsVariableCouldBeNullDueToWrite(String name) {
+  if (name.isEmpty) throw 'No name provided';
+  name = demangleMixinApplicationName(name);
+  return new Message(codeVariableCouldBeNullDueToWrite,
+      message:
+          """Variable '${name}' could be null due to a write occurring here.""",
+      tip: """Try null checking the variable after the write.""",
+      arguments: {'name': name});
+}
+
 // DO NOT EDIT. THIS FILE IS GENERATED. SEE TOP OF FILE.
 const Code<Null> codeVerificationErrorOriginContext =
     messageVerificationErrorOriginContext;
diff --git a/pkg/_fe_analyzer_shared/test/annotated_code_helper_test.dart b/pkg/_fe_analyzer_shared/test/annotated_code_helper_test.dart
index 9fb155800db..755d20c34ed 100644
--- a/pkg/_fe_analyzer_shared/test/annotated_code_helper_test.dart
+++ b/pkg/_fe_analyzer_shared/test/annotated_code_helper_test.dart
@@ -16,6 +16,7 @@ main() {
   testDir('pkg/_fe_analyzer_shared/test/flow_analysis/nullability/data');
   testDir('pkg/_fe_analyzer_shared/test/flow_analysis/reachability/data');
   testDir('pkg/_fe_analyzer_shared/test/flow_analysis/type_promotion/data');
+  testDir('pkg/_fe_analyzer_shared/test/flow_analysis/why_not_promoted/data');
   testDir('pkg/_fe_analyzer_shared/test/inheritance/data');
 }
 
diff --git a/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_mini_ast.dart b/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_mini_ast.dart
index 98386848e23..0c02855d82a 100644
--- a/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_mini_ast.dart
+++ b/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_mini_ast.dart
@@ -154,6 +154,11 @@ Statement switch_(Expression expression, List<SwitchCase> cases,
         {required bool isExhaustive}) =>
     new _Switch(expression, cases, isExhaustive);
 
+Expression this_(String type) => new _This(Type(type));
+
+Expression thisOrSuperPropertyGet(String name, {String type = 'Object?'}) =>
+    new _ThisOrSuperPropertyGet(name, type);
+
 Expression throw_(Expression operand) => new _Throw(operand);
 
 Statement tryCatch(List<Statement> body, List<CatchClause> catches) =>
@@ -273,12 +278,24 @@ abstract class Expression extends Node implements _Visitable<Type> {
   /// If `this` is an expression `x`, creates the expression `x || other`.
   Expression or(Expression other) => new _Logical(this, other, isAnd: false);
 
+  /// If `this` is an expression `x`, creates the expression `x.name`.
+  Expression propertyGet(String name, {String type = 'Object?'}) =>
+      new _PropertyGet(this, name, type);
+
   /// If `this` is an expression `x`, creates a pseudo-expression that models
   /// evaluation of `x` followed by execution of [stmt].  This can be used to
   /// test that flow analysis is in the correct state after an expression is
   /// visited.
   Expression thenStmt(Statement stmt) =>
       new _WrappedExpression(null, this, stmt);
+
+  /// Creates an [Expression] that, when analyzed, will behave the same as
+  /// `this`, but after visiting it, will cause [callback] to be passed the
+  /// non-promotion info associated with it.  If the expression has no
+  /// non-promotion info, an empty map will be passed to [callback].
+  Expression whyNotPromoted(
+          void Function(Map<Type, NonPromotionReason>) callback) =>
+      new _WhyNotPromoted(this, callback);
 }
 
 /// Test harness for creating flow analysis tests.  This class implements all
@@ -311,8 +328,10 @@ class Harness extends TypeOperations<Var, Type> {
     'int? <: num?': true,
     'int? <: Object': false,
     'int? <: Object?': true,
+    'Never <: Object?': true,
     'Null <: int': false,
     'Null <: Object': false,
+    'Null <: Object?': true,
     'num <: int': false,
     'num <: Iterable': false,
     'num <: List': false,
@@ -347,6 +366,7 @@ class Harness extends TypeOperations<Var, Type> {
     'Object <: int': false,
     'Object <: int?': false,
     'Object <: List': false,
+    'Object <: Null': false,
     'Object <: num': false,
     'Object <: num?': false,
     'Object <: Object?': true,
@@ -354,6 +374,7 @@ class Harness extends TypeOperations<Var, Type> {
     'Object? <: Object': false,
     'Object? <: int': false,
     'Object? <: int?': false,
+    'Object? <: Null': false,
     'String <: int': false,
     'String <: int?': false,
     'String <: num?': false,
@@ -364,6 +385,8 @@ class Harness extends TypeOperations<Var, Type> {
   static final Map<String, Type> _coreFactors = {
     'Object? - int': Type('Object?'),
     'Object? - int?': Type('Object'),
+    'Object? - Never': Type('Object?'),
+    'Object? - Null': Type('Object'),
     'Object? - num?': Type('Object'),
     'Object? - Object?': Type('Never?'),
     'Object? - String': Type('Object?'),
@@ -410,6 +433,9 @@ class Harness extends TypeOperations<Var, Type> {
 
   Harness({this.allowLocalBooleanVarsToPromote = false, this.legacy = false});
 
+  @override
+  Type get topType => Type('Object?');
+
   /// Updates the harness so that when a [factor] query is invoked on types
   /// [from] and [what], [result] will be returned.
   void addFactor(String from, String what, String result) {
@@ -597,15 +623,30 @@ class SwitchCase implements _Visitable<void> {
 /// testing.  This is essentially a thin wrapper around a string representation
 /// of the type.
 class Type {
+  static bool _allowComparisons = false;
+
   final String type;
 
   Type(this.type);
 
+  @override
+  int get hashCode {
+    if (!_allowComparisons) {
+      // The flow analysis engine should not hash types using hashCode.  It
+      // should compare them using TypeOperations.
+      fail('Unexpected use of operator== on types');
+    }
+    return type.hashCode;
+  }
+
   @override
   bool operator ==(Object other) {
-    // The flow analysis engine should not compare types using operator==.  It
-    // should compare them using TypeOperations.
-    fail('Unexpected use of operator== on types');
+    if (!_allowComparisons) {
+      // The flow analysis engine should not compare types using operator==.  It
+      // should compare them using TypeOperations.
+      fail('Unexpected use of operator== on types');
+    }
+    return other is Type && this.type == other.type;
   }
 
   @override
@@ -1424,6 +1465,29 @@ class _PlaceholderExpression extends Expression {
       type;
 }
 
+class _PropertyGet extends Expression {
+  final Expression target;
+
+  final String propertyName;
+
+  final String type;
+
+  _PropertyGet(this.target, this.propertyName, this.type);
+
+  @override
+  void _preVisit(AssignedVariables<Node, Var> assignedVariables) {
+    target._preVisit(assignedVariables);
+  }
+
+  @override
+  Type _visit(
+      Harness h, FlowAnalysis<Node, Statement, Expression, Var, Type> flow) {
+    target._visit(h, flow);
+    flow.propertyGet(this, target, propertyName);
+    return Type(type);
+  }
+}
+
 class _Return extends Statement {
   _Return() : super._();
 
@@ -1481,6 +1545,43 @@ class _Switch extends Statement {
   }
 }
 
+class _This extends Expression {
+  final Type type;
+
+  _This(this.type);
+
+  @override
+  String toString() => 'this';
+
+  @override
+  void _preVisit(AssignedVariables<Node, Var> assignedVariables) {}
+
+  @override
+  Type _visit(
+      Harness h, FlowAnalysis<Node, Statement, Expression, Var, Type> flow) {
+    flow.thisOrSuper(this);
+    return type;
+  }
+}
+
+class _ThisOrSuperPropertyGet extends Expression {
+  final String propertyName;
+
+  final String type;
+
+  _ThisOrSuperPropertyGet(this.propertyName, this.type);
+
+  @override
+  void _preVisit(AssignedVariables<Node, Var> assignedVariables) {}
+
+  @override
+  Type _visit(
+      Harness h, FlowAnalysis<Node, Statement, Expression, Var, Type> flow) {
+    flow.thisOrSuperPropertyGet(this, propertyName);
+    return Type(type);
+  }
+}
+
 class _Throw extends Expression {
   final Expression operand;
 
@@ -1622,6 +1723,37 @@ class _While extends Statement {
   }
 }
 
+class _WhyNotPromoted extends Expression {
+  final Expression target;
+
+  final void Function(Map<Type, NonPromotionReason>) callback;
+
+  _WhyNotPromoted(this.target, this.callback);
+
+  @override
+  String toString() => '$target (whyNotPromoted)';
+
+  @override
+  void _preVisit(AssignedVariables<Node, Var> assignedVariables) {
+    target._preVisit(assignedVariables);
+  }
+
+  @override
+  Type _visit(
+      Harness h, FlowAnalysis<Node, Statement, Expression, Var, Type> flow) {
+    var type = target._visit(h, flow);
+    flow.forwardExpression(this, target);
+    assert(!Type._allowComparisons);
+    Type._allowComparisons = true;
+    try {
+      callback(flow.whyNotPromoted(this));
+    } finally {
+      Type._allowComparisons = false;
+    }
+    return type;
+  }
+}
+
 class _WrappedExpression extends Expression {
   final Statement? before;
   final Expression expr;
@@ -1681,7 +1813,7 @@ class _Write extends Expression {
       Harness h, FlowAnalysis<Node, Statement, Expression, Var, Type> flow) {
     var rhs = this.rhs;
     var type = rhs == null ? variable.type : rhs._visit(h, flow);
-    flow.write(variable, type, rhs);
+    flow.write(this, variable, type, rhs);
     return type;
   }
 }
diff --git a/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_test.dart b/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_test.dart
index 9621ff73a37..1657689f172 100644
--- a/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_test.dart
+++ b/pkg/_fe_analyzer_shared/test/flow_analysis/flow_analysis_test.dart
@@ -499,6 +499,94 @@ main() {
       ]);
     });
 
+    test('equalityOp_end on property get preserves target variable', () {
+      // This is a regression test for a mistake made during the implementation
+      // of "why not promoted" functionality: when storing information about an
+      // attempt to promote a field (e.g. `x.y != null`) we need to make sure we
+      // don't wipe out information about the target variable (`x`).
+      var h = Harness();
+      var x = Var('x', 'C');
+      h.run([
+        declare(x, initialized: true),
+        checkAssigned(x, true),
+        if_(x.read.propertyGet('y').notEq(nullLiteral), [
+          checkAssigned(x, true),
+        ], [
+          checkAssigned(x, true),
+        ]),
+      ]);
+    });
+
+    test('equalityOp_end does not set reachability for `this`', () {
+      var h = Harness();
+      h.addSubtype('C', 'Object', true);
+      h.run([
+        if_(this_('C').is_('Null'), [
+          if_(this_('C').eq(nullLiteral), [
+            checkReachable(true),
+          ], [
+            checkReachable(true),
+          ]),
+        ]),
+      ]);
+    });
+
+    group('equalityOp_end does not set reachability for property gets', () {
+      test('on a variable', () {
+        var h = Harness();
+        var x = Var('x', 'C');
+        h.run([
+          declare(x, initialized: true),
+          if_(x.read.propertyGet('f').is_('Null'), [
+            if_(x.read.propertyGet('f').eq(nullLiteral), [
+              checkReachable(true),
+            ], [
+              checkReachable(true),
+            ]),
+          ]),
+        ]);
+      });
+
+      test('on an arbitrary expression', () {
+        var h = Harness();
+        h.run([
+          if_(expr('C').propertyGet('f').is_('Null'), [
+            if_(expr('C').propertyGet('f').eq(nullLiteral), [
+              checkReachable(true),
+            ], [
+              checkReachable(true),
+            ]),
+          ]),
+        ]);
+      });
+
+      test('on explicit this', () {
+        var h = Harness();
+        h.run([
+          if_(this_('C').propertyGet('f').is_('Null'), [
+            if_(this_('C').propertyGet('f').eq(nullLiteral), [
+              checkReachable(true),
+            ], [
+              checkReachable(true),
+            ]),
+          ]),
+        ]);
+      });
+
+      test('on implicit this/super', () {
+        var h = Harness();
+        h.run([
+          if_(thisOrSuperPropertyGet('f').is_('Null'), [
+            if_(thisOrSuperPropertyGet('f').eq(nullLiteral), [
+              checkReachable(true),
+            ], [
+              checkReachable(true),
+            ]),
+          ]),
+        ]);
+      });
+    });
+
     test('finish checks proper nesting', () {
       var h = Harness();
       var e = expr('Null');
@@ -1372,6 +1460,65 @@ main() {
       ]);
     });
 
+    test('isExpression_end() does not set reachability for `this`', () {
+      var h = Harness();
+      h.run([
+        if_(this_('C').is_('Never'), [
+          checkReachable(true),
+        ], [
+          checkReachable(true),
+        ]),
+      ]);
+    });
+
+    group('isExpression_end() does not set reachability for property gets', () {
+      test('on a variable', () {
+        var h = Harness();
+        var x = Var('x', 'C');
+        h.run([
+          declare(x, initialized: true),
+          if_(x.read.propertyGet('f').is_('Never'), [
+            checkReachable(true),
+          ], [
+            checkReachable(true),
+          ]),
+        ]);
+      });
+
+      test('on an arbitrary expression', () {
+        var h = Harness();
+        h.run([
+          if_(expr('C').propertyGet('f').is_('Never'), [
+            checkReachable(true),
+          ], [
+            checkReachable(true),
+          ]),
+        ]);
+      });
+
+      test('on explicit this', () {
+        var h = Harness();
+        h.run([
+          if_(this_('C').propertyGet('f').is_('Never'), [
+            checkReachable(true),
+          ], [
+            checkReachable(true),
+          ]),
+        ]);
+      });
+
+      test('on implicit this/super', () {
+        var h = Harness();
+        h.run([
+          if_(thisOrSuperPropertyGet('f').is_('Never'), [
+            checkReachable(true),
+          ], [
+            checkReachable(true),
+          ]),
+        ]);
+      });
+    });
+
     test('labeledBlock without break', () {
       var h = Harness();
       var x = Var('x', 'int?');
@@ -3262,7 +3409,7 @@ main() {
         // This should not happen in valid code, but test that we don't crash.
         var h = Harness();
         var s = FlowModel<Var, Type>(Reachability.initial).write(
-            objectQVar, Type('Object?'), new SsaNode<Var, Type>(null), h);
+            null, objectQVar, Type('Object?'), new SsaNode<Var, Type>(null), h);
         expect(s.variableInfo[objectQVar], isNull);
       });
 
@@ -3271,7 +3418,7 @@ main() {
         var s1 = FlowModel<Var, Type>(Reachability.initial)
             .declare(objectQVar, true);
         var s2 = s1.write(
-            objectQVar, Type('Object?'), new SsaNode<Var, Type>(null), h);
+            null, objectQVar, Type('Object?'), new SsaNode<Var, Type>(null), h);
         expect(s2, isNot(same(s1)));
         expect(s2.reachable, same(s1.reachable));
         expect(
@@ -3287,8 +3434,8 @@ main() {
         var h = Harness();
         var s1 = FlowModel<Var, Type>(Reachability.initial)
             .declare(objectQVar, false);
-        var s2 =
-            s1.write(objectQVar, Type('int?'), new SsaNode<Var, Type>(null), h);
+        var s2 = s1.write(
+            null, objectQVar, Type('int?'), new SsaNode<Var, Type>(null), h);
         expect(s2.reachable.overallReachable, true);
         expect(
             s2.infoFor(objectQVar),
@@ -3306,8 +3453,8 @@ main() {
             .tryPromoteForTypeCheck(h, _varRef(objectQVar), Type('int'))
             .ifTrue;
         expect(s1.variableInfo, contains(objectQVar));
-        var s2 =
-            s1.write(objectQVar, Type('int?'), new SsaNode<Var, Type>(null), h);
+        var s2 = s1.write(_MockNonPromotionReason(), objectQVar, Type('int?'),
+            new SsaNode<Var, Type>(null), h);
         expect(s2.reachable.overallReachable, true);
         expect(s2.variableInfo, {
           objectQVar: _matchVariableModel(
@@ -3333,8 +3480,8 @@ main() {
               assigned: true,
               unassigned: false)
         });
-        var s2 =
-            s1.write(objectQVar, Type('num'), new SsaNode<Var, Type>(null), h);
+        var s2 = s1.write(_MockNonPromotionReason(), objectQVar, Type('num'),
+            new SsaNode<Var, Type>(null), h);
         expect(s2.reachable.overallReachable, true);
         expect(s2.variableInfo, {
           objectQVar: _matchVariableModel(
@@ -3362,8 +3509,8 @@ main() {
               assigned: true,
               unassigned: false)
         });
-        var s2 =
-            s1.write(objectQVar, Type('num'), new SsaNode<Var, Type>(null), h);
+        var s2 = s1.write(_MockNonPromotionReason(), objectQVar, Type('num'),
+            new SsaNode<Var, Type>(null), h);
         expect(s2.reachable.overallReachable, true);
         expect(s2.variableInfo, {
           objectQVar: _matchVariableModel(
@@ -3389,8 +3536,8 @@ main() {
               assigned: true,
               unassigned: false)
         });
-        var s2 =
-            s1.write(objectQVar, Type('num'), new SsaNode<Var, Type>(null), h);
+        var s2 = s1.write(
+            null, objectQVar, Type('num'), new SsaNode<Var, Type>(null), h);
         expect(s2.reachable.overallReachable, true);
         expect(s2.variableInfo, isNot(same(s1.variableInfo)));
         expect(s2.variableInfo, {
@@ -3417,8 +3564,8 @@ main() {
               assigned: true,
               unassigned: false)
         });
-        var s2 =
-            s1.write(objectQVar, Type('int'), new SsaNode<Var, Type>(null), h);
+        var s2 = s1.write(
+            null, objectQVar, Type('int'), new SsaNode<Var, Type>(null), h);
         expect(s2.reachable.overallReachable, true);
         expect(s2.variableInfo, isNot(same(s1.variableInfo)));
         expect(s2.variableInfo, {
@@ -3440,7 +3587,8 @@ main() {
             x: _matchVariableModel(chain: null),
           });
 
-          var s2 = s1.write(x, Type('int'), new SsaNode<Var, Type>(null), h);
+          var s2 =
+              s1.write(null, x, Type('int'), new SsaNode<Var, Type>(null), h);
           expect(s2.variableInfo, {
             x: _matchVariableModel(chain: ['int']),
           });
@@ -3461,7 +3609,8 @@ main() {
           });
 
           // 'x' is write-captured, so not promoted
-          var s3 = s2.write(x, Type('int'), new SsaNode<Var, Type>(null), h);
+          var s3 =
+              s2.write(null, x, Type('int'), new SsaNode<Var, Type>(null), h);
           expect(s3.variableInfo, {
             x: _matchVariableModel(chain: null, writeCaptured: true),
           });
@@ -3480,7 +3629,7 @@ main() {
             ),
           });
           var s2 = s1.write(
-              objectQVar, Type('int'), new SsaNode<Var, Type>(null), h);
+              null, objectQVar, Type('int'), new SsaNode<Var, Type>(null), h);
           expect(s2.variableInfo, {
             objectQVar: _matchVariableModel(
               chain: ['int?', 'int'],
@@ -3502,7 +3651,7 @@ main() {
             ),
           });
           var s2 = s1.write(
-              objectQVar, Type('int'), new SsaNode<Var, Type>(null), h);
+              null, objectQVar, Type('int'), new SsaNode<Var, Type>(null), h);
           expect(s2.variableInfo, {
             objectQVar: _matchVariableModel(
               chain: ['Object', 'int'],
@@ -3524,8 +3673,8 @@ main() {
             ofInterest: ['num?'],
           ),
         });
-        var s2 =
-            s1.write(objectQVar, Type('num?'), new SsaNode<Var, Type>(null), h);
+        var s2 = s1.write(_MockNonPromotionReason(), objectQVar, Type('num?'),
+            new SsaNode<Var, Type>(null), h);
         expect(s2.variableInfo, {
           objectQVar: _matchVariableModel(
             chain: ['num?'],
@@ -3548,8 +3697,8 @@ main() {
             ofInterest: ['num?', 'int?'],
           ),
         });
-        var s2 =
-            s1.write(objectQVar, Type('int?'), new SsaNode<Var, Type>(null), h);
+        var s2 = s1.write(_MockNonPromotionReason(), objectQVar, Type('int?'),
+            new SsaNode<Var, Type>(null), h);
         expect(s2.variableInfo, {
           objectQVar: _matchVariableModel(
             chain: ['num?', 'int?'],
@@ -3618,7 +3767,8 @@ main() {
               ),
             });
 
-            var s2 = s1.write(x, Type('C'), new SsaNode<Var, Type>(null), h);
+            var s2 =
+                s1.write(null, x, Type('C'), new SsaNode<Var, Type>(null), h);
             expect(s2.variableInfo, {
               x: _matchVariableModel(
                 chain: ['Object', 'B'],
@@ -3643,7 +3793,8 @@ main() {
               ),
             });
 
-            var s2 = s1.write(x, Type('C'), new SsaNode<Var, Type>(null), h);
+            var s2 =
+                s1.write(null, x, Type('C'), new SsaNode<Var, Type>(null), h);
             expect(s2.variableInfo, {
               x: _matchVariableModel(
                 chain: ['Object', 'B'],
@@ -3668,7 +3819,8 @@ main() {
               ),
             });
 
-            var s2 = s1.write(x, Type('B'), new SsaNode<Var, Type>(null), h);
+            var s2 =
+                s1.write(null, x, Type('B'), new SsaNode<Var, Type>(null), h);
             expect(s2.variableInfo, {
               x: _matchVariableModel(
                 chain: ['Object', 'A'],
@@ -3694,7 +3846,7 @@ main() {
               ),
             });
             var s2 = s1.write(
-                objectQVar, Type('int'), new SsaNode<Var, Type>(null), h);
+                null, objectQVar, Type('int'), new SsaNode<Var, Type>(null), h);
             // It's ambiguous whether to promote to num? or num*, so we don't
             // promote.
             expect(s2, isNot(same(s1)));
@@ -3721,8 +3873,8 @@ main() {
               ofInterest: ['num?', 'num*'],
             ),
           });
-          var s2 = s1.write(
-              objectQVar, Type('num?'), new SsaNode<Var, Type>(null), h);
+          var s2 = s1.write(_MockNonPromotionReason(), objectQVar, Type('num?'),
+              new SsaNode<Var, Type>(null), h);
           // It's ambiguous whether to promote to num? or num*, but since the
           // written type is exactly num?, we use that.
           expect(s2.variableInfo, {
@@ -3754,7 +3906,8 @@ main() {
           ),
         });
 
-        var s2 = s1.write(x, Type('double'), new SsaNode<Var, Type>(null), h);
+        var s2 = s1.write(_MockNonPromotionReason(), x, Type('double'),
+            new SsaNode<Var, Type>(null), h);
         expect(s2.variableInfo, {
           x: _matchVariableModel(
             chain: ['num?', 'num'],
@@ -3908,11 +4061,11 @@ main() {
             .declare(c, false)
             .declare(d, false);
         var s1 = s0
-            .write(a, Type('int'), new SsaNode<Var, Type>(null), h)
-            .write(b, Type('int'), new SsaNode<Var, Type>(null), h);
+            .write(null, a, Type('int'), new SsaNode<Var, Type>(null), h)
+            .write(null, b, Type('int'), new SsaNode<Var, Type>(null), h);
         var s2 = s0
-            .write(a, Type('int'), new SsaNode<Var, Type>(null), h)
-            .write(c, Type('int'), new SsaNode<Var, Type>(null), h);
+            .write(null, a, Type('int'), new SsaNode<Var, Type>(null), h)
+            .write(null, c, Type('int'), new SsaNode<Var, Type>(null), h);
         var result = s1.rebaseForward(h, s2);
         expect(result.infoFor(a).assigned, true);
         expect(result.infoFor(b).assigned, true);
@@ -3978,7 +4131,8 @@ main() {
           var s0 = FlowModel<Var, Type>(Reachability.initial).declare(x, true);
           var s1 = s0;
           if (unsafe) {
-            s1 = s1.write(x, Type('Object?'), new SsaNode<Var, Type>(null), h);
+            s1 = s1.write(
+                null, x, Type('Object?'), new SsaNode<Var, Type>(null), h);
           }
           if (thisType != null) {
             s1 =
@@ -5363,6 +5517,173 @@ main() {
       ]);
     });
   });
+
+  group('why not promoted', () {
+    test('due to assignment', () {
+      var h = Harness();
+      var x = Var('x', 'int?');
+      late Expression writeExpression;
+      h.run([
+        declare(x, initialized: true),
+        if_(x.read.eq(nullLiteral), [
+          return_(),
+        ]),
+        checkPromoted(x, 'int'),
+        (writeExpression = x.write(expr('int?'))).stmt,
+        checkNotPromoted(x),
+        x.read.whyNotPromoted((reasons) {
+          expect(reasons.keys, unorderedEquals([Type('int')]));
+          var nonPromotionReason =
+              reasons.values.single as DemoteViaExplicitWrite<Var, Expression>;
+          expect(nonPromotionReason.writeExpression, same(writeExpression));
+        }).stmt,
+      ]);
+    });
+
+    test('due to assignment, multiple demotions', () {
+      var h = Harness();
+      var x = Var('x', 'Object?');
+      late Expression writeExpression;
+      h.run([
+        declare(x, initialized: true),
+        if_(x.read.isNot('int?'), [
+          return_(),
+        ]),
+        if_(x.read.eq(nullLiteral), [
+          return_(),
+        ]),
+        checkPromoted(x, 'int'),
+        (writeExpression = x.write(expr('Object?'))).stmt,
+        checkNotPromoted(x),
+        x.read.whyNotPromoted((reasons) {
+          expect(reasons.keys, unorderedEquals([Type('int'), Type('int?')]));
+          expect(
+              (reasons[Type('int')] as DemoteViaExplicitWrite<Var, Expression>)
+                  .writeExpression,
+              same(writeExpression));
+          expect(
+              (reasons[Type('int?')] as DemoteViaExplicitWrite<Var, Expression>)
+                  .writeExpression,
+              same(writeExpression));
+        }).stmt,
+      ]);
+    });
+
+    test('preserved in join when one branch unreachable', () {
+      var h = Harness();
+      var x = Var('x', 'int?');
+      late Expression writeExpression;
+      h.run([
+        declare(x, initialized: true),
+        if_(x.read.eq(nullLiteral), [
+          return_(),
+        ]),
+        checkPromoted(x, 'int'),
+        (writeExpression = x.write(expr('int?'))).stmt,
+        checkNotPromoted(x),
+        if_(expr('bool'), [
+          return_(),
+        ]),
+        x.read.whyNotPromoted((reasons) {
+          expect(reasons.keys, unorderedEquals([Type('int')]));
+          var nonPromotionReason =
+              reasons.values.single as DemoteViaExplicitWrite<Var, Expression>;
+          expect(nonPromotionReason.writeExpression, same(writeExpression));
+        }).stmt,
+      ]);
+    });
+
+    test('preserved in later promotions', () {
+      var h = Harness();
+      var x = Var('x', 'Object');
+      late Expression writeExpression;
+      h.run([
+        declare(x, initialized: true),
+        if_(x.read.is_('int', isInverted: true), [
+          return_(),
+        ]),
+        checkPromoted(x, 'int'),
+        (writeExpression = x.write(expr('Object'))).stmt,
+        checkNotPromoted(x),
+        if_(x.read.is_('num', isInverted: true), [
+          return_(),
+        ]),
+        checkPromoted(x, 'num'),
+        x.read.whyNotPromoted((reasons) {
+          var nonPromotionReason =
+              reasons[Type('int')] as DemoteViaExplicitWrite;
+          expect(nonPromotionReason.writeExpression, same(writeExpression));
+        }).stmt,
+      ]);
+    });
+
+    test('re-promotion', () {
+      var h = Harness();
+      var x = Var('x', 'int?');
+      h.run([
+        declare(x, initialized: true),
+        if_(x.read.eq(nullLiteral), [
+          return_(),
+        ]),
+        checkPromoted(x, 'int'),
+        x.write(expr('int?')).stmt,
+        checkNotPromoted(x),
+        if_(x.read.eq(nullLiteral), [
+          return_(),
+        ]),
+        checkPromoted(x, 'int'),
+        x.read.whyNotPromoted((reasons) {
+          expect(reasons, isEmpty);
+        }).stmt,
+      ]);
+    });
+
+    group('because field', () {
+      test('via explicit this', () {
+        var h = Harness();
+        h.run([
+          if_(this_('C').propertyGet('field').eq(nullLiteral), [
+            return_(),
+          ]),
+          this_('C').propertyGet('field').whyNotPromoted((reasons) {
+            expect(reasons.keys, unorderedEquals([Type('Object')]));
+            var nonPromotionReason = reasons.values.single;
+            expect(nonPromotionReason, TypeMatcher<FieldNotPromoted>());
+          }).stmt,
+        ]);
+      });
+
+      test('via implicit this/super', () {
+        var h = Harness();
+        h.run([
+          if_(thisOrSuperPropertyGet('field').eq(nullLiteral), [
+            return_(),
+          ]),
+          thisOrSuperPropertyGet('field').whyNotPromoted((reasons) {
+            expect(reasons.keys, unorderedEquals([Type('Object')]));
+            var nonPromotionReason = reasons.values.single;
+            expect(nonPromotionReason, TypeMatcher<FieldNotPromoted>());
+          }).stmt,
+        ]);
+      });
+
+      test('via variable', () {
+        var h = Harness();
+        var x = Var('x', 'C');
+        h.run([
+          declare(x, initialized: true),
+          if_(x.read.propertyGet('field').eq(nullLiteral), [
+            return_(),
+          ]),
+          x.read.propertyGet('field').whyNotPromoted((reasons) {
+            expect(reasons.keys, unorderedEquals([Type('Object')]));
+            var nonPromotionReason = reasons.values.single;
+            expect(nonPromotionReason, TypeMatcher<FieldNotPromoted>());
+          }).stmt,
+        ]);
+      });
+    });
+  });
 }
 
 /// Returns the appropriate matcher for expecting an assertion error to be
@@ -5434,3 +5755,12 @@ Matcher _matchVariableModel(
 
 Reference<Var, Type> _varRef(Var variable) =>
     new VariableReference<Var, Type>(variable);
+
+class _MockNonPromotionReason extends NonPromotionReason {
+  String get shortName => fail('Unexpected call to shortName');
+
+  R accept<R, Node extends Object, Expression extends Object,
+              Variable extends Object>(
+          NonPromotionReasonVisitor<R, Node, Expression, Variable> visitor) =>
+      fail('Unexpected call to accept');
+}
diff --git a/pkg/_fe_analyzer_shared/test/flow_analysis/why_not_promoted/data/assignment.dart b/pkg/_fe_analyzer_shared/test/flow_analysis/why_not_promoted/data/assignment.dart
new file mode 100644
index 00000000000..f867664d2ec
--- /dev/null
+++ b/pkg/_fe_analyzer_shared/test/flow_analysis/why_not_promoted/data/assignment.dart
@@ -0,0 +1,71 @@
+// Copyright (c) 2020, the Dart project authors. Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+abstract class C {
+  C? operator +(int i);
+  int get cProperty => 0;
+}
+
+direct_assignment(int? i, int? j) {
+  if (i == null) return;
+  /*cfe.update: explicitWrite*/ /*analyzer.explicitWrite*/ i = j;
+  i. /*notPromoted(explicitWrite)*/ isEven;
+}
+
+compound_assignment(C? c, int i) {
+  if (c == null) return;
+  /*cfe.update: explicitWrite*/ /*analyzer.explicitWrite*/ c += i;
+  c. /*notPromoted(explicitWrite)*/ cProperty;
+}
+
+via_postfix_op(C? c) {
+  if (c == null) return;
+  /*cfe.update: explicitWrite*/ /*analyzer.explicitWrite*/ c++;
+  c. /*notPromoted(explicitWrite)*/ cProperty;
+}
+
+via_prefix_op(C? c) {
+  if (c == null) return;
+  /*analyzer.explicitWrite*/ ++ /*cfe.update: explicitWrite*/ c;
+  c. /*notPromoted(explicitWrite)*/ cProperty;
+}
+
+via_for_each_statement(int? i, List<int?> list) {
+  if (i == null) return;
+  for (/*cfe.update: explicitWrite*/ /*analyzer.explicitWrite*/ i in list) {
+    i. /*notPromoted(explicitWrite)*/ isEven;
+  }
+}
+
+via_for_each_list_element(int? i, List<int?> list) {
+  if (i == null) return;
+  [
+    for (/*cfe.update: explicitWrite*/ /*analyzer.explicitWrite*/ i in list)
+      i. /*notPromoted(explicitWrite)*/ isEven
+  ];
+}
+
+via_for_each_set_element(int? i, List<int?> list) {
+  if (i == null) return;
+  ({
+    for (/*cfe.update: explicitWrite*/ /*analyzer.explicitWrite*/ i in list)
+      i. /*notPromoted(explicitWrite)*/ isEven
+  });
+}
+
+via_for_each_map_key(int? i, List<int?> list) {
+  if (i == null) return;
+  ({
+    for (/*cfe.update: explicitWrite*/ /*analyzer.explicitWrite*/ i in list)
+      i. /*notPromoted(explicitWrite)*/ isEven: null
+  });
+}
+
+via_for_each_map_value(int? i, List<int?> list) {
+  if (i == null) return;
+  ({
+    for (/*cfe.update: explicitWrite*/ /*analyzer.explicitWrite*/ i in list)
+      null: i. /*notPromoted(explicitWrite)*/ isEven
+  });
+}
diff --git a/pkg/_fe_analyzer_shared/test/flow_analysis/why_not_promoted/data/field.dart b/pkg/_fe_analyzer_shared/test/flow_analysis/why_not_promoted/data/field.dart
new file mode 100644
index 00000000000..0bbec4e7c6e
--- /dev/null
+++ b/pkg/_fe_analyzer_shared/test/flow_analysis/why_not_promoted/data/field.dart
@@ -0,0 +1,50 @@
+// Copyright (c) 2020, the Dart project authors. Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+class C {
+  int? i;
+  int? j;
+
+  get_field_via_explicit_this() {
+    if (this.i == null) return;
+    this.i. /*notPromoted(fieldNotPromoted(i))*/ isEven;
+  }
+
+  get_field_via_explicit_this_parenthesized() {
+    if ((this).i == null) return;
+    (this).i. /*notPromoted(fieldNotPromoted(i))*/ isEven;
+  }
+
+  get_field_by_implicit_this() {
+    if (i == null) return;
+    i. /*notPromoted(fieldNotPromoted(i))*/ isEven;
+  }
+}
+
+class D extends C {
+  get_field_via_explicit_super() {
+    if (super.i == null) return;
+    super.i. /*notPromoted(fieldNotPromoted(i))*/ isEven;
+  }
+
+  get_field_by_implicit_super() {
+    if (i == null) return;
+    i. /*notPromoted(fieldNotPromoted(i))*/ isEven;
+  }
+}
+
+get_field_via_prefixed_identifier(C c) {
+  if (c.i == null) return;
+  c.i. /*notPromoted(fieldNotPromoted(i))*/ isEven;
+}
+
+get_field_via_prefixed_identifier_mismatched_target(C c1, C c2) {
+  if (c1.i == null) return;
+  c2.i.isEven;
+}
+
+get_field_via_prefixed_identifier_mismatched_property(C c) {
+  if (c.i == null) return;
+  c.j.isEven;
+}
diff --git a/pkg/_fe_analyzer_shared/test/flow_analysis/why_not_promoted/data/marker.options b/pkg/_fe_analyzer_shared/test/flow_analysis/why_not_promoted/data/marker.options
new file mode 100644
index 00000000000..1ebb2bcd2cc
--- /dev/null
+++ b/pkg/_fe_analyzer_shared/test/flow_analysis/why_not_promoted/data/marker.options
@@ -0,0 +1,2 @@
+cfe=pkg/front_end/test/id_tests/why_not_promoted_test.dart
+analyzer=pkg/analyzer/test/id_tests/why_not_promoted_test.dart
\ No newline at end of file
diff --git a/pkg/analyzer/lib/error/listener.dart b/pkg/analyzer/lib/error/listener.dart
index 7de0ed73296..e89e8b6de24 100644
--- a/pkg/analyzer/lib/error/listener.dart
+++ b/pkg/analyzer/lib/error/listener.dart
@@ -94,16 +94,18 @@ class ErrorReporter {
   /// Report an error with the given [errorCode] and [arguments].
   /// The [node] is used to compute the location of the error.
   void reportErrorForNode(ErrorCode errorCode, AstNode node,
-      [List<Object?>? arguments]) {
-    reportErrorForOffset(errorCode, node.offset, node.length, arguments);
+      [List<Object?>? arguments, List<DiagnosticMessage>? messages]) {
+    reportErrorForOffset(
+        errorCode, node.offset, node.length, arguments, messages);
   }
 
   /// Report an error with the given [errorCode] and [arguments]. The location
   /// of the error is specified by the given [offset] and [length].
   void reportErrorForOffset(ErrorCode errorCode, int offset, int length,
-      [List<Object?>? arguments]) {
+      [List<Object?>? arguments, List<DiagnosticMessage>? messages]) {
     _convertElements(arguments);
-    var messages = _convertTypeNames(arguments);
+    messages ??= [];
+    messages.addAll(_convertTypeNames(arguments));
     _errorListener.onError(
         AnalysisError(_source, offset, length, errorCode, arguments, messages));
   }
diff --git a/pkg/analyzer/lib/src/dart/resolver/assignment_expression_resolver.dart b/pkg/analyzer/lib/src/dart/resolver/assignment_expression_resolver.dart
index a767e17b95f..d83f41847d2 100644
--- a/pkg/analyzer/lib/src/dart/resolver/assignment_expression_resolver.dart
+++ b/pkg/analyzer/lib/src/dart/resolver/assignment_expression_resolver.dart
@@ -26,7 +26,7 @@ class AssignmentExpressionResolver {
 
   AssignmentExpressionResolver({
     required ResolverVisitor resolver,
-  })  : _resolver = resolver,
+  })   : _resolver = resolver,
         _typePropertyResolver = resolver.typePropertyResolver,
         _inferenceHelper = resolver.inferenceHelper,
         _assignmentShared = AssignmentExpressionShared(
@@ -88,7 +88,8 @@ class AssignmentExpressionResolver {
 
     if (flow != null) {
       if (writeElement is PromotableElement) {
-        flow.write(writeElement, node.staticType!, hasRead ? null : right);
+        flow.write(
+            node, writeElement, node.staticType!, hasRead ? null : right);
       }
       if (isIfNull) {
         flow.ifNullExpression_end();
diff --git a/pkg/analyzer/lib/src/dart/resolver/binary_expression_resolver.dart b/pkg/analyzer/lib/src/dart/resolver/binary_expression_resolver.dart
index 1c8de42bf90..38fcc618153 100644
--- a/pkg/analyzer/lib/src/dart/resolver/binary_expression_resolver.dart
+++ b/pkg/analyzer/lib/src/dart/resolver/binary_expression_resolver.dart
@@ -28,7 +28,7 @@ class BinaryExpressionResolver {
   BinaryExpressionResolver({
     required ResolverVisitor resolver,
     required TypePromotionManager promoteManager,
-  })  : _resolver = resolver,
+  })   : _resolver = resolver,
         _promoteManager = promoteManager,
         _typePropertyResolver = resolver.typePropertyResolver,
         _inferenceHelper = resolver.inferenceHelper;
diff --git a/pkg/analyzer/lib/src/dart/resolver/flow_analysis_visitor.dart b/pkg/analyzer/lib/src/dart/resolver/flow_analysis_visitor.dart
index 4a01f6e187b..27d06a54f57 100644
--- a/pkg/analyzer/lib/src/dart/resolver/flow_analysis_visitor.dart
+++ b/pkg/analyzer/lib/src/dart/resolver/flow_analysis_visitor.dart
@@ -4,6 +4,7 @@
 
 import 'package:_fe_analyzer_shared/src/flow_analysis/flow_analysis.dart';
 import 'package:analyzer/dart/ast/ast.dart';
+import 'package:analyzer/dart/ast/syntactic_entity.dart';
 import 'package:analyzer/dart/ast/token.dart';
 import 'package:analyzer/dart/ast/visitor.dart';
 import 'package:analyzer/dart/element/element.dart';
@@ -40,6 +41,14 @@ class FlowAnalysisDataForTesting {
   final Map<Declaration,
           AssignedVariablesForTesting<AstNode, PromotableElement>>
       assignedVariables = {};
+
+  /// For each expression that led to an error because it was not promoted, a
+  /// string describing the reason it was not promoted.
+  Map<SyntacticEntity, String> nonPromotionReasons = {};
+
+  /// For each auxiliary AST node pointed to by a non-promotion reason, a string
+  /// describing the non-promotion reason pointing to it.
+  Map<AstNode, String> nonPromotionReasonTargets = {};
 }
 
 /// The helper for performing flow analysis during resolution.
@@ -332,6 +341,9 @@ class TypeSystemTypeOperations
 
   TypeSystemTypeOperations(this.typeSystem);
 
+  @override
+  DartType get topType => typeSystem.objectQuestion;
+
   @override
   TypeClassification classifyType(DartType type) {
     if (isSubtypeOf(type, typeSystem.typeProvider.objectType)) {
diff --git a/pkg/analyzer/lib/src/dart/resolver/function_expression_resolver.dart b/pkg/analyzer/lib/src/dart/resolver/function_expression_resolver.dart
index 830360d0bf4..d02413164d4 100644
--- a/pkg/analyzer/lib/src/dart/resolver/function_expression_resolver.dart
+++ b/pkg/analyzer/lib/src/dart/resolver/function_expression_resolver.dart
@@ -25,7 +25,7 @@ class FunctionExpressionResolver {
     required ResolverVisitor resolver,
     required MigrationResolutionHooks? migrationResolutionHooks,
     required TypePromotionManager promoteManager,
-  })  : _resolver = resolver,
+  })   : _resolver = resolver,
         _migrationResolutionHooks = migrationResolutionHooks,
         _inferenceHelper = resolver.inferenceHelper,
         _promoteManager = promoteManager;
diff --git a/pkg/analyzer/lib/src/dart/resolver/postfix_expression_resolver.dart b/pkg/analyzer/lib/src/dart/resolver/postfix_expression_resolver.dart
index 08ebc329062..c7af82901da 100644
--- a/pkg/analyzer/lib/src/dart/resolver/postfix_expression_resolver.dart
+++ b/pkg/analyzer/lib/src/dart/resolver/postfix_expression_resolver.dart
@@ -26,7 +26,7 @@ class PostfixExpressionResolver {
 
   PostfixExpressionResolver({
     required ResolverVisitor resolver,
-  })  : _resolver = resolver,
+  })   : _resolver = resolver,
         _typePropertyResolver = resolver.typePropertyResolver,
         _inferenceHelper = resolver.inferenceHelper,
         _assignmentShared = AssignmentExpressionShared(
@@ -173,7 +173,7 @@ class PostfixExpressionResolver {
         var element = operand.staticElement;
         if (element is PromotableElement) {
           _resolver.flowAnalysis?.flow
-              ?.write(element, operatorReturnType, null);
+              ?.write(node, element, operatorReturnType, null);
         }
       }
     }
diff --git a/pkg/analyzer/lib/src/dart/resolver/prefix_expression_resolver.dart b/pkg/analyzer/lib/src/dart/resolver/prefix_expression_resolver.dart
index 6901f05be06..f03bc53a36b 100644
--- a/pkg/analyzer/lib/src/dart/resolver/prefix_expression_resolver.dart
+++ b/pkg/analyzer/lib/src/dart/resolver/prefix_expression_resolver.dart
@@ -26,7 +26,7 @@ class PrefixExpressionResolver {
 
   PrefixExpressionResolver({
     required ResolverVisitor resolver,
-  })  : _resolver = resolver,
+  })   : _resolver = resolver,
         _typePropertyResolver = resolver.typePropertyResolver,
         _inferenceHelper = resolver.inferenceHelper,
         _assignmentShared = AssignmentExpressionShared(
@@ -209,7 +209,8 @@ class PrefixExpressionResolver {
         if (operand is SimpleIdentifier) {
           var element = operand.staticElement;
           if (element is PromotableElement) {
-            _resolver.flowAnalysis?.flow?.write(element, staticType, null);
+            _resolver.flowAnalysis?.flow
+                ?.write(node, element, staticType, null);
           }
         }
       }
diff --git a/pkg/analyzer/lib/src/dart/resolver/property_element_resolver.dart b/pkg/analyzer/lib/src/dart/resolver/property_element_resolver.dart
index 9a7c23b7194..00317e0a161 100644
--- a/pkg/analyzer/lib/src/dart/resolver/property_element_resolver.dart
+++ b/pkg/analyzer/lib/src/dart/resolver/property_element_resolver.dart
@@ -143,6 +143,7 @@ class PropertyElementResolver {
     }
 
     return _resolve(
+      node: node,
       target: prefix,
       isCascaded: false,
       isNullAware: false,
@@ -171,6 +172,7 @@ class PropertyElementResolver {
 
     if (target is SuperExpression) {
       return _resolveTargetSuperExpression(
+        node: node,
         target: target,
         propertyName: propertyName,
         hasRead: hasRead,
@@ -179,6 +181,7 @@ class PropertyElementResolver {
     }
 
     return _resolve(
+      node: node,
       target: target,
       isCascaded: node.target == null,
       isNullAware: node.isNullAware,
@@ -198,6 +201,9 @@ class PropertyElementResolver {
     if (hasRead) {
       var readLookup = _resolver.lexicalLookup(node: node, setter: false);
       readElementRequested = readLookup.requested;
+      if (readElementRequested is PropertyAccessorElement) {
+        _resolver.flowAnalysis?.flow?.thisOrSuperPropertyGet(node, node.name);
+      }
       _resolver.checkReadOfNotAssignedLocalVariable(node, readElementRequested);
     }
 
@@ -282,6 +288,7 @@ class PropertyElementResolver {
   }
 
   PropertyElementResolverResult _resolve({
+    required Expression node,
     required Expression target,
     required bool isCascaded,
     required bool isNullAware,
@@ -364,6 +371,8 @@ class PropertyElementResolver {
       nameErrorEntity: propertyName,
     );
 
+    _resolver.flowAnalysis?.flow?.propertyGet(node, target, propertyName.name);
+
     if (hasRead && result.needsGetterError) {
       _errorReporter.reportErrorForNode(
         CompileTimeErrorCode.UNDEFINED_GETTER,
@@ -595,6 +604,7 @@ class PropertyElementResolver {
   }
 
   PropertyElementResolverResult _resolveTargetSuperExpression({
+    required Expression node,
     required SuperExpression target,
     required SimpleIdentifier propertyName,
     required bool hasRead,
@@ -610,6 +620,8 @@ class PropertyElementResolver {
 
     if (targetType is InterfaceTypeImpl) {
       if (hasRead) {
+        _resolver.flowAnalysis?.flow
+            ?.propertyGet(node, target, propertyName.name);
         var name = Name(_definingLibrary.source.uri, propertyName.name);
         readElement = _resolver.inheritance
             .getMember2(targetType.element, name, forSuper: true);
diff --git a/pkg/analyzer/lib/src/dart/resolver/type_property_resolver.dart b/pkg/analyzer/lib/src/dart/resolver/type_property_resolver.dart
index fc603c5636d..15898fafb60 100644
--- a/pkg/analyzer/lib/src/dart/resolver/type_property_resolver.dart
+++ b/pkg/analyzer/lib/src/dart/resolver/type_property_resolver.dart
@@ -2,18 +2,23 @@
 // for details. All rights reserved. Use of this source code is governed by a
 // BSD-style license that can be found in the LICENSE file.
 
+import 'package:_fe_analyzer_shared/src/flow_analysis/flow_analysis.dart';
 import 'package:analyzer/dart/ast/ast.dart';
 import 'package:analyzer/dart/ast/syntactic_entity.dart';
 import 'package:analyzer/dart/element/element.dart';
 import 'package:analyzer/dart/element/type.dart';
+import 'package:analyzer/diagnostic/diagnostic.dart';
 import 'package:analyzer/src/dart/element/element.dart';
 import 'package:analyzer/src/dart/element/inheritance_manager3.dart';
 import 'package:analyzer/src/dart/element/type_provider.dart';
 import 'package:analyzer/src/dart/element/type_system.dart';
 import 'package:analyzer/src/dart/resolver/extension_member_resolver.dart';
+import 'package:analyzer/src/dart/resolver/flow_analysis_visitor.dart';
 import 'package:analyzer/src/dart/resolver/resolution_result.dart';
+import 'package:analyzer/src/diagnostic/diagnostic.dart';
 import 'package:analyzer/src/error/codes.dart';
 import 'package:analyzer/src/generated/resolver.dart';
+import 'package:analyzer/src/generated/source.dart';
 
 /// Helper for resolving properties (getters, setters, or methods).
 class TypePropertyResolver {
@@ -114,9 +119,30 @@ class TypePropertyResolver {
         }
       }
 
+      var whyNotPromoted = receiver == null
+          ? null
+          : _resolver.flowAnalysis?.flow?.whyNotPromoted(receiver);
+      List<DiagnosticMessage> messages = [];
+      if (whyNotPromoted != null) {
+        for (var entry in whyNotPromoted.entries) {
+          var whyNotPromotedVisitor = _WhyNotPromotedVisitor(
+              _resolver.source, _resolver.flowAnalysis!.dataForTesting);
+          if (_typeSystem.isPotentiallyNullable(entry.key)) continue;
+          if (_resolver.flowAnalysis!.dataForTesting != null) {
+            _resolver.flowAnalysis!.dataForTesting!
+                .nonPromotionReasons[nameErrorEntity] = entry.value.shortName;
+          }
+          var message = entry.value.accept(whyNotPromotedVisitor);
+          if (message != null) {
+            messages = [message];
+          }
+          break;
+        }
+      }
+
       _resolver.nullableDereferenceVerifier.report(
           receiverErrorNode, receiverType,
-          errorCode: errorCode, arguments: [name]);
+          errorCode: errorCode, arguments: [name], messages: messages);
       _reportedGetterError = true;
       _reportedSetterError = true;
 
@@ -264,3 +290,71 @@ class TypePropertyResolver {
     );
   }
 }
+
+class _WhyNotPromotedVisitor
+    implements
+        NonPromotionReasonVisitor<DiagnosticMessage?, AstNode, Expression,
+            PromotableElement> {
+  final Source source;
+
+  final FlowAnalysisDataForTesting? _dataForTesting;
+
+  _WhyNotPromotedVisitor(this.source, this._dataForTesting);
+
+  @override
+  DiagnosticMessage? visitDemoteViaExplicitWrite(
+      DemoteViaExplicitWrite<PromotableElement, Expression> reason) {
+    var writeExpression = reason.writeExpression;
+    if (_dataForTesting != null) {
+      _dataForTesting!.nonPromotionReasonTargets[writeExpression] =
+          reason.shortName;
+    }
+    var variableName = reason.variable.name;
+    if (variableName == null) return null;
+    return _contextMessageForWrite(variableName, writeExpression);
+  }
+
+  @override
+  DiagnosticMessage? visitDemoteViaForEachVariableWrite(
+      DemoteViaForEachVariableWrite<PromotableElement, AstNode> reason) {
+    var node = reason.node;
+    var variableName = reason.variable.name;
+    if (variableName == null) return null;
+    ForLoopParts parts;
+    if (node is ForStatement) {
+      parts = node.forLoopParts;
+    } else if (node is ForElement) {
+      parts = node.forLoopParts;
+    } else {
+      assert(false, 'Unexpected node type');
+      return null;
+    }
+    if (parts is ForEachPartsWithIdentifier) {
+      var identifier = parts.identifier;
+      if (_dataForTesting != null) {
+        _dataForTesting!.nonPromotionReasonTargets[identifier] =
+            reason.shortName;
+      }
+      return _contextMessageForWrite(variableName, identifier);
+    } else {
+      assert(false, 'Unexpected parts type');
+      return null;
+    }
+  }
+
+  @override
+  DiagnosticMessage? visitFieldNotPromoted(FieldNotPromoted reason) {
+    // TODO(paulberry): how to report this?
+    return null;
+  }
+
+  DiagnosticMessageImpl _contextMessageForWrite(
+      String variableName, Expression writeExpression) {
+    return DiagnosticMessageImpl(
+        filePath: source.fullName,
+        message:
+            "Variable '$variableName' could be null due to a write occurring here.",
+        offset: writeExpression.offset,
+        length: writeExpression.length);
+  }
+}
diff --git a/pkg/analyzer/lib/src/dart/resolver/variable_declaration_resolver.dart b/pkg/analyzer/lib/src/dart/resolver/variable_declaration_resolver.dart
index 68efd6cf33d..d0829f06cab 100644
--- a/pkg/analyzer/lib/src/dart/resolver/variable_declaration_resolver.dart
+++ b/pkg/analyzer/lib/src/dart/resolver/variable_declaration_resolver.dart
@@ -20,7 +20,7 @@ class VariableDeclarationResolver {
   VariableDeclarationResolver({
     required ResolverVisitor resolver,
     required bool strictInference,
-  })  : _resolver = resolver,
+  })   : _resolver = resolver,
         _strictInference = strictInference;
 
   void resolve(VariableDeclarationImpl node) {
diff --git a/pkg/analyzer/lib/src/error/nullable_dereference_verifier.dart b/pkg/analyzer/lib/src/error/nullable_dereference_verifier.dart
index e1dd8125494..1b5f21978b5 100644
--- a/pkg/analyzer/lib/src/error/nullable_dereference_verifier.dart
+++ b/pkg/analyzer/lib/src/error/nullable_dereference_verifier.dart
@@ -4,6 +4,7 @@
 
 import 'package:analyzer/dart/ast/ast.dart';
 import 'package:analyzer/dart/element/type.dart';
+import 'package:analyzer/diagnostic/diagnostic.dart';
 import 'package:analyzer/error/error.dart';
 import 'package:analyzer/error/listener.dart';
 import 'package:analyzer/src/dart/element/type.dart';
@@ -32,13 +33,16 @@ class NullableDereferenceVerifier {
   }
 
   void report(AstNode errorNode, DartType receiverType,
-      {ErrorCode? errorCode, List<String> arguments = const <String>[]}) {
+      {ErrorCode? errorCode,
+      List<String> arguments = const <String>[],
+      List<DiagnosticMessage>? messages}) {
     if (receiverType == _typeSystem.typeProvider.nullType) {
       errorCode = CompileTimeErrorCode.INVALID_USE_OF_NULL_VALUE;
     } else {
       errorCode ??= CompileTimeErrorCode.UNCHECKED_USE_OF_NULLABLE_VALUE;
     }
-    _errorReporter.reportErrorForNode(errorCode, errorNode, arguments);
+    _errorReporter.reportErrorForNode(
+        errorCode, errorNode, arguments, messages);
   }
 
   /// If the [receiverType] is potentially nullable, report it.
diff --git a/pkg/analyzer/lib/src/generated/resolver.dart b/pkg/analyzer/lib/src/generated/resolver.dart
index 14bea1bfc91..e2c892071ca 100644
--- a/pkg/analyzer/lib/src/generated/resolver.dart
+++ b/pkg/analyzer/lib/src/generated/resolver.dart
@@ -1158,8 +1158,7 @@ class ResolverVisitor extends ScopedVisitor {
     _enclosingFunction = node.declaredElement!;
 
     if (flowAnalysis != null) {
-      flowAnalysis!
-          .topLevelDeclaration_enter(node, node.parameters, node.body);
+      flowAnalysis!.topLevelDeclaration_enter(node, node.parameters, node.body);
       flowAnalysis!.executableDeclaration_enter(node, node.parameters, false);
     } else {
       _promoteManager.enterFunctionBody(node.body!);
@@ -1655,8 +1654,7 @@ class ResolverVisitor extends ScopedVisitor {
     _enclosingFunction = node.declaredElement!;
 
     if (flowAnalysis != null) {
-      flowAnalysis!
-          .topLevelDeclaration_enter(node, node.parameters, node.body);
+      flowAnalysis!.topLevelDeclaration_enter(node, node.parameters, node.body);
       flowAnalysis!.executableDeclaration_enter(node, node.parameters, false);
     } else {
       _promoteManager.enterFunctionBody(node.body);
diff --git a/pkg/analyzer/lib/src/generated/static_type_analyzer.dart b/pkg/analyzer/lib/src/generated/static_type_analyzer.dart
index e7d2de5eb87..009061d90d3 100644
--- a/pkg/analyzer/lib/src/generated/static_type_analyzer.dart
+++ b/pkg/analyzer/lib/src/generated/static_type_analyzer.dart
@@ -284,6 +284,7 @@ class StaticTypeAnalyzer extends SimpleAstVisitor<void> {
 
   @override
   void visitSuperExpression(SuperExpression node) {
+    _resolver.flowAnalysis?.flow?.thisOrSuper(node);
     var thisType = _resolver.thisType;
     if (thisType == null ||
         node.thisOrAncestorOfType<ExtensionDeclaration>() != null) {
@@ -304,6 +305,7 @@ class StaticTypeAnalyzer extends SimpleAstVisitor<void> {
   /// interface of the immediately enclosing class.</blockquote>
   @override
   void visitThisExpression(ThisExpression node) {
+    _resolver.flowAnalysis?.flow?.thisOrSuper(node);
     var thisType = _resolver.thisType;
     if (thisType == null) {
       // TODO(brianwilkerson) Report this error if it hasn't already been
diff --git a/pkg/analyzer/test/id_tests/why_not_promoted_test.dart b/pkg/analyzer/test/id_tests/why_not_promoted_test.dart
new file mode 100644
index 00000000000..be0a9c0d395
--- /dev/null
+++ b/pkg/analyzer/test/id_tests/why_not_promoted_test.dart
@@ -0,0 +1,87 @@
+// Copyright (c) 2020, the Dart project authors. Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+import 'dart:io';
+
+import 'package:_fe_analyzer_shared/src/testing/id.dart' show ActualData, Id;
+import 'package:_fe_analyzer_shared/src/testing/id_testing.dart';
+import 'package:analyzer/dart/ast/ast.dart';
+import 'package:analyzer/dart/element/null_safety_understanding_flag.dart';
+import 'package:analyzer/src/dart/analysis/testing_data.dart';
+import 'package:analyzer/src/dart/resolver/flow_analysis_visitor.dart';
+import 'package:analyzer/src/util/ast_data_extractor.dart';
+
+import '../util/id_testing_helper.dart';
+
+main(List<String> args) async {
+  Directory dataDir = Directory.fromUri(
+      Platform.script.resolve('../../../_fe_analyzer_shared/test/flow_analysis/'
+          'why_not_promoted/data'));
+  await NullSafetyUnderstandingFlag.enableNullSafetyTypes(() {
+    return runTests<String?>(dataDir,
+        args: args,
+        createUriForFileName: createUriForFileName,
+        onFailure: onFailure,
+        runTest: runTestFor(
+            const _WhyNotPromotedDataComputer(), [analyzerNnbdConfig]));
+  });
+}
+
+class _WhyNotPromotedDataComputer extends DataComputer<String?> {
+  const _WhyNotPromotedDataComputer();
+
+  @override
+  DataInterpreter<String?> get dataValidator =>
+      const _WhyNotPromotedDataInterpreter();
+
+  @override
+  bool get supportsErrors => true;
+
+  @override
+  void computeUnitData(TestingData testingData, CompilationUnit unit,
+      Map<Id, ActualData<String?>> actualMap) {
+    var flowResult =
+        testingData.uriToFlowAnalysisData[unit.declaredElement!.source.uri]!;
+    _WhyNotPromotedDataExtractor(
+            unit.declaredElement!.source.uri, actualMap, flowResult)
+        .run(unit);
+  }
+}
+
+class _WhyNotPromotedDataExtractor extends AstDataExtractor<String?> {
+  final FlowAnalysisDataForTesting _flowResult;
+
+  _WhyNotPromotedDataExtractor(
+      Uri uri, Map<Id, ActualData<String?>> actualMap, this._flowResult)
+      : super(uri, actualMap);
+
+  @override
+  String? computeNodeValue(Id id, AstNode node) {
+    String? nonPromotionReason = _flowResult.nonPromotionReasons[node];
+    if (nonPromotionReason != null) {
+      return 'notPromoted($nonPromotionReason)';
+    }
+    return _flowResult.nonPromotionReasonTargets[node];
+  }
+}
+
+class _WhyNotPromotedDataInterpreter implements DataInterpreter<String?> {
+  const _WhyNotPromotedDataInterpreter();
+
+  @override
+  String getText(String? actualData, [String? indentation]) =>
+      actualData.toString();
+
+  @override
+  String? isAsExpected(String? actualData, String? expectedData) {
+    if (actualData == expectedData) {
+      return null;
+    } else {
+      return 'Expected $expectedData, got $actualData';
+    }
+  }
+
+  @override
+  bool isEmpty(String? actualData) => actualData == null;
+}
diff --git a/pkg/analyzer/test/src/lint/lint_rule_test.dart b/pkg/analyzer/test/src/lint/lint_rule_test.dart
index c6a04fb411b..5db743af981 100644
--- a/pkg/analyzer/test/src/lint/lint_rule_test.dart
+++ b/pkg/analyzer/test/src/lint/lint_rule_test.dart
@@ -5,6 +5,7 @@
 import 'package:analyzer/dart/ast/ast.dart';
 import 'package:analyzer/dart/ast/token.dart';
 import 'package:analyzer/dart/element/element.dart';
+import 'package:analyzer/diagnostic/diagnostic.dart';
 import 'package:analyzer/error/error.dart';
 import 'package:analyzer/error/listener.dart';
 import 'package:analyzer/src/dart/ast/ast.dart';
@@ -80,7 +81,7 @@ class CollectingReporter extends ErrorReporter {
 
   @override
   void reportErrorForNode(ErrorCode errorCode, AstNode node,
-      [List<Object?>? arguments]) {
+      [List<Object?>? arguments, List<DiagnosticMessage>? messages]) {
     code = errorCode;
   }
 
diff --git a/pkg/analyzer/test/src/workspace/gn_test.dart b/pkg/analyzer/test/src/workspace/gn_test.dart
index 9441a01568d..d25eb2a902a 100644
--- a/pkg/analyzer/test/src/workspace/gn_test.dart
+++ b/pkg/analyzer/test/src/workspace/gn_test.dart
@@ -163,8 +163,8 @@ class GnWorkspaceTest with ResourceProviderMixin {
     newFile('/workspace/.fx-build-dir', content: '$buildDir\n');
     newFile(
         '/workspace/out/debug-x87_128/dartlang/gen/some/code/foo_package_config.json');
-    var workspace =
-        GnWorkspace.find(resourceProvider, convertPath('/workspace/some/code'))!;
+    var workspace = GnWorkspace.find(
+        resourceProvider, convertPath('/workspace/some/code'))!;
     expect(workspace.root, convertPath('/workspace'));
   }
 
@@ -189,8 +189,8 @@ class GnWorkspaceTest with ResourceProviderMixin {
     }
   ]
 }''');
-    var workspace =
-        GnWorkspace.find(resourceProvider, convertPath('/workspace/some/code'))!;
+    var workspace = GnWorkspace.find(
+        resourceProvider, convertPath('/workspace/some/code'))!;
     expect(workspace.root, convertPath('/workspace'));
     expect(workspace.packageMap.length, 1);
     expect(workspace.packageMap['flutter']![0].path,
@@ -218,8 +218,8 @@ class GnWorkspaceTest with ResourceProviderMixin {
     }
   ]
 }''');
-    var workspace =
-        GnWorkspace.find(resourceProvider, convertPath('/workspace/some/code'))!;
+    var workspace = GnWorkspace.find(
+        resourceProvider, convertPath('/workspace/some/code'))!;
     expect(workspace.root, convertPath('/workspace'));
     expect(workspace.packageMap.length, 1);
     expect(workspace.packageMap['flutter']![0].path,
@@ -245,8 +245,8 @@ class GnWorkspaceTest with ResourceProviderMixin {
     }
   ]
 }''');
-    var workspace =
-        GnWorkspace.find(resourceProvider, convertPath('/workspace/some/code'))!;
+    var workspace = GnWorkspace.find(
+        resourceProvider, convertPath('/workspace/some/code'))!;
     expect(workspace.root, convertPath('/workspace'));
     expect(workspace.packageMap.length, 1);
     expect(workspace.packageMap['flutter']![0].path,
@@ -273,8 +273,8 @@ class GnWorkspaceTest with ResourceProviderMixin {
     }
   ]
 }''');
-    var workspace =
-        GnWorkspace.find(resourceProvider, convertPath('/workspace/some/code'))!;
+    var workspace = GnWorkspace.find(
+        resourceProvider, convertPath('/workspace/some/code'))!;
     expect(workspace.root, convertPath('/workspace'));
     expect(workspace.packageMap.length, 1);
     expect(workspace.packageMap['flutter']![0].path,
@@ -318,8 +318,8 @@ class GnWorkspaceTest with ResourceProviderMixin {
     }
   ]
 }''');
-    var workspace =
-        GnWorkspace.find(resourceProvider, convertPath('/workspace/some/code'))!;
+    var workspace = GnWorkspace.find(
+        resourceProvider, convertPath('/workspace/some/code'))!;
     expect(workspace.root, convertPath('/workspace'));
     expect(workspace.packageMap.length, 1);
     expect(workspace.packageMap['rettulf']![0].path,
@@ -363,8 +363,8 @@ class GnWorkspaceTest with ResourceProviderMixin {
     }
   ]
 }''');
-    var workspace =
-        GnWorkspace.find(resourceProvider, convertPath('/workspace/some/code'))!;
+    var workspace = GnWorkspace.find(
+        resourceProvider, convertPath('/workspace/some/code'))!;
     expect(workspace.root, convertPath('/workspace'));
     expect(workspace.packageMap.length, 2);
     expect(workspace.packageMap['flutter']![0].path,
diff --git a/pkg/analyzer/tool/update_id_tests.dart b/pkg/analyzer/tool/update_id_tests.dart
index 4f7a5d6557e..44a93848bc9 100644
--- a/pkg/analyzer/tool/update_id_tests.dart
+++ b/pkg/analyzer/tool/update_id_tests.dart
@@ -17,4 +17,5 @@ const List<String> idTests = <String>[
   'pkg/analyzer/test/id_tests/nullability_test.dart',
   'pkg/analyzer/test/id_tests/reachability_test.dart',
   'pkg/analyzer/test/id_tests/type_promotion_test.dart',
+  'pkg/analyzer/test/id_tests/why_not_promoted_test.dart',
 ];
diff --git a/pkg/front_end/lib/src/fasta/kernel/inference_visitor.dart b/pkg/front_end/lib/src/fasta/kernel/inference_visitor.dart
index d0363bb377a..c2ff740e87b 100644
--- a/pkg/front_end/lib/src/fasta/kernel/inference_visitor.dart
+++ b/pkg/front_end/lib/src/fasta/kernel/inference_visitor.dart
@@ -5,10 +5,13 @@
 // @dart = 2.9
 
 import 'dart:core' hide MapEntry;
+import 'dart:core' as core;
 
+import 'package:_fe_analyzer_shared/src/flow_analysis/flow_analysis.dart';
 import 'package:_fe_analyzer_shared/src/util/link.dart';
 import 'package:front_end/src/api_prototype/lowering_predicates.dart';
-import 'package:kernel/ast.dart';
+import 'package:kernel/ast.dart'
+    hide Reference; // Work around https://github.com/dart-lang/sdk/issues/44667
 import 'package:kernel/src/legacy_erasure.dart';
 import 'package:kernel/type_algebra.dart' show Substitution;
 import 'package:kernel/type_environment.dart';
@@ -4738,12 +4741,31 @@ class InferenceVisitor
 
     readResult ??= new ExpressionInferenceResult(readType, read);
     if (!inferrer.isTopLevel && readTarget.isNullable) {
+      Map<DartType, NonPromotionReason> whyNotPromoted =
+          inferrer.flowAnalysis?.whyNotPromoted(receiver);
+      List<LocatedMessage> context;
+      if (whyNotPromoted != null && whyNotPromoted.isNotEmpty) {
+        _WhyNotPromotedVisitor whyNotPromotedVisitor =
+            new _WhyNotPromotedVisitor(inferrer);
+        for (core.MapEntry<DartType, NonPromotionReason> entry
+            in whyNotPromoted.entries) {
+          if (entry.key.isPotentiallyNullable) continue;
+          if (inferrer.dataForTesting != null) {
+            inferrer.dataForTesting.flowAnalysisResult
+                .nonPromotionReasons[read] = entry.value.shortName;
+          }
+          LocatedMessage message = entry.value.accept(whyNotPromotedVisitor);
+          context = [message];
+          break;
+        }
+      }
       readResult = inferrer.wrapExpressionInferenceResultInProblem(
           readResult,
           templateNullablePropertyAccessError.withArguments(
               propertyName.text, receiverType, inferrer.isNonNullableByDefault),
           read.fileOffset,
-          propertyName.text.length);
+          propertyName.text.length,
+          context: context);
     }
     return readResult;
   }
@@ -5709,8 +5731,13 @@ class InferenceVisitor
     ExpressionInferenceResult readResult = _computePropertyGet(
         node.fileOffset, receiver, receiverType, node.name, typeContext,
         isThisReceiver: node.receiver is ThisExpression);
-    return inferrer.createNullAwareExpressionInferenceResult(
-        readResult.inferredType, readResult.expression, nullAwareGuards);
+    inferrer.flowAnalysis.propertyGet(node, node.receiver, node.name.name);
+    ExpressionInferenceResult expressionInferenceResult =
+        inferrer.createNullAwareExpressionInferenceResult(
+            readResult.inferredType, readResult.expression, nullAwareGuards);
+    inferrer.flowAnalysis
+        .forwardExpression(expressionInferenceResult.nullAwareAction, node);
+    return expressionInferenceResult;
   }
 
   @override
@@ -5973,6 +6000,7 @@ class InferenceVisitor
   @override
   ExpressionInferenceResult visitSuperPropertyGet(
       SuperPropertyGet node, DartType typeContext) {
+    inferrer.flowAnalysis.thisOrSuperPropertyGet(node, node.name.name);
     if (node.interfaceTarget != null) {
       inferrer.instrumentation?.record(
           inferrer.uriForInstrumentation,
@@ -6160,6 +6188,7 @@ class InferenceVisitor
 
   ExpressionInferenceResult visitThisExpression(
       ThisExpression node, DartType typeContext) {
+    inferrer.flowAnalysis.thisOrSuper(node);
     return new ExpressionInferenceResult(inferrer.thisType, node);
   }
 
@@ -6280,7 +6309,7 @@ class InferenceVisitor
         fileOffset: node.fileOffset,
         isVoidAllowed: declaredOrInferredType is VoidType);
     inferrer.flowAnalysis
-        .write(variable, rhsResult.inferredType, rhsResult.expression);
+        .write(node, variable, rhsResult.inferredType, rhsResult.expression);
     DartType resultType = rhsResult.inferredType;
     Expression resultExpression;
     if (variable.lateSetter != null) {
@@ -6956,6 +6985,44 @@ class InferenceVisitor
   }
 }
 
+class _WhyNotPromotedVisitor
+    implements
+        NonPromotionReasonVisitor<LocatedMessage, Node, Expression,
+            VariableDeclaration> {
+  final TypeInferrerImpl inferrer;
+
+  _WhyNotPromotedVisitor(this.inferrer);
+
+  @override
+  LocatedMessage visitDemoteViaExplicitWrite(
+      DemoteViaExplicitWrite<VariableDeclaration, Expression> reason) {
+    if (inferrer.dataForTesting != null) {
+      inferrer.dataForTesting.flowAnalysisResult
+          .nonPromotionReasonTargets[reason.writeExpression] = reason.shortName;
+    }
+    int offset = reason.writeExpression.fileOffset;
+    return templateVariableCouldBeNullDueToWrite
+        .withArguments(reason.variable.name)
+        .withLocation(inferrer.helper.uri, offset, noLength);
+  }
+
+  @override
+  LocatedMessage visitDemoteViaForEachVariableWrite(
+      DemoteViaForEachVariableWrite<VariableDeclaration, Node> reason) {
+    int offset = (reason.node as TreeNode).fileOffset;
+    return templateVariableCouldBeNullDueToWrite
+        .withArguments(reason.variable.name)
+        .withLocation(inferrer.helper.uri, offset, noLength);
+  }
+
+  @override
+  LocatedMessage visitFieldNotPromoted(FieldNotPromoted reason) {
+    return templateFieldNotPromoted
+        .withArguments(reason.propertyName)
+        .withoutLocation();
+  }
+}
+
 class ForInResult {
   final VariableDeclaration variable;
   final Expression iterable;
@@ -7005,7 +7072,8 @@ class LocalForInVariable implements ForInVariable {
         isVoidAllowed: true);
 
     variableSet.value = rhs..parent = variableSet;
-    inferrer.flowAnalysis.write(variableSet.variable, rhsType, null);
+    inferrer.flowAnalysis
+        .write(variableSet, variableSet.variable, rhsType, null);
     return variableSet;
   }
 }
diff --git a/pkg/front_end/lib/src/fasta/type_inference/type_inference_engine.dart b/pkg/front_end/lib/src/fasta/type_inference/type_inference_engine.dart
index 9d674c08fa3..f2cb2c444ed 100644
--- a/pkg/front_end/lib/src/fasta/type_inference/type_inference_engine.dart
+++ b/pkg/front_end/lib/src/fasta/type_inference/type_inference_engine.dart
@@ -257,6 +257,14 @@ class FlowAnalysisResult {
 
   /// The assigned variables information that computed for the member.
   AssignedVariablesForTesting<TreeNode, VariableDeclaration> assignedVariables;
+
+  /// For each expression that led to an error because it was not promoted, a
+  /// string describing the reason it was not promoted.
+  final Map<TreeNode, String> nonPromotionReasons = {};
+
+  /// For each auxiliary AST node pointed to by a non-promotion reason, a string
+  /// describing the non-promotion reason pointing to it.
+  final Map<TreeNode, String> nonPromotionReasonTargets = {};
 }
 
 /// CFE-specific implementation of [TypeOperations].
@@ -265,6 +273,9 @@ class TypeOperationsCfe extends TypeOperations<VariableDeclaration, DartType> {
 
   TypeOperationsCfe(this.typeEnvironment);
 
+  @override
+  DartType get topType => typeEnvironment.objectNullableRawType;
+
   @override
   TypeClassification classifyType(DartType type) {
     if (type == null) {
diff --git a/pkg/front_end/lib/src/fasta/type_inference/type_inferrer.dart b/pkg/front_end/lib/src/fasta/type_inference/type_inferrer.dart
index 0b50fbb7f99..cfdc40c737c 100644
--- a/pkg/front_end/lib/src/fasta/type_inference/type_inferrer.dart
+++ b/pkg/front_end/lib/src/fasta/type_inference/type_inferrer.dart
@@ -1784,7 +1784,8 @@ class TypeInferrerImpl implements TypeInferrer {
     return createNullAwareExpressionInferenceResult(
         result.inferredType,
         helper.wrapInProblem(
-            result.nullAwareAction, message, fileOffset, length),
+            result.nullAwareAction, message, fileOffset, length,
+            context: context),
         result.nullAwareGuards);
   }
 
diff --git a/pkg/front_end/messages.status b/pkg/front_end/messages.status
index 245cd2db037..b9899510f3a 100644
--- a/pkg/front_end/messages.status
+++ b/pkg/front_end/messages.status
@@ -344,6 +344,8 @@ FieldNonNullableWithoutInitializerError/analyzerCode: Fail
 FieldNonNullableWithoutInitializerError/example: Fail
 FieldNonNullableWithoutInitializerWarning/analyzerCode: Fail
 FieldNonNullableWithoutInitializerWarning/example: Fail
+FieldNotPromoted/analyzerCode: Fail
+FieldNotPromoted/example: Fail
 FinalAndCovariant/part_wrapped_script2: Fail
 FinalAndCovariant/script2: Fail
 FinalFieldWithoutInitializer/example: Fail
@@ -793,6 +795,8 @@ ValueForRequiredParameterNotProvidedWarning/analyzerCode: Fail
 ValueForRequiredParameterNotProvidedWarning/example: Fail
 VarAsTypeName/part_wrapped_script1: Fail
 VarAsTypeName/script1: Fail # Too many problems
+VariableCouldBeNullDueToWrite/analyzerCode: Fail
+VariableCouldBeNullDueToWrite/example: Fail
 WeakWithStrongDillLibrary/analyzerCode: Fail
 WeakWithStrongDillLibrary/example: Fail
 WebLiteralCannotBeRepresentedExactly/analyzerCode: Fail
diff --git a/pkg/front_end/messages.yaml b/pkg/front_end/messages.yaml
index 2e197e95b4b..c27c2925217 100644
--- a/pkg/front_end/messages.yaml
+++ b/pkg/front_end/messages.yaml
@@ -4584,6 +4584,13 @@ MultipleVarianceModifiers:
   tip: "Use at most one of the 'in', 'out', or 'inout' modifiers."
   analyzerCode: ParserErrorCode.MULTIPLE_VARIANCE_MODIFIERS
 
+VariableCouldBeNullDueToWrite:
+  template: "Variable '#name' could be null due to a write occurring here."
+  tip: "Try null checking the variable after the write."
+
+FieldNotPromoted:
+  template: "'#name' refers to a property so it could not be promoted."
+
 NullablePropertyAccessError:
   template: "Property '#name' cannot be accessed on '#type' because it is potentially null."
   tip: "Try accessing using ?. instead."
diff --git a/pkg/front_end/test/id_tests/why_not_promoted_test.dart b/pkg/front_end/test/id_tests/why_not_promoted_test.dart
new file mode 100644
index 00000000000..0b0b6ee3fbf
--- /dev/null
+++ b/pkg/front_end/test/id_tests/why_not_promoted_test.dart
@@ -0,0 +1,93 @@
+// Copyright (c) 2020, the Dart project authors.  Please see the AUTHORS file
+// for details. All rights reserved. Use of this source code is governed by a
+// BSD-style license that can be found in the LICENSE file.
+
+// @dart = 2.9
+
+import 'dart:io' show Directory, Platform;
+
+import 'package:_fe_analyzer_shared/src/testing/id.dart' show ActualData, Id;
+import 'package:_fe_analyzer_shared/src/testing/id_testing.dart'
+    show DataInterpreter, runTests;
+import 'package:_fe_analyzer_shared/src/testing/id_testing.dart';
+import 'package:front_end/src/fasta/builder/member_builder.dart';
+import 'package:front_end/src/fasta/type_inference/type_inference_engine.dart';
+import 'package:front_end/src/testing/id_testing_helper.dart';
+import 'package:front_end/src/testing/id_testing_utils.dart';
+import 'package:kernel/ast.dart' hide Variance, MapEntry;
+
+main(List<String> args) async {
+  Directory dataDir = new Directory.fromUri(
+      Platform.script.resolve('../../../_fe_analyzer_shared/test/flow_analysis/'
+          'why_not_promoted/data'));
+  await runTests<String>(dataDir,
+      args: args,
+      createUriForFileName: createUriForFileName,
+      onFailure: onFailure,
+      runTest: runTestFor(
+          const WhyNotPromotedDataComputer(), [cfeNonNullableOnlyConfig]));
+}
+
+class WhyNotPromotedDataComputer extends DataComputer<String> {
+  const WhyNotPromotedDataComputer();
+
+  @override
+  DataInterpreter<String> get dataValidator =>
+      const _WhyNotPromotedDataInterpreter();
+
+  /// Errors are supported for testing erroneous code. The reported errors are
+  /// not tested.
+  @override
+  bool get supportsErrors => true;
+
+  /// Function that computes a data mapping for [member].
+  ///
+  /// Fills [actualMap] with the data.
+  void computeMemberData(
+      TestConfig config,
+      InternalCompilerResult compilerResult,
+      Member member,
+      Map<Id, ActualData<String>> actualMap,
+      {bool verbose}) {
+    MemberBuilderImpl memberBuilder =
+        lookupMemberBuilder(compilerResult, member);
+    member.accept(new WhyNotPromotedDataExtractor(compilerResult, actualMap,
+        memberBuilder.dataForTesting.inferenceData.flowAnalysisResult));
+  }
+}
+
+class WhyNotPromotedDataExtractor extends CfeDataExtractor<String> {
+  final FlowAnalysisResult _flowResult;
+
+  WhyNotPromotedDataExtractor(InternalCompilerResult compilerResult,
+      Map<Id, ActualData<String>> actualMap, this._flowResult)
+      : super(compilerResult, actualMap);
+
+  @override
+  String computeNodeValue(Id id, TreeNode node) {
+    String nonPromotionReason = _flowResult.nonPromotionReasons[node];
+    if (nonPromotionReason != null) {
+      return 'notPromoted($nonPromotionReason)';
+    }
+    return _flowResult.nonPromotionReasonTargets[node];
+  }
+}
+
+class _WhyNotPromotedDataInterpreter implements DataInterpreter<String> {
+  const _WhyNotPromotedDataInterpreter();
+
+  @override
+  String getText(String actualData, [String indentation]) => actualData;
+
+  @override
+  String isAsExpected(String actualData, String expectedData) {
+    if (actualData == expectedData) {
+      return null;
+    } else {
+      return 'Expected $expectedData, got $actualData';
+    }
+  }
+
+  @override
+  bool isEmpty(String actualData) => actualData == null;
+}
diff --git a/pkg/front_end/test/lint_test.status b/pkg/front_end/test/lint_test.status
index 27289546b3a..aaa6e982bbf 100644
--- a/pkg/front_end/test/lint_test.status
+++ b/pkg/front_end/test/lint_test.status
@@ -20,6 +20,7 @@ front_end/lib/src/fasta/incremental_compiler/ImportsTwice: Fail
 front_end/lib/src/fasta/kernel/body_builder/ImportsTwice: Fail
 front_end/lib/src/fasta/kernel/constant_evaluator/ExplicitType: Pass
 front_end/lib/src/fasta/kernel/expression_generator_helper/ImportsTwice: Fail
+front_end/lib/src/fasta/kernel/inference_visitor/ImportsTwice: Fail
 front_end/lib/src/fasta/kernel/kernel_api/Exports: Fail
 front_end/lib/src/fasta/kernel/kernel_ast_api/Exports: Fail
 front_end/lib/src/fasta/kernel/kernel_builder/Exports: Fail
diff --git a/pkg/front_end/test/spell_checking_list_code.txt b/pkg/front_end/test/spell_checking_list_code.txt
index 572493d8689..92adf25808c 100644
--- a/pkg/front_end/test/spell_checking_list_code.txt
+++ b/pkg/front_end/test/spell_checking_list_code.txt
@@ -498,6 +498,7 @@ h
 hacky
 hadn't
 hang
+happy
 hardcode
 harness
 hashes
@@ -847,6 +848,7 @@ player
 plugin
 pm
 pn
+pointed
 pointwise
 polluted
 pool
diff --git a/pkg/front_end/tool/update_all.dart b/pkg/front_end/tool/update_all.dart
index 41ba6a1aea8..c25162c9099 100644
--- a/pkg/front_end/tool/update_all.dart
+++ b/pkg/front_end/tool/update_all.dart
@@ -19,6 +19,7 @@ const List<String> idTests = <String>[
   'pkg/front_end/test/id_tests/nullability_test.dart',
   'pkg/front_end/test/id_tests/reachability_test.dart',
   'pkg/front_end/test/id_tests/type_promotion_test.dart',
+  'pkg/front_end/test/id_tests/why_not_promoted_test.dart',
   'pkg/front_end/test/language_versioning/language_versioning_test.dart',
   'pkg/front_end/test/patching/patching_test.dart',
   'pkg/front_end/test/static_types/static_type_test.dart',
diff --git a/pkg/nnbd_migration/lib/src/decorated_type_operations.dart b/pkg/nnbd_migration/lib/src/decorated_type_operations.dart
index 4c776c82c8f..0f9328ab147 100644
--- a/pkg/nnbd_migration/lib/src/decorated_type_operations.dart
+++ b/pkg/nnbd_migration/lib/src/decorated_type_operations.dart
@@ -20,6 +20,14 @@ class DecoratedTypeOperations
   DecoratedTypeOperations(
       this._typeSystem, this._variableRepository, this._graph);
 
+  @override
+  DecoratedType get topType {
+    // This is only needed for explaining to the user why fields aren't
+    // promoted, functionality of flow analysis that we don't take advantage of
+    // during migration.  So this method should never be called.
+    throw StateError('Unexpected call to topType');
+  }
+
   @override
   TypeClassification classifyType(DecoratedType type) {
     if (type.type.isDartCoreNull) {
diff --git a/pkg/nnbd_migration/lib/src/edge_builder.dart b/pkg/nnbd_migration/lib/src/edge_builder.dart
index c074a4a098a..81382391e0c 100644
--- a/pkg/nnbd_migration/lib/src/edge_builder.dart
+++ b/pkg/nnbd_migration/lib/src/edge_builder.dart
@@ -407,7 +407,7 @@ class EdgeBuilder extends GeneralizingAstVisitor<DecoratedType>
     }
 
     var expressionType = _handleAssignment(node.rightHandSide,
-        destinationExpression: node.leftHandSide,
+        assignmentExpression: node,
         compoundOperatorInfo: isCompound ? node : null,
         questionAssignNode: isQuestionAssign ? node : null,
         sourceIsSetupCall: sourceIsSetupCall);
@@ -1387,7 +1387,7 @@ class EdgeBuilder extends GeneralizingAstVisitor<DecoratedType>
       if (operand is SimpleIdentifier) {
         var element = getWriteOrReadElement(operand);
         if (element is PromotableElement) {
-          _flowAnalysis.write(element, writeType, null);
+          _flowAnalysis.write(node, element, writeType, null);
         }
       }
       return targetType;
@@ -1438,7 +1438,7 @@ class EdgeBuilder extends GeneralizingAstVisitor<DecoratedType>
         if (operand is SimpleIdentifier) {
           var element = getWriteOrReadElement(operand);
           if (element is PromotableElement) {
-            _flowAnalysis.write(element, staticType, null);
+            _flowAnalysis.write(node, element, staticType, null);
           }
         }
       }
@@ -2285,26 +2285,28 @@ class EdgeBuilder extends GeneralizingAstVisitor<DecoratedType>
   /// Creates the necessary constraint(s) for an assignment of the given
   /// [expression] to a destination whose type is [destinationType].
   ///
-  /// Optionally, the caller may supply a [destinationExpression] instead of
+  /// Optionally, the caller may supply an [assignmentExpression] instead of
   /// [destinationType].  In this case, then the type comes from visiting the
-  /// destination expression.  If the destination expression refers to a local
-  /// variable, we mark it as assigned in flow analysis at the proper time.
+  /// LHS of the assignment expression.  If the LHS of the assignment expression
+  /// refers to a local variable, we mark it as assigned in flow analysis at the
+  /// proper time.
   ///
   /// Set [wrapFuture] to true to handle assigning Future<flatten(T)> to R.
   DecoratedType _handleAssignment(Expression expression,
       {DecoratedType destinationType,
-      Expression destinationExpression,
+      AssignmentExpression assignmentExpression,
       AssignmentExpression compoundOperatorInfo,
       AssignmentExpression questionAssignNode,
       bool fromDefaultValue = false,
       bool wrapFuture = false,
       bool sourceIsSetupCall = false}) {
     assert(
-        (destinationExpression == null) != (destinationType == null),
-        'Either destinationExpression or destinationType should be supplied, '
+        (assignmentExpression == null) != (destinationType == null),
+        'Either assignmentExpression or destinationType should be supplied, '
         'but not both');
     PromotableElement destinationLocalVariable;
     if (destinationType == null) {
+      var destinationExpression = assignmentExpression.leftHandSide;
       if (destinationExpression is SimpleIdentifier) {
         var element = getWriteOrReadElement(destinationExpression);
         if (element is PromotableElement) {
@@ -2345,7 +2347,7 @@ class EdgeBuilder extends GeneralizingAstVisitor<DecoratedType>
               source: destinationType,
               destination: _createNonNullableType(compoundOperatorInfo),
               hard: _postDominatedLocals
-                  .isReferenceInScope(destinationExpression));
+                  .isReferenceInScope(assignmentExpression.leftHandSide));
           DecoratedType compoundOperatorType = getOrComputeElementType(
               compoundOperatorMethod,
               targetType: destinationType);
@@ -2403,8 +2405,8 @@ class EdgeBuilder extends GeneralizingAstVisitor<DecoratedType>
         }
       }
       if (destinationLocalVariable != null) {
-        _flowAnalysis.write(destinationLocalVariable, sourceType,
-            compoundOperatorInfo == null ? expression : null);
+        _flowAnalysis.write(assignmentExpression, destinationLocalVariable,
+            sourceType, compoundOperatorInfo == null ? expression : null);
       }
       if (questionAssignNode != null) {
         _flowAnalysis.ifNullExpression_end();
@@ -2419,9 +2421,9 @@ class EdgeBuilder extends GeneralizingAstVisitor<DecoratedType>
         _guards.removeLast();
       }
     }
-    if (destinationExpression != null) {
-      var element =
-          _postDominatedLocals.referencedElement(destinationExpression);
+    if (assignmentExpression != null) {
+      var element = _postDominatedLocals
+          .referencedElement(assignmentExpression.leftHandSide);
       if (element != null) {
         _postDominatedLocals.removeFromAllScopes(element);
         _elementsWrittenToInLocalFunction?.add(element);
diff --git a/tools/generate_package_config.dart b/tools/generate_package_config.dart
index 9369cce572b..08b79205d6e 100644
--- a/tools/generate_package_config.dart
+++ b/tools/generate_package_config.dart
@@ -48,6 +48,8 @@ void main(List<String> args) {
         'pkg/_fe_analyzer_shared/test/flow_analysis/reachability/'),
     packageDirectory(
         'pkg/_fe_analyzer_shared/test/flow_analysis/type_promotion/'),
+    packageDirectory(
+        'pkg/_fe_analyzer_shared/test/flow_analysis/why_not_promoted//'),
     packageDirectory('pkg/_fe_analyzer_shared/test/inheritance/'),
   ];