Skip to content

Commit

Permalink
new solver: make apply query response infallible
Browse files Browse the repository at this point in the history
For this we have to provide the necessary information when canonicalizing
the input, guaranteeing that if the canonical query successfully instantiates
some inference variable, it will also succeed in the caller. This means we
have to not merge universes in the canonical input.
  • Loading branch information
lcnr committed Feb 2, 2024
1 parent fb4bca0 commit feff26b
Show file tree
Hide file tree
Showing 20 changed files with 418 additions and 207 deletions.
2 changes: 1 addition & 1 deletion compiler/rustc_infer/src/infer/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ pub mod opaque_types;
pub mod outlives;
mod projection;
pub mod region_constraints;
mod relate;
pub mod relate;
pub mod resolve;
pub mod type_variable;
mod undo_log;
Expand Down
12 changes: 6 additions & 6 deletions compiler/rustc_infer/src/infer/relate/combine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -335,7 +335,7 @@ impl<'tcx> InferCtxt<'tcx> {
Ok(value)
}

fn unify_integral_variable(
pub(super) fn unify_integral_variable(
&self,
vid_is_expected: bool,
vid: ty::IntVid,
Expand All @@ -352,7 +352,7 @@ impl<'tcx> InferCtxt<'tcx> {
}
}

fn unify_float_variable(
pub(super) fn unify_float_variable(
&self,
vid_is_expected: bool,
vid: ty::FloatVid,
Expand All @@ -366,7 +366,7 @@ impl<'tcx> InferCtxt<'tcx> {
Ok(Ty::new_float(self.tcx, val))
}

fn unify_effect_variable(
pub(super) fn unify_effect_variable(
&self,
vid_is_expected: bool,
vid: ty::EffectVid,
Expand Down Expand Up @@ -564,23 +564,23 @@ pub trait ObligationEmittingRelation<'tcx>: TypeRelation<'tcx> {
fn alias_relate_direction(&self) -> ty::AliasRelationDirection;
}

fn int_unification_error<'tcx>(
pub(super) fn int_unification_error<'tcx>(
a_is_expected: bool,
v: (ty::IntVarValue, ty::IntVarValue),
) -> TypeError<'tcx> {
let (a, b) = v;
TypeError::IntMismatch(ExpectedFound::new(a_is_expected, a, b))
}

fn float_unification_error<'tcx>(
pub(super) fn float_unification_error<'tcx>(
a_is_expected: bool,
v: (ty::FloatVarValue, ty::FloatVarValue),
) -> TypeError<'tcx> {
let (ty::FloatVarValue(a), ty::FloatVarValue(b)) = v;
TypeError::FloatMismatch(ExpectedFound::new(a_is_expected, a, b))
}

fn effect_unification_error<'tcx>(
pub(super) fn effect_unification_error<'tcx>(
_tcx: TyCtxt<'tcx>,
_a_is_expected: bool,
(_a, _b): (EffectVarValue<'tcx>, EffectVarValue<'tcx>),
Expand Down
6 changes: 6 additions & 0 deletions compiler/rustc_infer/src/infer/relate/generalize.rs
Original file line number Diff line number Diff line change
Expand Up @@ -269,6 +269,8 @@ where
ty::Invariant => {
if self.for_universe.can_name(universe) {
return Ok(t);
} else if self.infcx.next_trait_solver() && self.in_alias {
return Err(TypeError::Mismatch);
}
}

Expand Down Expand Up @@ -400,6 +402,8 @@ where
let r_universe = self.infcx.universe_of_region(r);
if self.for_universe.can_name(r_universe) {
return Ok(r);
} else if self.infcx.next_trait_solver() && self.in_alias {
return Err(TypeError::Mismatch);
}
}

Expand Down Expand Up @@ -439,6 +443,8 @@ where
ConstVariableValue::Unknown { origin, universe } => {
if self.for_universe.can_name(universe) {
Ok(c)
} else if self.infcx.next_trait_solver() && self.in_alias {
return Err(TypeError::Mismatch);
} else {
let new_var_id = variable_table
.new_key(ConstVariableValue::Unknown {
Expand Down
266 changes: 266 additions & 0 deletions compiler/rustc_infer/src/infer/relate/instantiate_unchecked.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,266 @@
use super::combine::{float_unification_error, int_unification_error};
use crate::infer::{InferCtxt, SubregionOrigin, TypeTrace, ValuePairs};

use rustc_middle::infer::unify_key::{ConstVariableValue, EffectVarValue};
use rustc_middle::traits::ObligationCause;
use rustc_middle::ty::error::ExpectedFound;
use rustc_middle::ty::relate::{self, structurally_relate_tys, Relate, RelateResult, TypeRelation};
use rustc_middle::ty::visit::MaxUniverse;
use rustc_middle::ty::IntVarValue::{IntType, UintType};
use rustc_middle::ty::TypeVisitable;
use rustc_middle::ty::{self, Ty, TyCtxt};
use rustc_middle::ty::{GenericArgsRef, InferConst};
use rustc_middle::ty::{InferCtxtLike, TyVar};

use rustc_hir::def_id::DefId;

/// A visitor to instantiate inference variables assuming that the
/// instantiation will definitely succeed.
///
/// Using this in places where that may not be the case can easily
/// result in bugs or unsoudness. Used when instantiating a canonical
/// response in the new solver.
///
/// Unlike `Equate` this always structurally relates aliases, meaning
/// it always succeeds without emitting any nested obligations.
pub struct InstantiateUnchecked<'a, 'tcx> {
infcx: &'a InferCtxt<'tcx>,
cause: &'a ObligationCause<'tcx>,
}

impl<'a, 'tcx> InstantiateUnchecked<'a, 'tcx> {
pub fn new(
infcx: &'a InferCtxt<'tcx>,
cause: &'a ObligationCause<'tcx>,
) -> InstantiateUnchecked<'a, 'tcx> {
InstantiateUnchecked { infcx, cause }
}

/// Used by debug assertions to detect some unsound uses of this
/// visitor.
fn infer_var_can_name<T: TypeVisitable<TyCtxt<'tcx>>>(
&self,
universe_of_infer: ty::UniverseIndex,
value: T,
) -> bool {
let mut visitor = MaxUniverse::new();
value.visit_with(&mut visitor);
universe_of_infer.can_name(visitor.max_universe())
}
}

impl<'tcx> TypeRelation<'tcx> for InstantiateUnchecked<'_, 'tcx> {
fn tag(&self) -> &'static str {
"InstantiateUnchecked"
}

fn tcx(&self) -> TyCtxt<'tcx> {
self.infcx.tcx
}

fn a_is_expected(&self) -> bool {
true
}

fn relate_item_args(
&mut self,
_item_def_id: DefId,
a_arg: GenericArgsRef<'tcx>,
b_arg: GenericArgsRef<'tcx>,
) -> RelateResult<'tcx, GenericArgsRef<'tcx>> {
relate::relate_args_invariantly(self, a_arg, b_arg)
}

fn relate_with_variance<T: Relate<'tcx>>(
&mut self,
_: ty::Variance,
_info: ty::VarianceDiagInfo<'tcx>,
a: T,
b: T,
) -> RelateResult<'tcx, T> {
self.relate(a, b)
}

#[instrument(skip(self), level = "debug")]
fn tys(&mut self, a: Ty<'tcx>, b: Ty<'tcx>) -> RelateResult<'tcx, Ty<'tcx>> {
if a == b {
return Ok(a);
}

let infcx = self.infcx;
let a = infcx.inner.borrow_mut().type_variables().replace_if_possible(a);
let b = infcx.inner.borrow_mut().type_variables().replace_if_possible(b);

// This is pretty much a copy of `Equate::tys` and `fn super_combine_consts`.
// We cannot use these directly as they emit `AliasRelate` goals when
// relate aliases.
match (a.kind(), b.kind()) {
(&ty::Infer(TyVar(a_vid)), &ty::Infer(TyVar(b_vid))) => {
infcx.inner.borrow_mut().type_variables().equate(a_vid, b_vid);
Ok(a)
}

(&ty::Infer(TyVar(a_vid)), _) => {
debug_assert!(self.infer_var_can_name(infcx.universe_of_ty(a_vid).unwrap(), b));
infcx.inner.borrow_mut().type_variables().instantiate(a_vid, b);
Ok(b)
}

(_, &ty::Infer(TyVar(b_vid))) => {
debug_assert!(self.infer_var_can_name(infcx.universe_of_ty(b_vid).unwrap(), a));
infcx.inner.borrow_mut().type_variables().instantiate(b_vid, a);
Ok(a)
}

(&ty::Infer(ty::IntVar(a_vid)), &ty::Infer(ty::IntVar(b_vid))) => {
infcx
.inner
.borrow_mut()
.int_unification_table()
.unify_var_var(a_vid, b_vid)
.map_err(|e| int_unification_error(true, e))?;
Ok(a)
}
(&ty::Infer(ty::IntVar(v_id)), &ty::Int(v)) => {
infcx.unify_integral_variable(true, v_id, IntType(v))
}
(&ty::Int(v), &ty::Infer(ty::IntVar(v_id))) => {
infcx.unify_integral_variable(false, v_id, IntType(v))
}
(&ty::Infer(ty::IntVar(v_id)), &ty::Uint(v)) => {
infcx.unify_integral_variable(true, v_id, UintType(v))
}
(&ty::Uint(v), &ty::Infer(ty::IntVar(v_id))) => {
infcx.unify_integral_variable(false, v_id, UintType(v))
}

// Relate floating-point variables to other types
(&ty::Infer(ty::FloatVar(a_vid)), &ty::Infer(ty::FloatVar(b_vid))) => {
infcx
.inner
.borrow_mut()
.float_unification_table()
.unify_var_var(a_vid, b_vid)
.map_err(|e| float_unification_error(true, e))?;
Ok(a)
}
(&ty::Infer(ty::FloatVar(v_id)), &ty::Float(v)) => {
infcx.unify_float_variable(true, v_id, v)
}
(&ty::Float(v), &ty::Infer(ty::FloatVar(v_id))) => {
infcx.unify_float_variable(false, v_id, v)
}

_ => structurally_relate_tys(self, a, b),
}
}

fn regions(
&mut self,
a: ty::Region<'tcx>,
b: ty::Region<'tcx>,
) -> RelateResult<'tcx, ty::Region<'tcx>> {
debug!("{}.regions({:?}, {:?})", self.tag(), a, b);
let origin = SubregionOrigin::Subtype(Box::new(TypeTrace {
cause: self.cause.clone(),
values: ValuePairs::Regions(ExpectedFound::new(true, a, b)),
}));
self.infcx.inner.borrow_mut().unwrap_region_constraints().make_eqregion(origin, a, b);
Ok(a)
}

fn consts(
&mut self,
a: ty::Const<'tcx>,
b: ty::Const<'tcx>,
) -> RelateResult<'tcx, ty::Const<'tcx>> {
let infcx = self.infcx;
let a = infcx.shallow_resolve(a);
let b = infcx.shallow_resolve(b);
match (a.kind(), b.kind()) {
(
ty::ConstKind::Infer(InferConst::Var(a_vid)),
ty::ConstKind::Infer(InferConst::Var(b_vid)),
) => {
infcx.inner.borrow_mut().const_unification_table().union(a_vid, b_vid);
Ok(a)
}

(
ty::ConstKind::Infer(InferConst::EffectVar(a_vid)),
ty::ConstKind::Infer(InferConst::EffectVar(b_vid)),
) => {
infcx
.inner
.borrow_mut()
.effect_unification_table()
.unify_var_var(a_vid, b_vid)
.map_err(|_| bug!("unexpected error"))?;
Ok(a)
}

// All other cases of inference with other variables are errors.
(
ty::ConstKind::Infer(InferConst::Var(_) | InferConst::EffectVar(_)),
ty::ConstKind::Infer(_),
)
| (
ty::ConstKind::Infer(_),
ty::ConstKind::Infer(InferConst::Var(_) | InferConst::EffectVar(_)),
) => {
bug!(
"tried to combine ConstKind::Infer/ConstKind::Infer(InferConst::Var): {a:?} and {b:?}"
)
}

(ty::ConstKind::Infer(InferConst::Var(a_vid)), _) => {
debug_assert!(self.infer_var_can_name(infcx.universe_of_ct(a_vid).unwrap(), b));
infcx
.inner
.borrow_mut()
.const_unification_table()
.union_value(a_vid, ConstVariableValue::Known { value: b });
Ok(b)
}

(_, ty::ConstKind::Infer(InferConst::Var(b_vid))) => {
debug_assert!(self.infer_var_can_name(infcx.universe_of_ct(b_vid).unwrap(), a));
infcx
.inner
.borrow_mut()
.const_unification_table()
.union_value(b_vid, ConstVariableValue::Known { value: a });
Ok(a)
}

(ty::ConstKind::Infer(InferConst::EffectVar(vid)), _) => {
infcx.unify_effect_variable(true, vid, EffectVarValue::Const(b))
}

(_, ty::ConstKind::Infer(InferConst::EffectVar(vid))) => {
infcx.unify_effect_variable(false, vid, EffectVarValue::Const(a))
}

_ => ty::relate::structurally_relate_consts(self, a, b),
}
}

fn binders<T>(
&mut self,
a: ty::Binder<'tcx, T>,
b: ty::Binder<'tcx, T>,
) -> RelateResult<'tcx, ty::Binder<'tcx, T>>
where
T: Relate<'tcx>,
{
if a != b {
// This differs from `Equate`; we only care about structural equality here.
assert_eq!(a.bound_vars(), b.bound_vars());
let (a, b) = self
.infcx
.instantiate_binder_with_placeholders(a.map_bound(|a| (a, b.skip_binder())));
self.relate(a, b)?;
}
Ok(a)
}
}
1 change: 1 addition & 0 deletions compiler/rustc_infer/src/infer/relate/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ mod equate;
pub(super) mod generalize;
mod glb;
mod higher_ranked;
pub mod instantiate_unchecked;
mod lattice;
mod lub;
pub mod nll;
Expand Down
2 changes: 0 additions & 2 deletions compiler/rustc_middle/src/traits/solve/inspect.rs
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,6 @@ pub struct GoalEvaluation<'tcx> {
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
pub kind: GoalEvaluationKind<'tcx>,
pub evaluation: CanonicalGoalEvaluation<'tcx>,
/// The nested goals from instantiating the query response.
pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
}

#[derive(Eq, PartialEq)]
Expand Down
15 changes: 1 addition & 14 deletions compiler/rustc_middle/src/traits/solve/inspect/format.rs
Original file line number Diff line number Diff line change
Expand Up @@ -48,20 +48,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
},
};
writeln!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))?;
if eval.returned_goals.len() > 0 {
writeln!(self.f, "NESTED GOALS ADDED TO CALLER: [")?;
self.nested(|this| {
for goal in eval.returned_goals.iter() {
writeln!(this.f, "ADDED GOAL: {goal:?},")?;
}
Ok(())
})?;

writeln!(self.f, "]")
} else {
Ok(())
}
self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))
}

pub(super) fn format_canonical_goal_evaluation(
Expand Down
Loading

0 comments on commit feff26b

Please sign in to comment.