1
Fork 0

Fall back to bidirectional normalizes-to if no subst-eq in alias-eq goal

This commit is contained in:
Michael Goulet 2023-05-27 19:27:59 +00:00
parent 7a2cdf20e4
commit 3ea7c512bd
4 changed files with 145 additions and 23 deletions

View file

@ -79,12 +79,22 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
// them. This is necessary for inference during typeck.
//
// As this is incomplete, we must not do so during coherence.
match (self.solver_mode(), subst_relate_response) {
(SolverMode::Normal, Ok(response)) => Ok(response),
(SolverMode::Normal, Err(NoSolution)) | (SolverMode::Coherence, _) => {
match self.solver_mode() {
SolverMode::Normal => {
if let Ok(subst_relate_response) = subst_relate_response {
Ok(subst_relate_response)
} else if let Ok(bidirectional_normalizes_to_response) = self
.assemble_bidirectional_normalizes_to_candidate(
param_env, lhs, rhs, direction,
)
{
Ok(bidirectional_normalizes_to_response)
} else {
self.flounder(&candidates)
}
}
SolverMode::Coherence => self.flounder(&candidates),
}
}
}
}
@ -100,27 +110,40 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
invert: Invert,
) -> QueryResult<'tcx> {
self.probe(|ecx| {
ecx.normalizes_to_inner(param_env, alias, other, direction, invert)?;
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
}
fn normalizes_to_inner(
&mut self,
param_env: ty::ParamEnv<'tcx>,
alias: ty::AliasTy<'tcx>,
other: ty::Term<'tcx>,
direction: ty::AliasRelationDirection,
invert: Invert,
) -> Result<(), NoSolution> {
let other = match direction {
// This is purely an optimization.
ty::AliasRelationDirection::Equate => other,
ty::AliasRelationDirection::Subtype => {
let fresh = ecx.next_term_infer_of_kind(other);
let fresh = self.next_term_infer_of_kind(other);
let (sub, sup) = match invert {
Invert::No => (fresh, other),
Invert::Yes => (other, fresh),
};
ecx.sub(param_env, sub, sup)?;
self.sub(param_env, sub, sup)?;
fresh
}
};
ecx.add_goal(Goal::new(
ecx.tcx(),
self.add_goal(Goal::new(
self.tcx(),
param_env,
ty::Binder::dummy(ty::ProjectionPredicate { projection_ty: alias, term: other }),
));
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
Ok(())
}
fn assemble_subst_relate_candidate(
@ -143,4 +166,30 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
}
fn assemble_bidirectional_normalizes_to_candidate(
&mut self,
param_env: ty::ParamEnv<'tcx>,
lhs: ty::Term<'tcx>,
rhs: ty::Term<'tcx>,
direction: ty::AliasRelationDirection,
) -> QueryResult<'tcx> {
self.probe(|ecx| {
ecx.normalizes_to_inner(
param_env,
lhs.to_alias_ty(ecx.tcx()).unwrap(),
rhs,
direction,
Invert::No,
)?;
ecx.normalizes_to_inner(
param_env,
rhs.to_alias_ty(ecx.tcx()).unwrap(),
lhs,
direction,
Invert::Yes,
)?;
ecx.evaluate_added_goals_and_make_canonical_response(Certainty::Yes)
})
}
}

View file

@ -0,0 +1,21 @@
// compile-flags: -Ztrait-solver=next
// check-pass
#![feature(type_alias_impl_trait)]
// Similar to tests/ui/traits/new-solver/tait-eq-proj.rs
// but check the alias-sub relation in the other direction.
type Tait = impl Iterator<Item = impl Sized>;
fn mk<T>() -> T { todo!() }
fn a() {
let x: Tait = mk();
let mut array = mk();
let mut z = IntoIterator::into_iter(array);
z = x;
array = [0i32; 32];
}
fn main() {}

View file

@ -0,0 +1,35 @@
// compile-flags: -Ztrait-solver=next
// check-pass
#![feature(type_alias_impl_trait)]
type Tait = impl Iterator<Item = impl Sized>;
/*
Consider the goal - AliasRelate(Tait, <[i32; 32] as IntoIterator>::IntoIter)
which is registered on the line above.
A. SubstRelate - fails (of course).
B. NormalizesToRhs - Tait normalizes-to <[i32; 32] as IntoIterator>::IntoIter
* infer definition - Tait := <[i32; 32] as IntoIterator>::IntoIter
C. NormalizesToLhs - <[i32; 32] as IntoIterator>::IntoIter normalizes-to Tait
* Find impl candidate, after substitute - std::array::IntoIter<i32, 32>
* Equate std::array::IntoIter<i32, 32> and Tait
* infer definition - Tait := std::array::IntoIter<i32, 32>
B and C are not equal, but they are equivalent modulo normalization.
We get around this by evaluating both the NormalizesToRhs and NormalizesToLhs
goals together. Essentially:
A alias-relate B if A normalizes-to B and B normalizes-to A.
*/
fn a() {
let _: Tait = IntoIterator::into_iter([0i32; 32]);
}
fn main() {}

View file

@ -0,0 +1,17 @@
// compile-flags: -Ztrait-solver=next
// check-pass
// Not exactly sure if this is the inference behavior we *want*,
// but it is a side-effect of the lazy normalization of TAITs.
#![feature(type_alias_impl_trait)]
type Tait = impl Sized;
type Tait2 = impl Sized;
fn mk<T>() -> T { todo!() }
fn main() {
let x: Tait = 1u32;
let y: Tait2 = x;
}