Normalize types when normalizing terms in normalize.rs, and therefore…

… avoid some normalization in term.rs and vcgen.rs.

creusot/src/backend/logic/vcgen.rs

@@ -345,9 +345,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             TermKind::Tuple { fields } => self.build_vc_slice(fields, &|flds| k(Exp::Tuple(flds))),
             // Same as for tuples
             TermKind::Constructor { variant, fields, .. } => {
-                let ty =
-                    self.ctx.borrow().normalize_erasing_regions(self.param_env, t.creusot_ty());
-                let TyKind::Adt(adt, subst) = ty.kind() else { unreachable!() };
+                let TyKind::Adt(adt, subst) = t.creusot_ty().kind() else { unreachable!() };
                 self.build_vc_slice(fields, &|fields| {
                     let ctor = constructor(
                         *self.names.borrow_mut(),
@@ -406,9 +404,7 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             }),
             // VC(A.f, Q) = VC(A, |a| Q(a.f))
             TermKind::Projection { lhs, name } => {
-                let ty =
-                    self.ctx.borrow().normalize_erasing_regions(self.param_env, lhs.creusot_ty());
-                let field = match ty.kind() {
+                let field = match lhs.creusot_ty().kind() {
                     TyKind::Closure(did, substs) => {
                         self.names.borrow_mut().field(*did, substs, *name).as_ident()
                     }
@@ -462,9 +458,8 @@ impl<'a, 'tcx> VCGen<'a, 'tcx> {
             Pattern::Constructor { variant, fields, substs } => {
                 let fields =
                     fields.into_iter().map(|pat| self.build_pattern_inner(bounds, pat)).collect();
-                let substs = self.ctx.borrow().normalize_erasing_regions(self.param_env, *substs);
                 if self.ctx.borrow().def_kind(variant) == DefKind::Variant {
-                    Pat::ConsP(self.names.borrow_mut().constructor(*variant, substs), fields)
+                    Pat::ConsP(self.names.borrow_mut().constructor(*variant, *substs), fields)
                 } else if fields.len() == 0 {
                     Pat::TupleP(vec![])
                 } else {

creusot/src/backend/term.rs

@@ -122,8 +122,7 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
                 }
             }
             TermKind::Constructor { variant, fields, .. } => {
-                let ty = self.names.normalize(self.ctx, term.creusot_ty());
-                let TyKind::Adt(adt, subst) = ty.kind() else { unreachable!() };
+                let TyKind::Adt(adt, subst) = term.creusot_ty().kind() else { unreachable!() };
                 let fields = fields.into_iter().map(|f| self.lower_term(f)).collect();
                 constructor(self.names, fields, adt.variant(*variant).def_id, subst)
             }
@@ -173,10 +172,9 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
                 Exp::Tuple(fields.into_iter().map(|f| self.lower_term(f)).collect())
             }
             TermKind::Projection { box lhs, name } => {
-                let base_ty = self.names.normalize(self.ctx, lhs.creusot_ty());
-                let lhs = self.lower_term(lhs);
+                let lhs_low = self.lower_term(lhs);
 
-                let field = match base_ty.kind() {
+                let field = match lhs.creusot_ty().kind() {
                     TyKind::Closure(did, substs) => self.names.field(*did, substs, *name),
                     TyKind::Adt(def, substs) => self.names.field(def.did(), substs, *name),
                     TyKind::Tuple(f) => {
@@ -185,14 +183,14 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
 
                         return Exp::Let {
                             pattern: Pat::TupleP(fields),
-                            arg: Box::new(lhs),
+                            arg: Box::new(lhs_low),
                             body: Box::new(Exp::var("a")),
                         };
                     }
                     k => unreachable!("Projection from {k:?}"),
                 };
 
-                lhs.field(&field.as_ident())
+                lhs_low.field(&field.as_ident())
             }
             TermKind::Closure { body, .. } => {
                 let TyKind::Closure(id, subst) = term.creusot_ty().kind() else {
@@ -232,9 +230,8 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
         match pat {
             Pattern::Constructor { variant, fields, substs } => {
                 let fields = fields.into_iter().map(|pat| self.lower_pat(pat)).collect();
-                let substs = self.names.normalize(self.ctx, *substs);
                 if self.ctx.def_kind(variant) == DefKind::Variant {
-                    Pat::ConsP(self.names.constructor(*variant, substs), fields)
+                    Pat::ConsP(self.names.constructor(*variant, *substs), fields)
                 } else if fields.len() == 0 {
                     Pat::TupleP(vec![])
                 } else {

creusot/src/translation/function/terminator.rs

@@ -335,7 +335,6 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
             return;
         }
         // We are indeed in program code.
-        let func_param_env = self.ctx.param_env(fun_def_id);
 
         // Check that we do not call `GhostBox::into_inner` in normal code
         if is_ghost_into_inner(self.ctx.tcx, fun_def_id) {
@@ -379,6 +378,7 @@ impl<'tcx> BodyTranslator<'_, 'tcx> {
                 )
                 .emit();
         } else {
+            let func_param_env = self.ctx.param_env(fun_def_id);
             // Check and reject instantiation of a <T: Deref> with a ghost parameter.
             let deref_trait_id = self.ctx.require_lang_item(rustc_hir::LangItem::Deref, None);
             let infer_ctx = self.ctx.infer_ctxt().build();

creusot/src/translation/pearlite/normalize.rs

@@ -14,8 +14,7 @@ pub(crate) fn normalize<'tcx>(
     mut term: Term<'tcx>,
 ) -> Term<'tcx> {
     NormalizeTerm { param_env, tcx }.visit_mut_term(&mut term);
-    // FIXME: we should normalize here, but it diverges when normalizing specification of partial_eq
-    // let term = tcx.normalize_erasing_regions(param_env, term);
+    let term = tcx.normalize_erasing_regions(param_env, term);
     term
 }
 
@@ -38,7 +37,6 @@ impl<'tcx> TermVisitorMut<'tcx> for NormalizeTerm<'tcx> {
                     *id = method.0;
                     *subst = method.1;
                 }
-                *subst = self.tcx.normalize_erasing_regions(self.param_env, *subst);
 
                 if is_box_new(self.tcx, *id) {
                     let arg = args.remove(0);

creusot/src/translation/specification.rs

@@ -432,7 +432,6 @@ pub(crate) fn pre_sig_of<'tcx>(
     ctx: &mut TranslationCtx<'tcx>,
     def_id: DefId,
 ) -> PreSignature<'tcx> {
-    let param_env = ctx.param_env(def_id);
     let (inputs, output) = inputs_and_output(ctx.tcx, def_id);
 
     let mut contract = crate::specification::contract_of(ctx, def_id);
@@ -466,7 +465,7 @@ pub(crate) fn pre_sig_of<'tcx>(
 
             let term = Term::call(
                 ctx.tcx,
-                param_env,
+                ctx.param_env(def_id),
                 unnest_id,
                 unnest_subst,
                 vec![Term::var(self_, env_ty).cur(), Term::var(self_, env_ty).fin()],