[Agda] heap mistery

[Martin Escardo]

This is regarding a heap-exhaustion problem I discussed earlier.

I prove an existential Theorem, and then define

program₁ : ₂ℕ → ℕ → ₂
program₁ α m = ∃-witness(Theorem α m)

program₂ : ₂ℕ → (m : ℕ) → (smaller(m + 1) → ℕ)
program₂ α m = ∃-witness(∃-elim (Theorem α m))

This makes Agda compilation run for some time until the heap is exhausted.

Now I instead define the two programs by pattern matching rather than
the destructors ∃-witness and ∃-elim (first and second projection):

program₁ : ₂ℕ → ℕ → ₂
program₁ α m = f(Theorem α m)
  where
   f : Finite-Pigeonhole α m → ₂
   f(∃-intro b proof) = b                 -- f is ∃-witness!!!

program₂ : ₂ℕ → (m : ℕ) → (smaller(m + 1) → ℕ)
program₂ α m = f(Theorem α m)
  where
   f : Finite-Pigeonhole α m → (smaller(m + 1) → ℕ)
   f(∃-intro b (∃-intro s proof)) = s     -- f is ∃-witness o ∃-elim!!!

Compilation is instanteneous and succeeds using neglegible memory.

What is going on?

This is how I defined ∃-witness and ∃-elim:

data ∃ {X : Set} (A : X → Ω) : Ω where
      ∃-intro : (x₀ : X) → A x₀ → ∃ \(x : X) → A x

∃-witness : {X : Set} {A : X → Ω} → (∃ \(x : X) → A x) → X
∃-witness (∃-intro x a) = x

∃-elim : {X : Set} {A : X → Ω} →
   (proof : ∃ \(x : X) → A x) → A (∃-witness proof)
∃-elim (∃-intro x a) = a

That is, using the same kind of pattern matching!!!

Thanks,
Martin