Skip to content

Commit c3b4349

Browse files
borsbors
committed
Auto merge of #656 - flodiebold:opaque-trait-parameters, r=jackh726
Fix handling of variables in goal for new alias clauses The new clauses for alias types (`<X as Y>::Z: Trait :- T: Trait, <X as Y>::Z == T` etc.) were generated using the provided goal, without regard for bound variables. This led to e.g. the new test failing in the recursive solver. Alternatively, it might be better to generate the clauses without using the specific types in the goal. (CC #568.)
2 parents 84b2491 + 3b10bb1 commit c3b4349

File tree

2 files changed

+88
-59
lines changed

2 files changed

+88
-59
lines changed

‎chalk-solve/src/clauses.rs

Lines changed: 67 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -724,34 +724,38 @@ fn push_alias_implemented_clause<I: Interner>(
724724
TyKind::Alias(alias.clone())
725725
);
726726

727-
let binders = Binders::with_fresh_type_var(interner, |ty_var| ty_var);
728-
729-
// forall<..., T> {
730-
// <X as Y>::Z: Trait :- T: Trait, <X as Y>::Z == T
731-
// }
732-
builder.push_binders(&binders, |builder, bound_var| {
733-
let fresh_self_subst = Substitution::from_iter(
734-
interner,
735-
std::iter::once(bound_var.clone().cast(interner)).chain(
736-
trait_ref.substitution.as_slice(interner)[1..]
737-
.iter()
738-
.cloned(),
739-
),
740-
);
741-
let fresh_self_trait_ref = TraitRef {
742-
trait_id: trait_ref.trait_id,
743-
substitution: fresh_self_subst,
744-
};
745-
builder.push_clause(
746-
DomainGoal::Holds(WhereClause::Implemented(trait_ref.clone())),
747-
&[
748-
DomainGoal::Holds(WhereClause::Implemented(fresh_self_trait_ref)),
749-
DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
750-
alias: alias.clone(),
751-
ty: bound_var,
752-
})),
753-
],
754-
);
727+
// TODO: instead generate clauses without reference to the specific type parameters of the goal?
728+
let generalized = generalize::Generalize::apply(interner, &(trait_ref, alias));
729+
builder.push_binders(&generalized, |builder, (trait_ref, alias)| {
730+
let binders = Binders::with_fresh_type_var(interner, |ty_var| ty_var);
731+
732+
// forall<..., T> {
733+
// <X as Y>::Z: Trait :- T: Trait, <X as Y>::Z == T
734+
// }
735+
builder.push_binders(&binders, |builder, bound_var| {
736+
let fresh_self_subst = Substitution::from_iter(
737+
interner,
738+
std::iter::once(bound_var.clone().cast(interner)).chain(
739+
trait_ref.substitution.as_slice(interner)[1..]
740+
.iter()
741+
.cloned(),
742+
),
743+
);
744+
let fresh_self_trait_ref = TraitRef {
745+
trait_id: trait_ref.trait_id,
746+
substitution: fresh_self_subst,
747+
};
748+
builder.push_clause(
749+
DomainGoal::Holds(WhereClause::Implemented(trait_ref.clone())),
750+
&[
751+
DomainGoal::Holds(WhereClause::Implemented(fresh_self_trait_ref)),
752+
DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
753+
alias: alias.clone(),
754+
ty: bound_var,
755+
})),
756+
],
757+
);
758+
});
755759
});
756760
}
757761

@@ -767,40 +771,44 @@ fn push_alias_alias_eq_clause<I: Interner>(
767771
TyKind::Alias(alias.clone())
768772
);
769773

770-
let binders = Binders::with_fresh_type_var(interner, |ty_var| ty_var);
771-
772-
// forall<..., T> {
773-
// <<X as Y>::A as Z>::B == U :- <T as Z>::B == U, <X as Y>::A == T
774-
// }
775-
builder.push_binders(&binders, |builder, bound_var| {
776-
let fresh_self_subst = Substitution::from_iter(
777-
interner,
778-
std::iter::once(bound_var.clone().cast(interner)).chain(
779-
projection_ty.substitution.as_slice(interner)[1..]
780-
.iter()
781-
.cloned(),
782-
),
783-
);
784-
let fresh_alias = AliasTy::Projection(ProjectionTy {
785-
associated_ty_id: projection_ty.associated_ty_id,
786-
substitution: fresh_self_subst,
787-
});
788-
builder.push_clause(
789-
DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
790-
alias: AliasTy::Projection(projection_ty.clone()),
791-
ty: ty.clone(),
792-
})),
793-
&[
774+
// TODO: instead generate clauses without reference to the specific type parameters of the goal?
775+
let generalized = generalize::Generalize::apply(interner, &(projection_ty, ty, alias));
776+
builder.push_binders(&generalized, |builder, (projection_ty, ty, alias)| {
777+
let binders = Binders::with_fresh_type_var(interner, |ty_var| ty_var);
778+
779+
// forall<..., T> {
780+
// <<X as Y>::A as Z>::B == U :- <T as Z>::B == U, <X as Y>::A == T
781+
// }
782+
builder.push_binders(&binders, |builder, bound_var| {
783+
let fresh_self_subst = Substitution::from_iter(
784+
interner,
785+
std::iter::once(bound_var.clone().cast(interner)).chain(
786+
projection_ty.substitution.as_slice(interner)[1..]
787+
.iter()
788+
.cloned(),
789+
),
790+
);
791+
let fresh_alias = AliasTy::Projection(ProjectionTy {
792+
associated_ty_id: projection_ty.associated_ty_id,
793+
substitution: fresh_self_subst,
794+
});
795+
builder.push_clause(
794796
DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
795-
alias: fresh_alias,
797+
alias: AliasTy::Projection(projection_ty.clone()),
796798
ty: ty.clone(),
797799
})),
798-
DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
799-
alias: alias.clone(),
800-
ty: bound_var,
801-
})),
802-
],
803-
);
800+
&[
801+
DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
802+
alias: fresh_alias,
803+
ty: ty.clone(),
804+
})),
805+
DomainGoal::Holds(WhereClause::AliasEq(AliasEq {
806+
alias: alias.clone(),
807+
ty: bound_var,
808+
})),
809+
],
810+
);
811+
});
804812
});
805813
}
806814

‎tests/test/opaque_types.rs

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -172,6 +172,27 @@ fn opaque_generics() {
172172
}
173173
}
174174

175+
#[test]
176+
fn opaque_trait_generic() {
177+
test! {
178+
program {
179+
trait Trait<T> {}
180+
struct Foo {}
181+
impl Trait<u32> for Foo {}
182+
183+
opaque type Bar: Trait<u32> = Foo;
184+
}
185+
186+
goal {
187+
exists<T> {
188+
Bar: Trait<T>
189+
}
190+
} yields {
191+
"Unique; substitution [?0 := Uint(U32)]"
192+
}
193+
}
194+
}
195+
175196
#[test]
176197
fn opaque_auto_traits() {
177198
test! {

0 commit comments

Comments
 (0)