[Agda] Termination checker change?

[Pierre Hyvernat]

>Yes, indeed, the termination checker has changed, due to a soundness 
>issue.
>
>Currently, it does not look through pairs anymore, so you have to 
>curry your functions.
>
It looks a little subtler than that

  test4 : (W × (One -> One)) -> One
  test4 < Empty , f > = *
  test4 < Branch a t , f > = test4 < t (br a) , (λ x → f x) >

is accepted, while

  test3 : (W × (One -> One)) -> One
  test3 < Empty , f > = *
  test3 < Branch a t , f > = test3 < t (br a) , (λ x → x) >

is not...

(The only difference is the second component of the pair in the 
recursive call...)

Does it mean it doesn't accept any kind of deep-pattern matching?


>I have an idea to bring uncurried functions back (in a sound way), but 
>will need some time to implement it.
>
Is the actual termination checker of Agda described somewhere. Last time 
I checked, the wiki 
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.TerminationChecker
wasn't accurate.

I once had understood that the termination checker used both a variant 
of the size-change principle, together with some sized-typed principle.
If so, do the two notions interact in some non-trivial way?
A quick look at the source seems to indicate they do not...
Is that right?



===== file test.agda =====
module test where

record One : Set where constructor *

record _×_ (A : Set) (B : Set) : Set where
  constructor <_,_>
  field
    fst : A
    snd : B

module Problem (A : Set) (D : A -> Set) (br : (a : A) -> D a) where

  data W : Set where
    Empty : W
    Branch : (a : A) -> (f : (d : D a) -> W) -> W

  test3 : (W × (One -> One)) -> One
  test3 < Empty , f > = *
  test3 < Branch a t , f > = test3 < t (br a) , (λ x → x) >

  test4 : (W × (One -> One)) -> One
  test4 < Empty , f > = *
  test4 < Branch a t , f > = test4 < t (br a) , (λ x → f x) >

==========

Pierre
-- 
Things are more like they are today than they ever
were before.
    -- Dwight Eisenhower