From 95242af3e010fe55a4bcbf85bf183227cb5634c8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 8 Feb 2022 19:51:32 +0100
Subject: Fix some issues in Invariants

---
 src/Invariants.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/Invariants.ml b/src/Invariants.ml
index fe1b5e82..fff5b897 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -442,11 +442,19 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
               fields_with_types
         (* Assumed type case *)
         | V.Adt av, T.Adt (T.Assumed aty_id, regions, tys) -> (
-            assert (av.V.variant_id = None);
+            assert (av.V.variant_id = None || aty_id = T.Option);
             match (aty_id, av.V.field_values, regions, tys) with
             (* Box *)
-            | T.Box, [ boxed_value ], [], [ boxed_ty ] ->
-                assert (boxed_value.V.ty = boxed_ty)
+            | T.Box, [ inner_value ], [], [ inner_ty ]
+            | T.Option, [ inner_value ], [], [ inner_ty ] ->
+                assert (inner_value.V.ty = inner_ty)
+            | T.Option, _, [], [ _ ] ->
+                (* Option::None: nothing to check *)
+                ()
+            | T.Vec, fvs, [], [ vec_ty ] ->
+                List.iter
+                  (fun (v : V.typed_value) -> assert (v.ty = vec_ty))
+                  fvs
             | _ -> failwith "Erroneous type")
         | V.Bottom, _ -> (* Nothing to check *) ()
         | V.Borrow bc, T.Ref (_, ref_ty, rkind) -> (
-- 
cgit v1.2.3