[Agda] Strange behaviour of instance search.

[effectfully]

Nils Anders Danielsson, thanks for the response. It's a neat trick,
but it comes at the price of additional pattern matching on indices in
every function, defined by recursion on contexts. I would also need to
write (∀ {n} {Γ : Con n} -> e) instead of (∀{Γ} -> e). And it looks a
bit strange to change the encoding because of syntactic sugar. I can
define two kinds of terms, indexed by two kinds of contexts... Not
sure.

Anyway, that's a useful and general technique, which I'll be keeping in mind.

BTW, we can generalize the Jigger a bit to write things like

    example : Syntax 0
    example = 3 # λ h f x → (1 # λ t → t · h) · (f · x)

https://github.com/effectfully/random-stuff/blob/master/stuff/NaryJigger.agda