mk_EqualityType_ind missing *_def theorem for imported mutual datatype

[xxnapaxx]

HOL4/CakeML translator missing theorem PoC

This is a minimal reproducer for a CakeML translator exception in ml_translatorLib.mk_EqualityType_ind.

Reproduce

The PoC files are stored with .txt extensions for issue upload. Before running, restore these names in this directory:

Holmakefile.txt -> Holmakefile
baseScript.sml.txt -> baseScript.sml
pocScript.sml.txt -> pocScript.sml

Then build the poc theory object with CAKEMLDIR set to a CakeML source checkout:

CAKEMLDIR=/path/to/cakeml/source Holmake -q clean
CAKEMLDIR=/path/to/cakeml/source Holmake -j 1 -q pocTheory.uo

pocTheory.uo is not an input file that must already exist. It is the Holmake target for the theory declared by Theory poc in pocScript.sml.
Passing pocScript.sml as the target would only name an existing source file;
it would not request the compiled HOL theory object.

Observed

While register_type handles a datatype group imported from another theory, it prints this internal exception:

Exception raised at ml_translatorLib.mk_EqualityType_ind:
at DB.fetch: theorem poc$BASE_B_TYPE_def not found

The last line uses the public EqualityType_rule API for the same type so the
PoC exits non-zero instead of only printing the swallowed exception.

Expected

The translator should either find the theorem generated for the mutually recursive type invariant group or report a coherent public failure that does not depend on a non-existent per-type _def theorem.

Log

<<HOL message: Created theory "base">>
Saved theorem _______ "datatype_a"
Saved theorem _______ "a_11"
Saved theorem _______ "a_nchotomy"
Saved theorem _______ "a_Axiom"
Saved theorem _______ "a_induction"
Saved theorem _______ "a_case_cong"
Saved theorem _______ "a_case_eq"
Saved theorem _______ "b_11"
Saved theorem _______ "b_distinct"
Saved theorem _______ "b_nchotomy"
Saved theorem _______ "b_Axiom"
Saved theorem _______ "b_induction"
Saved theorem _______ "b_case_cong"
Saved theorem _______ "b_case_eq"
<<HOL message: Defined types: "a", "b">>
Exporting theory "base" ... done.
Theory "base" took 0.01444s to build
Exporting theory "base" ... done.
Theory "base" took 0.08735s to build
<<HOL message: Created theory "poc">>
Loading translation: basisProg ... done.
Adding type :a
Adding type :b
Adding nsLookup representation thms for 568 consts [basisProg_env_9, basisProg_env_8, ..., SexpProg_env]
Adding nsLookup representation thms for [init_env]
<<HOL message: Termination argument ignored (term. proved automatically)>>
Saved definition ____ "BASE_A_TYPE_def"
<<HOL warning: ThmSetData.revise_data:
Theorems in set "compute":
ADD<poc$BASE_A_TYPE_def>
invalidated by NewBinding("BASE_A_TYPE_def", {private=false,loc=Unknown,class=Thm})>>
Saved theorem _______ "BASE_A_TYPE_def"
Attempting proof of: EqualityType BASE_A_TYPE

Exception raised at ml_translatorLib.mk_EqualityType_ind:
at DB.fetch: theorem poc$BASE_B_TYPE_def not found
.. cannot do EqualityType proof.
Attempting proof of: EqualityType BASE_B_TYPE

Exception raised at ml_translatorLib.mk_EqualityType_ind:
at DB.fetch: theorem poc$BASE_B_TYPE_def not found
.. cannot do EqualityType proof.
Adding type :a.
Saved theorem _______ "nsLookup_poc_env_pfun_eqs"
Proof of

EqualityType BASE_B_TYPE

failed.
error in quse /home/napa/sora/.harness/issue-artifacts/hol4-missing-theorem/pocScript.sml : HOL_ERR (HOL_ERROR {message = "QCHANGED_CONSEQ_CONV", origins = [{origin_function = "ConseqConv", origin_structure = "bool", source_location = Loc_Unknown}]})
error in load /home/napa/sora/.harness/issue-artifacts/hol4-missing-theorem/pocScript : HOL_ERR (HOL_ERROR {message = "QCHANGED_CONSEQ_CONV", origins = [{origin_function = "ConseqConv", origin_structure = "bool", source_location = Loc_Unknown}]})
Uncaught exception at /home/napa/.local/share/HOL/src/1/Tactical.sml:74: HOL_ERR (HOL_ERROR {message = "QCHANGED_CONSEQ_CONV", origins = [{origin_function = "ConseqConv", origin_structure = "bool", source_location = Loc_Unknown}]})

End of Log

baseScript.sml.txt
Holmakefile.txt
pocScript.sml.txt
README.md

[xrchz]

The pocScript.sml here looks like nonsense to me. This is mixing old-style and modern Theory syntax. But more importantly, this is not using the translator APIs in any way that makes sense. For reference here's the pocScript.sml:

open HolKernel Parse boolLib bossLib;
open preamble basis ml_translatorLib ml_progLib;
Theory poc
Ancestors base basis_ffi
Libs preamble basis ml_translatorLib ml_progLib
val _ = translation_extends "basisProg";
val _ = register_type ``:a``;
val _ = EqualityType_rule [] ``:b``;
val _ = export_theory ();

[xxnapaxx]

Thanks, I understand your point. Please treat this reproducer as-is.

My concern was mainly the failure mode: an internal-looking exception is printed/exposed, and the run then fails in a confusing way. Personally I do not consider that good behavior for a public tool/API; unsupported input should ideally fail with a clearer public-facing error.

That said, I respect your assessment and the project’s priorities. Please feel free to close this if you do not think it is actionable.

[ordinarymath]

IMO this is not a HOL issue it's a CakeML translator issue... CakeML is making incorrect assumptions and expecting something to be a HOL4 api when it's not.