Resolve type dependencies as per #357

[ssyram]

Added a new pass to resolve the type dependencies problem as mentioned in #357. The algorithm is generally as described but could be explained in more detail as that the type declarations come in the following order:

• All internal type forward declarations for structs and unions (but not enum, not type alias);
• All additional forward type declarations (will this happen? not sure, just for robustness);
• All enum type definitions --- as enum types are translated as alias of uint8_t, they have the property that: (1) they cannot be forward declared; and (2) they are standalone;
• All type alias in topological order: the above three should contain all possible types that can be referenced in type alias definitions;
• All struct/union type definitions in topological order: at this point all types that can be referenced in struct/union fields should be there;

[protz]

What I do not understand is why you need a new phase. Based on reading the code, the purpose of your patch seems to be:

• putting type declarations in topological order
• inserting forward declarations as needed to break cycles.
  This is exactly what https://github.com/FStarLang/karamel/blob/master/lib/Monomorphization.ml#L174 is doing; see also https://github.com/FStarLang/karamel/blob/master/lib/Monomorphization.ml#L364, a comment I added more recently after looking at this code.

I am wondering if you could minimize the issue. I know it's not easy, but right now it's hard to justify adding new code without a test case (for regressions) and without a clear understanding of the problem (to make sure we know why we have to add new code).

[ssyram]

Thanks for this! After a more careful inspection, I found that the issues are mainly from the newly generated types, would it be possible that the newly generated types from the pass resolving matching are not properly handled? I tried to reproduce, but the generated codes are over 40k lines and depend heavily on some other internal libraries, the error might be triggered by some complex internal inter-dependencies... So instead I would like to argue for theoretical guarantees.

Actually, in our use case there are a bunch of errors complaining both about (1) unknown identifiers, where not even the forward declaration is provided, and (2) "incomplete types" that requires full definition instead of a forward declaration.

At least by this pass, I would claim that the current PR is a more explicit (we now have an independent pass and people easily know where to resort to when they need to) and systematic approach that essentially we may easily provide a proof to the validity of the above order that we can show:

Assuming every external type does not depend on any internal type and they are properly included at the beginning, by such an order, there will be no compiler complain about (1) unknown type identifiers, (2) incomplete types and (3) incompatible type definition.

where (3) means the forward declaration kind must match that of its definition, for which typical wrong cases are the enum types, they are translated as synonym to u8, so they cannot be declared as structs. The proof is rather straightforward.

But yes, I agree that it is a problem if we don't have any test case. So I'm OK to leave this PR open until we actually find some minimal reproduction of the errors.