"Unification incomplete for case" error message could be improved

[JonathanAldrich]

Due to a typo I put the wrong metavariable inside [brackets] in a case rule construct. This resulted in a "Unification incomplete for case" error message.

Here's the offending code:

                case rule
                    d6: e3 => e5
                    d7: e4[e3'] => e1'
                    ----------------------------- eval-let
                    _: let x = e3 in e4[x] => e1'
                is
                    proof by unproved
                end case

based on the obvious big-step rule for let. Obviously the e3' should be e5 here...but the typo was a bit hard to find.

It's probably genuinely hard to produce a good error message in this case, but I wonder if a bit of engineering could at least pinpoint e3' as the cause of the problem? In this case e3' was already bound, and e5 is fresh, so it should be possible in principle to detect that e3' is the problem.

Not super high priority but this is the kind of thing we should fix to make SASyLF more usable.

[boyland]

True. Incomplete unification is difficult technically to handle because the failure doesn't give any information. But it should be possible to rummage around and guess possible problems.

[JonathanAldrich]

I put another example of this problem in the error-examples Google Drive folder, shared with John Boyland. I'm not putting this on GitHub because it contains a partial solution to homework exercises.

[boyland]

[like] John T Boyland reacted to your message:

…

________________________________ From: Jonathan Aldrich ***@***.***> Sent: Thursday, November 14, 2024 10:08:55 PM To: boyland/sasylf ***@***.***> Cc: John T Boyland ***@***.***>; Assign ***@***.***> Subject: Re: [boyland/sasylf] "Unification incomplete for case" error message could be improved (Issue #116) I put another example of this problem in the error-examples Google Drive folder, shared with John Boyland. I'm not putting this on GitHub because it contains a partial solution to homework exercises. — Reply to this email directly, view it on GitHub<#116 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AAJDNU2QUZ7LKTL6HVFRBM32AUNPPAVCNFSM6AAAAABRZ4XGWSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDINZXGUYDKMBQGE>. You are receiving this because you were assigned.Message ID: ***@***.***>

[boyland]

The obvious helpful error message for your first example would be that the pattern restricts e3'. The easiest way to get this result would be for the unification to fail but there is a danger that this would be unsound (failed unification can lead to cases being discarded).