The translator should not accept types where mangled constructor names would clash

[oskarabrahamsson]

The translator mangles the names of functions and type constructors to fit with the CakeML grammar. This mangling can produce non-distinct constructor names, which makes the translator fail. This issue is about how this failure should look.

Here is a minimal example where the translator renames both constructors to A:

Datatype: foo = a | A int
End
val r = register_type “:foo”;

It would be good if the system did a sanity-check and failed early with a descriptive error message that explained why this datatype definition won't work (e.g. "name mangling produces duplicate constructor id's" or something). Instead it fails later when trying to prove an EqualityType theorem:

Attempting proof of: EqualityType SCRATCH_FOO_TYPE
Exception- HOL_ERR {message = "unsolved goals", origin_function = "TAC_PROOF", origin_structure = "Tactical"} raised

[myreen]

One could address a slightly broader question: should the translator mangle names at all and if so how?

The current way it changes constructor names is a bit arbitrary. Note that the translator usually does not have to change the names at all, e.g. as far as the CakeML semantics is concerned names a and A are both fine constructor names (the only problem is that users can't type a in concrete syntax and have it parsed correctly).

[oskarabrahamsson]

One could address a slightly broader question: should the translator mangle names at all and if so how?

I agree that it should be an option whether or not to mangle names, but I think the issue here is not that the translator makes a choice, but that:

• it keeps the user in the dark about it
• it fails late in a mysterious way when it could fail early and explain why.

There are other things that should cause the translator to fail early, for instance when the definition you give the translator contains an unknown constant, or other things that can be detected without attempting costly theorem proving.