Skip to content

Commit

Permalink
Generalize program clause for AliasEq goal with nested alias
Browse files Browse the repository at this point in the history
  • Loading branch information
@lowr
lowr committed Jun 13, 2023
1 parent 1635ed5 commit 91c24e3
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 91c24e3

Please sign in to comment.