Normalize term in projection predicate (#565)

crates/flux-middle/src/rty/fold.rs

@@ -16,8 +16,9 @@ use super::{
     subst::EVarSubstFolder,
     AliasTy, BaseTy, Binder, BoundVariableKind, Clause, ClauseKind, Constraint, Expr, ExprKind,
     FnOutput, FnSig, FnTraitPredicate, FuncSort, GeneratorObligPredicate, GenericArg, Index,
-    Invariant, KVar, Name, OpaqueArgsMap, Opaqueness, PolyFuncSort, ProjectionPredicate, PtrKind,
-    Qualifier, ReLateBound, Region, Sort, TraitPredicate, TraitRef, Ty, TyKind,
+    Invariant, KVar, Name, OpaqueArgsMap, Opaqueness, OutlivesPredicate, PolyFuncSort,
+    ProjectionPredicate, PtrKind, Qualifier, ReLateBound, Region, Sort, TraitPredicate, TraitRef,
+    Ty, TyKind,
 };
 use crate::{
     global_env::GlobalEnv,
@@ -429,6 +430,7 @@ impl TypeVisitable for ClauseKind {
             ClauseKind::Trait(pred) => pred.visit_with(visitor),
             ClauseKind::Projection(pred) => pred.visit_with(visitor),
             ClauseKind::GeneratorOblig(pred) => pred.visit_with(visitor),
+            ClauseKind::TypeOutlives(pred) => pred.visit_with(visitor),
         }
     }
 }
@@ -442,10 +444,26 @@ impl TypeFoldable for ClauseKind {
             ClauseKind::GeneratorOblig(pred) => {
                 Ok(ClauseKind::GeneratorOblig(pred.try_fold_with(folder)?))
             }
+            ClauseKind::TypeOutlives(pred) => {
+                Ok(ClauseKind::TypeOutlives(pred.try_fold_with(folder)?))
+            }
         }
     }
 }
 
+impl<T: TypeVisitable, U: TypeVisitable> TypeVisitable for OutlivesPredicate<T, U> {
+    fn visit_with<V: TypeVisitor>(&self, visitor: &mut V) -> ControlFlow<V::BreakTy, ()> {
+        self.0.visit_with(visitor)?;
+        self.1.visit_with(visitor)
+    }
+}
+
+impl<T: TypeFoldable, U: TypeFoldable> TypeFoldable for OutlivesPredicate<T, U> {
+    fn try_fold_with<F: FallibleTypeFolder>(&self, folder: &mut F) -> Result<Self, F::Error> {
+        Ok(OutlivesPredicate(self.0.try_fold_with(folder)?, self.1.try_fold_with(folder)?))
+    }
+}
+
 impl TypeVisitable for TraitPredicate {
     fn visit_with<V: TypeVisitor>(&self, visitor: &mut V) -> ControlFlow<V::BreakTy, ()> {
         self.trait_ref.visit_with(visitor)

crates/flux-middle/src/rty/mod.rs

@@ -28,7 +28,7 @@ use rustc_macros::{Decodable, Encodable, TyDecodable, TyEncodable};
 use rustc_middle::ty::ParamConst;
 pub use rustc_middle::{
     mir::Mutability,
-    ty::{AdtFlags, ClosureKind, FloatTy, IntTy, ParamTy, ScalarInt, UintTy},
+    ty::{AdtFlags, ClosureKind, FloatTy, IntTy, OutlivesPredicate, ParamTy, ScalarInt, UintTy},
 };
 use rustc_span::Symbol;
 pub use rustc_target::abi::{VariantIdx, FIRST_VARIANT};
@@ -105,9 +105,12 @@ pub enum ClauseKind {
     FnTrait(FnTraitPredicate),
     Trait(TraitPredicate),
     Projection(ProjectionPredicate),
+    TypeOutlives(TypeOutlivesPredicate),
     GeneratorOblig(GeneratorObligPredicate),
 }
 
+pub type TypeOutlivesPredicate = OutlivesPredicate<Ty, Region>;
+
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub struct TraitPredicate {
     pub trait_ref: TraitRef,
@@ -1695,6 +1698,7 @@ mod pretty {
                 ClauseKind::Trait(pred) => w!("Trait ({pred:?})"),
                 ClauseKind::Projection(pred) => w!("Projection ({pred:?})"),
                 ClauseKind::GeneratorOblig(pred) => w!("Projection ({pred:?})"),
+                ClauseKind::TypeOutlives(pred) => w!("Outlives ({:?}, {:?})", &pred.0, &pred.1),
             }
         }
     }

crates/flux-middle/src/rty/refining.rs

@@ -130,6 +130,10 @@ impl<'a, 'tcx> Refiner<'a, 'tcx> {
                 };
                 rty::ClauseKind::Projection(pred)
             }
+            rustc::ty::ClauseKind::TypeOutlives(pred) => {
+                let pred = rty::OutlivesPredicate(self.as_default().refine_ty(&pred.0)?, pred.1);
+                rty::ClauseKind::TypeOutlives(pred)
+            }
         };
         let kind = rty::Binder::new(kind, List::empty());
         Ok(Some(rty::Clause { kind }))
@@ -282,6 +286,7 @@ impl<'a, 'tcx> Refiner<'a, 'tcx> {
             _ => Ok(rty::Ty::exists(ty)),
         }
     }
+
     fn refine_alias_kind(kind: &rustc::ty::AliasKind) -> rty::AliasKind {
         match kind {
             rustc::ty::AliasKind::Projection => rty::AliasKind::Projection,

crates/flux-middle/src/rustc/lowering.rs

@@ -24,8 +24,8 @@ use super::{
     ty::{
         AdtDef, AdtDefData, AliasKind, Binder, BoundRegion, BoundVariableKind, Clause, ClauseKind,
         Const, FieldDef, FnSig, GenericArg, GenericParamDef, GenericParamDefKind,
-        GenericPredicates, Generics, PolyFnSig, TraitPredicate, TraitRef, Ty, ValueConst,
-        VariantDef,
+        GenericPredicates, Generics, PolyFnSig, TraitPredicate, TraitRef, Ty,
+        TypeOutlivesPredicate, ValueConst, VariantDef,
     },
 };
 use crate::{
@@ -849,6 +849,13 @@ fn lower_clause<'tcx>(
                 .emit(sess)?;
             ClauseKind::Projection(ProjectionPredicate { projection_ty, term })
         }
+        rustc_ty::ClauseKind::TypeOutlives(outlives_pred) => {
+            ClauseKind::TypeOutlives(
+                lower_type_outlives(tcx, outlives_pred)
+                    .map_err(|err| errors::UnsupportedGenericBound::new(span, err.descr))
+                    .emit(sess)?,
+            )
+        }
         _ => {
             return Err(sess.emit_err(errors::UnsupportedGenericBound::new(
                 span,
@@ -859,6 +866,13 @@ fn lower_clause<'tcx>(
     Ok(Clause::new(kind))
 }
 
+fn lower_type_outlives<'tcx>(
+    tcx: TyCtxt<'tcx>,
+    pred: rustc_ty::TypeOutlivesPredicate<'tcx>,
+) -> Result<TypeOutlivesPredicate, UnsupportedReason> {
+    Ok(rustc_ty::OutlivesPredicate(lower_ty(tcx, pred.0)?, lower_region(&pred.1)?))
+}
+
 mod errors {
     use flux_macros::Diagnostic;
     use rustc_middle::mir as rustc_mir;

crates/flux-middle/src/rustc/ty.rs

@@ -13,8 +13,8 @@ use rustc_middle::ty::{AdtFlags, ParamConst};
 pub use rustc_middle::{
     mir::Mutability,
     ty::{
-        BoundRegionKind, BoundVar, DebruijnIndex, EarlyBoundRegion, FloatTy, IntTy, ParamTy,
-        RegionVid, ScalarInt, UintTy,
+        BoundRegionKind, BoundVar, DebruijnIndex, EarlyBoundRegion, FloatTy, IntTy,
+        OutlivesPredicate, ParamTy, RegionVid, ScalarInt, UintTy,
     },
 };
 use rustc_span::{symbol::kw, Symbol};
@@ -72,8 +72,11 @@ pub struct Clause {
 pub enum ClauseKind {
     Trait(TraitPredicate),
     Projection(ProjectionPredicate),
+    TypeOutlives(TypeOutlivesPredicate),
 }
 
+pub type TypeOutlivesPredicate = OutlivesPredicate<Ty, Region>;
+
 #[derive(PartialEq, Eq, Hash, Debug)]
 pub struct TraitPredicate {
     pub trait_ref: TraitRef,

crates/flux-refineck/src/checker.rs

@@ -610,8 +610,9 @@ impl<'a, 'tcx, M: Mode> Checker<'a, 'tcx, M> {
                 rty::ClauseKind::GeneratorOblig(gen_pred) => {
                     self.check_oblig_generator_pred(rcx, &obligs.snapshot, gen_pred)?;
                 }
-                rty::ClauseKind::Projection(_) => (),
-                rty::ClauseKind::Trait(_) => (),
+                rty::ClauseKind::Projection(_)
+                | rty::ClauseKind::Trait(_)
+                | rty::ClauseKind::TypeOutlives(_) => {}
             }
         }
         Ok(())

crates/flux-refineck/src/constraint_gen.rs

@@ -198,7 +198,6 @@ impl<'a, 'tcx> ConstrGen<'a, 'tcx> {
                 .collect_vec();
 
         let genv = self.genv;
-        let callsite_def_id = self.def_id;
         let span = self.span;
 
         if let Some(did) = callee_def_id {
@@ -228,7 +227,7 @@ impl<'a, 'tcx> ConstrGen<'a, 'tcx> {
                 },
                 |sort, mode| infcx.fresh_infer_var(sort, mode),
             )
-            .normalize_projections(genv, infcx.region_infcx, callsite_def_id, infcx.refparams)?;
+            .normalize_projections(genv, infcx.region_infcx, infcx.def_id, infcx.refparams)?;
 
         let obligs = if let Some(did) = callee_def_id {
             mk_obligations(genv, did, &generic_args, &refine_args)?
@@ -278,13 +277,19 @@ impl<'a, 'tcx> ConstrGen<'a, 'tcx> {
                     .normalize_projections(
                         infcx.genv,
                         infcx.region_infcx,
-                        callsite_def_id,
+                        infcx.def_id,
                         infcx.refparams,
                     )?;
+                let term = projection_pred.term.normalize_projections(
+                    infcx.genv,
+                    infcx.region_infcx,
+                    infcx.def_id,
+                    infcx.refparams,
+                )?;
 
                 // TODO: does this really need to be invariant? https://github.com/flux-rs/flux/pull/478#issuecomment-1654035374
-                infcx.subtyping(rcx, &impl_elem, &projection_pred.term)?;
-                infcx.subtyping(rcx, &projection_pred.term, &impl_elem)?;
+                infcx.subtyping(rcx, &impl_elem, &term)?;
+                infcx.subtyping(rcx, &term, &impl_elem)?;
             }
         }
         // Replace evars

crates/flux-tests/tests/pos/surface/trait04.rs

@@ -0,0 +1,6 @@
+const A: &[i32] = &[0];
+const B: &[i32] = &[1];
+
+fn test() -> Vec<&'static i32> {
+    A.iter().chain(B).collect()
+}