@@ -2667,6 +2667,19 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        */
       predicate stepLanguageSpecific(AstNode n1, TypePath prefix1, AstNode n2, TypePath prefix2);
 
+      /**
+       * Like `stepLanguageSpecific`, but allows for recursion through type inference, which
+       * has the consequence that it cannot be used in the logic for inferring certain type
+       * information.
+       *
+       * Only use this predicate when using `stepLanguageSpecific` results in non-monotonicity.
+       */
+      default predicate stepLanguageSpecificExtra(
+        AstNode n1, TypePath prefix1, AstNode n2, TypePath prefix2
+      ) {
+        none()
+      }
+
       /**
        * Gets the inferred type of `n` at `path`.
        *
@@ -2684,6 +2697,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        * in `inferTypeLanguageSpecific`; if in doubt, use `inferTypeLanguageSpecific` instead.
        */
       default Type inferTypeCertainLanguageSpecific(AstNode n, TypePath path) { none() }
+
+      /**
+       * Holds if contextual inference is allowed for the node `n` at the type path
+       * `path`. This has the same effect as assigning `UnknownType` to `n` at `path`,
+       * but prevents propagation of `UnknownType` from `n` to other nodes.
+       */
+      default predicate allowContextualInference(AstNode n, TypePath path) { none() }
     }
 
     module Make3<InputSig3 Input3> {
@@ -2893,6 +2913,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
       private predicate step(AstNode n1, TypePath prefix1, AstNode n2, TypePath prefix2) {
         stepLanguageSpecific(n1, prefix1, n2, prefix2)
         or
+        stepLanguageSpecificExtra(n1, prefix1, n2, prefix2)
+        or
         Certain::stepCertain(n1, prefix1, n2, prefix2)
         or
         prefix1.isEmpty() and
@@ -3234,70 +3256,97 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        * This module identifies calls where the return type may need to be inferred from the
        * context, and also implements logic for performing contextual inference.
        */
-      private module ContextualTyping {
-        pragma[nomagic]
-        private TypeParameter getAConstrained(TypeParameter tp) {
-          result = getATypeParameterConstraint(tp).getTypeAt(_)
-        }
-
+      module ContextualTyping {
         /**
-         * Holds if callable `c` mentions type parameter `tp` at some parameter,
-         * possibly via a constraint on another mentioned type parameter.
+         * Provides the input to `ContextualReturnType`.
          */
-        pragma[nomagic]
-        private predicate mentionsTypeParameterAtParameter(Callable c, TypeParameter tp) {
-          tp = getAConstrained*(c.getParameter(_).getType().getTypeAt(_))
+        signature module ContextualReturnTypeInputSig {
+          /** Holds if `c` has the type parameter `tp` at its return type at `path`. */
+          default predicate callableHasTypeParameterAtReturnType(
+            Callable c, TypePath path, TypeParameter tp
+          ) {
+            tp = getCallableReturnType(c, path)
+          }
+
+          /** Gets a parameter of `c`. */
+          default Parameter getACallableParameter(Callable c) { result = c.getParameter(_) }
         }
 
         /**
-         * Holds if the return type of the callable `c` at `path` is type parameter
-         * `tp`, and `tp` does not appear in the type of any parameter of `c`.
-         *
-         * In this case, the context in which `p` is called may be needed to infer
-         * the instantiation of `tp`.
-         *
-         * This covers functions like `Default::default` and `Vec::new` in Rust.
+         * Provide logic for identifying calls where the return type may need to be inferred from the context.
          */
-        pragma[nomagic]
-        private predicate callableReturnContextTypedAt(Callable c, TypePath path, TypeParameter tp) {
-          tp = getCallableReturnType(c, path) and
-          not mentionsTypeParameterAtParameter(c, tp)
-        }
+        module ContextualReturnType<ContextualReturnTypeInputSig Input> {
+          pragma[nomagic]
+          private TypeParameter getAConstrained(TypeParameter tp) {
+            result = getATypeParameterConstraint(tp).getTypeAt(_)
+          }
 
-        bindingset[invocation, target]
-        pragma[inline_late]
-        private predicate hasTypeArgument(Invocation invocation, Callable target, TypeParameter tp) {
-          exists(Type t |
-            InvocationTypeQualifierMatching::typeMatch(invocation, _, _, _, t, tp) and
-            not t instanceof PseudoType
-          )
-          or
-          exists(InvocationMatching::getTypeArgument(invocation, target, tp, _))
-        }
+          /**
+           * Holds if callable `c` mentions type parameter `tp` at some parameter,
+           * possibly via a constraint on another mentioned type parameter.
+           */
+          pragma[nomagic]
+          private predicate mentionsTypeParameterAtParameter(Callable c, TypeParameter tp) {
+            tp = getAConstrained*(Input::getACallableParameter(c).getType().getTypeAt(_))
+          }
 
-        /**
-         * Holds if `invocation` resolves to some target where the return type at `path`
-         * may have to be inferred from the context.
-         */
-        pragma[nomagic]
-        predicate needsContextualTyping(Invocation invocation, TypePath path) {
-          exists(Callable target, TypeParameter tp |
-            target = invocation.getATargetForTypeQualifierMatching()
+          /**
+           * Holds if the return type of the callable `c` at `path` is type parameter
+           * `tp`, and `tp` does not appear in the type of any parameter of `c`.
+           *
+           * In this case, the context in which `p` is called may be needed to infer
+           * the instantiation of `tp`.
+           *
+           * This covers functions like `Default::default` and `Vec::new` in Rust.
+           */
+          pragma[nomagic]
+          private predicate callableReturnContextTypedAt(Callable c, TypePath path, TypeParameter tp) {
+            Input::callableHasTypeParameterAtReturnType(c, path, tp) and
+            not mentionsTypeParameterAtParameter(c, tp)
+          }
+
+          bindingset[invocation, target]
+          pragma[inline_late]
+          private predicate hasTypeArgument(Invocation invocation, Callable target, TypeParameter tp) {
+            exists(Type t |
+              InvocationTypeQualifierMatching::typeMatch(invocation, _, _, _, t, tp) and
+              not t instanceof PseudoType
+            )
             or
-            target = invocation.getTarget(_)
-          |
-            callableReturnContextTypedAt(target, path, tp) and
-            // check that no explicit type arguments have been supplied that bind `tp`
-            not exists(TypeParameter supplied |
-              tp = getAConstrained*(supplied) and
-              hasTypeArgument(invocation, target, supplied)
+            exists(InvocationMatching::getTypeArgument(invocation, target, tp, _))
+          }
+
+          /**
+           * Holds if `invocation` resolves to some target where the return type at `path`
+           * may have to be inferred from the context.
+           */
+          pragma[nomagic]
+          predicate needsContextualTyping(Invocation invocation, TypePath path) {
+            exists(Callable target, TypeParameter tp |
+              target = invocation.getATargetForTypeQualifierMatching()
+              or
+              target = invocation.getTarget(_)
+            |
+              callableReturnContextTypedAt(target, path, tp) and
+              // check that no explicit type arguments have been supplied that bind `tp`
+              not exists(TypeParameter supplied |
+                tp = getAConstrained*(supplied) and
+                hasTypeArgument(invocation, target, supplied)
+              )
             )
-          )
+          }
         }
 
+        private module DefaultContextualReturnTypeInput implements ContextualReturnTypeInputSig { }
+
+        predicate needsContextualTyping =
+          ContextualReturnType<DefaultContextualReturnTypeInput>::needsContextualTyping/2;
+
         pragma[nomagic]
         predicate hasUnknownTypeAt(AstNode n, TypePath path) {
           inferType(n, path) instanceof UnknownType
+          or
+          allowContextualInference(n, path)
         }
 
         pragma[nomagic]
@@ -3326,10 +3375,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         private Type inferTypeContextualCand1(AstNode n, TypePath prefix, TypePath path) {
           result = inferTypeContextualCand0(n, path) and
           hasUnknownType(n) and
-          prefix = path.getAPrefix() and
-          // no need to propagate `UnknownType`s contextually; `n` must already have an
-          // `UnknownType` at some prefix of `path`
-          not result instanceof UnknownType
+          prefix = path.getAPrefix()
         }
 
         pragma[nomagic]
@@ -3465,6 +3511,38 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         }
       }
 
+      /**
+       * Holds if the type of `n` at `path` is `t` and the `j`th element of `path`
+       * corresponds to the `i`th type parameter of the unknown type.
+       */
+      pragma[nomagic]
+      private predicate infersUnknownTypeArg0(AstNode n, int i, int j, TypePath path, Type t) {
+        exists(TypeParameter tp |
+          ContextualTyping::hasUnknownType(n) and
+          tp = any(UnknownType ut).getPositionalTypeParameter(i) and
+          t = inferType(n, path) and
+          not t instanceof UnknownType and
+          tp = path.getElement(j)
+        )
+      }
+
+      /**
+       * Holds if the type of `n` at `path` is `t`, where
+       * `path = prefix ++ tp_i ++ suffix` and `tp_i` is the `i`th type parameter
+       * of the unknown type.
+       */
+      pragma[nomagic]
+      private predicate infersUnknownTypeArg1(
+        AstNode n, TypePath prefix, int i, TypePath suffix, Type t
+      ) {
+        exists(TypePath path, int j, TypePath suffix0 |
+          infersUnknownTypeArg0(n, i, j, path, t) and
+          prefix = path.getProperPrefix(j) and
+          path = prefix.appendInverse(suffix0) and
+          suffix0.isCons(_, suffix)
+        )
+      }
+
       /**
        * Holds if `n` has unknown type at `prefix`, but is still able to
        * infer a known type at `suffix` for the `i`th type parameter of whatever
@@ -3486,13 +3564,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
       private predicate infersUnknownTypeArg(
         AstNode n, TypePath prefix, int i, TypePath suffix, Type t
       ) {
-        exists(TypeParameter tp, TypePath suffix0 |
-          ContextualTyping::hasUnknownTypeAt(n, prefix) and
-          suffix0.isCons(tp, suffix) and
-          tp = any(UnknownType ut).getPositionalTypeParameter(i) and
-          t = inferType(n, prefix.appendInverse(suffix0)) and
-          not t instanceof UnknownType
-        )
+        ContextualTyping::hasUnknownTypeAt(n, prefix) and
+        infersUnknownTypeArg1(n, prefix, i, suffix, t)
       }
 
       pragma[nomagic]
 
@@ -36,13 +36,7 @@ predicate isInTypeContext(Expr expr) {
   or
   expr.getParent() instanceof TypeConstraint
   or
-  exists(Identifier id | id = NameBinding::getStaticBindingTargetFromRef(expr) |
-    id = any(ClassLikeDeclaration c).getNameNode()
-    or
-    id = any(TypeAliasDeclaration t).getNameNode()
-    or
-    id = any(TypeParameter t).getNameNode()
-  )
+  exists(NameBinding::getTypeFromRef(expr))
   or
   any(ExprPositionsPlugin p).isInTypeContext(expr)
   or
 
@@ -810,6 +810,22 @@ NameBinding getStaticBindingTargetFromRef(AstNode access) {
   result = getStaticBindingTargetFromIdentifier(getIdentifierFromRef(access))
 }
 
+/**
+ * Gets the type being accessed by `access`, if any.
+ */
+Identifier getTypeFromRef(AstNode access) {
+  result = getStaticBindingTargetFromRef(access) and
+  (
+    result = any(ClassLikeDeclaration c).getNameNode()
+    or
+    result = any(TypeAliasDeclaration t).getNameNode()
+    or
+    result = any(TypeParameter t).getNameNode()
+    or
+    result = any(AssociatedTypeDeclaration t).getNameNode()
+  )
+}
+
 /**
  * Gets the name of the implicit receiver parameter in scope at `callable` (possibly declared by an outer callable).
  *
 
@@ -80,6 +80,9 @@ abstract private class TypeImpl extends TType {
    */
   TypeParameter getATypeParameter() { result = this.getPositionalTypeParameter(_) }
 
+  /** Gets the name node of this type, if any. */
+  abstract Identifier getNameNode();
+
   /** Gets a textual representation of this type. */
   abstract string toString();
 
@@ -99,6 +102,8 @@ class ClassLikeDeclarationType extends TypeImpl, TClassLikeDeclarationType {
 
   string getName() { result = c.getName() }
 
+  override Identifier getNameNode() { result = c.getNameNode() }
+
   override TypeParameter getPositionalTypeParameter(int i) {
     result = TTypeParameterType(c.getTypeParameter(i))
   }
@@ -117,7 +122,9 @@ class ClassLikeDeclarationType extends TypeImpl, TClassLikeDeclarationType {
 /**
  * A pseudo type that does not correspond to any concrete type in the source code.
  */
-abstract class PseudoType extends TypeImpl { }
+abstract class PseudoType extends TypeImpl {
+  override Identifier getNameNode() { none() }
+}
 
 /**
  * A type representing an unknown type.
@@ -173,6 +180,8 @@ class TypeParameterType extends TypeParameter, TTypeParameterType {
 
   override ClassLikeDeclaration getDeclaringItem() { typeParam = result.getATypeParameter() }
 
+  override Identifier getNameNode() { result = typeParam.getNameNode() }
+
   override string toString() { result = typeParam.getName() }
 
   override Location getLocation() { result = typeParam.getLocation() }
@@ -192,6 +201,8 @@ class AssociatedTypeParameterType extends TypeParameter, TAssociatedTypeParamete
 
   override ClassLikeDeclaration getDeclaringItem() { result = c }
 
+  override Identifier getNameNode() { result = assocTypeDecl.getNameNode() }
+
   override string toString() {
     if inherited = true
     then result = assocTypeDecl.getName() + " (inherited)"
@@ -213,6 +224,8 @@ class UnknownTypeTypeParameter extends TypeParameter, TUnknownTypeTypeParameter
 
   override AstNode getDeclaringItem() { none() }
 
+  override Identifier getNameNode() { none() }
+
   override TypeParameter getPositionalTypeParameter(int j) { none() }
 
   override string toString() { result = "unknown type parameter " + i }