diff --git a/c/cert/src/rules/DCL40-C/IncompatibleFunctionDeclarations.ql b/c/cert/src/rules/DCL40-C/IncompatibleFunctionDeclarations.ql
index 95ef0fd68..8cab442e5 100644
--- a/c/cert/src/rules/DCL40-C/IncompatibleFunctionDeclarations.ql
+++ b/c/cert/src/rules/DCL40-C/IncompatibleFunctionDeclarations.ql
@@ -19,6 +19,12 @@ import codingstandards.c.cert
 import codingstandards.cpp.types.Compatible
 import ExternalIdentifiers
 
+predicate interestedInFunctions(FunctionDeclarationEntry f1, FunctionDeclarationEntry f2) {
+  not f1 = f2 and
+  f1.getDeclaration() = f2.getDeclaration() and
+  f1.getName() = f2.getName()
+}
+
 from ExternalIdentifiers d, FunctionDeclarationEntry f1, FunctionDeclarationEntry f2
 where
   not isExcluded(f1, Declarations2Package::incompatibleFunctionDeclarationsQuery()) and
@@ -29,10 +35,12 @@ where
   f1.getName() = f2.getName() and
   (
     //return type check
-    not FunctionDeclarationTypeEquivalence<TypesCompatibleConfig>::equalReturnTypes(f1, f2)
+    not FunctionDeclarationTypeEquivalence<TypesCompatibleConfig, interestedInFunctions/2>::equalReturnTypes(f1,
+      f2)
     or
     //parameter type check
-    not FunctionDeclarationTypeEquivalence<TypesCompatibleConfig>::equalParameterTypes(f1, f2)
+    not FunctionDeclarationTypeEquivalence<TypesCompatibleConfig, interestedInFunctions/2>::equalParameterTypes(f1,
+      f2)
   ) and
   // Apply ordering on start line, trying to avoid the optimiser applying this join too early
   // in the pipeline
diff --git a/c/misra/src/rules/RULE-23-5/DangerousDefaultSelectionForPointerInGeneric.ql b/c/misra/src/rules/RULE-23-5/DangerousDefaultSelectionForPointerInGeneric.ql
index a009ba1b2..f2961e263 100644
--- a/c/misra/src/rules/RULE-23-5/DangerousDefaultSelectionForPointerInGeneric.ql
+++ b/c/misra/src/rules/RULE-23-5/DangerousDefaultSelectionForPointerInGeneric.ql
@@ -20,18 +20,14 @@ import codingstandards.cpp.types.LvalueConversion
 import codingstandards.cpp.types.SimpleAssignment
 
 predicate typesCompatible(Type t1, Type t2) {
-  TypeEquivalence<TypesCompatibleConfig, TypeFromGeneric>::equalTypes(t1, t2)
+  TypeEquivalence<TypesCompatibleConfig, relevantTypes/2>::equalTypes(t1, t2)
 }
 
-class TypeFromGeneric extends Type {
-  TypeFromGeneric() {
-    exists(C11GenericExpr g |
-      (
-        this = g.getAssociationType(_) or
-        this = g.getControllingExpr().getFullyConverted().getType()
-      )
-    )
-  }
+predicate relevantTypes(Type a, Type b) {
+  exists(C11GenericExpr g |
+    a = g.getAnAssociationType() and
+    b = getLvalueConverted(g.getControllingExpr().getFullyConverted().getType())
+  )
 }
 
 predicate missesOnPointerConversion(Type provided, Type expected) {
@@ -40,11 +36,11 @@ predicate missesOnPointerConversion(Type provided, Type expected) {
   // But 6.5.16.1 simple assignment constraints would have been satisfied:
   (
     // Check as if the controlling expr is assigned to the expected type:
-    SimpleAssignment<TypeFromGeneric>::satisfiesSimplePointerAssignment(expected, provided)
+    SimpleAssignment<relevantTypes/2>::satisfiesSimplePointerAssignment(expected, provided)
     or
     // Since developers typically rely on the compiler to catch const/non-const assignment
     // errors, don't assume a const-to-non-const generic selection miss was intentional.
-    SimpleAssignment<TypeFromGeneric>::satisfiesSimplePointerAssignment(provided, expected)
+    SimpleAssignment<relevantTypes/2>::satisfiesSimplePointerAssignment(provided, expected)
   )
 }
 
diff --git a/c/misra/src/rules/RULE-8-3/DeclarationsOfAFunctionSameNameAndType.ql b/c/misra/src/rules/RULE-8-3/DeclarationsOfAFunctionSameNameAndType.ql
index 2de2e4fd0..fe0ae81ab 100644
--- a/c/misra/src/rules/RULE-8-3/DeclarationsOfAFunctionSameNameAndType.ql
+++ b/c/misra/src/rules/RULE-8-3/DeclarationsOfAFunctionSameNameAndType.ql
@@ -16,6 +16,11 @@ import cpp
 import codingstandards.c.misra
 import codingstandards.cpp.types.Compatible
 
+predicate interestedInFunctions(FunctionDeclarationEntry f1, FunctionDeclarationEntry f2) {
+  not f1 = f2 and
+  f1.getDeclaration() = f2.getDeclaration()
+}
+
 from FunctionDeclarationEntry f1, FunctionDeclarationEntry f2, string case, string pluralDo
 where
   not isExcluded(f1, Declarations4Package::declarationsOfAFunctionSameNameAndTypeQuery()) and
@@ -24,12 +29,14 @@ where
   f1.getDeclaration() = f2.getDeclaration() and
   //return type check
   (
-    not FunctionDeclarationTypeEquivalence<TypeNamesMatchConfig>::equalReturnTypes(f1, f2) and
+    not FunctionDeclarationTypeEquivalence<TypeNamesMatchConfig, interestedInFunctions/2>::equalReturnTypes(f1,
+      f2) and
     case = "return type" and
     pluralDo = "does"
     or
     //parameter type check
-    not FunctionDeclarationTypeEquivalence<TypeNamesMatchConfig>::equalParameterTypes(f1, f2) and
+    not FunctionDeclarationTypeEquivalence<TypeNamesMatchConfig, interestedInFunctions/2>::equalParameterTypes(f1,
+      f2) and
     case = "parameter types" and
     pluralDo = "do"
     or
diff --git a/c/misra/src/rules/RULE-8-3/DeclarationsOfAnObjectSameNameAndType.ql b/c/misra/src/rules/RULE-8-3/DeclarationsOfAnObjectSameNameAndType.ql
index 12ff583b6..36a84b3b9 100644
--- a/c/misra/src/rules/RULE-8-3/DeclarationsOfAnObjectSameNameAndType.ql
+++ b/c/misra/src/rules/RULE-8-3/DeclarationsOfAnObjectSameNameAndType.ql
@@ -16,15 +16,6 @@ import cpp
 import codingstandards.c.misra
 import codingstandards.cpp.types.Compatible
 
-class RelevantType extends Type {
-  RelevantType() {
-    exists(VariableDeclarationEntry decl |
-      (relevantPair(decl, _) or relevantPair(_, decl)) and
-      decl.getType() = this
-    )
-  }
-}
-
 predicate relevantPair(VariableDeclarationEntry decl1, VariableDeclarationEntry decl2) {
   not decl1 = decl2 and
   not decl1.getVariable().getDeclaringType().isAnonymous() and
@@ -43,12 +34,20 @@ predicate relevantPair(VariableDeclarationEntry decl1, VariableDeclarationEntry
   )
 }
 
+predicate relevantTypes(Type a, Type b) {
+  exists(VariableDeclarationEntry varA, VariableDeclarationEntry varB |
+    a = varA.getType() and
+    b = varB.getType() and
+    relevantPair(varA, varB)
+  )
+}
+
 from VariableDeclarationEntry decl1, VariableDeclarationEntry decl2
 where
   not isExcluded(decl1, Declarations4Package::declarationsOfAnObjectSameNameAndTypeQuery()) and
   not isExcluded(decl2, Declarations4Package::declarationsOfAnObjectSameNameAndTypeQuery()) and
   relevantPair(decl1, decl2) and
-  not TypeEquivalence<TypeNamesMatchConfig, RelevantType>::equalTypes(decl1.getType(),
+  not TypeEquivalence<TypeNamesMatchConfig, relevantTypes/2>::equalTypes(decl1.getType(),
     decl2.getType())
 select decl1,
   "The object $@ of type " + decl1.getType().toString() +
diff --git a/c/misra/src/rules/RULE-8-4/CompatibleDeclarationFunctionDefined.ql b/c/misra/src/rules/RULE-8-4/CompatibleDeclarationFunctionDefined.ql
index 98876ad1b..73abc1e04 100644
--- a/c/misra/src/rules/RULE-8-4/CompatibleDeclarationFunctionDefined.ql
+++ b/c/misra/src/rules/RULE-8-4/CompatibleDeclarationFunctionDefined.ql
@@ -19,6 +19,17 @@ import codingstandards.c.misra
 import codingstandards.cpp.Identifiers
 import codingstandards.cpp.types.Compatible
 
+predicate interestedInFunctions(FunctionDeclarationEntry f1, FunctionDeclarationEntry f2) {
+  f1.getDeclaration() instanceof ExternalIdentifiers and
+  f1.isDefinition() and
+  f1.getDeclaration() = f2.getDeclaration() and
+  // This condition should always hold, but removing it affects join order performance.
+  f1.getName() = f2.getName() and
+  not f2.isDefinition() and
+  not f1.isFromTemplateInstantiation(_) and
+  not f2.isFromTemplateInstantiation(_)
+}
+
 from FunctionDeclarationEntry f1
 where
   not isExcluded(f1, Declarations4Package::compatibleDeclarationFunctionDefinedQuery()) and
@@ -38,10 +49,12 @@ where
       f2.getDeclaration() = f1.getDeclaration() and
       (
         //return types differ
-        not FunctionDeclarationTypeEquivalence<TypesCompatibleConfig>::equalReturnTypes(f1, f2)
+        not FunctionDeclarationTypeEquivalence<TypesCompatibleConfig, interestedInFunctions/2>::equalReturnTypes(f1,
+          f2)
         or
         //parameter types differ
-        not FunctionDeclarationTypeEquivalence<TypesCompatibleConfig>::equalParameterTypes(f1, f2)
+        not FunctionDeclarationTypeEquivalence<TypesCompatibleConfig, interestedInFunctions/2>::equalParameterTypes(f1,
+          f2)
         or
         //parameter names differ
         parameterNamesUnmatched(f1, f2)
diff --git a/c/misra/src/rules/RULE-8-4/CompatibleDeclarationObjectDefined.ql b/c/misra/src/rules/RULE-8-4/CompatibleDeclarationObjectDefined.ql
index 613ce5680..bed30d673 100644
--- a/c/misra/src/rules/RULE-8-4/CompatibleDeclarationObjectDefined.ql
+++ b/c/misra/src/rules/RULE-8-4/CompatibleDeclarationObjectDefined.ql
@@ -19,13 +19,13 @@ import codingstandards.c.misra
 import codingstandards.cpp.Identifiers
 import codingstandards.cpp.types.Compatible
 
-class RelevantType extends Type {
-  RelevantType() {
-    exists(VariableDeclarationEntry decl |
-      count(VariableDeclarationEntry others | others.getDeclaration() = decl.getDeclaration()) > 1 and
-      decl.getType() = this
-    )
-  }
+predicate relevantTypes(Type a, Type b) {
+  exists(VariableDeclarationEntry varA, VariableDeclarationEntry varB |
+    not varA = varB and
+    varA.getDeclaration() = varB.getDeclaration() and
+    a = varA.getType() and
+    b = varB.getType()
+  )
 }
 
 from VariableDeclarationEntry decl1
@@ -37,7 +37,7 @@ where
   not exists(VariableDeclarationEntry decl2 |
     not decl2.isDefinition() and
     decl1.getDeclaration() = decl2.getDeclaration() and
-    TypeEquivalence<TypesCompatibleConfig, RelevantType>::equalTypes(decl1.getType(),
+    TypeEquivalence<TypesCompatibleConfig, relevantTypes/2>::equalTypes(decl1.getType(),
       decl2.getType())
   )
 select decl1, "No separate compatible declaration found for this definition."
diff --git a/change_notes/2025-04-25-improve-type-comparison-performance.md b/change_notes/2025-04-25-improve-type-comparison-performance.md
new file mode 100644
index 000000000..39c462fbf
--- /dev/null
+++ b/change_notes/2025-04-25-improve-type-comparison-performance.md
@@ -0,0 +1,6 @@
+ - `RULE-8-3`, `RULE-8-4`, `DCL40-C`, `RULE-23-5`: `DeclarationsOfAFunctionSameNameAndType.ql`, `DeclarationsOfAnObjectSameNameAndType.ql`, `CompatibleDeclarationOfFunctionDefined.ql`, `CompatibleDeclarationObjectDefined.ql`, `IncompatibleFunctionDeclarations.ql`, `DangerousDefaultSelectionForPointerInGeneric.ql`:
+   - Added pragmas to alter join order on function parameter equivalence (names and types).
+   - Refactored expression which the optimizer was confused by, and compiled into a cartesian product. 
+   - Altered the module `Compatible.qll` to compute equality in two stages. Firstly, all pairs of possible type comparisons (including recursive comparisons) are found, then those pairwise comparisons are evaluated in a second stage. This greatly reduces the number of comparisons and greatly improves performance.
+ - `RULE-23-5`: `DangerousDefaultSelectionForPointerInGeneric.ql`:
+   - Altered the module `SimpleAssignment.qll` in accordance with the changes to `Compatible.qll`.
\ No newline at end of file
diff --git a/cpp/common/src/codingstandards/cpp/types/Compatible.qll b/cpp/common/src/codingstandards/cpp/types/Compatible.qll
index d6f65126e..c4ee9a22e 100644
--- a/cpp/common/src/codingstandards/cpp/types/Compatible.qll
+++ b/cpp/common/src/codingstandards/cpp/types/Compatible.qll
@@ -25,7 +25,7 @@ class VariableType extends Type {
 }
 
 predicate parameterNamesUnmatched(FunctionDeclarationEntry f1, FunctionDeclarationEntry f2) {
-  f1.getDeclaration() = f2.getDeclaration() and
+  pragma[only_bind_into](f1).getDeclaration() = pragma[only_bind_into](f2).getDeclaration() and
   exists(string p1Name, string p2Name, int i |
     p1Name = f1.getParameterDeclarationEntry(i).getName() and
     p2Name = f2.getParameterDeclarationEntry(i).getName()
@@ -53,8 +53,11 @@ module TypesCompatibleConfig implements TypeEquivalenceSig {
     or
     // Enum types are compatible with one of char, int, or signed int, but the implementation
     // decides.
-    [t1, t2] instanceof Enum and
-    ([t1, t2] instanceof CharType or [t1, t2] instanceof IntType)
+    t1 instanceof Enum and
+    (t2 instanceof CharType or t2 instanceof IntType)
+    or
+    t2 instanceof Enum and
+    (t1 instanceof CharType or t1 instanceof IntType)
   }
 
   bindingset[t1, t2]
@@ -69,6 +72,7 @@ module TypesCompatibleConfig implements TypeEquivalenceSig {
 /**
  * Utilize QlBuiltins::InternSets to efficiently compare the sets of specifiers on two types.
  */
+bindingset[t1, t2]
 private predicate specifiersMatchExactly(Type t1, Type t2) {
   t1 = t2
   or
@@ -204,79 +208,214 @@ signature module TypeEquivalenceSig {
 module DefaultEquivalence implements TypeEquivalenceSig { }
 
 /**
- * A signature class used to restrict the set of types considered by `TypeEquivalence`, for
+ * A signature predicate used to restrict the set of types considered by `TypeEquivalence`, for
  * performance reasons.
  */
-signature class TypeSubset extends Type;
+signature predicate interestedInEquality(Type a, Type b);
 
 /**
  * A module to check the equivalence of two types, as defined by the provided `TypeEquivalenceSig`.
  *
- * For performance reasons, this module is designed to be used with a `TypeSubset` that restricts
- * the set of considered types. All types reachable (in the type graph) from a type in the subset
- * will be considered. (See `RelevantType`.)
+ * For performance reasons, this module is designed to be used with a predicate
+ * `interestedInEquality` that restricts the set of considered pairwise comparisons.
  *
  * To use this module, define a `TypeEquivalenceSig` module and implement a subset of `Type` that
  * selects the relevant root types to be considered. Then use the predicate `equalTypes(a, b)`.
+ * Note that `equalTypes(a, b)` only holds if `interestedIn(a, b)` holds. A type is always
+ * considered to be equal to itself, and this module does not support configurations that declare
+ * otherwise. Additionally, `interestedIn(a, b)` implies `interestedIn(b, a)`.
+ *
+ * This module will recursively select pairs of types to be compared. For instance, if
+ * `interestedInEquality(a, b)` holds, then types `a` and `b` will be compared. If
+ * `Config::equalPointerTypes(a, b, true)` holds, then the pointed-to types of `a` and `b` will be
+ * compared. However, if `Config::equalPointerTypes(a, b, false)` holds, then `a` and `b` will be
+ * compared, but their pointed-to types will not. Similarly, inner types will not be compared if
+ * `Config::overrideTypeComparison(a, b, _)` holds. For detail, see the module predicates
+ * `shouldRecurseOn` and `interestedInNestedTypes`.
  */
-module TypeEquivalence<TypeEquivalenceSig Config, TypeSubset T> {
+module TypeEquivalence<TypeEquivalenceSig Config, interestedInEquality/2 interestedIn> {
   /**
-   * Check whether two types are equivalent, as defined by the `TypeEquivalenceSig` module.
+   * Performance-related predicate that holds for a pair of types `(a, b)` such that
+   * `interestedIn(a, b)` holds, or there exists a pair of types `(c, d)` such that
+   * `interestedIn(c, d)` holds, and computing `equalTypes(a, b)` requires computing
+   * `equalTypes(c, d)`.
+   *
+   * The goal of this predicate is to force top down rather than bottom up evaluation of type
+   * equivalence. That is to say, if we compare array types `int[]` and `int[]`, we to compare that
+   * both types are arrays first, and then compare that their base types are equal. Naively, CodeQL
+   * is liable to compute this kind of recursive equality in a bottom up fashion, where the cross
+   * product of all types is considered in computing `equalTypes(a, b)`.
+   *
+   * This interoperates with the predicate `shouldRecurseOn` to find types that will be compared,
+   * along with the inner types of those types that will be compared. See `shouldRecurseOn` for
+   * cases where this algorithm will or will not recurse. We still need to know which types are
+   * compared, even if we do not recurse on them, in order to properly constrain `equalTypes(x, y)`
+   * to hold for types such as leaf types, where we do not recurse during comparison.
+   *
+   * At each stage of recursion, we specify `pragma[only_bind_into]` to ensure that the
+   * prior `shouldRecurseOn` results are considered first in the pipeline.
    */
-  predicate equalTypes(RelevantType t1, RelevantType t2) {
-    if Config::overrideTypeComparison(t1, t2, _)
-    then Config::overrideTypeComparison(t1, t2, true)
-    else
-      if t1 instanceof TypedefType and Config::resolveTypedefs()
-      then equalTypes(t1.(TypedefType).getBaseType(), t2)
-      else
-        if t2 instanceof TypedefType and Config::resolveTypedefs()
-        then equalTypes(t1, t2.(TypedefType).getBaseType())
-        else (
-          not t1 instanceof DerivedType and
-          not t2 instanceof DerivedType and
-          not t1 instanceof TypedefType and
-          not t2 instanceof TypedefType and
-          LeafEquiv::getEquivalenceClass(t1) = LeafEquiv::getEquivalenceClass(t2)
-          or
-          equalDerivedTypes(t1, t2)
-          or
-          equalTypedefTypes(t1, t2)
-          or
-          equalFunctionTypes(t1, t2)
+  private predicate interestedInNestedTypes(Type t1, Type t2) {
+    // Base case: config specifies that these root types will be compared.
+    interestedInUnordered(t1, t2)
+    or
+    // If derived types are compared, their base types must be compared.
+    exists(DerivedType t1Derived, DerivedType t2Derived |
+      not t1Derived instanceof SpecifiedType and
+      not t2Derived instanceof SpecifiedType and
+      shouldRecurseOn(pragma[only_bind_into](t1Derived), pragma[only_bind_into](t2Derived)) and
+      t1 = t1Derived.getBaseType() and
+      t2 = t2Derived.getBaseType()
+    )
+    or
+    // If specified types are compared, their unspecified types must be compared.
+    exists(SpecifiedType t1Spec, SpecifiedType t2Spec |
+      shouldRecurseOn(pragma[only_bind_into](t1Spec), pragma[only_bind_into](t2Spec)) and
+      (
+        t1 = unspecify(t1Spec) and
+        t2 = unspecify(t2Spec)
+      )
+    )
+    or
+    // If function types are compared, their return types and parameter types must be compared.
+    exists(FunctionType t1Func, FunctionType t2Func |
+      shouldRecurseOn(pragma[only_bind_into](t1Func), pragma[only_bind_into](t2Func)) and
+      (
+        t1 = t1Func.getReturnType() and
+        t2 = t2Func.getReturnType()
+        or
+        exists(int i |
+          t1 = t1Func.getParameterType(pragma[only_bind_out](i)) and
+          t2 = t2Func.getParameterType(i)
         )
+      )
+    )
+    or
+    // If the config says to resolve typedefs, and a typedef type is compared to a non-typedef
+    // type, then the non-typedef type must be compared to the base type of the typedef.
+    Config::resolveTypedefs() and
+    exists(TypedefType tdtype |
+      tdtype.getBaseType() = t1 and
+      shouldRecurseOn(pragma[only_bind_into](tdtype), t2)
+      or
+      tdtype.getBaseType() = t2 and
+      shouldRecurseOn(t1, pragma[only_bind_into](tdtype))
+    )
+    or
+    // If two typedef types are compared, then their base types must be compared.
+    exists(TypedefType t1Typedef, TypedefType t2Typedef |
+      shouldRecurseOn(pragma[only_bind_into](t1Typedef), pragma[only_bind_into](t2Typedef)) and
+      (
+        t1 = t1Typedef.getBaseType() and
+        t2 = t2Typedef.getBaseType()
+      )
+    )
   }
 
   /**
-   * A type that is either part of the type subset, or that is reachable from a type in the subset.
+   * Performance related predicate to force top down rather than bottom up evaluation of type
+   * equivalence.
+   *
+   * This predicate is used to determine whether we should recurse on a type. It is used in
+   * conjunction with the `interestedInNestedTypes` predicate to only recurse on types that are
+   * being compared.
+   *
+   * We don't recurse on identical types, as they are already equal. We also don't recurse on
+   * types that are overriden by `Config::overrideTypeComparison`, as that predicate determines
+   * their equalivance.
+   *
+   * For the other types, we have a set of predicates such as `Config::equalPointerTypes` that
+   * holds for `(x, y, true)` if the types `x` and `y` should be considered equivalent when the
+   * pointed-to types of `x` and `y` are equivalent. If the predicate does not hold, or holds for
+   * `(x, y, false)`, then we do not recurse on the types.
+   *
+   * We do not recurse on leaf types.
    */
-  private class RelevantType instanceof Type {
-    RelevantType() { exists(T t | typeGraph*(t, this)) }
-
-    string toString() { result = this.(Type).toString() }
-  }
-
-  private class RelevantDerivedType extends RelevantType instanceof DerivedType {
-    RelevantType getBaseType() { result = this.(DerivedType).getBaseType() }
+  private predicate shouldRecurseOn(Type t1, Type t2) {
+    // We only recurse on types we are comparing.
+    interestedInNestedTypes(pragma[only_bind_into](t1), pragma[only_bind_into](t2)) and
+    // We don't recurse on identical types, as they are already equal.
+    not t1 = t2 and
+    // We don't recurse on overriden comparisons
+    not Config::overrideTypeComparison(t1, t2, _) and
+    (
+      // These pointer types are equal if their base types are equal: recurse.
+      Config::equalPointerTypes(t1, t2, true)
+      or
+      // These array types are equal if their base types are equal: recurse.
+      Config::equalArrayTypes(t1, t2, true)
+      or
+      // These reference types are equal if their base types are equal: recurse.
+      Config::equalReferenceTypes(t1, t2, true)
+      or
+      // These routine types are equal if their return and parameter types are equal: recurse.
+      Config::equalRoutineTypes(t1, t2, true, true)
+      or
+      // These function pointer-ish types are equal if their return and parameter types are equal: recurse.
+      Config::equalFunctionPointerIshTypes(t1, t2, true, true)
+      or
+      // These typedef types are equal if their base types are equal: recurse.
+      Config::equalTypedefTypes(t1, t2, true)
+      or
+      // These specified types are equal if their unspecified types are equal: recurse.
+      Config::equalSpecifiedTypes(t1, t2, true)
+      or
+      // We resolve typedefs, and one of these types is a typedef type: recurse.
+      Config::resolveTypedefs() and
+      (
+        t1 instanceof TypedefType
+        or
+        t2 instanceof TypedefType
+      )
+    )
   }
 
-  private class RelevantFunctionType extends RelevantType instanceof FunctionType {
-    RelevantType getReturnType() { result = this.(FunctionType).getReturnType() }
-
-    RelevantType getParameterType(int i) { result = this.(FunctionType).getParameterType(i) }
+  /**
+   * Check whether two types are equivalent, as defined by the `TypeEquivalenceSig` module.
+   *
+   * This only holds if the specified predicate `interestedIn` holds for the types, or
+   * `interestedInNestedTypes` holds for the types, and holds if `t1` and `t2` are identical,
+   * regardless of how `TypeEquivalenceSig` is defined.
+   */
+  predicate equalTypes(Type t1, Type t2) {
+    interestedInNestedTypes(pragma[only_bind_into](t1), pragma[only_bind_into](t2)) and
+    (
+      t1 = t2
+      or
+      not t1 = t2 and
+      if Config::overrideTypeComparison(t1, t2, _)
+      then Config::overrideTypeComparison(t1, t2, true)
+      else (
+        equalLeafRelation(t1, t2)
+        or
+        equalDerivedTypes(t1, t2)
+        or
+        equalFunctionTypes(t1, t2)
+        or
+        Config::resolveTypedefs() and
+        (
+          equalTypes(t1.(TypedefType).getBaseType(), t2)
+          or
+          equalTypes(t1, t2.(TypedefType).getBaseType())
+        )
+        or
+        not Config::resolveTypedefs() and
+        equalTypedefTypes(t1, t2)
+      )
+    )
   }
 
-  private class RelevantTypedefType extends RelevantType instanceof TypedefType {
-    RelevantType getBaseType() { result = this.(TypedefType).getBaseType() }
+  /** Whether two types will be compared, regardless of order (a, b) or (b, a). */
+  private predicate interestedInUnordered(Type t1, Type t2) {
+    interestedIn(t1, t2) or
+    interestedIn(t2, t1)
   }
 
-  private module LeafEquiv = QlBuiltins::EquivalenceRelation<RelevantType, equalLeafRelation/2>;
-
-  private predicate equalLeafRelation(RelevantType t1, RelevantType t2) {
-    Config::equalLeafTypes(t1, t2)
-  }
+  bindingset[t1, t2]
+  private predicate equalLeafRelation(LeafType t1, LeafType t2) { Config::equalLeafTypes(t1, t2) }
 
-  private RelevantType unspecify(SpecifiedType t) {
+  bindingset[t]
+  private Type unspecify(SpecifiedType t) {
     // This subtly and importantly handles the complicated cases of typedefs. Under most scenarios,
     // if we see a typedef in `equalTypes()` we can simply get the base type and continue. However,
     // there is an exception if we have a specified type that points to a typedef that points to
@@ -290,7 +429,7 @@ module TypeEquivalence<TypeEquivalenceSig Config, TypeSubset T> {
   }
 
   bindingset[t1, t2]
-  private predicate equalDerivedTypes(RelevantDerivedType t1, RelevantDerivedType t2) {
+  private predicate equalDerivedTypes(DerivedType t1, DerivedType t2) {
     exists(Boolean baseTypesEqual |
       (baseTypesEqual = true implies equalTypes(t1.getBaseType(), t2.getBaseType())) and
       (
@@ -312,7 +451,7 @@ module TypeEquivalence<TypeEquivalenceSig Config, TypeSubset T> {
   }
 
   bindingset[t1, t2]
-  private predicate equalFunctionTypes(RelevantFunctionType t1, RelevantFunctionType t2) {
+  private predicate equalFunctionTypes(FunctionType t1, FunctionType t2) {
     exists(Boolean returnTypeEqual, Boolean parameterTypesEqual |
       (returnTypeEqual = true implies equalTypes(t1.getReturnType(), t2.getReturnType())) and
       (
@@ -331,7 +470,7 @@ module TypeEquivalence<TypeEquivalenceSig Config, TypeSubset T> {
   }
 
   bindingset[t1, t2]
-  private predicate equalTypedefTypes(RelevantTypedefType t1, RelevantTypedefType t2) {
+  private predicate equalTypedefTypes(TypedefType t1, TypedefType t2) {
     exists(Boolean baseTypesEqual |
       (baseTypesEqual = true implies equalTypes(t1.getBaseType(), t2.getBaseType())) and
       Config::equalTypedefTypes(t1, t2, baseTypesEqual)
@@ -339,18 +478,48 @@ module TypeEquivalence<TypeEquivalenceSig Config, TypeSubset T> {
   }
 }
 
-module FunctionDeclarationTypeEquivalence<TypeEquivalenceSig Config> {
+signature predicate interestedInFunctionDeclarations(
+  FunctionDeclarationEntry f1, FunctionDeclarationEntry f2
+);
+
+module FunctionDeclarationTypeEquivalence<
+  TypeEquivalenceSig Config, interestedInFunctionDeclarations/2 interestedInFunctions>
+{
+  private predicate interestedInReturnTypes(Type a, Type b) {
+    exists(FunctionDeclarationEntry aFun, FunctionDeclarationEntry bFun |
+      interestedInFunctions(pragma[only_bind_into](aFun), pragma[only_bind_into](bFun)) and
+      a = aFun.getType() and
+      b = bFun.getType()
+    )
+  }
+
+  private predicate interestedInParameterTypes(Type a, Type b) {
+    exists(FunctionDeclarationEntry aFun, FunctionDeclarationEntry bFun, int i |
+      interestedInFunctions(pragma[only_bind_into](aFun), pragma[only_bind_into](bFun)) and
+      a = aFun.getParameterDeclarationEntry(i).getType() and
+      b = bFun.getParameterDeclarationEntry(i).getType()
+    )
+  }
+
   predicate equalReturnTypes(FunctionDeclarationEntry f1, FunctionDeclarationEntry f2) {
-    TypeEquivalence<Config, FunctionSignatureType>::equalTypes(f1.getType(), f2.getType())
+    interestedInFunctions(f1, f2) and
+    TypeEquivalence<Config, interestedInReturnTypes/2>::equalTypes(f1.getType(), f2.getType())
   }
 
   predicate equalParameterTypes(FunctionDeclarationEntry f1, FunctionDeclarationEntry f2) {
+    interestedInFunctions(f1, f2) and
     f1.getDeclaration() = f2.getDeclaration() and
     forall(int i | exists([f1, f2].getParameterDeclarationEntry(i)) |
-      TypeEquivalence<Config, FunctionSignatureType>::equalTypes(f1.getParameterDeclarationEntry(i)
-            .getType(), f2.getParameterDeclarationEntry(i).getType())
+      equalParameterTypesAt(f1, f2, pragma[only_bind_into](i))
     )
   }
+
+  predicate equalParameterTypesAt(FunctionDeclarationEntry f1, FunctionDeclarationEntry f2, int i) {
+    interestedInFunctions(f1, f2) and
+    f1.getDeclaration() = f2.getDeclaration() and
+    TypeEquivalence<Config, interestedInParameterTypes/2>::equalTypes(f1.getParameterDeclarationEntry(pragma[only_bind_into](i))
+          .getType(), f2.getParameterDeclarationEntry(pragma[only_bind_into](i)).getType())
+  }
 }
 
 /**
@@ -370,3 +539,11 @@ private class FunctionType extends Type {
     result = this.(FunctionPointerIshType).getParameterType(i)
   }
 }
+
+private class LeafType extends Type {
+  LeafType() {
+    not this instanceof DerivedType and
+    not this instanceof FunctionType and
+    not this instanceof FunctionType
+  }
+}
diff --git a/cpp/common/src/codingstandards/cpp/types/SimpleAssignment.qll b/cpp/common/src/codingstandards/cpp/types/SimpleAssignment.qll
index 4f7a85c80..a31400a34 100644
--- a/cpp/common/src/codingstandards/cpp/types/SimpleAssignment.qll
+++ b/cpp/common/src/codingstandards/cpp/types/SimpleAssignment.qll
@@ -8,42 +8,67 @@
 import codingstandards.cpp.types.LvalueConversion
 import codingstandards.cpp.types.Compatible
 
-module SimpleAssignment<TypeSubset T> {
-  final private class FinalType = Type;
-
-  private class RelevantType extends FinalType {
-    RelevantType() { exists(T t | typeGraph*(t, this) or typeGraph(getLvalueConverted(t), this)) }
-
-    string toString() { result = "relevant type" }
-  }
-
+module SimpleAssignment<interestedInEquality/2 checksAssignment> {
   /**
    * Whether a pair of qualified or unqualified pointer types satisfy the simple assignment
    * constraints from 6.5.16.1.
    *
    * There are additional constraints not implemented here involving one or more arithmetic types.
    */
-  predicate satisfiesSimplePointerAssignment(RelevantType left, RelevantType right) {
+  predicate satisfiesSimplePointerAssignment(Type left, Type right) {
+    checksAssignment(left, right) and
     simplePointerAssignmentImpl(getLvalueConverted(left), right)
   }
 
+  private predicate satisfiedWhenTypesCompatible(Type left, Type right, Type checkA, Type checkB) {
+    interestedInTypes(left, right) and
+    exists(Type leftBase, Type rightBase |
+      // The left operand has atomic, qualified, or unqualified pointer type:
+      leftBase = left.stripTopLevelSpecifiers().(PointerType).getBaseType() and
+      rightBase = right.stripTopLevelSpecifiers().(PointerType).getBaseType() and
+      (
+        // and both operands are pointers to qualified or unqualified versions of compatible types:
+        checkA = leftBase.stripTopLevelSpecifiers() and
+        checkB = rightBase.stripTopLevelSpecifiers()
+      ) and
+      // and the type pointed to by the left has all the qualifiers of the type pointed to by the
+      // right:
+      forall(Specifier s | s = rightBase.getASpecifier() | s = leftBase.getASpecifier())
+    )
+  }
+
+  predicate interestedInTypes(Type left, Type right) {
+    exists(Type unconverted |
+      left = getLvalueConverted(unconverted) and
+      checksAssignment(unconverted, right)
+    )
+  }
+
+  predicate checksCompatibility(Type left, Type right) {
+    // Check if the types are compatible
+    exists(Type assignA, Type assignB |
+      checksAssignment(assignA, assignB) and
+      satisfiedWhenTypesCompatible(assignA, assignB, left, right)
+    )
+  }
+
   /**
    * Implementation of 6.5.16.1 for a pair of pointer types, that assumes lvalue conversion has been
    * performed on the left operand.
    */
-  private predicate simplePointerAssignmentImpl(RelevantType left, RelevantType right) {
-    exists(RelevantType leftBase, RelevantType rightBase |
+  bindingset[left, right]
+  private predicate simplePointerAssignmentImpl(Type left, Type right) {
+    exists(Type checkA, Type checkB |
+      satisfiedWhenTypesCompatible(left, right, checkA, checkB) and
+      TypeEquivalence<TypesCompatibleConfig, checksCompatibility/2>::equalTypes(checkA, checkB)
+    )
+    or
+    exists(Type leftBase, Type rightBase |
       // The left operand has atomic, qualified, or unqualified pointer type:
       leftBase = left.stripTopLevelSpecifiers().(PointerType).getBaseType() and
       rightBase = right.stripTopLevelSpecifiers().(PointerType).getBaseType() and
-      (
-        // and both operands are pointers to qualified or unqualified versions of compatible types:
-        TypeEquivalence<TypesCompatibleConfig, RelevantType>::equalTypes(leftBase
-              .stripTopLevelSpecifiers(), rightBase.stripTopLevelSpecifiers())
-        or
-        // or one operand is a pointer to a qualified or unqualified version of void
-        [leftBase, rightBase].stripTopLevelSpecifiers() instanceof VoidType
-      ) and
+      // or one operand is a pointer to a qualified or unqualified version of void
+      [leftBase, rightBase].stripTopLevelSpecifiers() instanceof VoidType and
       // and the type pointed to by the left has all the qualifiers of the type pointed to by the
       // right:
       forall(Specifier s | s = rightBase.getASpecifier() | s = leftBase.getASpecifier())