[CakeML-dev] [ExternalEmail] Re: "Overloading constraints were unsatisfiable"

Michael.Norrish at data61.csiro.au Michael.Norrish at data61.csiro.au
Mon Jan 9 23:16:31 UTC 2017


I hope the latest commit of mine (7f2c629) to HOL improves this situation a bit.

Let me know of any examples that you think warrant better error messages.

Michael

On 6/1/17, 14:02, "Michael.Norrish at data61.csiro.au" <Michael.Norrish at data61.csiro.au> wrote:

    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.
    
    Michael
    
    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.
        
        Scott
        _______________________________________________
        Developers mailing list
        Developers at cakeml.org
        https://lists.cakeml.org/listinfo/developers
        
    
    _______________________________________________
    Developers mailing list
    Developers at cakeml.org
    https://lists.cakeml.org/listinfo/developers
    



More information about the Developers mailing list