Skip to content

Commit

Permalink
Auto merge of #792 - lowr:fix/generalize-alias-alias-eq-clause, r=jac…
Browse files Browse the repository at this point in the history 
…kh726

Generalize program clause for `AliasEq` goal with nested alias

Consider a goal: `AliasEq(<<?0 as X>::A as Y>::B = <<?1 as X>::A as Y>::B)`. This is expected to (eventually) flounder when the traits are non-enumerable and the variables are yet to be known, but it's currently **disproven**:

1. the goal is canonicalized as follows:
    - `forall<T, U> AliasEq(<<T as X>::A as Y>::B = <<U as X>::A as Y>::B)`
1. we produce the following `ProgramClause` that could match:
    - `forall<T, U, ..> AliasEq(<<T as X>::A as Y>::B = <<U as X>::A as Y>::B) :- AliasEq(..), AliasEq(..)`
1. the consequence of the (instantiated) clause is unified with the goal, which produces a subgoal:
    - `AliasEq(<<?0 as X>::A as Y>::B = <<?1 as X>::A as Y>::B)`
    - this is because when we unify rhs of `AliasEq`, we see two `AliasTy`s that we cannot unify structurally, forcing us to produce the subgoal
1. boom, cycle emerged, goal disproven!

The problem is that because we're reusing the original goal as the consequence of the program clause we expect them to unify structurally, however we cannot unify aliases structurally in general (e.g. `<?0 as X>::A = <?1 as X>::A` does not imply `?0 = ?1`).

This PR solves it by placing a fresh variable in rhs of the consequence `AliasEq` instead of reusing the original term. This ensures that rhs of the original `AliasEq` goal is preserved via unification without producing subgoals even if it's an alias.

See rust-lang/rust-analyzer#14369 for a real world case where this issue arises.
  • Loading branch information
@bors
bors committed Jun 14, 2023
2 parents 1635ed5 + 91c24e3 commit 88fd1c2
Show file tree
Hide file tree
Showing 2 changed files with 98 additions and 43 deletions.
104 changes: 61 additions & 43 deletions chalk-solve/src/clauses.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -512,12 +512,7 @@ pub fn program_clauses_that_could_match<I: Interner>(
// An alias could normalize to anything, including an
// opaque type, so push a clause that asks for the self
// type to be normalized and return.
push_alias_alias_eq_clause(
builder,
proj.clone(),
alias_eq.ty.clone(),
alias.clone(),
);
push_alias_alias_eq_clause(builder, proj.clone(), alias.clone());
return Ok(clauses);
}
TyKind::OpaqueType(opaque_ty_id, _) => {
Expand Down Expand Up @@ -781,12 +776,10 @@ fn push_alias_implemented_clause<I: Interner>(
// TODO: instead generate clauses without reference to the specific type parameters of the goal?
let generalized = generalize::Generalize::apply(interner, (trait_ref, alias));
builder.push_binders(generalized, |builder, (trait_ref, alias)| {
let binders = Binders::with_fresh_type_var(interner, |ty_var| ty_var);

// forall<..., T> {
// <X as Y>::Z: Trait :- T: Trait, <X as Y>::Z == T
// }
builder.push_binders(binders, |builder, bound_var| {
builder.push_bound_ty(|builder, bound_var| {
let fresh_self_subst = Substitution::from_iter(
interner,
std::iter::once(bound_var.clone().cast(interner)).chain(
Expand Down Expand Up @@ -816,7 +809,6 @@ fn push_alias_implemented_clause<I: Interner>(
fn push_alias_alias_eq_clause<I: Interner>(
builder: &mut ClauseBuilder<'_, I>,
projection_ty: ProjectionTy<I>,
ty: Ty<I>,
alias: AliasTy<I>,
) {
let interner = builder.interner();
Expand All @@ -827,43 +819,69 @@ fn push_alias_alias_eq_clause<I: Interner>(
assert_eq!(*self_ty.kind(interner), TyKind::Alias(alias.clone()));

// TODO: instead generate clauses without reference to the specific type parameters of the goal?
let generalized = generalize::Generalize::apply(interner, (projection_ty, ty, alias));
builder.push_binders(generalized, |builder, (projection_ty, ty, alias)| {
let binders = Binders::with_fresh_type_var(interner, |ty_var| ty_var);

// forall<..., T> {
let generalized = generalize::Generalize::apply(interner, (projection_ty, alias));
builder.push_binders(generalized, |builder, (projection_ty, alias)| {
// Given the following canonical goal:
//
// ```
// forall<...> {
// <<X as Y>::A as Z>::B == W
// }
// ```
//
// we generate:
//
// ```
// forall<..., T, U> {
// <<X as Y>::A as Z>::B == U :- <T as Z>::B == U, <X as Y>::A == T
// }
builder.push_binders(binders, |builder, bound_var| {
let (_, trait_args, assoc_args) = builder.db.split_projection(&projection_ty);
let fresh_self_subst = Substitution::from_iter(
interner,
assoc_args
.iter()
.cloned()
.chain(std::iter::once(bound_var.clone().cast(interner)))
.chain(trait_args[1..].iter().cloned()),
);
let fresh_alias = AliasTy::Projection(ProjectionTy {
associated_ty_id: projection_ty.associated_ty_id,
substitution: fresh_self_subst,
});
builder.push_clause(
DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
alias: AliasTy::Projection(projection_ty.clone()),
ty: ty.clone(),
})),
&[
DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
alias: fresh_alias,
ty: ty.clone(),
})),
// ```
//
// `T` and `U` are `intermediate_eq_ty` and `eq_ty` respectively below.
//
// Note that we used to "reuse" `W` and push:
//
// ```
// forall<..., T> {
// <<X as Y>::A as Z>::B == W :- <T as Z>::B == W, <X as Y>::A == T
// }
// ```
//
// but it caused a cycle which led to false `NoSolution` under certain conditions, in
// particular when `W` itself is a nested projection type. See test
// `nested_proj_eq_nested_proj_should_flounder`.
builder.push_bound_ty(|builder, intermediate_eq_ty| {
builder.push_bound_ty(|builder, eq_ty| {
let (_, trait_args, assoc_args) = builder.db.split_projection(&projection_ty);
let fresh_self_subst = Substitution::from_iter(
interner,
assoc_args
.iter()
.cloned()
.chain(std::iter::once(intermediate_eq_ty.clone().cast(interner)))
.chain(trait_args[1..].iter().cloned()),
);
let fresh_alias = AliasTy::Projection(ProjectionTy {
associated_ty_id: projection_ty.associated_ty_id,
substitution: fresh_self_subst,
});
builder.push_clause(
DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
alias: alias.clone(),
ty: bound_var,
alias: AliasTy::Projection(projection_ty.clone()),
ty: eq_ty.clone(),
})),
],
);
&[
DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
alias: fresh_alias,
ty: eq_ty,
})),
DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
alias,
ty: intermediate_eq_ty,
})),
],
);
});
});
});
}
Expand Down
37 changes: 37 additions & 0 deletions tests/test/projection.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1189,3 +1189,40 @@ fn projection_from_super_trait_bounds() {
}
}
}

#[test]
fn nested_proj_eq_nested_proj_should_flounder() {
test! {
program {
#[non_enumerable]
trait Trait1 {
type Assoc: Trait2;
}
#[non_enumerable]
trait Trait2 {
type Assoc;
}

impl Trait1 for () {
type Assoc = ();
}
impl Trait1 for i32 {
type Assoc = ();
}
impl Trait2 for () {
type Assoc = ();
}
}

goal {
exists<T, U> {
<<T as Trait1>::Assoc as Trait2>::Assoc = <<U as Trait1>::Assoc as Trait2>::Assoc
}
} yields[SolverChoice::slg_default()] {
// FIXME
expect![[r#"Ambiguous; definite substitution for<?U0> { [?0 := ^0.0, ?1 := ^0.0] }"#]]
} yields[SolverChoice::recursive_default()] {
expect![[r#"Ambiguous; no inference guidance"#]]
}
}
}

0 comments on commit 88fd1c2

Please sign in to comment.