20070604-1

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.