It should be possible to detect termination when an argument is smaller than a *dotted* pattern. For instance, the following code should terminate:

module Test where data Nat : Set where zero : Nat suc : Nat -> Nat data Bool : Set where true : Bool false : Bool _&&_ : Bool -> Bool -> Bool true && b = b false && b = false data Ty : {_ : Nat} -> Set where Base : forall {n} -> Ty {suc n} Arr : forall {n} -> Ty {n} -> Ty {n} -> Ty {suc n} subty : forall {n} -> Ty {n} -> Ty {n} -> Bool subty Base Base = true subty (Arr σ τ) (Arr σ' τ') = subty σ' σ && subty τ τ' subty _ _ = false

Currently the termination checker cannot see that in both the two recursive calls of `subty`

the first (hidden) argument is strictly smaller than on the LHS.

Andreas: Discussed that with Ulf. The internal syntax erases the dotted patterns constructed during pattern checking. This is an optimization for speeding up execution, but the "logical" reading (fully reconstruced form) of the second clause is

subty {suc n} (Arr {n} σ τ) (Arr {n} σ' τ') = subty {n} σ' σ && subty {n} τ τ'

To keep internally a fully reconstructed form is probably not only useful for the termination checker but also for other static analyses.

To print back the fully reconstructed form, as for instance Twelf does, is also a good feedback to the user: He sees how the system "understood" his input, and he can check that it understood it correctly. See Main.PrintReconstructedTerms feature request.