[ fix #7392 ] Ensure wildcards and variable instances are kept

[jespercockx]

This fixes #7392 by always preserving variables and wildcards as let bindings if they are instances. This got a bit fiddlier that I'd like because we don't want to add a let binding when the variable or wildcard corresponds to a variable in the context that is already bound as an instance. To make up for the messiness, I also simplified some of the existing logic.

[andreasabel]

Seems test/interaction/Issue2183 got a name change:

-((last . 2) . (agda2-make-case-action '("foo zero refl = ?" "foo (suc m) refl = ?")))
+((last . 2) . (agda2-make-case-action '("foo zero refl = ?" "foo (suc n) refl = ?")))

There is also a failure of the std-lib test. Why does the workflow pull agda/agda-stdlib#52e361da32173aa7cf12fccdd923a446549ddfa7 when experimental is set to agda/agda-stdlib#b0505d661fbbfecf7ffeae20cc4b48c8ef41e078 ?
https://github.com/agda/agda/actions/runs/14627339257/job/41042832980?pr=7819#step:2:106

[jespercockx]

There's two other failures in the interaction test suite, as well as a failure in the standard library. It seems this PR which was meant as a simple fix triggers some other unexpected behaviors, I'll have to investigate further.

[plt-amy]

The two other interaction tests are also different names getting chosen, which I guess I could see the contents of this PR causing; but the stdlib failures are Haskell build plan issues, which seem to be because of an unrelated bump to the submodule?

[andreasabel]

but the stdlib failures are Haskell build plan issues, which seem to be because of an unrelated bump to the submodule?

I can't really explain this because the submodule is not bumped in this PR. Maybe a rebase will magically fix it?

[plt-amy]

I didn't check it out locally but it was my guess because GitHub seems to think the submodule changed: https://github.com/agda/agda/pull/7819/files#diff-84d0ef8629c8f1a8ae111de4886ae863f654076e5fb2f611fd38134ac52db3df

[andreasabel]

@plt-amy: thanks, this change somehow slipped my attention.

make fast-forward-std-lib gets the std-lib submodule back to experimental. I pushed a commit to this extent.

@jespercockx You might have accidentally packed in the std-lib submodule in your commit. This happens for me e.g. if I do a stage all in magit, then I have to explicitly unstage the submodules.

[andreasabel]

The more serious problem is that one test got broken:

--- a/test/interaction/ExpandEllipsis.out
+++ b/test/interaction/ExpandEllipsis.out
@@ -1,12 +1,28 @@
 (agda2-status-action "")
 (agda2-info-action "*Type-checking*" "" nil)
 (agda2-highlight-clear)
+(agda2-info-action "*Error*" "ExpandEllipsis.agda:22.1-8: error: [IllTypedPatternAfterWithAbstraction] Ill-typed pattern after with abstraction: _ (perhaps you can replace it by `_`?) when checking the clause left hand side ExpandEllipsis.with-28 q _" nil)
+((last . 3) . (agda2-maybe-goto '("ExpandEllipsis.agda" . 343)))
+(agda2-highlight-load-and-delete-action)
+(agda2-status-action "")
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-info-action "*Error*" "ExpandEllipsis.agda:22.1-8: error: [IllTypedPatternAfterWithAbstraction] Ill-typed pattern after with abstraction: _ (perhaps you can replace it by `_`?) when checking the clause left hand side ExpandEllipsis.with-28 q _" nil)
+((last . 3) . (agda2-maybe-goto '("ExpandEllipsis.agda" . 343)))
+(agda2-highlight-load-and-delete-action)
+(agda2-status-action "")
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-info-action "*Error*" "ExpandEllipsis.agda:22.1-8: error: [IllTypedPatternAfterWithAbstraction] Ill-typed pattern after with abstraction: _ (perhaps you can replace it by `_`?) when checking the clause left hand side ExpandEllipsis.with-28 q _" nil)
+((last . 3) . (agda2-maybe-goto '("ExpandEllipsis.agda" . 343)))
+(agda2-highlight-load-and-delete-action)
+(agda2-status-action "")
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-info-action "*Error*" "ExpandEllipsis.agda:22.1-8: error: [IllTypedPatternAfterWithAbstraction] Ill-typed pattern after with abstraction: _ (perhaps you can replace it by `_`?) when checking the clause left hand side ExpandEllipsis.with-28 q _" nil)
+((last . 3) . (agda2-maybe-goto '("ExpandEllipsis.agda" . 343)))
+(agda2-highlight-load-and-delete-action)
 (agda2-status-action "")
-(agda2-info-action "*All Goals*" "?0 : Nat ?1 : q ?2 : Nat " nil)
-((last . 1) . (agda2-goals-action '(0 1 2)))
-((last . 2) . (agda2-make-case-action '("test0 x | q = ?")))
-((last . 1) . (agda2-goals-action '(0 1 2)))
-((last . 2) . (agda2-make-case-action '("test1 (zero _) | q = ?")))
-((last . 1) . (agda2-goals-action '(0 1 2)))
-((last . 2) . (agda2-make-case-action '("test1 {.(suc n)} (suc {n} i) | q = ?")))
-((last . 1) . (agda2-goals-action '(0 1 2)))

[andreasabel]

Breaks test/interaction/ExpandEllipsis