[Agda] strange Termination problem

[mechvel at scico.botik.ru]

Please, why does  Agda 2.6.2.1  reports "Termination checking failed"
for the following program?
(not a full code)

------------------------------------------------------
foo :  ∀ {e lev} → e ReducesLevel lev →
                  sizeHead (reduceLevel e lev) <nn (lSize lev)

foo {e} {d , ps} (d≢0 , any-e-reduces-ps) =
                         aux d ps d≢0 any-e-reduces-ps
   where
   aux : (d : ℕ) (ps : Patterns) → d ≢ 0 →
         let lev = (d , ps)
         in
         Any (e Reduces_) ps →
         sizeHead (reduceLevel e lev) <nn (lSize lev)

   aux 0       _             _     _                  =  anything
   aux _       _             _     (there _)          =  anything
   aux (suc d) (p ∷ [])      _     (here e-reduces-p) =  anything
   aux (suc d) (p ∷ p' ∷ ps) 1+d≢0 (here e-reduces-p) =

     aux' (e reduces? p) (any? (e reduces?_) (p' ∷ ps))  -- line 1669
     where
     1+d = suc d

     lev tail : DimLevel
     lev  = (1+d , p ∷ p' ∷ ps)
     tail = (1+d , p' ∷ ps)

     |pp'ps|          = length (p ∷ p' ∷ ps)
     redexes          = reduceLevel e lev
     tail-redexes     = reduceLevel e tail
     sh[tail-redexes] = sizeHead tail-redexes
     d₂    = proj₁ sh[tail-redexes]
     |ps₂| = proj₂ sh[tail-redexes]

     aux' :  Dec (e Reduces p) → Dec (Any (e Reduces_) (p' ∷ ps)) →
             sizeHead (reduceLevel e lev) <nn (1+d , |pp'ps|)

     aux' (no ¬reduces-p) _  = contradiction e-reduces-p ¬reduces-p
     aux' (yes reduces-p) (no ¬e-reduces-any-p'ps) =  anything
     aux' (yes reduces-p) (yes e-reduces-any-p'ps) =

       aux'' (d₂ <? 1+d) (aux 1+d (p' ∷ ps) 1+d≢0 e-reduces-any-p'ps)  -- 
line 1691
       where
       aux'' : Dec (d₂ < 1+d) → sh[tail-redexes] <nn (lSize tail) →
                                sizeHead redexes <nn (1+d , |pp'ps|)
       aux'' _ _ = anything
------------------------------------------------------


It reports
-----------------------------
Termination checking failed for the following functions:
Problematic calls:
  aux' (e reduces? p) (any? (_reduces?_ e) (p' ∷ ps))
     (at  1669,29-33)

  aux (1+d d p p' ps 1+d≢0 e-reduces-p) (p' ∷ ps) 1+d≢0 
e-reduces-any-p'ps
     (at  1691,34-37)
-----------------------------

The only recursive call is for  aux.
The head call is
   aux (suc d) (p ∷ p' ∷ ps) 1+d≢0 (here e-reduces-p).

It calls for
   aux' (e reduces? p) (any? (e reduces?_) (p' ∷ ps)).

And this latter calls for
   aux'' (d₂ <? 1+d) (aux 1+d (p' ∷ ps) 1+d≢0 e-reduces-any-p'ps)

The latter call for  aux  has  (p' ∷ ps)
among arguments,
while the head call of  aux  had  (p ∷ p' ∷ ps)
for this argument.

{-# OPTIONS --termination-depth=3 #-}  does not help.

Can you, please, give a hint:
why structural recursion does not work here?


Also the report prints  "aux (1+d d p p' ps 1+d≢0 e-reduces-p) ..."
instead of
         "aux (1+d (p' ∷ ps) 1+d≢0 e-reduces-p) ...".

It is misleading, because  aux  has four arguments,
while the report prints six arguments.

?

------
Sergei