[Agda] Termination checker change?

[Pierre Hyvernat]

Hi...

I've noticed that the termination checker of Agda 2.3.3 (and 2.4.1) 
doesn't accept a rather innocent function...
(Agda 2.3.2 does accept it.)


Basically, a structurally recursive function on a W-type isn't seen as 
terminating when the argument is "hidden" inside a pair whose second 
projection is a function.

Here is the problematic definition, simplified for the occasion
(<_,_> is the constructor for pairs, and Empty and Branch are 
constructors for W types)

  test : (W × (One -> One)) -> One
  test < Empty , _ > = *
  test < Branch a t , _ > = test < t (br a) , (λ _ -> *) >

and the unproblematic one (without pairs)

  test2 : W -> (One -> One) -> One
  test2 Empty r = ⋆
  test2 (Branch a t) _ = test2 (t (br a)) (λ _ -> *)


test is tagged as non-terminating while test2 is tagged as 
terminating...

(Note that replacing "One -> One" by "One" in the type of test doesn't 
show the problem!)


Is there an explanation, or is that a bug?


===== 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

  -- non-terminating!!!
  test : (W × (One -> One)) -> One
  test < Empty , _ > = *
  test < Branch a t , _ > = test < t (br a) , (λ _ -> *) >

  -- terminating
  test2 : W -> (One -> One) -> One
  test2 Empty r = *
  test2 (Branch a t) _ = test2 (t (br a)) (λ _ -> *)

  --terminating
  test3 : (W × One) -> One
  test3 < Empty , _ > = *
  test3 < Branch a t , _ > = test3 < t (br a) , * >
==========

Pierre
-- 
We biologists have a special word for stable.
It is "dead".