Skip to content

Commit

Permalink
Auto merge of #112875 - compiler-errors:negative-coherence-rework, r=…
Browse files Browse the repository at this point in the history
…lcnr

Rework negative coherence to properly consider impls that only partly overlap

This PR implements a modified negative coherence that handles impls that only have partial overlap.

It does this by:
1. taking both impl trait refs, instantiating them with infer vars
2. equating both trait refs
3. taking the equated trait ref (which represents the two impls' intersection), and resolving any vars
4. plugging all remaining infer vars with placeholder types

these placeholder-plugged trait refs can then be used normally with the new trait solver, since we no longer have to worry about the issue with infer vars in param-envs.

We use the **new trait solver** to reason correctly about unnormalized trait refs (due to deferred projection equality), since this avoid having to normalize anything under param-envs with infer vars in them.

This PR then additionally:
* removes the `FnPtr` knowable hack by implementing proper negative `FnPtr` trait bounds for rigid types.

---

An example:

Consider these two partially overlapping impls:

```
impl<T, U> PartialEq<&U> for &T where T: PartialEq<U> {}
impl<F> PartialEq<F> for F where F: FnPtr {}
```

Under the old algorithm, we would take one of these impls and replace it with infer vars, then try unifying it with the other impl under identity substitutions. This is not possible in either direction, since it either sets `T = U`, or tries to equate `F = &?0`.

Under the new algorithm, we try to unify `?0: PartialEq<?0>` with `&?1: PartialEq<&?2>`. This gives us `?0 = &?1 = &?2` and thus `?1 = ?2`. The intersection of these two trait refs therefore looks like: `&?1: PartialEq<&?1>`. After plugging this with placeholders, we get a trait ref that looks like `&!0: PartialEq<&!0>`, with the first impl having substs `?T = ?U = !0` and the second having substs `?F = &!0`[^1].

Then we can take the param-env from the first impl, and try to prove the negated where clause of the second.

We know that `&!0: !FnPtr` never holds, since it's a rigid type that is also not a fn ptr, we successfully detect that these impls may never overlap.

[^1]: For the purposes of this example, I just ignored lifetimes, since it doesn't really matter.
  • Loading branch information
bors committed Oct 26, 2023
2 parents 056f5b0 + 0626f2e commit 9ab0749
Show file tree
Hide file tree
Showing 19 changed files with 314 additions and 143 deletions.
1 change: 1 addition & 0 deletions compiler/rustc_middle/src/ty/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -233,6 +233,7 @@ impl MainDefinition {
#[derive(Clone, Debug, TypeFoldable, TypeVisitable)]
pub struct ImplHeader<'tcx> {
pub impl_def_id: DefId,
pub impl_args: ty::GenericArgsRef<'tcx>,
pub self_ty: Ty<'tcx>,
pub trait_ref: Option<TraitRef<'tcx>>,
pub predicates: Vec<Predicate<'tcx>>,
Expand Down
2 changes: 2 additions & 0 deletions compiler/rustc_trait_selection/src/solve/assembly/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,8 @@ pub(super) trait GoalKind<'tcx>:

fn trait_ref(self, tcx: TyCtxt<'tcx>) -> ty::TraitRef<'tcx>;

fn polarity(self) -> ty::ImplPolarity;

fn with_self_ty(self, tcx: TyCtxt<'tcx>, self_ty: Ty<'tcx>) -> Self;

fn trait_def_id(self, tcx: TyCtxt<'tcx>) -> DefId;
Expand Down
4 changes: 4 additions & 0 deletions compiler/rustc_trait_selection/src/solve/project_goals/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,10 @@ impl<'tcx> assembly::GoalKind<'tcx> for ProjectionPredicate<'tcx> {
self.projection_ty.trait_ref(tcx)
}

fn polarity(self) -> ty::ImplPolarity {
ty::ImplPolarity::Positive
}

fn with_self_ty(self, tcx: TyCtxt<'tcx>, self_ty: Ty<'tcx>) -> Self {
self.with_self_ty(tcx, self_ty)
}
Expand Down
31 changes: 23 additions & 8 deletions compiler/rustc_trait_selection/src/solve/trait_goals.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,10 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
self.trait_ref
}

fn polarity(self) -> ty::ImplPolarity {
self.polarity
}

fn with_self_ty(self, tcx: TyCtxt<'tcx>, self_ty: Ty<'tcx>) -> Self {
self.with_self_ty(tcx, self_ty)
}
Expand Down Expand Up @@ -238,14 +242,25 @@ impl<'tcx> assembly::GoalKind<'tcx> for TraitPredicate<'tcx> {
ecx: &mut EvalCtxt<'_, 'tcx>,
goal: Goal<'tcx, Self>,
) -> QueryResult<'tcx> {
if goal.predicate.polarity != ty::ImplPolarity::Positive {
return Err(NoSolution);
}

if let ty::FnPtr(..) = goal.predicate.self_ty().kind() {
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
} else {
Err(NoSolution)
let self_ty = goal.predicate.self_ty();
match goal.predicate.polarity {
ty::ImplPolarity::Positive => {
if self_ty.is_fn_ptr() {
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
} else {
Err(NoSolution)
}
}
ty::ImplPolarity::Negative => {
// If a type is rigid and not a fn ptr, then we know for certain
// that it does *not* implement `FnPtr`.
if !self_ty.is_fn_ptr() && self_ty.is_known_rigid() {
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
} else {
Err(NoSolution)
}
}
ty::ImplPolarity::Reservation => bug!(),
}
}

Expand Down
Loading

0 comments on commit 9ab0749

Please sign in to comment.