From 3d762f6aca41c7c4cee2a9a2cfd5a2a42a811854 Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Fri, 5 Jan 2024 14:18:09 -0500
Subject: [PATCH] fix tuple types slipping through ast_simplify, fixes #857

---
 source/rust_verify_test/tests/regression.rs | 22 +++++++++++++++++++++
 source/vir/src/ast_simplify.rs              |  4 +++-
 2 files changed, 25 insertions(+), 1 deletion(-)

diff --git a/source/rust_verify_test/tests/regression.rs b/source/rust_verify_test/tests/regression.rs
index 2b42c6ccc4..59337f2d50 100644
--- a/source/rust_verify_test/tests/regression.rs
+++ b/source/rust_verify_test/tests/regression.rs
@@ -1209,3 +1209,25 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+test_verify_one_file! {
+    #[test] struct_with_updater_and_tuple_type_in_field_issue857 verus_code! {
+        use vstd::prelude::*;
+        use vstd::set::*;
+
+        pub struct S {
+            pub n: int,
+            pub s: Set<(int, int)>,
+        }
+
+        pub open spec fn f(s1: S, s2: S) -> bool {
+            s2 == S { n: s1.n + 1, ..s1 }
+        }
+
+        pub proof fn test(se: Set<(int, int)>) {
+            let s1 = S { n: 20, s: se };
+            let s2 = S { n: 21, s: se };
+            assert(f(s1, s2));
+        }
+    } => Ok(())
+}
diff --git a/source/vir/src/ast_simplify.rs b/source/vir/src/ast_simplify.rs
index 5db8c8bbd2..b4114f0cb4 100644
--- a/source/vir/src/ast_simplify.rs
+++ b/source/vir/src/ast_simplify.rs
@@ -902,8 +902,10 @@ pub fn simplify_krate(ctx: &mut GlobalCtx, krate: &Krate) -> Result<Krate, VirEr
     // Pre-emptively add this because unit values might be added later.
     state.tuple_type_name(0);
 
-    let functions = vec_map_result(functions, |f| simplify_function(ctx, &mut state, f))?;
     let mut datatypes = vec_map_result(&datatypes, |d| simplify_datatype(&mut state, d))?;
+    ctx.datatypes =
+        Arc::new(datatypes.iter().map(|d| (d.x.path.clone(), d.x.variants.clone())).collect());
+    let functions = vec_map_result(functions, |f| simplify_function(ctx, &mut state, f))?;
     let trait_impls = vec_map_result(&trait_impls, |t| simplify_trait_impl(&mut state, t))?;
     let assoc_type_impls =
         vec_map_result(&assoc_type_impls, |a| simplify_assoc_type_impl(&mut state, a))?;