[Agda] Strange behaviour of instance search.

[effectfully]

Hi. I want to adapt Conor McBride's trick

    https://personal.cis.strath.ac.uk/conor.mcbride/fooling/Jigger.agda

to basic encoding of STLC:

    data _⊢_ Γ : Type -> Set where
      var : ∀ {σ}   -> σ ∈ Γ     -> Γ ⊢ σ
      ƛ_  : ∀ {σ τ} -> Γ ▻ σ ⊢ τ -> Γ ⊢ σ ⇒ τ
      _·_ : ∀ {σ τ} -> Γ ⊢ σ ⇒ τ -> Γ ⊢ σ     -> Γ ⊢ τ

I started from

    _▻▻_ : Con -> Con -> Con
    Γ ▻▻  ε      = Γ
    Γ ▻▻ (Δ ▻ σ) = Γ ▻▻ Δ ▻ σ

    postulate
      naive-lam : ∀ {Γ σ τ} -> ((∀ {Δ} -> Γ ▻ σ ▻▻ Δ ⊢ σ) -> Γ ▻ σ ⊢
τ) -> Γ ⊢ σ ⇒ τ

    yellow : Term (ι ⇒ ι)
    yellow = naive-lam λ x -> x

But Agda can't infer `Δ' from (Γ ▻ σ ▻▻ Δ), since there is pattern
matching on `Δ'.
So I switched to instance arguments:

    postulate
      _extends_ : Con -> Con -> Set

      instance
        extends-stop : ∀ {Γ} -> Γ extends Γ
        extends-skip : ∀ {Γ Δ σ} {{_ : Δ extends Γ}} -> (Δ ▻ σ) extends Γ

      lam : ∀ {Γ σ τ} -> ((∀ {Δ} {{_ : Δ extends (Γ ▻ σ)}} -> Δ ⊢ σ)
-> Γ ▻ σ ⊢ τ) -> Γ ⊢ σ ⇒ τ

    I : Term (ι ⇒ ι)
    I = lam λ x -> x

    K : Term (ι ⇒ ι ⇒ ι)
    K = lam λ x -> lam λ y -> x

So far so good, but when I tried

    A : Term ((ι ⇒ ι) ⇒ ι ⇒ ι)
    A = lam λ f -> lam λ x -> f · x

Agda just started to consume memory, and I killed the process after it
had eaten 1+ GB of memory.

But if I provide instance arguments explicitly

    A : Term ((ι ⇒ ι) ⇒ ι ⇒ ι)
    A = lam λ f -> lam λ x -> f {{extends-skip {{extends-stop}}}} · x
{{extends-stop}}

Agda happily accepts the definition.

Is it the expected behaviour?

The code: https://github.com/effectfully/random-stuff/blob/master/stuff/TypedJigger.agda