[CakeML-dev] "Overloading constraints were unsatisfiable"

Scott Owens S.A.Owens at kent.ac.uk
Thu Jan 5 14:29:49 UTC 2017

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.


More information about the Developers mailing list