[CakeML-dev] Translation failure

[Scott Owens]

I’m seeing the translator fail on a pretty simple function that coverts inferencer types to strings in inferProgScript.sml on the type-error-loc branch. The error message is unhelpful.

Improved induction theorem: inf_type_to_string_ind
Failed translation: inf_type_to_string, inf_types_to_string
Exception- HOL_ERR {message = "not an \"=\"", origin_function = "dest_eq(_ty)", origin_structure = "boolSyntax"} raised

Does anyone have any ideas what the problem might be, or tips on debugging translator failures?

Scott