From 0946857d256e467982d5b0fec50303586ec79ff4 Mon Sep 17 00:00:00 2001
From: Nico Lehmann <nico.lehmannm@gmail.com>
Date: Sun, 15 Oct 2023 15:55:06 -0700
Subject: [PATCH] Add forgoten test file

---
 .../flux-refineck/src/type_env/projection.rs  | 31 +++++++++++--------
 .../tests/neg/surface/invariant00.rs          | 14 +++++++++
 2 files changed, 32 insertions(+), 13 deletions(-)
 create mode 100644 crates/flux-tests/tests/neg/surface/invariant00.rs

diff --git a/crates/flux-refineck/src/type_env/projection.rs b/crates/flux-refineck/src/type_env/projection.rs
index b28f0a817b..f041fbad75 100644
--- a/crates/flux-refineck/src/type_env/projection.rs
+++ b/crates/flux-refineck/src/type_env/projection.rs
@@ -361,7 +361,7 @@ impl FallibleTypeFolder for Unfolder<'_, '_, '_> {
         let Some(elem) = self.cursor.next() else {
             return self.unfold(ty);
         };
-        let ty = self.rcx.unpack_with(ty, UnpackFlags::SHALLOW);
+        let ty = self.unpack(ty);
         match elem {
             PlaceElem::Deref => self.deref(&ty),
             PlaceElem::Field(f) => self.field(&ty, f),
@@ -413,11 +413,11 @@ impl<'a, 'rcx, 'tcx> Unfolder<'a, 'rcx, 'tcx> {
                 Ok(Ty::ptr(PtrKind::Box, Path::from(loc)))
             }
         } else if ty.is_struct() {
-            let ty = self.rcx.unpack_with(ty, UnpackFlags::SHALLOW);
+            let ty = self.unpack(ty);
             let ty = self.downcast(&ty, FIRST_VARIANT)?;
             Ok(ty)
         } else if ty.is_array() || ty.is_slice() {
-            Ok(self.rcx.unpack_with(ty, UnpackFlags::SHALLOW))
+            Ok(self.unpack(ty))
         } else {
             Ok(ty.clone())
         }
@@ -478,7 +478,7 @@ impl<'a, 'rcx, 'tcx> Unfolder<'a, 'rcx, 'tcx> {
                 let mut fields = downcast_struct(self.genv, adt, args, idx)?
                     .into_iter()
                     .map(|ty| {
-                        let ty = self.rcx.unpack_with(&ty, self.unpack_flags_for_downcast());
+                        let ty = self.unpack_for_downcast(&ty);
                         self.assume_invariants(&ty);
                         ty
                     })
@@ -503,7 +503,7 @@ impl<'a, 'rcx, 'tcx> Unfolder<'a, 'rcx, 'tcx> {
                 let fields = downcast(self.genv, self.rcx, adt, args, variant, idx)?
                     .into_iter()
                     .map(|ty| {
-                        let ty = self.rcx.unpack_with(&ty, self.unpack_flags_for_downcast());
+                        let ty = self.unpack_for_downcast(&ty);
                         self.assume_invariants(&ty);
                         ty
                     })
@@ -532,6 +532,19 @@ impl<'a, 'rcx, 'tcx> Unfolder<'a, 'rcx, 'tcx> {
         Ok(())
     }
 
+    fn unpack(&mut self, ty: &Ty) -> Ty {
+        self.rcx.unpack_with(ty, UnpackFlags::SHALLOW)
+    }
+
+    fn unpack_for_downcast(&mut self, ty: &Ty) -> Ty {
+        let flags = if self.in_ref == Some(Mutability::Mut) {
+            UnpackFlags::NO_UNPACK_EXISTS | UnpackFlags::SHALLOW
+        } else {
+            UnpackFlags::SHALLOW
+        };
+        self.rcx.unpack_with(ty, flags)
+    }
+
     fn assume_invariants(&mut self, ty: &Ty) {
         self.rcx
             .assume_invariants(ty, self.checker_conf.check_overflow);
@@ -542,14 +555,6 @@ impl<'a, 'rcx, 'tcx> Unfolder<'a, 'rcx, 'tcx> {
         self.cursor.change_root(path);
     }
 
-    fn unpack_flags_for_downcast(&self) -> UnpackFlags {
-        if self.in_ref == Some(Mutability::Mut) {
-            UnpackFlags::NO_UNPACK_EXISTS
-        } else {
-            UnpackFlags::empty()
-        }
-    }
-
     fn should_continue(&mut self) -> bool {
         if self.has_work {
             self.has_work = false;
diff --git a/crates/flux-tests/tests/neg/surface/invariant00.rs b/crates/flux-tests/tests/neg/surface/invariant00.rs
new file mode 100644
index 0000000000..9eae918967
--- /dev/null
+++ b/crates/flux-tests/tests/neg/surface/invariant00.rs
@@ -0,0 +1,14 @@
+//! Check that we don't assume invariants under a generic type argument.
+
+struct S<T> {
+    x: T,
+}
+
+// We don't assume `n >= 0` from the `u32[n]` inside `S`, that would be unsound in general.
+#[flux::sig(fn(i32[@n], S<u32[n]>))]
+fn test(x: i32, _: S<u32>) {
+    assert(x >= 0); //~ERROR refinement type error
+}
+
+#[flux::sig(fn(bool[true]))]
+fn assert(_: bool) {}