More whack-a-mole with scopes

crates/flux-infer/src/infer.rs

@@ -61,6 +61,7 @@ pub enum ConstrReason {
     Assign,
     Ret,
     Fold,
+    FoldLocal,
     Assert(&'static str),
     Div,
     Rem,

crates/flux-refineck/src/checker.rs

@@ -827,9 +827,11 @@ impl<'ck, 'genv, 'tcx, M: Mode> Checker<'ck, 'genv, 'tcx, M> {
             .replace_evars(&evars_sol)
             .replace_bound_refts_with(|sort, _, _| infcx.define_vars(sort));
 
+        infcx.push_scope();
         env.update_ensures(infcx, &output, self.check_overflow());
-
         fold_local_ptrs(infcx, env, span)?;
+        let evars_sol = infcx.pop_scope().with_span(span)?;
+        infcx.replace_evars(&evars_sol);
 
         Ok(output.ret)
     }

crates/flux-refineck/src/lib.rs

@@ -220,7 +220,9 @@ fn report_errors(genv: GlobalEnv, errors: Vec<Tag>) -> Result<(), ErrorGuarantee
             ConstrReason::Rem => genv.sess().emit_err(errors::RemError { span }),
             ConstrReason::Goto(_) => genv.sess().emit_err(errors::GotoError { span }),
             ConstrReason::Assert(msg) => genv.sess().emit_err(errors::AssertError { span, msg }),
-            ConstrReason::Fold => genv.sess().emit_err(errors::FoldError { span }),
+            ConstrReason::Fold | ConstrReason::FoldLocal => {
+                genv.sess().emit_err(errors::FoldError { span })
+            }
             ConstrReason::Overflow => genv.sess().emit_err(errors::OverflowError { span }),
             ConstrReason::Other => genv.sess().emit_err(errors::UnknownError { span }),
         });

crates/flux-refineck/src/type_env.rs

@@ -228,7 +228,7 @@ impl<'a> TypeEnv<'a> {
 
     pub(crate) fn fold_local_ptrs(&mut self, infcx: &mut InferCtxtAt) -> InferResult<()> {
         for (loc, bound, ty) in self.bindings.local_ptrs() {
-            infcx.subtyping(&ty, &bound, ConstrReason::Fold)?;
+            infcx.subtyping(&ty, &bound, ConstrReason::FoldLocal)?;
             self.bindings.remove_local(&loc);
         }
         Ok(())

tests/tests/todo/issue-899c.rs

@@ -0,0 +1,58 @@
+use core::slice::{Iter, SliceIndex};
+
+
+pub trait Queue<T> {
+    /// Returns true if the queue is full, false otherwise.
+    fn is_full(&self) -> bool;
+
+    /// If the queue isn't full, add a new element to the back of the queue.
+    /// Returns whether the element was added.
+    #[flux_rs::sig(fn(self: &strg Self, _) -> bool ensures self: Self)]
+    fn enqueue(&mut self, val: T) -> bool;
+}
+
+
+#[flux_rs::extern_spec]
+impl<T> [T] {
+    #[flux_rs::sig(fn(&[T][@len]) -> usize[len])]
+    fn len(v: &[T]) -> usize;
+}
+
+
+#[flux_rs::refined_by(ring_len: int, hd: int, tl: int)]
+#[flux_rs::invariant(ring_len > 1)]
+pub struct RingBuffer<'a, T: 'a> {
+    #[field({&mut [T][ring_len] | ring_len > 1})]
+    ring: &'a mut [T],
+    #[field({usize[hd] | hd < ring_len})]
+    head: usize,
+    #[field({usize[tl] | tl < ring_len})]
+    tail: usize,
+}
+
+impl<T: Copy> Queue<T> for RingBuffer<'_, T> {
+    fn is_full(&self) -> bool {
+        self.head == ((self.tail + 1) % self.ring.len())
+    }
+
+    #[flux_rs::sig(fn(self: &strg Self, _) -> bool ensures self: Self)]
+    fn enqueue(&mut self, val: T) -> bool {
+        if self.is_full() {
+            // Incrementing tail will overwrite head
+            false
+        } else {
+            self.ring[self.tail] = val;
+            self.tail = (self.tail + 1) % self.ring.len();
+            true
+        }
+    }
+}
+
+// This code causes an ICE
+fn get_ring_buffer() -> &'static mut RingBuffer<'static, usize> {unimplemented!()}
+
+fn enqueue_task() {
+    let rb = get_ring_buffer();
+    rb.enqueue(3);
+}
+