[Agda] Termination checking

[Francesco Mazzoli]

Why doesn't the following definition pass the termination checker?

````
lookup : ∀ {ol nl} d -> Fin ol -> Subst d ol nl -> Tm nl
lookup .0               v       id                    = var v
lookup d                zero    (t ∷ ρ)               = t
lookup d                (suc v) (t ∷ ρ)               = lookup d v ρ
lookup .(suc (d₁ + d₂)) v       (⟦_⟫_⟧ {d₁} {d₂} ρ σ) = lookup (d₁ +
d₂) v (ρ ⟫ σ)
````

The problemating call is the last one, but it should be fairly clear
that `lookup` is structural on d.

The full listing:

````
mutual
  data Tm (l : ℕ) : Set where
    var   : Fin l -> Tm l
    _·_   : Tm l -> Tm l -> Tm l
    lam   : Tm (suc l) -> Tm l
    ⟦_,_⟧ : ∀ {d ol} -> Tm ol -> Subst d ol l -> Tm l

  data Subst : (d : ℕ)(ol : ℕ)(nl : ℕ) -> Set where
    id    : ∀ {ol} -> Subst 0 ol ol
    _∷_   : ∀ {d ol nl} -> Tm nl -> Subst d ol nl -> Subst d (suc ol) nl
    ⟦_⟫_⟧ : ∀ {d₁ d₂ ol l nl} -> Subst d₁ ol l -> Subst d₂ l nl ->
Subst (suc (d₁ + d₂)) ol nl

_⟫_ : ∀ {d₁ d₂ ol l nl} -> Subst d₁ ol l -> Subst d₂ l nl -> Subst (d₁
+ d₂) ol nl
id ⟫ σ = σ
(t ∷ ρ) ⟫ σ = ⟦ t , σ ⟧ ∷ (ρ ⟫ σ)
_⟫_ .{suc (d₁ + d₂)} {d₃} {ol} {_} {nl} (⟦_⟫_⟧ {d₁} {d₂} ρ σ) γ =
  subst (λ d → Subst d ol nl) (lm d₁ d₂ d₃) (ρ ⟫ ⟦ σ ⟫ γ ⟧)
  where
    lm : ∀ n m k -> n + suc (m + k) ≡ suc (n + m + k)
    lm zero m k = refl
    lm (suc n) m k = cong suc (lm n m k)

lookup : ∀ {ol nl} d -> Fin ol -> Subst d ol nl -> Tm nl
lookup .0               v       id                    = var v
lookup d                zero    (t ∷ ρ)               = t
lookup d                (suc v) (t ∷ ρ)               = lookup d v ρ
lookup .(suc (d₁ + d₂)) v       (⟦_⟫_⟧ {d₁} {d₂} ρ σ) = lookup (d₁ +
d₂) v (ρ ⟫ σ)
````

Francesco