[CakeML-dev] "Overloading constraints were unsatisfiable"

Michael.Norrish at data61.csiro.au Michael.Norrish at data61.csiro.au
Fri Jan 6 03:02:47 UTC 2017

I agree that these are annoying – and they’re the result of changes I made to the parsing and type-checking infrastructure relatively recently, so I think the situation is worse than it used to be. I’ll try to isolate a test case and improve things.  

In the short term, having less overloading (as suggested) is the way to go. 

This can be done in big swoops by using set_grammar_ancestry after a call to new_theory to make parsing happen only with respect to particular ancestries.


On 5/1/17, 22:29, "Scott Owens" <S.A.Owens at kent.ac.uk> wrote:

    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.
    Developers mailing list
    Developers at cakeml.org

More information about the Developers mailing list