Tony Beta Lambda

Agda is not able to infer [this](https://gist.github.com/tonyxty/93715418155f5a2374799904b9be57ef). And I think we might need some innovation to solve inference problems for such instances.

> Agda is not able to infer [this](https://gist.github.com/tonyxty/93715418155f5a2374799904b9be57ef). Apologies, I think I might have misunderstood Agda's instance mechanism, and I need some time to revise the code. Please ignore my...

Ok, turns out it's the problem with what Agda calls "overlapping instances." If you add `OPTIONS --overlapping-instances` then the code, well, still doesn't compile and Agda enters an infinite loop....

> What we need is a BFS, but that's going to consume too much memory. So maybe we should adopt [IDDFS](https://en.wikipedia.org/wiki/Iterative_deepening_depth-first_search), which is going to guarantee a shortest instance resolution...

> Do you want to write `x.v` or just `v`? The title of the issue makes me think that you want the latter, but the text itself has the former...

How about an extra setup option, something like ````lua require("nvim-tree").setup({filters = { find_filtered = "unhide" // "ignore", "alert", "unhide" }})

nay, the problem seems to persist

and it seems that I can't reopen the issue. perhaps some repo collaborator can verify the problem and reopen it?