From 32ccf0e70039d17853b32228f011cf93136022e8 Mon Sep 17 00:00:00 2001
From: Jonas Hansen <ganymed92@gmail.com>
Date: Thu, 28 Apr 2022 17:01:56 +0200
Subject: [PATCH] Erase regions in constraint solving

---
 .../src/encoder/mir/specifications/constraints.rs    | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs
index 51fcb67df35..059becbc438 100644
--- a/prusti-viper/src/encoder/mir/specifications/constraints.rs
+++ b/prusti-viper/src/encoder/mir/specifications/constraints.rs
@@ -9,6 +9,7 @@ use rustc_hir::def_id::{DefId, LocalDefId};
 use rustc_middle::{
     ty,
     ty::subst::{Subst, SubstsRef},
+    ty::TypeFoldable,
 };
 use rustc_span::{MultiSpan, Span};
 
@@ -153,15 +154,18 @@ pub mod trait_bounds {
         // contain a behavioral subtyping check which will be performed on the
         // resolved spec.
         let param_env_lookup = if let Some(caller_def_id) = context.caller_proc_def_id {
-            env.tcx().param_env(caller_def_id)
+            env.tcx().param_env_reveal_all_normalized(caller_def_id)
         } else {
-            env.tcx().param_env(context.proc_def_id)
+            env.tcx().param_env_reveal_all_normalized(context.proc_def_id)
         };
 
         let all_bounds_satisfied = param_env_constraint
             .caller_bounds()
             .iter()
-            .all(|predicate| env.evaluate_predicate(predicate, param_env_lookup));
+            .all(|predicate| {
+                let predicate = env.tcx().erase_regions(predicate);
+                env.evaluate_predicate(predicate, param_env_lookup)
+            });
 
         trace!("Constraint fulfilled: {all_bounds_satisfied}");
         all_bounds_satisfied
@@ -228,7 +232,7 @@ pub mod trait_bounds {
             .cloned()
             .unwrap_or_default();
         for spec_id in pres.iter().chain(posts.iter()) {
-            let param_env = env.tcx().param_env(spec_id.to_def_id());
+            let param_env = env.tcx().param_env_reveal_all_normalized(spec_id.to_def_id());
             let spec_span = env.tcx().def_span(spec_id.to_def_id());
             let attrs = env.tcx().get_attrs(spec_id.to_def_id());
             if has_trait_bounds_ghost_constraint(attrs) {