[Agda] On termination checkers

[david.janin at labri.fr]

Hello,

While translating from CoQ to Agda the paper [I] « One Monad to Prove Them All » 
by Sandra, Dylus, Jan Christiansen, and Finn Teegen,  I am bumping into the following 
feature of Agda termination checker that sounds (to me)  quite uncomfortable.

Simply (and possibly wrongly) said, it seems that with nested data type definitions, 
helper functions on the most nested type cannot be used in inductive definitions of 
functions on the least nested one. Instead, we are forced (at least I feel forced)  
to inline / unfold these helper functions by hand, and later redo proofs about them.

Of course, this feature does not reduce the set of possible inductive definitions but 
make them more tedious to write down. With data types parameterized by Free Functor 
as in [I], this forbids (me) using bind in recursive function over these types, which is a burden…

I guess this is a story well known by experts in Agda, 
and I’ve noticed in Jesper thesis (Example 2.32. p 57) that
there are indeed tricky issues around this problem.

Still, how can I cope with it ? Any suggestion much welcome, 

Best, 
David

***
Below the simplest example I could build illustrating my point.
The same example, given below, is accepted in CoQ.

*** in Agda

data Pack  (A : Set) : Set where
 pack : A -> Pack  A

unpack : ∀ {A} -> Pack A -> A
unpack (pack a) = a

data PList (A : Set) : Set where
 pnil : PList A
 pcons : A -> Pack (PList A) -> PList A

pappend : ∀ {A : Set} -> PList A  -> PList A   -> PList A
pappend {A} pnil l = l
pappend {A} (pcons a pp@(pack l')) l
--  = pcons a (pack (pappend   l' l))  -- (1) termination check succeeds
 = pcons a (pack (pappend  (unpack pp) l))  — (2) termination check fails

*** in CoQ

Inductive Pack (A : Type) : Type :=
 pack : A -> Pack A.

Arguments pack : default implicits.

Definition unpack  {A : Type} (pp : Pack A) : A :=
 match pp with
    pack a =>  a
 end.

Inductive PList (A : Type) : Type :=
 pnil : PList A
| pcons : A -> Pack (PList A) -> PList A.

Arguments pcons : default implicits.
Arguments pnil {A}.

Fixpoint pappend {A : Set} (l1 l2 : PList A) : PList A :=
 match l1 with 
   pnil => l2
  | pcons x pp => pcons x (pack (pappend (unpack pp) l2))
 end.