Canonicalize effect vars in new solver

This commit is contained in:
Michael Goulet 2023-09-14 17:24:18 +00:00
parent ae9465fee3
commit 280f058560
4 changed files with 47 additions and 2 deletions

View File

@ -1335,6 +1335,10 @@ impl<'tcx> InferCtxt<'tcx> {
self.inner.borrow_mut().const_unification_table().find(var)
}
pub fn root_effect_var(&self, var: ty::EffectVid<'tcx>) -> ty::EffectVid<'tcx> {
self.inner.borrow_mut().effect_unification_table().find(var)
}
/// Resolves an int var to a rigid int type, if it was constrained to one,
/// or else the root int var in the unification table.
pub fn opportunistic_resolve_int_var(&self, vid: ty::IntVid) -> Ty<'tcx> {

View File

@ -365,8 +365,16 @@ impl<'tcx> TypeFolder<TyCtxt<'tcx>> for Canonicalizer<'_, 'tcx> {
// FIXME: we should fold this ty eventually
CanonicalVarKind::Const(ui, c.ty())
}
ty::ConstKind::Infer(ty::InferConst::EffectVar(_)) => {
bug!("effect var has no universe")
ty::ConstKind::Infer(ty::InferConst::EffectVar(vid)) => {
assert_eq!(
self.infcx.root_effect_var(vid),
vid,
"effect var should have been resolved"
);
let None = self.infcx.probe_effect_var(vid) else {
bug!("effect var should have been resolved");
};
CanonicalVarKind::Effect
}
ty::ConstKind::Infer(ty::InferConst::Fresh(_)) => {
bug!("fresh var during canonicalization: {c:?}")

View File

@ -382,6 +382,17 @@ impl<'tcx> TypeFolder<TyCtxt<'tcx>> for EagerResolver<'_, 'tcx> {
}
}
}
ty::ConstKind::Infer(ty::InferConst::EffectVar(vid)) => {
debug_assert_eq!(c.ty(), self.infcx.tcx.types.bool);
match self.infcx.probe_effect_var(vid) {
Some(c) => c.as_const(self.infcx.tcx),
None => ty::Const::new_infer(
self.infcx.tcx,
ty::InferConst::EffectVar(self.infcx.root_effect_var(vid)),
self.infcx.tcx.types.bool,
),
}
}
_ => {
if c.has_infer() {
c.super_fold_with(self)

View File

@ -0,0 +1,22 @@
// compile-flags: -Ztrait-solver=next
// check-pass
#![feature(effects)]
#![feature(const_trait_impl)]
#[const_trait]
trait Foo {
fn foo();
}
trait Bar {}
impl const Foo for i32 {
fn foo() {}
}
impl<T> const Foo for T where T: Bar {
fn foo() {}
}
fn main() {}