[Agda] Termination checking regression (Matrix-shaped orders?)

[Dominique Devriese]

All,

I have some code that used to termination check, but which no longer
does with the Darcs version of Agda, perhaps due to the 18-2-2013
change titled "Disabled matrix-shaped orders in the termination
checker."?

The problem seems to be that (suc n, t) is no longer considered
smaller than (n, lambda s t).  Defining SomeExpr as an inductive data
type instead of a record does not seem to help, so it does not appear
to be caused by the record eliminator translation...

Can anyone suggest an alternative way to make this termination check
with the current Agda? Note: I would like to keep using the Induction
stuff, although the reason I need it is not shown in this simplified
example.

Thanks
Dominique

  module Test where

  open import Data.Unit
  open import Data.Nat
  open import Data.Fin
  open import Data.Product

  -- simplified from Induction (standard lib)
  RecStruct : Set → Set₁
  RecStruct A = (A → Set) → (A → Set)

  RecursorBuilder : {A : Set} → RecStruct A → Set₁
  RecursorBuilder Rec = ∀ P → (∀ x → Rec P x → P x) → ∀ x → Rec P x

  data Expr (n : ℕ) : Set where
    var      : (x : Fin n) → Expr n
    lambda   : (s : Expr n) → (t : Expr (suc n)) → Expr n
    appl     : (f : Expr n) → (val : Expr n) → Expr n

  SomeExpr : Set
  SomeExpr = ∃ Expr

  SyntacticInductionStruct : RecStruct SomeExpr
  SyntacticInductionStruct P (n , var x) = ⊤
  SyntacticInductionStruct P (n , lambda s t) = P (n , s) × P (suc n , t)
  SyntacticInductionStruct P (n , appl f val) = P (n , f) × P (n , val)

  rec-builder : RecursorBuilder SyntacticInductionStruct
  rec-builder P f (n , var x) = tt
  rec-builder P f (n , lambda s t) =
    f (n , s) (rec-builder P f (n , s)) , f (suc n , t) (rec-builder P
f (suc n , t))
  rec-builder P f (n , appl f′ val) =
    f (n , f′) (rec-builder P f (n , f′)) , f (n , val) (rec-builder P
f (n , val))