#664 wrongly reorders extracted C mutually recursive types with monomorphization in the middle

[tahina-pro]

Consider the following F* datatype:

module U8 = FStar.UInt8
module U64 = FStar.UInt64

noeq
type slice (a: Type0) : Type0 = { elt: ref a; len: U64.t; }

[@@no_auto_projectors]
noeq
type object9_array = {
  object9_array_length_size: U8.t;
  object9_array_ptr: slice object9_raw;
}

and object9_map = {
  object9_map_length_size: U8.t;
  object9_map_ptr: slice object9_map_entry;
}

and object9_raw =
| OBJECT9_Case_Simple: v: U8.t -> object9_raw
| OBJECT9_Case_Array: v: object9_array -> object9_raw
| OBJECT9_Case_Map: v: object9_map -> object9_raw

and object9_map_entry = {
  object9_map_entry_key: object9_raw;
  object9_map_entry_value: object9_raw;
}

Before #664, this test successfully compiled to C (with gcc 13.3.0.) But since #664, the C compiler has failed to compile it, with the following error message:

In file included from .output/MutualStruct.out/MutualStruct.c:8:
.output/MutualStruct.out/MutualStruct.h:188:15: error: field ‘object9_map_entry_key’ has incomplete type
  188 |   object9_raw object9_map_entry_key;
      |               ^~~~~~~~~~~~~~~~~~~~~
.output/MutualStruct.out/MutualStruct.h:189:15: error: field ‘object9_map_entry_value’ has incomplete type
  189 |   object9_raw object9_map_entry_value;
      |               ^~~~~~~~~~~~~~~~~~~~~~~
cc1: note: unrecognized command-line option ‘-Wno-unknown-warning-option’ may have been intended to silence earlier diagnostics
Warning 3: run_or_warn: the following command failed:
cc -I /home/tahina/everest/karamel/krmllib/dist/minimal -I /home/tahina/everest/karamel/krmllib -I /home/tahina/everest/karamel/include -I .output/MutualStruct.out -Wall -Werror -Wno-unknown-warning-option -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -Wno-parentheses -std=c11 -c .output/MutualStruct.out/MutualStruct.c -o .output/MutualStruct.out/MutualStruct.o
Warning 3 is fatal, exiting.

It turns out that #664 changed the order of data types in the extracted C header file. Before #664, they were produced in the same order as in the original F* file, and I was relying on this fact to extract EverCBOR to C, following my comment in test/MutualStruct.fst:

karamel/test/MutualStruct.fst

Lines 25 to 27 in f8832a2

	// The order of mutually recursive type
	// definitions should match that of C, in the sense that types that
	// depend on other types only behind `ref` should be defined first.

With #664, this no longer seems to be the case. Here is the diff on the produced header file:

--- MutualStruct.before.h       2026-02-05 17:23:55.072542263 +0000
+++ MutualStruct.after.h        2026-02-05 17:23:57.482542524 +0000
@@ -153,6 +157,8 @@

 typedef struct object9_raw_s object9_raw;

+typedef struct object9_raw_s object9_raw;
+
 typedef struct slice__MutualStruct_object9_raw_s
 {
   object9_raw *elt;
@@ -167,7 +173,16 @@
 }
 object9_array;

-typedef struct object9_map_entry_s object9_map_entry;
+typedef struct object9_raw_s object9_raw;
+
+typedef struct object9_raw_s object9_raw;
+
+typedef struct object9_map_entry_s
+{
+  object9_raw object9_map_entry_key;
+  object9_raw object9_map_entry_value;
+}
+object9_map_entry;

 typedef struct slice__MutualStruct_object9_map_entry_s
 {
@@ -201,13 +216,6 @@
 }
 object9_raw;

-typedef struct object9_map_entry_s
-{
-  object9_raw object9_map_entry_key;
-  object9_raw object9_map_entry_value;
-}
-object9_map_entry;
-
 bool f9(object9_map x);

[tahina-pro]

To help debug, you can use my fork's _taramana_676 branch:

• tahina-pro/karamel@d8cec62 adds the above object9 test into test/MutualStruct.fst before Fix some normalization issues in monomorphization #664 was merged
• tahina-pro/karamel@8ab12b7 merges Fix some normalization issues in monomorphization #664
• tahina-pro/karamel@4316b26 merges the latest Karamel master as of today

In all cases, you can run make -C test MutualStruct.test

[protz]

Ouch. Thanks for the repro. I'll take a look, and worst case scenario, I'll revert to the earlier logic.

Are you doing a big toolchain upgrade?

[tahina-pro]

Ouch. Thanks for the repro. I'll take a look, and worst case scenario, I'll revert to the earlier logic.
Are you doing a big toolchain upgrade?

Thanks in advance Jonathan!

As of today, EverParse master is still using Karamel fb36fec (and similarly old versions of F* and Pulse), but there is a PR, project-everest/everparse#244, which intends to upgrade EverParse to the most recent Karamel, F* and Pulse. That being said:

• That PR has a few admit()s (unrelated to Karamel) that I believe should take longer than fixing this issue here (unless I am mistaken with how hard this issue is)
• F* and Pulse are evolving fast and have needed many more code changes in EverParse than Karamel has.

So, while I intend to enable automatic upgrades of F*, Pulse, and ideally Karamel, for that PR, I would be fine with staying with an older Karamel and only taking updates to F* and Pulse, until those admit()s are fixed.

Thus, I don't believe it would be wise to revert to the old logic at this point, unless you really believe that it would be too hard to fix this issue and that reverting would have sufficiently low impact on the users of #664.