[CakeML-dev] "Overloading constraints were unsatisfiable"

[Scott Owens]

As I’m trying to update the source_to_mod lang proofs, I’m spending a lot of time trying to fix theorem statements where the HOL error message is 

Exception- HOL_ERR {message = "in unknown location:\nOverloading constraints were unsatisfiable", origin_function = "type-analysis", origin_structure = "Preterm"} raised

with *no* error location.

This is really annoying, and I guess is stems from using the same names for everything in the source and mod semantic theories.

Any hints on how to get some more effective error messages would be great. Ultimately, I guess that HOL itself needs to improve.

Scott