erase regions less eagerly for method calls

viperproject · Jul 22, 2022 · 1a06b91 · 1a06b91
1 parent 8ed4eb2
commit 1a06b91
Showing 1 changed file with 6 additions and 2 deletions.
diff --git a/prusti-interface/src/environment/mod.rs b/prusti-interface/src/environment/mod.rs
@@ -510,10 +510,14 @@ impl<'tcx> Environment<'tcx> {
         let param_env = self.tcx.param_env(caller_def_id);
 
         // `resolve_instance` below requires normalized substs.
-        let call_substs = self.tcx.normalize_erasing_regions(param_env, call_substs);
+        let normalized_call_substs = self.tcx.normalize_erasing_regions(param_env, call_substs);
 
-        traits::resolve_instance(self.tcx, param_env.and((called_def_id, call_substs)))
+        traits::resolve_instance(self.tcx, param_env.and((called_def_id, normalized_call_substs)))
             .map(|opt_instance| opt_instance
+                // if the resolved instance is the same as what we queried for
+                // anyway, ignore it: this way we keep the regions in substs
+                // at least for non-trait-impl method calls
+                .filter(|instance| instance.def_id() != called_def_id)
                 .map(|instance| (instance.def_id(), instance.substs))
                 .unwrap_or((called_def_id, call_substs)))
             .unwrap_or((called_def_id, call_substs))