From 0df4ef66155bb0760b3093f40165d5e320040f88 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Fri, 30 Jun 2023 20:59:35 -0700
Subject: [PATCH] add a test that fails compilation: incomplete type generated
 too early

---
 test/MutualStruct.fst | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/test/MutualStruct.fst b/test/MutualStruct.fst
index e4259e349..17ca28b75 100644
--- a/test/MutualStruct.fst
+++ b/test/MutualStruct.fst
@@ -87,3 +87,27 @@ and object6_pair = {
   object6_pair_payload: object6;
 }
 *)
+
+// This test extracts. It should compile, but the C compiler complains with object7_pair incomplete because KaRaMeL extracted it too early
+
+noeq
+type object7_tagged = {
+  object7_tagged_tag: U64.t;
+  object7_tagged_payload: ref object7;
+}
+and object7_map = {
+  object7_map_entry_count: U64.t;
+  object7_map_payload: ref object7_pair;
+}
+and object7_case = {
+  object7_case_tagged: object7_tagged;
+  object7_case_map: object7_map;
+}
+and object7 = {
+  object7_type: U8.t;
+  object7_payload: object7_case;
+}
+and object7_pair = {
+  object7_pair_fst: object7;
+  object7_pair_snd: object7;
+}