Translating mutually recursive datatypes produces a bunch of warnings

[ordinarymath]

Doing

Datatype:
  a = A b ;
  b = B a | C num
End

and then calling

val _ = register_type ``:a``;

produces a bunch of warnings.
As far as I can remember these warnings are indeed that the equality thm not being proved.
Even if it's spurious it needs redesign anyway to remove the exception driven control flow.
In the case of the warning being invalid it's probably mk_EqualityType_thm succeeding once and failing for the rest of the cases.
I believe the fix should probably be replacing this bit below

cakeml/translator/ml_translatorLib.sml

Lines 1611 to 1612 in 87d99d1

	val eq_lemmas = (map (fn ty => (ty, mk_EqualityType_thm is_exn_type ty
	|> simp_eq_lemma)) tys)

with some call to a mk_EqualityType_thms which is mk_EqualityType_thm refactored. You can't really separate the equality proof anyway and do it one by one.

Stuff to do to ensure this is fixed (assuming equality thms aren't being proved) .
Add a translation of a function that calls equality of the mutually recursive type to the ml_translator_testScript. Note it's just extending this bit

cakeml/translator/ml_translator_testScript.sml

Lines 14 to 28 in 87d99d1

	Datatype:
	a_ty = A1 | B1 (b_ty list) ;
	b_ty = B2 | A2 a_ty
	End
	val _ = register_type “:a_ty”;
	val ty = “:a_ty”;
	Definition dest_A2_def:
	dest_A2 (A2 a) = SOME a ∧
	dest_A2 _ = NONE
	End
	val r = translate dest_A2_def;

NB: also can be used to check if the warnings are spurious.

Also right now ml_translator_testScript already spews out these warnings if I can remember correctly. It doesn't translate a function which calls equality for the mutrec datatype though.

Note I haven't looked at the translator deeply in sometime but I recall this issue and was planning to fix it but ran out of cycles.