[CakeML-dev] "Overloading constraints were unsatisfiable"

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Thu Jan 5 15:46:52 UTC 2017


Two things you can try include:

When you run into this error, write explicit theory qualifiers on some
of the constants in your statement and try again. If you disambiguate
the overloading sufficiently, you might get a more informative type
error message.

Overload the ambiguous constants temporarily within the theory to
non-ambiguous names (within that theory) and use those instead.

On 5 January 2017 at 06: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.
>
> Scott
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers



More information about the Developers mailing list