Merge pull request #21151 from hvitved/rust/disable-universal-conds-by-default

Type inference: Disable universal conditions by default
This commit is contained in:
Tom Hvitved
2026-01-22 11:19:50 +01:00
committed by GitHub
5 changed files with 20 additions and 40 deletions

View File

@@ -117,8 +117,6 @@ module SatisfiesBlanketConstraint<
predicate relevantConstraint(ArgumentTypeAndBlanketOffset ato, Type constraint) {
relevantConstraint(ato, _, constraint.(TraitType).getTrait())
}
predicate useUniversalConditions() { none() }
}
private module SatisfiesBlanketConstraint =

View File

@@ -2200,8 +2200,6 @@ private module MethodResolution {
exists(mc) and
constraint.(TraitType).getTrait() instanceof DerefTrait
}
predicate useUniversalConditions() { none() }
}
private module MethodCallSatisfiesDerefConstraint =
@@ -3613,8 +3611,6 @@ private module AwaitSatisfiesConstraintInput implements SatisfiesConstraintInput
exists(term) and
constraint.(TraitType).getTrait() instanceof FutureTrait
}
predicate useUniversalConditions() { none() }
}
pragma[nomagic]
@@ -3811,8 +3807,6 @@ private module ForIterableSatisfiesConstraintInput implements
t instanceof IntoIteratorTrait
)
}
predicate useUniversalConditions() { none() }
}
pragma[nomagic]
@@ -3864,8 +3858,6 @@ private module InvokedClosureSatisfiesConstraintInput implements
exists(term) and
constraint.(TraitType).getTrait() instanceof FnOnceTrait
}
predicate useUniversalConditions() { none() }
}
/** Gets the type of `ce` when viewed as an implementation of `FnOnce`. */

View File

@@ -438,7 +438,7 @@ mod method_non_parametric_trait_impl {
let thing = MyThing { a: S1 };
let i = thing.convert_to(); // $ type=i:S1 target=T::convert_to
let j = convert_to(thing); // $ type=j:S1 target=convert_to
let j = convert_to(thing); // $ target=convert_to $ MISSING: type=j:S1 -- the blanket implementation `impl<T: MyTrait<S1>> ConvertTo<S1> for T` is currently not included in the constraint analysis
}
}

View File

@@ -7151,8 +7151,6 @@ inferType
| main.rs:440:17:440:21 | thing | | main.rs:224:5:227:5 | MyThing |
| main.rs:440:17:440:21 | thing | A | main.rs:235:5:236:14 | S1 |
| main.rs:440:17:440:34 | thing.convert_to() | | main.rs:235:5:236:14 | S1 |
| main.rs:441:13:441:13 | j | | main.rs:235:5:236:14 | S1 |
| main.rs:441:17:441:33 | convert_to(...) | | main.rs:235:5:236:14 | S1 |
| main.rs:441:28:441:32 | thing | | main.rs:224:5:227:5 | MyThing |
| main.rs:441:28:441:32 | thing | A | main.rs:235:5:236:14 | S1 |
| main.rs:450:26:450:29 | SelfParam | | main.rs:449:5:453:5 | Self [trait OverlappingTrait] |

View File

@@ -841,15 +841,6 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
signature module SatisfiesConstraintInputSig<HasTypeTreeSig HasTypeTree> {
/** Holds if it is relevant to know if `term` satisfies `constraint`. */
predicate relevantConstraint(HasTypeTree term, Type constraint);
/**
* Holds if constraints that are satisfied through conditions that are
* universally quantified type parameters should be used. Such type
* parameters might have type parameter constraints, and these are _not_
* checked. Hence using these represent a trade-off between too many
* constraints and too few constraints being satisfied.
*/
default predicate useUniversalConditions() { any() }
}
module SatisfiesConstraint<
@@ -901,12 +892,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
TypeMention constraintMention
) {
exists(Type type | hasTypeConstraint(tt, type, constraint) |
useUniversalConditions() and // todo: remove, and instead check constraints
not exists(countConstraintImplementations(type, constraint)) and
conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
resolveTypeMentionRoot(condition) = abs.getATypeParameter() and
constraint = resolveTypeMentionRoot(constraintMention)
or
// TODO: Handle universal conditions properly, which means checking type parameter constraints
// Also remember to update logic in `hasNotConstraintMention`
//
// not exists(countConstraintImplementations(type, constraint)) and
// conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
// resolveTypeMentionRoot(condition) = abs.getATypeParameter() and
// constraint = resolveTypeMentionRoot(constraintMention)
// or
countConstraintImplementations(type, constraint) > 0 and
rootTypesSatisfaction(type, constraint, abs, condition, constraintMention) and
// When there are multiple ways the type could implement the
@@ -936,18 +929,17 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
pragma[nomagic]
private predicate hasNotConstraintMention(HasTypeTree tt, Type constraint) {
exists(Type type | hasTypeConstraint(tt, type, constraint) |
(
not useUniversalConditions()
or
exists(countConstraintImplementations(type, constraint))
or
forall(TypeAbstraction abs, TypeMention condition, TypeMention constraintMention |
conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
resolveTypeMentionRoot(condition) = abs.getATypeParameter()
|
not constraint = resolveTypeMentionRoot(constraintMention)
)
) and
// TODO: Handle universal conditions properly, which means taking type parameter constraints into account
// (
// exists(countConstraintImplementations(type, constraint))
// or
// forall(TypeAbstraction abs, TypeMention condition, TypeMention constraintMention |
// conditionSatisfiesConstraintTypeAt(abs, condition, constraintMention, _, _) and
// resolveTypeMentionRoot(condition) = abs.getATypeParameter()
// |
// not constraint = resolveTypeMentionRoot(constraintMention)
// )
// ) and
(
countConstraintImplementations(type, constraint) = 0
or