fix tuple types slipping through ast_simplify, fixes #857

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(())
+}

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))?;