Agsy/Auto panics with -r in the presence of a pattern synonym

[kindaro]

See:

module x where

data X : Set
  where x : X

pattern y = x

theorem : X
theorem = {-r }0

(You will need to erase the hole and make a new one in the same place for Agda to understand what you mean.)

If you try to fill the hole with automatic proof search, you will see an error like this:

Panic: Unbound name: x.y[0,6]@ModuleNameHash 15504699851561257075

Without -r, the hole is automatically filled with y.

I am on Agda 2.6.3 built recently from source.

[andreasabel]

Thanks for reporting, @kindaro. Auto has no maintainer, so there is little hope this is going to be fixed...

[kindaro]

Wow well good to know. I am learning Agda yet so I cannot solve this myself but maybe some time later I could!

[jespercockx]

This might be the same problem as #5551, so not a problem with auto itself after all.