Erase regions in constraint solving

viperproject · Apr 28, 2022 · ae6589d · ae6589d
1 parent e9419cd
commit ae6589d
Showing 1 changed file with 7 additions and 4 deletions.
diff --git a/prusti-viper/src/encoder/mir/specifications/constraints.rs b/prusti-viper/src/encoder/mir/specifications/constraints.rs
@@ -153,15 +153,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 +231,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) {