[Agda] Termination checker change?

[Andreas Abel]

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.

I have an idea to bring uncurried functions back (in a sound way), but 
will need some time to implement it.

Cheers,
Andreas

On 05.06.2014 16:09, Pierre Hyvernat wrote:
> 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


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/