diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll b/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll
index 51781a473057..c2c7730d4e9a 100644
--- a/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll
+++ b/rust/ql/lib/codeql/rust/internal/typeinference/BlanketImplementation.qll
@@ -100,7 +100,7 @@ module SatisfiesBlanketConstraint<
   }
 
   private module SatisfiesBlanketConstraintInput implements
-    SatisfiesConstraintInputSig<ArgumentTypeAndBlanketOffset>
+    SatisfiesTypeInputSig<ArgumentTypeAndBlanketOffset>
   {
     pragma[nomagic]
     additional predicate relevantConstraint(
@@ -120,7 +120,7 @@ module SatisfiesBlanketConstraint<
   }
 
   private module SatisfiesBlanketConstraint =
-    SatisfiesConstraint<ArgumentTypeAndBlanketOffset, SatisfiesBlanketConstraintInput>;
+    SatisfiesType<ArgumentTypeAndBlanketOffset, SatisfiesBlanketConstraintInput>;
 
   /**
    * Holds if the argument type `at` satisfies the first non-trivial blanket
diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll
index 0f65d21dcf71..35dd9854c399 100644
--- a/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll
+++ b/rust/ql/lib/codeql/rust/internal/typeinference/FunctionOverloading.qll
@@ -14,13 +14,13 @@ private import TypeInference
 private import FunctionType
 
 pragma[nomagic]
-private Type resolveNonTypeParameterTypeAt(TypeMention tm, TypePath path) {
+private Type resolveNonTypeParameterTypeAt(PreTypeMention tm, TypePath path) {
   result = tm.getTypeAt(path) and
   not result instanceof TypeParameter
 }
 
 bindingset[t1, t2]
-private predicate typeMentionEqual(TypeMention t1, TypeMention t2) {
+private predicate typeMentionEqual(PreTypeMention t1, PreTypeMention t2) {
   forex(TypePath path, Type type | resolveNonTypeParameterTypeAt(t1, path) = type |
     resolveNonTypeParameterTypeAt(t2, path) = type
   )
@@ -28,7 +28,7 @@ private predicate typeMentionEqual(TypeMention t1, TypeMention t2) {
 
 pragma[nomagic]
 private predicate implSiblingCandidate(
-  Impl impl, TraitItemNode trait, Type rootType, TypeMention selfTy
+  Impl impl, TraitItemNode trait, Type rootType, PreTypeMention selfTy
 ) {
   trait = impl.(ImplItemNode).resolveTraitTy() and
   selfTy = impl.getSelfTy() and
@@ -52,7 +52,7 @@ pragma[inline]
 private predicate implSiblings(TraitItemNode trait, Impl impl1, Impl impl2) {
   impl1 != impl2 and
   (
-    exists(Type rootType, TypeMention selfTy1, TypeMention selfTy2 |
+    exists(Type rootType, PreTypeMention selfTy1, PreTypeMention selfTy2 |
       implSiblingCandidate(impl1, trait, rootType, selfTy1) and
       implSiblingCandidate(impl2, trait, rootType, selfTy2) and
       // In principle the second conjunct below should be superflous, but we still
@@ -76,6 +76,15 @@ private predicate implSiblings(TraitItemNode trait, Impl impl1, Impl impl2) {
 pragma[nomagic]
 private predicate implHasSibling(ImplItemNode impl, Trait trait) { implSiblings(trait, impl, _) }
 
+pragma[nomagic]
+predicate implHasAmbigousSiblingAt(ImplItemNode impl, Trait trait, TypePath path) {
+  exists(ImplItemNode impl2 |
+    implSiblings(trait, impl, impl2) and
+    resolveNonTypeParameterTypeAt(impl.getTraitPath(), path) !=
+      resolveNonTypeParameterTypeAt(impl2.getTraitPath(), path)
+  )
+}
+
 /**
  * Holds if `f` is a function declared inside `trait`, and the type of `f` at
  * `pos` and `path` is `traitTp`, which is a type parameter of `trait`.
diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll b/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll
index 70dfe9e90056..2b7b4ec5c01c 100644
--- a/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll
+++ b/rust/ql/lib/codeql/rust/internal/typeinference/TypeInference.qll
@@ -41,6 +41,12 @@ private module Input implements InputSig1<Location>, InputSig2<PreTypeMention> {
 
   class TypeAbstraction = TA::TypeAbstraction;
 
+  predicate typeAbstractionHasAmbigousConstraintAt(
+    TypeAbstraction abs, Type constraint, TypePath path
+  ) {
+    FunctionOverloading::implHasAmbigousSiblingAt(abs, constraint.(TraitType).getTrait(), path)
+  }
+
   class TypeArgumentPosition extends TTypeArgumentPosition {
     int asMethodTypeArgumentPosition() { this = TMethodTypeArgumentPosition(result) }
 
@@ -127,17 +133,15 @@ private module Input implements InputSig1<Location>, InputSig2<PreTypeMention> {
 
   PreTypeMention getABaseTypeMention(Type t) { none() }
 
-  Type getATypeParameterConstraint(TypeParameter tp, TypePath path) {
-    exists(TypeMention tm | result = tm.getTypeAt(path) |
-      tm = tp.(TypeParamTypeParameter).getTypeParam().getATypeBound().getTypeRepr() or
-      tm = tp.(SelfTypeParameter).getTrait() or
-      tm =
-        tp.(ImplTraitTypeTypeParameter)
-            .getImplTraitTypeRepr()
-            .getTypeBoundList()
-            .getABound()
-            .getTypeRepr()
-    )
+  PreTypeMention getATypeParameterConstraint(TypeParameter tp) {
+    result = tp.(TypeParamTypeParameter).getTypeParam().getATypeBound().getTypeRepr() or
+    result = tp.(SelfTypeParameter).getTrait() or
+    result =
+      tp.(ImplTraitTypeTypeParameter)
+          .getImplTraitTypeRepr()
+          .getTypeBoundList()
+          .getABound()
+          .getTypeRepr()
   }
 
   /**
@@ -1126,7 +1130,7 @@ private module ContextTyping {
     or
     exists(TypeParameter mid |
       assocFunctionMentionsTypeParameterAtNonRetPos(i, f, mid) and
-      tp = getATypeParameterConstraint(mid, _)
+      tp = getATypeParameterConstraint(mid).getTypeAt(_)
     )
   }
 
@@ -2237,7 +2241,7 @@ private module MethodResolution {
     }
 
     private module MethodCallSatisfiesDerefConstraintInput implements
-      SatisfiesConstraintInputSig<MethodCallDerefCand>
+      SatisfiesTypeInputSig<MethodCallDerefCand>
     {
       pragma[nomagic]
       predicate relevantConstraint(MethodCallDerefCand mc, Type constraint) {
@@ -2247,7 +2251,7 @@ private module MethodResolution {
     }
 
     private module MethodCallSatisfiesDerefConstraint =
-      SatisfiesConstraint<MethodCallDerefCand, MethodCallSatisfiesDerefConstraintInput>;
+      SatisfiesType<MethodCallDerefCand, MethodCallSatisfiesDerefConstraintInput>;
 
     pragma[nomagic]
     private AssociatedTypeTypeParameter getDerefTargetTypeParameter() {
@@ -3683,7 +3687,7 @@ final private class AwaitTarget extends Expr {
   Type getTypeAt(TypePath path) { result = inferType(this, path) }
 }
 
-private module AwaitSatisfiesConstraintInput implements SatisfiesConstraintInputSig<AwaitTarget> {
+private module AwaitSatisfiesTypeInput implements SatisfiesTypeInputSig<AwaitTarget> {
   pragma[nomagic]
   predicate relevantConstraint(AwaitTarget term, Type constraint) {
     exists(term) and
@@ -3691,13 +3695,12 @@ private module AwaitSatisfiesConstraintInput implements SatisfiesConstraintInput
   }
 }
 
-private module AwaitSatisfiesConstraint =
-  SatisfiesConstraint<AwaitTarget, AwaitSatisfiesConstraintInput>;
+private module AwaitSatisfiesType = SatisfiesType<AwaitTarget, AwaitSatisfiesTypeInput>;
 
 pragma[nomagic]
 private Type inferAwaitExprType(AstNode n, TypePath path) {
   exists(TypePath exprPath |
-    AwaitSatisfiesConstraint::satisfiesConstraintType(n.(AwaitExpr).getExpr(), _, exprPath, result) and
+    AwaitSatisfiesType::satisfiesConstraintType(n.(AwaitExpr).getExpr(), _, exprPath, result) and
     exprPath.isCons(getFutureOutputTypeParameter(), path)
   )
 }
@@ -3876,9 +3879,7 @@ final private class ForIterableExpr extends Expr {
   Type getTypeAt(TypePath path) { result = inferType(this, path) }
 }
 
-private module ForIterableSatisfiesConstraintInput implements
-  SatisfiesConstraintInputSig<ForIterableExpr>
-{
+private module ForIterableSatisfiesTypeInput implements SatisfiesTypeInputSig<ForIterableExpr> {
   predicate relevantConstraint(ForIterableExpr term, Type constraint) {
     exists(term) and
     exists(Trait t | t = constraint.(TraitType).getTrait() |
@@ -3899,15 +3900,15 @@ private AssociatedTypeTypeParameter getIntoIteratorItemTypeParameter() {
   result = getAssociatedTypeTypeParameter(any(IntoIteratorTrait t).getItemType())
 }
 
-private module ForIterableSatisfiesConstraint =
-  SatisfiesConstraint<ForIterableExpr, ForIterableSatisfiesConstraintInput>;
+private module ForIterableSatisfiesType =
+  SatisfiesType<ForIterableExpr, ForIterableSatisfiesTypeInput>;
 
 pragma[nomagic]
 private Type inferForLoopExprType(AstNode n, TypePath path) {
   // type of iterable -> type of pattern (loop variable)
   exists(ForExpr fe, TypePath exprPath, AssociatedTypeTypeParameter tp |
     n = fe.getPat() and
-    ForIterableSatisfiesConstraint::satisfiesConstraintType(fe.getIterable(), _, exprPath, result) and
+    ForIterableSatisfiesType::satisfiesConstraintType(fe.getIterable(), _, exprPath, result) and
     exprPath.isCons(tp, path)
   |
     tp = getIntoIteratorItemTypeParameter()
@@ -3933,8 +3934,7 @@ final private class InvokedClosureExpr extends Expr {
   CallExpr getCall() { result = call }
 }
 
-private module InvokedClosureSatisfiesConstraintInput implements
-  SatisfiesConstraintInputSig<InvokedClosureExpr>
+private module InvokedClosureSatisfiesTypeInput implements SatisfiesTypeInputSig<InvokedClosureExpr>
 {
   predicate relevantConstraint(InvokedClosureExpr term, Type constraint) {
     exists(term) and
@@ -3942,12 +3942,12 @@ private module InvokedClosureSatisfiesConstraintInput implements
   }
 }
 
-private module InvokedClosureSatisfiesConstraint =
-  SatisfiesConstraint<InvokedClosureExpr, InvokedClosureSatisfiesConstraintInput>;
+private module InvokedClosureSatisfiesType =
+  SatisfiesType<InvokedClosureExpr, InvokedClosureSatisfiesTypeInput>;
 
 /** Gets the type of `ce` when viewed as an implementation of `FnOnce`. */
 private Type invokedClosureFnTypeAt(InvokedClosureExpr ce, TypePath path) {
-  InvokedClosureSatisfiesConstraint::satisfiesConstraintType(ce, _, path, result)
+  InvokedClosureSatisfiesType::satisfiesConstraintType(ce, _, path, result)
 }
 
 /**
diff --git a/rust/ql/lib/codeql/rust/internal/typeinference/TypeMention.qll b/rust/ql/lib/codeql/rust/internal/typeinference/TypeMention.qll
index dcb3fc0b0f49..9346f0e8c2a8 100644
--- a/rust/ql/lib/codeql/rust/internal/typeinference/TypeMention.qll
+++ b/rust/ql/lib/codeql/rust/internal/typeinference/TypeMention.qll
@@ -696,6 +696,16 @@ private module PreTypeMention = MkTypeMention<preGetAdditionalPathTypeAt/2>;
 
 class PreTypeMention = PreTypeMention::TypeMention;
 
+private class TraitOrTmTrait extends AstNode {
+  Type getTypeAt(TypePath path) {
+    pathTypeAsTraitAssoc(_, _, this, _, _) and
+    result = this.(PreTypeMention).getTypeAt(path)
+    or
+    result = TTrait(this) and
+    path.isEmpty()
+  }
+}
+
 /**
  * Holds if `path` accesses an associated type `alias` from `trait` on a
  * concrete type given by `tm`.
@@ -705,7 +715,7 @@ class PreTypeMention = PreTypeMention::TypeMention;
  * when `path` is of the form `Self::AssocType`.
  */
 private predicate pathConcreteTypeAssocType(
-  Path path, PreTypeMention tm, TraitItemNode trait, AstNode implOrTmTrait, TypeAlias alias
+  Path path, PreTypeMention tm, TraitItemNode trait, TraitOrTmTrait traitOrTmTrait, TypeAlias alias
 ) {
   exists(Path qualifier |
     qualifier = path.getQualifier() and
@@ -714,30 +724,32 @@ private predicate pathConcreteTypeAssocType(
     // path of the form `<Type as Trait>::AssocType`
     //                    ^^^ tm          ^^^^^^^^^ name
     exists(string name |
-      pathTypeAsTraitAssoc(path, tm, implOrTmTrait, trait, name) and
+      pathTypeAsTraitAssoc(path, tm, traitOrTmTrait, trait, name) and
       getTraitAssocType(trait, name) = alias
     )
     or
     // path of the form `Self::AssocType` within an `impl` block
     //                tm ^^^^  ^^^^^^^^^ name
-    implOrTmTrait =
-      any(ImplItemNode impl |
-        alias = resolvePath(path) and
-        qualifier = impl.getASelfPath() and
-        tm = impl.(Impl).getSelfTy() and
-        trait.getAnAssocItem() = alias
-      )
+    exists(ImplItemNode impl |
+      alias = resolvePath(path) and
+      qualifier = impl.getASelfPath() and
+      tm = impl.(Impl).getSelfTy() and
+      trait.getAnAssocItem() = alias and
+      traitOrTmTrait = trait
+    )
   )
 }
 
-private module PathSatisfiesConstraintInput implements SatisfiesConstraintInputSig<PreTypeMention> {
-  predicate relevantConstraint(PreTypeMention tm, Type constraint) {
-    pathConcreteTypeAssocType(_, tm, constraint.(TraitType).getTrait(), _, _)
+private module PathSatisfiesConstraintInput implements
+  SatisfiesConstraintInputSig<PreTypeMention, TraitOrTmTrait>
+{
+  predicate relevantConstraint(PreTypeMention tm, TraitOrTmTrait constraint) {
+    pathConcreteTypeAssocType(_, tm, _, constraint, _)
   }
 }
 
 private module PathSatisfiesConstraint =
-  SatisfiesConstraint<PreTypeMention, PathSatisfiesConstraintInput>;
+  SatisfiesConstraint<PreTypeMention, TraitOrTmTrait, PathSatisfiesConstraintInput>;
 
 /**
  * Gets the type of `path` at `typePath` when `path` accesses an associated type
@@ -745,26 +757,12 @@ private module PathSatisfiesConstraint =
  */
 private Type getPathConcreteAssocTypeAt(Path path, TypePath typePath) {
   exists(
-    PreTypeMention tm, ImplItemNode impl, TraitItemNode trait, TraitType t, AstNode implOrTmTrait,
+    PreTypeMention tm, ImplItemNode impl, TraitItemNode trait, TraitOrTmTrait traitOrTmTrait,
     TypeAlias alias, TypePath path0
   |
-    pathConcreteTypeAssocType(path, tm, trait, implOrTmTrait, alias) and
-    t = TTrait(trait) and
-    PathSatisfiesConstraint::satisfiesConstraintTypeThrough(tm, impl, t, path0, result) and
+    pathConcreteTypeAssocType(path, tm, trait, traitOrTmTrait, alias) and
+    PathSatisfiesConstraint::satisfiesConstraintTypeThrough(tm, impl, traitOrTmTrait, path0, result) and
     path0.isCons(TAssociatedTypeTypeParameter(trait, alias), typePath)
-  |
-    implOrTmTrait instanceof Impl
-    or
-    // When `path` is of the form `<Type as Trait>::AssocType` we need to check
-    // that `impl` is not more specific than the mentioned trait
-    implOrTmTrait =
-      any(PreTypeMention tmTrait |
-        not exists(TypePath path1, Type t1 |
-          t1 = impl.getTraitPath().(PreTypeMention).getTypeAt(path1) and
-          not t1 instanceof TypeParameter and
-          t1 != tmTrait.getTypeAt(path1)
-        )
-      )
   )
 }
 
diff --git a/rust/ql/test/library-tests/type-inference/overloading.rs b/rust/ql/test/library-tests/type-inference/overloading.rs
index 0bf6598c1d12..d76a28e9ad2d 100644
--- a/rust/ql/test/library-tests/type-inference/overloading.rs
+++ b/rust/ql/test/library-tests/type-inference/overloading.rs
@@ -400,3 +400,36 @@ mod from_default {
         x
     }
 }
+
+mod trait_bound_impl_overlap {
+    trait MyTrait<T> {
+        fn f(&self) -> T;
+    }
+
+    struct S<T>(T);
+
+    impl MyTrait<i32> for S<i32> {
+        fn f(&self) -> i32 {
+            0
+        }
+    }
+
+    impl MyTrait<i64> for S<i32> {
+        fn f(&self) -> i64 {
+            0
+        }
+    }
+
+    fn call_f<T1, T2: MyTrait<T1>>(x: T2) -> T1 {
+        x.f() // $ target=f
+    }
+
+    fn test() {
+        let x = S(0);
+        let y = call_f(x); // $ target=call_f type=y:i32
+        let z: i32 = y;
+
+        let x = S(0);
+        let y = call_f::<i32, _>(x); // $ target=call_f type=y:i32
+    }
+}
diff --git a/rust/ql/test/library-tests/type-inference/type-inference.expected b/rust/ql/test/library-tests/type-inference/type-inference.expected
index d3ec61e96034..952d41e59b15 100644
--- a/rust/ql/test/library-tests/type-inference/type-inference.expected
+++ b/rust/ql/test/library-tests/type-inference/type-inference.expected
@@ -4012,6 +4012,23 @@ inferCertainType
 | overloading.rs:397:10:397:10 | b |  | {EXTERNAL LOCATION} | bool |
 | overloading.rs:397:25:401:5 | { ... } |  | overloading.rs:372:5:372:14 | S1 |
 | overloading.rs:398:20:398:20 | b |  | {EXTERNAL LOCATION} | bool |
+| overloading.rs:406:14:406:18 | SelfParam |  | {EXTERNAL LOCATION} | & |
+| overloading.rs:406:14:406:18 | SelfParam | TRef | overloading.rs:405:5:407:5 | Self [trait MyTrait] |
+| overloading.rs:412:14:412:18 | SelfParam |  | {EXTERNAL LOCATION} | & |
+| overloading.rs:412:14:412:18 | SelfParam | TRef | overloading.rs:409:5:409:19 | S |
+| overloading.rs:412:14:412:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:412:28:414:9 | { ... } |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:418:14:418:18 | SelfParam |  | {EXTERNAL LOCATION} | & |
+| overloading.rs:418:14:418:18 | SelfParam | TRef | overloading.rs:409:5:409:19 | S |
+| overloading.rs:418:14:418:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:418:28:420:9 | { ... } |  | {EXTERNAL LOCATION} | i64 |
+| overloading.rs:423:36:423:36 | x |  | overloading.rs:423:19:423:33 | T2 |
+| overloading.rs:423:49:425:5 | { ... } |  | overloading.rs:423:15:423:16 | T1 |
+| overloading.rs:424:9:424:9 | x |  | overloading.rs:423:19:423:33 | T2 |
+| overloading.rs:427:15:434:5 | { ... } |  | {EXTERNAL LOCATION} | () |
+| overloading.rs:430:13:430:13 | z |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:433:13:433:13 | y |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:433:17:433:35 | call_f::<...>(...) |  | {EXTERNAL LOCATION} | i32 |
 | pattern_matching.rs:13:26:133:1 | { ... } |  | {EXTERNAL LOCATION} | Option |
 | pattern_matching.rs:13:26:133:1 | { ... } | T | {EXTERNAL LOCATION} | () |
 | pattern_matching.rs:15:5:18:5 | if ... {...} |  | {EXTERNAL LOCATION} | () |
@@ -12675,6 +12692,44 @@ inferType
 | overloading.rs:399:17:399:29 | ...::from(...) |  | overloading.rs:372:5:372:14 | S1 |
 | overloading.rs:399:28:399:28 | s |  | overloading.rs:364:5:365:13 | S |
 | overloading.rs:400:9:400:9 | x |  | overloading.rs:372:5:372:14 | S1 |
+| overloading.rs:406:14:406:18 | SelfParam |  | {EXTERNAL LOCATION} | & |
+| overloading.rs:406:14:406:18 | SelfParam | TRef | overloading.rs:405:5:407:5 | Self [trait MyTrait] |
+| overloading.rs:412:14:412:18 | SelfParam |  | {EXTERNAL LOCATION} | & |
+| overloading.rs:412:14:412:18 | SelfParam | TRef | overloading.rs:409:5:409:19 | S |
+| overloading.rs:412:14:412:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:412:28:414:9 | { ... } |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:413:13:413:13 | 0 |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:418:14:418:18 | SelfParam |  | {EXTERNAL LOCATION} | & |
+| overloading.rs:418:14:418:18 | SelfParam | TRef | overloading.rs:409:5:409:19 | S |
+| overloading.rs:418:14:418:18 | SelfParam | TRef.T | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:418:28:420:9 | { ... } |  | {EXTERNAL LOCATION} | i64 |
+| overloading.rs:419:13:419:13 | 0 |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:419:13:419:13 | 0 |  | {EXTERNAL LOCATION} | i64 |
+| overloading.rs:423:36:423:36 | x |  | overloading.rs:423:19:423:33 | T2 |
+| overloading.rs:423:49:425:5 | { ... } |  | overloading.rs:423:15:423:16 | T1 |
+| overloading.rs:424:9:424:9 | x |  | overloading.rs:423:19:423:33 | T2 |
+| overloading.rs:424:9:424:13 | x.f() |  | overloading.rs:423:15:423:16 | T1 |
+| overloading.rs:427:15:434:5 | { ... } |  | {EXTERNAL LOCATION} | () |
+| overloading.rs:428:13:428:13 | x |  | overloading.rs:409:5:409:19 | S |
+| overloading.rs:428:13:428:13 | x | T | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:428:17:428:20 | S(...) |  | overloading.rs:409:5:409:19 | S |
+| overloading.rs:428:17:428:20 | S(...) | T | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:428:19:428:19 | 0 |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:429:13:429:13 | y |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:429:17:429:25 | call_f(...) |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:429:24:429:24 | x |  | overloading.rs:409:5:409:19 | S |
+| overloading.rs:429:24:429:24 | x | T | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:430:13:430:13 | z |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:430:22:430:22 | y |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:432:13:432:13 | x |  | overloading.rs:409:5:409:19 | S |
+| overloading.rs:432:13:432:13 | x | T | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:432:17:432:20 | S(...) |  | overloading.rs:409:5:409:19 | S |
+| overloading.rs:432:17:432:20 | S(...) | T | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:432:19:432:19 | 0 |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:433:13:433:13 | y |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:433:17:433:35 | call_f::<...>(...) |  | {EXTERNAL LOCATION} | i32 |
+| overloading.rs:433:34:433:34 | x |  | overloading.rs:409:5:409:19 | S |
+| overloading.rs:433:34:433:34 | x | T | {EXTERNAL LOCATION} | i32 |
 | pattern_matching.rs:13:26:133:1 | { ... } |  | {EXTERNAL LOCATION} | Option |
 | pattern_matching.rs:13:26:133:1 | { ... } | T | {EXTERNAL LOCATION} | () |
 | pattern_matching.rs:14:9:14:13 | value |  | {EXTERNAL LOCATION} | Option |
diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll
index c33c49e7a168..b3820ac6d8b2 100644
--- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll
+++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll
@@ -336,7 +336,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
      * ```
      * the type parameter `T` has the constraint `IComparable<T>`.
      */
-    Type getATypeParameterConstraint(TypeParameter tp, TypePath path);
+    TypeMention getATypeParameterConstraint(TypeParameter tp);
 
     /**
      * Holds if
@@ -385,6 +385,35 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
     predicate conditionSatisfiesConstraint(
       TypeAbstraction abs, TypeMention condition, TypeMention constraint, boolean transitive
     );
+
+    /**
+     * Holds if the constraint belonging to `abs` with root type `constraint` is
+     * ambigous at `path`, meaning that there is _some_ other abstraction `abs2`
+     * with a structurally identical condition and root constraint type `constraint`,
+     * and where the constraints differ at `path`.
+     *
+     * Example:
+     *
+     * ```rust
+     * trait Trait<TTrait> { }
+     *
+     *    impl<T> Trait<i32> for Foo<T> { ... }
+     * //     ^^^ `abs`
+     * //         ^^^^^ `constraint`
+     * //                        ^^^^^^ `condition`
+     *
+     *    impl<T> Trait<i64> for Foo<T> { }
+     * //     ^^^ `abs2`
+     * //         ^^^^^ `constraint`
+     * //                        ^^^^^^ `condition2`
+     * ```
+     *
+     * In the above, `abs` and `abs2` have structurally identical conditions,
+     * `condition` and `condition2`, and they differ at the path `"TTrait"`.
+     */
+    predicate typeAbstractionHasAmbigousConstraintAt(
+      TypeAbstraction abs, Type constraint, TypePath path
+    );
   }
 
   module Make2<HasTypeTreeSig TypeMention, InputSig2<TypeMention> Input2> {
@@ -820,38 +849,43 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
 
     private import BaseTypes
 
-    signature module SatisfiesConstraintInputSig<HasTypeTreeSig HasTypeTree> {
+    /** Provides the input to `SatisfiesConstraint`. */
+    signature module SatisfiesConstraintInputSig<HasTypeTreeSig Term, HasTypeTreeSig Constraint> {
       /** Holds if it is relevant to know if `term` satisfies `constraint`. */
-      predicate relevantConstraint(HasTypeTree term, Type constraint);
+      predicate relevantConstraint(Term term, Constraint constraint);
     }
 
     module SatisfiesConstraint<
-      HasTypeTreeSig HasTypeTree, SatisfiesConstraintInputSig<HasTypeTree> Input>
+      HasTypeTreeSig Term, HasTypeTreeSig Constraint,
+      SatisfiesConstraintInputSig<Term, Constraint> Input>
     {
       private import Input
 
       pragma[nomagic]
-      private Type getTypeAt(HasTypeTree term, TypePath path) {
+      private Type getTypeAt(Term term, TypePath path) {
         relevantConstraint(term, _) and
         result = term.getTypeAt(path)
       }
 
       /** Holds if the type tree has the type `type` and should satisfy `constraint`. */
       pragma[nomagic]
-      private predicate hasTypeConstraint(HasTypeTree term, Type type, Type constraint) {
+      private predicate hasTypeConstraint(
+        Term term, Type type, Constraint constraint, Type constraintRoot
+      ) {
         type = getTypeAt(term, TypePath::nil()) and
-        relevantConstraint(term, constraint)
+        relevantConstraint(term, constraint) and
+        constraintRoot = constraint.getTypeAt(TypePath::nil())
       }
 
-      private module IsInstantiationOfInput implements
-        IsInstantiationOfInputSig<HasTypeTree, TypeMention>
+      private module TermIsInstantiationOfConditionInput implements
+        IsInstantiationOfInputSig<Term, TypeMention>
       {
-        predicate potentialInstantiationOf(HasTypeTree tt, TypeAbstraction abs, TypeMention cond) {
-          exists(Type constraint, Type type |
-            hasTypeConstraint(tt, type, constraint) and
-            rootTypesSatisfaction(type, constraint, abs, cond, _) and
+        predicate potentialInstantiationOf(Term tt, TypeAbstraction abs, TypeMention cond) {
+          exists(Constraint constraint, Type type, Type constraintRoot |
+            hasTypeConstraint(tt, type, constraint, constraintRoot) and
+            rootTypesSatisfaction(type, constraintRoot, abs, cond, _) and
             // We only need to check instantiations where there are multiple candidates.
-            multipleConstraintImplementations(type, constraint)
+            multipleConstraintImplementations(type, constraintRoot)
           )
         }
 
@@ -860,18 +894,18 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         }
       }
 
-      private module SatisfiesConstraintIsInstantiationOf =
-        IsInstantiationOf<HasTypeTree, TypeMention, IsInstantiationOfInput>;
+      private module TermIsInstantiationOfCondition =
+        IsInstantiationOf<Term, TypeMention, TermIsInstantiationOfConditionInput>;
 
       /**
        * Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
        */
       pragma[nomagic]
       private predicate hasConstraintMention(
-        HasTypeTree tt, TypeAbstraction abs, TypeMention condition, Type constraint,
-        TypeMention constraintMention
+        Term tt, TypeAbstraction abs, TypeMention condition, Constraint constraint,
+        Type constraintRoot, TypeMention constraintMention
       ) {
-        exists(Type type | hasTypeConstraint(tt, type, constraint) |
+        exists(Type type | hasTypeConstraint(tt, type, constraint, constraintRoot) |
           // TODO: Handle universal conditions properly, which means checking type parameter constraints
           // Also remember to update logic in `hasNotConstraintMention`
           //
@@ -880,23 +914,23 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
           // getTypeMentionRoot(condition) = abs.getATypeParameter() and
           // constraint = getTypeMentionRoot(constraintMention)
           // or
-          countConstraintImplementations(type, constraint) > 0 and
-          rootTypesSatisfaction(type, constraint, abs, condition, constraintMention) and
+          countConstraintImplementations(type, constraintRoot) > 0 and
+          rootTypesSatisfaction(type, constraintRoot, abs, condition, constraintMention) and
           // When there are multiple ways the type could implement the
           // constraint we need to find the right implementation, which is the
           // one where the type instantiates the precondition.
-          if multipleConstraintImplementations(type, constraint)
-          then SatisfiesConstraintIsInstantiationOf::isInstantiationOf(tt, abs, condition)
+          if multipleConstraintImplementations(type, constraintRoot)
+          then TermIsInstantiationOfCondition::isInstantiationOf(tt, abs, condition)
           else any()
         )
       }
 
       pragma[nomagic]
       private predicate isNotInstantiationOf(
-        HasTypeTree tt, TypeAbstraction abs, TypeMention condition, Type root
+        Term tt, TypeAbstraction abs, TypeMention condition, Type root
       ) {
         exists(TypePath path |
-          SatisfiesConstraintIsInstantiationOf::isNotInstantiationOf(tt, abs, condition, path) and
+          TermIsInstantiationOfCondition::isNotInstantiationOf(tt, abs, condition, path) and
           path.isCons(root.getATypeParameter(), _)
         )
       }
@@ -907,8 +941,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        * This predicate is an approximation of `not hasConstraintMention(tt, constraint)`.
        */
       pragma[nomagic]
-      private predicate hasNotConstraintMention(HasTypeTree tt, Type constraint) {
-        exists(Type type | hasTypeConstraint(tt, type, constraint) |
+      private predicate hasNotConstraintMention(Term tt, Constraint constraint, Type constraintRoot) {
+        exists(Type type | hasTypeConstraint(tt, type, constraint, constraintRoot) |
           // TODO: Handle universal conditions properly, which means taking type parameter constraints into account
           // (
           //   exists(countConstraintImplementations(type, constraint))
@@ -921,13 +955,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
           //   )
           // ) and
           (
-            countConstraintImplementations(type, constraint) = 0
+            countConstraintImplementations(type, constraintRoot) = 0
             or
-            not rootTypesSatisfaction(type, constraint, _, _, _)
+            not rootTypesSatisfaction(type, constraintRoot, _, _, _)
             or
-            multipleConstraintImplementations(type, constraint) and
+            multipleConstraintImplementations(type, constraintRoot) and
             forex(TypeAbstraction abs, TypeMention condition |
-              rootTypesSatisfaction(type, constraint, abs, condition, _)
+              rootTypesSatisfaction(type, constraintRoot, abs, condition, _)
             |
               isNotInstantiationOf(tt, abs, condition, type)
             )
@@ -937,21 +971,40 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
 
       pragma[nomagic]
       private predicate satisfiesConstraintTypeMention0(
-        HasTypeTree tt, Type constraint, TypeAbstraction abs, TypeMention sub, TypePath path, Type t
+        Term tt, Constraint constraint, Type constraintRoot, TypeMention constraintMention,
+        TypeAbstraction abs, TypeMention sub, TypePath path, Type t
+      ) {
+        hasConstraintMention(tt, abs, sub, constraint, constraintRoot, constraintMention) and
+        conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t)
+      }
+
+      pragma[nomagic]
+      private predicate satisfiesConstraintTypeMention1(
+        Term tt, Constraint constraint, Type constraintRoot, TypeAbstraction abs, TypeMention sub,
+        TypePath path, Type t
       ) {
         exists(TypeMention constraintMention |
-          hasConstraintMention(tt, abs, sub, constraint, constraintMention) and
-          conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path, t)
+          satisfiesConstraintTypeMention0(tt, constraint, constraintRoot, constraintMention, abs,
+            sub, path, t)
+        |
+          if typeAbstractionHasAmbigousConstraintAt(abs, constraintRoot, path)
+          then
+            not exists(TypePath path1, Type t1 |
+              conditionSatisfiesConstraintTypeAt(abs, sub, constraintMention, path1, t1) and
+              not t1 instanceof TypeParameter and
+              t1 != constraint.getTypeAt(path1)
+            )
+          else any()
         )
       }
 
       pragma[inline]
       private predicate satisfiesConstraintTypeMentionInline(
-        HasTypeTree tt, TypeAbstraction abs, Type constraint, TypePath path,
+        Term tt, Constraint constraint, Type constraintRoot, TypeAbstraction abs, TypePath path,
         TypePath pathToTypeParamInSub
       ) {
         exists(TypeMention sub, TypeParameter tp |
-          satisfiesConstraintTypeMention0(tt, constraint, abs, sub, path, tp) and
+          satisfiesConstraintTypeMention1(tt, constraint, constraintRoot, abs, sub, path, tp) and
           tp = abs.getATypeParameter() and
           sub.getTypeAt(pathToTypeParamInSub) = tp
         )
@@ -959,30 +1012,34 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
 
       pragma[nomagic]
       private predicate satisfiesConstraintTypeMention(
-        HasTypeTree tt, Type constraint, TypePath path, TypePath pathToTypeParamInSub
+        Term tt, Constraint constraint, TypePath path, TypePath pathToTypeParamInSub
       ) {
-        satisfiesConstraintTypeMentionInline(tt, _, constraint, path, pathToTypeParamInSub)
+        satisfiesConstraintTypeMentionInline(tt, constraint, _, _, path, pathToTypeParamInSub)
       }
 
       pragma[nomagic]
       private predicate satisfiesConstraintTypeMentionThrough(
-        HasTypeTree tt, TypeAbstraction abs, Type constraint, TypePath path,
+        Term tt, TypeAbstraction abs, Constraint constraint, Type constraintRoot, TypePath path,
         TypePath pathToTypeParamInSub
       ) {
-        satisfiesConstraintTypeMentionInline(tt, abs, constraint, path, pathToTypeParamInSub)
+        satisfiesConstraintTypeMentionInline(tt, constraint, constraintRoot, abs, path,
+          pathToTypeParamInSub)
       }
 
       pragma[inline]
       private predicate satisfiesConstraintTypeNonTypeParamInline(
-        HasTypeTree tt, TypeAbstraction abs, Type constraint, TypePath path, Type t
+        Term tt, TypeAbstraction abs, Constraint constraint, Type constraintRoot, TypePath path,
+        Type t
       ) {
-        satisfiesConstraintTypeMention0(tt, constraint, abs, _, path, t) and
+        satisfiesConstraintTypeMention1(tt, constraint, constraintRoot, abs, _, path, t) and
         not t = abs.getATypeParameter()
       }
 
       pragma[nomagic]
-      private predicate hasTypeConstraint(HasTypeTree term, Type constraint) {
-        hasTypeConstraint(term, constraint, constraint)
+      private predicate hasTypeConstraint(Term term, Constraint constraint) {
+        exists(Type constraintRoot |
+          hasTypeConstraint(term, constraintRoot, constraint, constraintRoot)
+        )
       }
 
       /**
@@ -990,8 +1047,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        * with the type `t` at `path`.
        */
       pragma[nomagic]
-      predicate satisfiesConstraintType(HasTypeTree tt, Type constraint, TypePath path, Type t) {
-        satisfiesConstraintTypeNonTypeParamInline(tt, _, constraint, path, t)
+      predicate satisfiesConstraintType(Term tt, Constraint constraint, TypePath path, Type t) {
+        satisfiesConstraintTypeNonTypeParamInline(tt, _, constraint, _, path, t)
         or
         exists(TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix |
           satisfiesConstraintTypeMention(tt, constraint, prefix0, pathToTypeParamInSub) and
@@ -1009,12 +1066,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        */
       pragma[nomagic]
       predicate satisfiesConstraintTypeThrough(
-        HasTypeTree tt, TypeAbstraction abs, Type constraint, TypePath path, Type t
+        Term tt, TypeAbstraction abs, Constraint constraint, TypePath path, Type t
       ) {
-        satisfiesConstraintTypeNonTypeParamInline(tt, abs, constraint, path, t)
+        satisfiesConstraintTypeNonTypeParamInline(tt, abs, constraint, _, path, t)
         or
         exists(TypePath prefix0, TypePath pathToTypeParamInSub, TypePath suffix |
-          satisfiesConstraintTypeMentionThrough(tt, abs, constraint, prefix0, pathToTypeParamInSub) and
+          satisfiesConstraintTypeMentionThrough(tt, abs, constraint, _, prefix0,
+            pathToTypeParamInSub) and
           getTypeAt(tt, pathToTypeParamInSub.appendInverse(suffix)) = t and
           path = prefix0.append(suffix)
         )
@@ -1035,15 +1093,47 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        * `dissatisfiesConstraint` will hold.
        */
       pragma[nomagic]
-      predicate dissatisfiesConstraint(HasTypeTree tt, Type constraint) {
-        hasNotConstraintMention(tt, constraint) and
-        exists(Type t |
-          hasTypeConstraint(tt, t, constraint) and
-          t != constraint
+      predicate dissatisfiesConstraint(Term tt, Constraint constraint) {
+        hasNotConstraintMention(tt, constraint, _) and
+        exists(Type t, Type constraintRoot |
+          hasTypeConstraint(tt, t, constraint, constraintRoot) and // todo
+          t != constraintRoot
         )
       }
     }
 
+    /** Provides the input to `SatisfiesType`. */
+    signature module SatisfiesTypeInputSig<HasTypeTreeSig Term> {
+      /** Holds if it is relevant to know if `term` satisfies `constraint`. */
+      predicate relevantConstraint(Term term, Type constraint);
+    }
+
+    /**
+     * A helper module wrapping `SatisfiesConstraint` where the constraint is simply a type.
+     */
+    module SatisfiesType<HasTypeTreeSig Term, SatisfiesTypeInputSig<Term> Input> {
+      private import Input
+
+      final private class TypeFinal = Type;
+
+      private class TypeAsTypeTree extends TypeFinal {
+        Type getTypeAt(TypePath path) {
+          result = this and
+          path.isEmpty()
+        }
+      }
+
+      private module SatisfiesConstraintInput implements
+        SatisfiesConstraintInputSig<Term, TypeAsTypeTree>
+      {
+        predicate relevantConstraint(Term term, TypeAsTypeTree constraint) {
+          Input::relevantConstraint(term, constraint)
+        }
+      }
+
+      import SatisfiesConstraint<Term, TypeAsTypeTree, SatisfiesConstraintInput>
+    }
+
     /** Provides the input to `MatchingWithEnvironment`. */
     signature module MatchingWithEnvironmentInputSig {
       /**
@@ -1266,7 +1356,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
       private module AccessConstraint {
         predicate relevantAccessConstraint(
           Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath path,
-          Type constraint
+          TypeMention constraint
         ) {
           target = a.getTarget(e) and
           typeParameterConstraintHasTypeParameter(target, apos, path, constraint, _, _)
@@ -1294,7 +1384,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
           }
 
           /** Gets the constraint that this relevant access should satisfy. */
-          Type getConstraint(Declaration target) {
+          TypeMention getConstraint(Declaration target) {
             relevantAccessConstraint(a, e, target, apos, path, result)
           }
 
@@ -1306,20 +1396,20 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         }
 
         private module SatisfiesConstraintInput implements
-          SatisfiesConstraintInputSig<RelevantAccess>
+          SatisfiesConstraintInputSig<RelevantAccess, TypeMention>
         {
-          predicate relevantConstraint(RelevantAccess at, Type constraint) {
+          predicate relevantConstraint(RelevantAccess at, TypeMention constraint) {
             constraint = at.getConstraint(_)
           }
         }
 
         predicate satisfiesConstraintType(
           Access a, AccessEnvironment e, Declaration target, AccessPosition apos, TypePath prefix,
-          Type constraint, TypePath path, Type t
+          TypeMention constraint, TypePath path, Type t
         ) {
           exists(RelevantAccess ra |
             ra = MkRelevantAccess(a, apos, e, prefix) and
-            SatisfiesConstraint<RelevantAccess, SatisfiesConstraintInput>::satisfiesConstraintType(ra,
+            SatisfiesConstraint<RelevantAccess, TypeMention, SatisfiesConstraintInput>::satisfiesConstraintType(ra,
               constraint, path, t) and
             constraint = ra.getConstraint(target)
           )
@@ -1429,17 +1519,17 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
        */
       pragma[nomagic]
       private predicate typeParameterConstraintHasTypeParameter(
-        Declaration target, AccessPosition apos, TypePath pathToConstrained, Type constraint,
+        Declaration target, AccessPosition apos, TypePath pathToConstrained, TypeMention constraint,
         TypePath pathToTp, TypeParameter tp
       ) {
         exists(DeclarationPosition dpos, TypeParameter constrainedTp |
           accessDeclarationPositionMatch(apos, dpos) and
           constrainedTp = target.getTypeParameter(_) and
           tp = target.getTypeParameter(_) and
-          tp = getATypeParameterConstraint(constrainedTp, pathToTp) and
+          tp = constraint.getTypeAt(pathToTp) and
           constrainedTp != tp and
           constrainedTp = target.getDeclaredType(dpos, pathToConstrained) and
-          constraint = getATypeParameterConstraint(constrainedTp, TypePath::nil())
+          constraint = getATypeParameterConstraint(constrainedTp)
         )
       }
 
@@ -1448,7 +1538,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
         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 |
+        exists(TypeMention constraint, AccessPosition apos, TypePath pathToTp, TypePath pathToTp2 |
           typeParameterConstraintHasTypeParameter(target, apos, pathToTp2, constraint, pathToTp, tp) and
           AccessConstraint::satisfiesConstraintType(a, e, target, apos, pathToTp2, constraint,
             pathToTp.appendInverse(path), t)