diff --git a/rust/ql/lib/codeql/rust/internal/TypeInference.qll b/rust/ql/lib/codeql/rust/internal/TypeInference.qll
index bcb8e5e1ff6b..5342bf335da6 100644
--- a/rust/ql/lib/codeql/rust/internal/TypeInference.qll
+++ b/rust/ql/lib/codeql/rust/internal/TypeInference.qll
@@ -1910,7 +1910,9 @@ private predicate isMethodCall(MethodCall mc, Type rootType, string name, int ar
   arity = mc.getNumberOfArguments()
 }
 
-private module IsInstantiationOfInput implements IsInstantiationOfInputSig<MethodCall> {
+private module IsInstantiationOfInput implements
+  IsInstantiationOfInputSig<MethodCall, TypeMentionTypeTree>
+{
   /** Holds if `mc` specifies a trait and might target a method in `impl`. */
   pragma[nomagic]
   private predicate methodCallTraitCandidate(MethodCall mc, Impl impl) {
@@ -1939,7 +1941,9 @@ private module IsInstantiationOfInput implements IsInstantiationOfInputSig<Metho
   private TypeRepr getImplSelfTy(Impl impl) { result = impl.getSelfTy() }
 
   pragma[nomagic]
-  predicate potentialInstantiationOf(MethodCall mc, TypeAbstraction impl, TypeMention constraint) {
+  predicate potentialInstantiationOf(
+    MethodCall mc, TypeAbstraction impl, TypeMentionTypeTree constraint
+  ) {
     constraint = getImplSelfTy(impl) and
     (
       methodCallTraitCandidate(mc, impl)
@@ -1958,7 +1962,7 @@ private module IsInstantiationOfInput implements IsInstantiationOfInputSig<Metho
     )
   }
 
-  predicate relevantTypeMention(TypeMention constraint) {
+  predicate relevantTypeMention(TypeMentionTypeTree constraint) {
     exists(Impl impl | methodCandidate(_, _, _, impl) and constraint = impl.getSelfTy())
   }
 }
@@ -2119,14 +2123,16 @@ private predicate methodCallHasNoInherentTarget(MethodCall mc) {
       methodCandidate(rootType, name, arity, impl) and
       not impl.hasTrait()
     |
-      IsInstantiationOf<MethodCall, IsInstantiationOfInput>::isNotInstantiationOf(mc, impl, _)
+      IsInstantiationOf<MethodCall, TypeMentionTypeTree, IsInstantiationOfInput>::isNotInstantiationOf(mc,
+        impl, _)
     )
   )
 }
 
 pragma[nomagic]
 private predicate methodCallHasImplCandidate(MethodCall mc, Impl impl) {
-  IsInstantiationOf<MethodCall, IsInstantiationOfInput>::isInstantiationOf(mc, impl, _) and
+  IsInstantiationOf<MethodCall, TypeMentionTypeTree, IsInstantiationOfInput>::isInstantiationOf(mc,
+    impl, _) and
   if impl.hasTrait() and not exists(mc.getTrait())
   then
     // inherent methods take precedence over trait methods, so only allow
@@ -2267,11 +2273,11 @@ private class AmbigousAssocFunctionCallExpr extends MkAmbigousAssocFunctionCallE
 }
 
 private module AmbigousAssocFuncIsInstantiationOfInput implements
-  IsInstantiationOfInputSig<AmbigousAssocFunctionCallExpr>
+  IsInstantiationOfInputSig<AmbigousAssocFunctionCallExpr, TypeMentionTypeTree>
 {
   pragma[nomagic]
   predicate potentialInstantiationOf(
-    AmbigousAssocFunctionCallExpr ce, TypeAbstraction impl, TypeMention constraint
+    AmbigousAssocFunctionCallExpr ce, TypeAbstraction impl, TypeMentionTypeTree constraint
   ) {
     exists(FunctionCallExpr call, Function resolved, Function cand, int pos |
       ce = MkAmbigousAssocFunctionCallExpr(call, resolved, pos) and
@@ -2297,7 +2303,7 @@ private ItemNode resolveUnambigousFunctionCallTarget(FunctionCallExpr call) {
 pragma[nomagic]
 private Function resolveAmbigousFunctionCallTargetFromIndex(FunctionCallExpr call, int index) {
   exists(Impl impl, int pos, Function resolved |
-    IsInstantiationOf<AmbigousAssocFunctionCallExpr, AmbigousAssocFuncIsInstantiationOfInput>::isInstantiationOf(MkAmbigousAssocFunctionCallExpr(call,
+    IsInstantiationOf<AmbigousAssocFunctionCallExpr, TypeMentionTypeTree, AmbigousAssocFuncIsInstantiationOfInput>::isInstantiationOf(MkAmbigousAssocFunctionCallExpr(call,
         resolved, pos), impl, _) and
     result = call.getAnAmbigousCandidateRanked(impl, pos, resolved, index)
   |
diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll
index 32615dc46cd6..5bf4032a3b81 100644
--- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll
+++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll
@@ -494,6 +494,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
   module Make2<InputSig2 Input2> {
     private import Input2
 
+    final private class FinalTypeMention = TypeMention;
+
+    /** An adapter for type mentions to implement `HasTypeTreeSig`. */
+    final class TypeMentionTypeTree extends FinalTypeMention {
+      Type getTypeAt(TypePath path) { result = this.resolveTypeAt(path) }
+    }
+
     /** Gets the type at the empty path of `tm`. */
     bindingset[tm]
     pragma[inline_late]
@@ -502,7 +509,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
     }
 
     /** Provides the input to `IsInstantiationOf`. */
-    signature module IsInstantiationOfInputSig<HasTypeTreeSig App> {
+    signature module IsInstantiationOfInputSig<HasTypeTreeSig App, HasTypeTreeSig Constraint> {
       /**
        * Holds if `abs` is a type abstraction, `tm` occurs in the scope of
        * `abs`, and `app` is potentially an application/instantiation of `abs`.
@@ -523,46 +530,45 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        * accessing the `bar` method of `foo` potentially instantiates the `impl`
        * block with a type argument for `A`.
        */
-      predicate potentialInstantiationOf(App app, TypeAbstraction abs, TypeMention tm);
+      predicate potentialInstantiationOf(App app, TypeAbstraction abs, Constraint tm);
 
       /**
        * Holds if `constraint` might occur as the third argument of
        * `potentialInstantiationOf`. Defaults to simply projecting the third
        * argument of `potentialInstantiationOf`.
        */
-      default predicate relevantTypeMention(TypeMention tm) { potentialInstantiationOf(_, _, tm) }
+      default predicate relevantTypeMention(Constraint tm) { potentialInstantiationOf(_, _, tm) }
     }
 
     /**
      * Provides functionality for determining if a type is a possible
      * instantiation of a type mention containing type parameters.
      */
-    module IsInstantiationOf<HasTypeTreeSig App, IsInstantiationOfInputSig<App> Input> {
+    module IsInstantiationOf<
+      HasTypeTreeSig App, HasTypeTreeSig Constraint,
+      IsInstantiationOfInputSig<App, Constraint> Input>
+    {
       private import Input
 
       /** Gets the `i`th path in `tm` per some arbitrary order. */
       pragma[nomagic]
-      private TypePath getNthPath(TypeMention tm, int i) {
+      private TypePath getNthPath(Constraint tm, int i) {
         result =
-          rank[i + 1](TypePath path |
-            exists(tm.resolveTypeAt(path)) and relevantTypeMention(tm)
-          |
-            path
-          )
+          rank[i + 1](TypePath path | exists(tm.getTypeAt(path)) and relevantTypeMention(tm) | path)
       }
 
       pragma[nomagic]
       private Type resolveNthTypeAt(
-        App app, TypeAbstraction abs, TypeMention tm, int i, TypePath path
+        App app, TypeAbstraction abs, Constraint tm, int i, TypePath path
       ) {
         potentialInstantiationOf(app, abs, tm) and
         path = getNthPath(tm, i) and
-        result = tm.resolveTypeAt(path)
+        result = tm.getTypeAt(path)
       }
 
       pragma[nomagic]
       private predicate satisfiesConcreteTypesFromIndex(
-        App app, TypeAbstraction abs, TypeMention tm, int i
+        App app, TypeAbstraction abs, Constraint tm, int i
       ) {
         exists(Type t, TypePath path |
           t = resolveNthTypeAt(app, abs, tm, i, path) and
@@ -574,7 +580,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
 
       /** Holds if all the concrete types in `tm` also occur in `app`. */
       pragma[nomagic]
-      private predicate satisfiesConcreteTypes(App app, TypeAbstraction abs, TypeMention tm) {
+      private predicate satisfiesConcreteTypes(App app, TypeAbstraction abs, Constraint tm) {
         satisfiesConcreteTypesFromIndex(app, abs, tm, max(int i | exists(getNthPath(tm, i))))
       }
 
@@ -592,14 +598,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        * arbitrary order, if any.
        */
       pragma[nomagic]
-      private TypePath getNthTypeParameterPath(TypeMention tm, TypeParameter tp, int i) {
+      private TypePath getNthTypeParameterPath(Constraint tm, TypeParameter tp, int i) {
         result =
-          rank[i + 1](TypePath path | tp = tm.resolveTypeAt(path) and relevantTypeMention(tm) | path)
+          rank[i + 1](TypePath path | tp = tm.getTypeAt(path) and relevantTypeMention(tm) | path)
       }
 
       pragma[nomagic]
       private predicate typeParametersEqualFromIndexBase(
-        App app, TypeAbstraction abs, TypeMention tm, TypeParameter tp, TypePath path
+        App app, TypeAbstraction abs, Constraint tm, TypeParameter tp, TypePath path
       ) {
         path = getNthTypeParameterPath(tm, tp, 0) and
         satisfiesConcreteTypes(app, abs, tm) and
@@ -609,7 +615,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
 
       pragma[nomagic]
       private predicate typeParametersEqualFromIndex(
-        App app, TypeAbstraction abs, TypeMention tm, TypeParameter tp, Type t, int i
+        App app, TypeAbstraction abs, Constraint tm, TypeParameter tp, Type t, int i
       ) {
         exists(TypePath path |
           t = app.getTypeAt(path) and
@@ -623,7 +629,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
       }
 
       private predicate typeParametersEqual(
-        App app, TypeAbstraction abs, TypeMention tm, TypeParameter tp
+        App app, TypeAbstraction abs, Constraint tm, TypeParameter tp
       ) {
         satisfiesConcreteTypes(app, abs, tm) and
         tp = getNthTypeParameter(abs, _) and
@@ -639,7 +645,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
       }
 
       private predicate typeParametersHaveEqualInstantiationFromIndex(
-        App app, TypeAbstraction abs, TypeMention tm, int i
+        App app, TypeAbstraction abs, Constraint tm, int i
       ) {
         exists(TypeParameter tp | tp = getNthTypeParameter(abs, i) |
           typeParametersEqual(app, abs, tm, tp) and
@@ -662,7 +668,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        * - `Pair<int, string>` is _not_ an instantiation of `Pair<string, string>`
        */
       pragma[nomagic]
-      predicate isInstantiationOf(App app, TypeAbstraction abs, TypeMention tm) {
+      predicate isInstantiationOf(App app, TypeAbstraction abs, Constraint tm) {
         // We only need to check equality if the concrete types are satisfied.
         satisfiesConcreteTypes(app, abs, tm) and
         // Check if all the places where the same type parameter occurs in `tm`
@@ -684,7 +690,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        * Holds if `app` is _not_ a possible instantiation of `tm`.
        */
       pragma[nomagic]
-      predicate isNotInstantiationOf(App app, TypeAbstraction abs, TypeMention tm) {
+      predicate isNotInstantiationOf(App app, TypeAbstraction abs, Constraint tm) {
         // `app` and `tm` differ on a concrete type
         exists(Type t, TypePath path |
           t = resolveNthTypeAt(app, abs, tm, _, path) and
@@ -721,14 +727,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         )
       }
 
-      final private class FinalTypeMention = TypeMention;
-
-      final private class TypeMentionTypeTree extends FinalTypeMention {
-        Type getTypeAt(TypePath path) { result = this.resolveTypeAt(path) }
-      }
-
       private module IsInstantiationOfInput implements
-        IsInstantiationOfInputSig<TypeMentionTypeTree>
+        IsInstantiationOfInputSig<TypeMentionTypeTree, TypeMentionTypeTree>
       {
         pragma[nomagic]
         private predicate typeCondition(
@@ -745,7 +745,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         }
 
         predicate potentialInstantiationOf(
-          TypeMentionTypeTree constraint, TypeAbstraction abs, TypeMention condition
+          TypeMentionTypeTree constraint, TypeAbstraction abs, TypeMentionTypeTree condition
         ) {
           exists(Type type |
             typeConstraint(type, constraint) and typeCondition(type, abs, condition)
@@ -769,7 +769,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
           conditionSatisfiesConstraint(abs, condition, midConstraint) and
           // NOTE: `midAbs` describe the free type variables in `midCondition`, hence
           // we use that for instantiation check.
-          IsInstantiationOf<TypeMentionTypeTree, IsInstantiationOfInput>::isInstantiationOf(midConstraint,
+          IsInstantiationOf<TypeMentionTypeTree, TypeMentionTypeTree, IsInstantiationOfInput>::isInstantiationOf(midConstraint,
             midAbs, midCondition)
         |
           conditionSatisfiesConstraintTypeAt(midAbs, midCondition, constraint, path, t) and
@@ -933,8 +933,12 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         relevantConstraint(term, constraint)
       }
 
-      private module IsInstantiationOfInput implements IsInstantiationOfInputSig<HasTypeTree> {
-        predicate potentialInstantiationOf(HasTypeTree tt, TypeAbstraction abs, TypeMention cond) {
+      private module IsInstantiationOfInput implements
+        IsInstantiationOfInputSig<HasTypeTree, TypeMentionTypeTree>
+      {
+        predicate potentialInstantiationOf(
+          HasTypeTree tt, TypeAbstraction abs, TypeMentionTypeTree cond
+        ) {
           exists(Type constraint, Type type |
             hasTypeConstraint(tt, type, constraint) and
             rootTypesSatisfaction(type, constraint, abs, cond, _) and
@@ -943,7 +947,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
           )
         }
 
-        predicate relevantTypeMention(TypeMention constraint) {
+        predicate relevantTypeMention(TypeMentionTypeTree constraint) {
           rootTypesSatisfaction(_, _, _, constraint, _)
         }
       }
@@ -969,8 +973,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
           // one where the type instantiates the precondition.
           if multipleConstraintImplementations(type, constraint)
           then
-            IsInstantiationOf<HasTypeTree, IsInstantiationOfInput>::isInstantiationOf(tt, abs,
-              condition)
+            IsInstantiationOf<HasTypeTree, TypeMentionTypeTree, IsInstantiationOfInput>::isInstantiationOf(tt,
+              abs, condition)
           else any()
         )
       }
@@ -1018,8 +1022,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
       }
     }
 
-    /** Provides the input to `Matching`. */
-    signature module MatchingInputSig {
+    /** Provides the input to `MatchingWithEnvironment`. */
+    signature module MatchingWithEnvironmentInputSig {
       /**
        * A position inside a declaration. For example, the integer position of a
        * parameter inside a method or the return type of a method.
@@ -1064,6 +1068,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         string toString();
       }
 
+      /** An environment to track during type matching. */
+      bindingset[this]
+      class AccessEnvironment {
+        /** Gets a textual representation of this environment. */
+        bindingset[this]
+        string toString();
+      }
+
       /** An access that targets a declaration, for example a method call. */
       class Access {
         /** Gets a textual representation of this access. */
@@ -1082,15 +1094,17 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         Type getTypeArgument(TypeArgumentPosition tapos, TypePath path);
 
         /**
-         * Gets the inferred type at `path` for the position `apos` of this access.
+         * Gets the inferred type at `path` for the position `apos` and environment `e`
+         * of this access.
          *
          * For example, if this access is the method call `M(42)`, then the inferred
          * type at argument position `0` is `int`.
          */
-        Type getInferredType(AccessPosition apos, TypePath path);
+        bindingset[e]
+        Type getInferredType(AccessEnvironment e, AccessPosition apos, TypePath path);
 
-        /** Gets the declaration that this access targets. */
-        Declaration getTarget();
+        /** Gets the declaration that this access targets in environment `e`. */
+        Declaration getTarget(AccessEnvironment e);
       }
 
       /** Holds if `apos` and `dpos` match. */
@@ -1128,20 +1142,21 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
      *
      * Matching takes both base types and explicit type arguments into account.
      */
-    module Matching<MatchingInputSig Input> {
+    module MatchingWithEnvironment<MatchingWithEnvironmentInputSig Input> {
       private import Input
 
       /**
-       * Holds if `a` targets `target` and the type for `apos` at `path` in `a`
-       * is `t` after adjustment by `target`.
+       * Holds if `a` targets `target` in environment `e` and the type for `apos` at `path`
+       * in `a` is `t` after adjustment by `target`.
        */
       pragma[nomagic]
       private predicate adjustedAccessType(
-        Access a, AccessPosition apos, Declaration target, TypePath path, Type t
+        Access a, AccessEnvironment e, AccessPosition apos, Declaration target, TypePath path,
+        Type t
       ) {
-        target = a.getTarget() and
+        target = a.getTarget(e) and
         exists(TypePath path0, Type t0 |
-          t0 = a.getInferredType(apos, path0) and
+          t0 = a.getInferredType(e, apos, path0) and
           adjustAccessType(apos, target, path0, t0, path, t)
         )
       }
@@ -1165,47 +1180,53 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
       }
 
       /**
-       * Holds if the type `t` at `path` of `a` matches the type parameter `tp`
-       * of `target`.
+       * Holds if the type `t` at `path` of `a` in environment `e` matches the type
+       * parameter `tp` of `target`.
        */
       pragma[nomagic]
       private predicate directTypeMatch(
-        Access a, Declaration target, TypePath path, Type t, TypeParameter tp
+        Access a, AccessEnvironment e, Declaration target, TypePath path, Type t, TypeParameter tp
       ) {
         not exists(getTypeArgument(a, target, tp, _)) and
         exists(AccessPosition apos, DeclarationPosition dpos, TypePath pathToTypeParam |
           tp = target.getDeclaredType(dpos, pathToTypeParam) and
           accessDeclarationPositionMatch(apos, dpos) and
-          adjustedAccessType(a, apos, target, pathToTypeParam.appendInverse(path), t)
+          adjustedAccessType(a, e, apos, target, pathToTypeParam.appendInverse(path), t)
         )
       }
 
       private module AccessBaseType {
         /**
-         * Holds if inferring types at `a` might depend on the type at `path` of
-         * `apos` having `base` as a transitive base type.
+         * Holds if inferring types at `a` in environment `e` might depend on the type at
+         * `path` of `apos` having `base` as a transitive base type.
          */
-        private predicate relevantAccess(Access a, AccessPosition apos, Type base) {
+        private predicate relevantAccess(
+          Access a, AccessEnvironment e, AccessPosition apos, Type base
+        ) {
           exists(Declaration target, DeclarationPosition dpos |
-            adjustedAccessType(a, apos, target, _, _) and
+            adjustedAccessType(a, e, apos, target, _, _) and
             accessDeclarationPositionMatch(apos, dpos) and
             declarationBaseType(target, dpos, base, _, _)
           )
         }
 
         pragma[nomagic]
-        private Type inferTypeAt(Access a, AccessPosition apos, TypeParameter tp, TypePath suffix) {
-          relevantAccess(a, apos, _) and
+        private Type inferTypeAt(
+          Access a, AccessEnvironment e, AccessPosition apos, TypeParameter tp, TypePath suffix
+        ) {
+          relevantAccess(a, e, apos, _) and
           exists(TypePath path0 |
-            result = a.getInferredType(apos, path0) and
+            result = a.getInferredType(e, apos, path0) and
             path0.isCons(tp, suffix)
           )
         }
 
         /**
          * Holds if `baseMention` is a (transitive) base type mention of the
-         * type of `a` at position `apos` at path `pathToSub`, and `t` is
-         * mentioned (implicitly) at `path` inside `base`. For example, in
+         * type of `a` at position `apos` at path `pathToSub` in environment
+         * `e`, and `t` is mentioned (implicitly) at `path` inside `base`.
+         *
+         * For example, in
          *
          * ```csharp
          * class C<T1> { }
@@ -1234,15 +1255,16 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
          * `Base<C<T3>>` | `"T2.T1.T1"` | `int`
          */
         predicate hasBaseTypeMention(
-          Access a, AccessPosition apos, TypeMention baseMention, TypePath path, Type t
+          Access a, AccessEnvironment e, AccessPosition apos, TypeMention baseMention,
+          TypePath path, Type t
         ) {
-          relevantAccess(a, apos, resolveTypeMentionRoot(baseMention)) and
-          exists(Type sub | sub = a.getInferredType(apos, TypePath::nil()) |
+          relevantAccess(a, e, apos, resolveTypeMentionRoot(baseMention)) and
+          exists(Type sub | sub = a.getInferredType(e, apos, TypePath::nil()) |
             baseTypeMentionHasNonTypeParameterAt(sub, baseMention, path, t)
             or
             exists(TypePath prefix, TypePath suffix, TypeParameter tp |
               baseTypeMentionHasTypeParameterAt(sub, baseMention, prefix, tp) and
-              t = inferTypeAt(a, apos, tp, suffix) and
+              t = inferTypeAt(a, e, apos, tp, suffix) and
               path = prefix.append(suffix)
             )
           )
@@ -1251,35 +1273,39 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
 
       private module AccessConstraint {
         predicate relevantAccessConstraint(
-          Access a, Declaration target, AccessPosition apos, TypePath path, Type constraint
+          Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath path,
+          Type constraint
         ) {
-          target = a.getTarget() and
+          target = a.getTarget(e) and
           typeParameterConstraintHasTypeParameter(target, apos, path, constraint, _, _)
         }
 
         private newtype TRelevantAccess =
-          MkRelevantAccess(Access a, Declaration target, AccessPosition apos, TypePath path) {
-            relevantAccessConstraint(a, target, apos, path, _)
+          MkRelevantAccess(
+            Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath path
+          ) {
+            relevantAccessConstraint(a, e, target, apos, path, _)
           }
 
         /**
-         * If the access `a` for `apos` and `path` has an inferred type which
-         * type inference requires to satisfy some constraint.
+         * If the access `a` for `apos`, environment `e`, and `path` has an inferred type
+         * which type inference requires to satisfy some constraint.
          */
         private class RelevantAccess extends MkRelevantAccess {
           Access a;
+          AccessEnvironment e;
           Declaration target;
           AccessPosition apos;
           TypePath path;
 
-          RelevantAccess() { this = MkRelevantAccess(a, target, apos, path) }
+          RelevantAccess() { this = MkRelevantAccess(a, e, target, apos, path) }
 
           Type getTypeAt(TypePath suffix) {
-            adjustedAccessType(a, apos, target, path.appendInverse(suffix), result)
+            adjustedAccessType(a, e, apos, target, path.appendInverse(suffix), result)
           }
 
           /** Holds if this relevant access should satisfy `constraint`. */
-          Type getConstraint() { relevantAccessConstraint(a, target, apos, path, result) }
+          Type getConstraint() { relevantAccessConstraint(a, e, target, apos, path, result) }
 
           string toString() {
             result = a.toString() + ", " + apos.toString() + ", " + path.toString()
@@ -1297,24 +1323,24 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         }
 
         predicate satisfiesConstraintType(
-          Access a, Declaration target, AccessPosition apos, TypePath prefix, Type constraint,
-          TypePath path, Type t
+          Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath prefix,
+          Type constraint, TypePath path, Type t
         ) {
           SatisfiesConstraint<RelevantAccess, SatisfiesConstraintInput>::satisfiesConstraintType(MkRelevantAccess(a,
-              target, apos, prefix), constraint, path, t)
+              e, target, apos, prefix), constraint, path, t)
         }
       }
 
       /**
-       * Holds if the type of `a` at `apos` has the base type `base`, and when
-       * viewed as an element of that type has the type `t` at `path`.
+       * Holds if the type of `a` at `apos` in environment `e` has the base type `base`,
+       * and when viewed as an element of that type has the type `t` at `path`.
        */
       pragma[nomagic]
       private predicate accessBaseType(
-        Access a, AccessPosition apos, Type base, TypePath path, Type t
+        Access a, AccessEnvironment e, AccessPosition apos, Type base, TypePath path, Type t
       ) {
         exists(TypeMention tm |
-          AccessBaseType::hasBaseTypeMention(a, apos, tm, path, t) and
+          AccessBaseType::hasBaseTypeMention(a, e, apos, tm, path, t) and
           base = resolveTypeMentionRoot(tm)
         )
       }
@@ -1332,9 +1358,9 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
       }
 
       /**
-       * Holds if the (transitive) base type `t` at `path` of `a` for some
-       * `AccessPosition` matches the type parameter `tp`, which is used in the
-       * declared types of `target`.
+       * Holds if the (transitive) base type `t` at `path` of `a` in environment `e`
+       * for some `AccessPosition` matches the type parameter `tp`, which is used in
+       * the declared types of `target`.
        *
        * For example, in
        *
@@ -1365,27 +1391,27 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        */
       pragma[nomagic]
       private predicate baseTypeMatch(
-        Access a, Declaration target, TypePath path, Type t, TypeParameter tp
+        Access a, AccessEnvironment e, Declaration target, TypePath path, Type t, TypeParameter tp
       ) {
         not exists(getTypeArgument(a, target, tp, _)) and
-        target = a.getTarget() and
+        target = a.getTarget(e) and
         exists(AccessPosition apos, DeclarationPosition dpos, Type base, TypePath pathToTypeParam |
-          accessBaseType(a, apos, base, pathToTypeParam.appendInverse(path), t) and
+          accessBaseType(a, e, apos, base, pathToTypeParam.appendInverse(path), t) and
           declarationBaseType(target, dpos, base, pathToTypeParam, tp) and
           accessDeclarationPositionMatch(apos, dpos)
         )
       }
 
       /**
-       * Holds if for `a` and corresponding `target`, the type parameter `tp` is
-       * matched by a type argument at the access with type `t` and type path
+       * Holds if for `a` and corresponding `target` in environment `e`, the type parameter
+       * `tp` is matched by a type argument at the access with type `t` and type path
        * `path`.
        */
       pragma[nomagic]
       private predicate explicitTypeMatch(
-        Access a, Declaration target, TypePath path, Type t, TypeParameter tp
+        Access a, AccessEnvironment e, Declaration target, TypePath path, Type t, TypeParameter tp
       ) {
-        target = a.getTarget() and
+        target = a.getTarget(e) and
         t = getTypeArgument(a, target, tp, path)
       }
 
@@ -1427,36 +1453,36 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
 
       pragma[nomagic]
       private predicate typeConstraintBaseTypeMatch(
-        Access a, Declaration target, TypePath path, Type t, TypeParameter tp
+        Access a, AccessEnvironment e, Declaration target, TypePath path, Type t, TypeParameter tp
       ) {
         not exists(getTypeArgument(a, target, tp, _)) and
         exists(Type constraint, AccessPosition apos, TypePath pathToTp, TypePath pathToTp2 |
           typeParameterConstraintHasTypeParameter(target, apos, pathToTp2, constraint, pathToTp, tp) and
-          AccessConstraint::satisfiesConstraintType(a, target, apos, pathToTp2, constraint,
+          AccessConstraint::satisfiesConstraintType(a, e, target, apos, pathToTp2, constraint,
             pathToTp.appendInverse(path), t)
         )
       }
 
       pragma[inline]
       private predicate typeMatch(
-        Access a, Declaration target, TypePath path, Type t, TypeParameter tp
+        Access a, AccessEnvironment e, Declaration target, TypePath path, Type t, TypeParameter tp
       ) {
         // A type given at the access corresponds directly to the type parameter
         // at the target.
-        explicitTypeMatch(a, target, path, t, tp)
+        explicitTypeMatch(a, e, target, path, t, tp)
         or
         // We can infer the type of `tp` from one of the access positions
-        directTypeMatch(a, target, path, t, tp)
+        directTypeMatch(a, e, target, path, t, tp)
         or
         // We can infer the type of `tp` by going up the type hiearchy
-        baseTypeMatch(a, target, path, t, tp)
+        baseTypeMatch(a, e, target, path, t, tp)
         or
         // We can infer the type of `tp` by a type constraint
-        typeConstraintBaseTypeMatch(a, target, path, t, tp)
+        typeConstraintBaseTypeMatch(a, e, target, path, t, tp)
       }
 
       /**
-       * Gets the inferred type of `a` at `path` for position `apos`.
+       * Gets the inferred type of `a` at `path` for position `apos` and environment `e`.
        *
        * For example, in
        *
@@ -1494,25 +1520,168 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        * `"T2.T1.T1"` | `int`
        */
       pragma[nomagic]
-      Type inferAccessType(Access a, AccessPosition apos, TypePath path) {
+      Type inferAccessType(Access a, AccessEnvironment e, AccessPosition apos, TypePath path) {
         exists(DeclarationPosition dpos | accessDeclarationPositionMatch(apos, dpos) |
           // A suffix of `path` leads to a type parameter in the target
           exists(Declaration target, TypePath prefix, TypeParameter tp, TypePath suffix |
             tp = target.getDeclaredType(dpos, prefix) and
             path = prefix.append(suffix) and
-            typeMatch(a, target, suffix, result, tp)
+            typeMatch(a, e, target, suffix, result, tp)
           )
           or
           // `path` corresponds directly to a concrete type in the declaration
           exists(Declaration target |
             result = target.getDeclaredType(dpos, path) and
-            target = a.getTarget() and
+            target = a.getTarget(e) and
             not result instanceof TypeParameter
           )
         )
       }
     }
 
+    /** Provides the input to `Matching`. */
+    signature module MatchingInputSig {
+      /**
+       * A position inside a declaration. For example, the integer position of a
+       * parameter inside a method or the return type of a method.
+       */
+      bindingset[this]
+      class DeclarationPosition {
+        /** Gets a textual representation of this position. */
+        bindingset[this]
+        string toString();
+      }
+
+      /** A declaration, for example a method. */
+      class Declaration {
+        /** Gets a textual representation of this declaration. */
+        string toString();
+
+        /** Gets the location of this declaration. */
+        Location getLocation();
+
+        /** Gets the type parameter at position `tppos` of this declaration, if any. */
+        TypeParameter getTypeParameter(TypeParameterPosition tppos);
+
+        /**
+         * Gets the declared type of this declaration at `path` for position `dpos`.
+         *
+         * For example, if this declaration is the method `int M(bool b)`,
+         * then the declared type at parameter position `0` is `bool`, the
+         * declared type at the `this` position is the class type, and the
+         * declared return type is `int`.
+         */
+        Type getDeclaredType(DeclarationPosition dpos, TypePath path);
+      }
+
+      /**
+       * A position inside an access. For example, the integer position of an
+       * argument inside a method call.
+       */
+      bindingset[this]
+      class AccessPosition {
+        /** Gets a textual representation of this position. */
+        bindingset[this]
+        string toString();
+      }
+
+      /** An access that targets a declaration, for example a method call. */
+      class Access {
+        /** Gets a textual representation of this access. */
+        string toString();
+
+        /** Gets the location of this access. */
+        Location getLocation();
+
+        /**
+         * Gets the type at `path` for the type argument at position `tapos` of
+         * this access, if any.
+         *
+         * For example, in a method call like `M<int>()`, `int` is an explicit
+         * type argument at position `0`.
+         */
+        Type getTypeArgument(TypeArgumentPosition tapos, TypePath path);
+
+        /**
+         * Gets the inferred type at `path` for the position `apos` of this access.
+         *
+         * For example, if this access is the method call `M(42)`, then the inferred
+         * type at argument position `0` is `int`.
+         */
+        Type getInferredType(AccessPosition apos, TypePath path);
+
+        /** Gets the declaration that this access targets. */
+        Declaration getTarget();
+      }
+
+      /** Holds if `apos` and `dpos` match. */
+      bindingset[apos]
+      bindingset[dpos]
+      predicate accessDeclarationPositionMatch(AccessPosition apos, DeclarationPosition dpos);
+
+      /**
+       * Holds if matching an inferred type `t` at `path` inside an access at `apos`
+       * against the declaration `target` means that the type should be adjusted to
+       * `tAdj` at `pathAdj`.
+       *
+       * For example, in
+       *
+       * ```csharp
+       * void M(int? i) {}
+       * M(42);
+       * ```
+       *
+       * the inferred type of `42` is `int`, but it should be adjusted to `int?`
+       * when matching against `M`.
+       */
+      bindingset[apos, target, path, t]
+      default predicate adjustAccessType(
+        AccessPosition apos, Declaration target, TypePath path, Type t, TypePath pathAdj, Type tAdj
+      ) {
+        pathAdj = path and
+        tAdj = t
+      }
+    }
+
+    /**
+     * Provides logic for matching types at accesses against types at the
+     * declarations that the accesses target.
+     *
+     * Matching takes both base types and explicit type arguments into account.
+     */
+    module Matching<MatchingInputSig Input> {
+      private module Inp implements MatchingWithEnvironmentInputSig {
+        private import codeql.util.Unit
+        import Input
+
+        predicate adjustAccessType = Input::adjustAccessType/6;
+
+        class AccessEnvironment = Unit;
+
+        final private class AccessFinal = Input::Access;
+
+        class Access extends AccessFinal {
+          Type getInferredType(AccessEnvironment e, AccessPosition apos, TypePath path) {
+            exists(e) and
+            result = super.getInferredType(apos, path)
+          }
+
+          Declaration getTarget(AccessEnvironment e) {
+            exists(e) and
+            result = super.getTarget()
+          }
+        }
+      }
+
+      private module M = MatchingWithEnvironment<Inp>;
+
+      import M
+
+      Type inferAccessType(Input::Access a, Input::AccessPosition apos, TypePath path) {
+        result = M::inferAccessType(a, _, apos, path)
+      }
+    }
+
     /** Provides consistency checks. */
     module Consistency {
       query predicate missingTypeParameterId(TypeParameter tp) {