diff --git a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll index 7f78bea7d5d..1eaf6ef8e84 100644 --- a/shared/typeinference/codeql/typeinference/internal/TypeInference.qll +++ b/shared/typeinference/codeql/typeinference/internal/TypeInference.qll @@ -796,6 +796,14 @@ module Make1 Input1> { ) } + /** + * Holds if there is multiple ways in which a type with `conditionRoot` at + * the root can satisfy a constraint with `constraintRoot` at the root. + */ + predicate multipleConstraintImplementations(Type conditionRoot, Type constraintRoot) { + countConstraintImplementations(conditionRoot, constraintRoot) > 1 + } + /** * Holds if `baseMention` is a (transitive) base type mention of `sub`, * and `t` is mentioned (implicitly) at `path` inside `baseMention`. For @@ -902,14 +910,20 @@ module Make1 Input1> { { private import Input + /** Holds if the type tree has the type `type` and should satisfy `constraint`. */ + pragma[nomagic] + private predicate hasTypeConstraint(HasTypeTree term, Type type, Type constraint) { + type = term.getTypeAt(TypePath::nil()) and + relevantConstraint(term, constraint) + } + private module IsInstantiationOfInput implements IsInstantiationOfInputSig { predicate potentialInstantiationOf(HasTypeTree tt, TypeAbstraction abs, TypeMention cond) { exists(Type constraint, Type type | - type = tt.getTypeAt(TypePath::nil()) and - relevantConstraint(tt, constraint) and + hasTypeConstraint(tt, type, constraint) and rootTypesSatisfaction(type, constraint, abs, cond, _) and // We only need to check instantiations where there are multiple candidates. - countConstraintImplementations(type, constraint) > 1 + multipleConstraintImplementations(type, constraint) ) } @@ -918,13 +932,6 @@ module Make1 Input1> { } } - /** Holds if the type tree has the type `type` and should satisfy `constraint`. */ - pragma[nomagic] - private predicate hasTypeConstraint(HasTypeTree term, Type type, Type constraint) { - type = term.getTypeAt(TypePath::nil()) and - relevantConstraint(term, constraint) - } - /** * Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`. */ @@ -944,7 +951,7 @@ module Make1 Input1> { // 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 countConstraintImplementations(type, constraint) > 1 + if multipleConstraintImplementations(type, constraint) then IsInstantiationOf::isInstantiationOf(tt, abs, sub) else any()