[Agda] using (Acc _<_)

[Sergei Meshveliani]

Dear all,

I wonder why the version II below is not type-checked:

--------------------------------------------------
{-# OPTIONS --termination-depth=2 #-}

foo : (x : Bin) (nz : x ≢ 0#) → Acc _<_ x →
let 2x≢0 = x≢0⇒2x≢0 nz
in
2* x < 2^ (1+ (log₂ (2* x) 2x≢0))

foo 0# nz _ = contradiction refl nz
foo (2suc x) x'≢0 (acc wf-x') =
-- acc-x' -- II
...
where
sx = suc x; x' = 2suc x
2x'≢0 = x≢0⇒2x≢0 x'≢0; 2sx≢0 = x≢0⇒2x≢0 suc≢0; sx<x' = suc<2suc x

-- acc-sx : Acc _<_ sx -- II
-- acc-sx = acc-2suc⇒acc-suc acc-x'

lt0 : 2suc x < 2^ (log₂ (2* (2suc x)) 2x'≢0)
lt0 =
begin
2suc x ≡[ 2suc-as∘ x ]
2* sx <[ foo sx suc≢0 (wf-x' _ sx<x')
-- acc-sx -- II
]
...

∎
-----------------------------------------------------

The code is not self-contained, but I hope, Agda developers can explain
the effect.

Here foo is applied recursively to the argument sx, which is smaller
than x'.
There are three places marked with "II".
The version II is produced by
* changing (acc wf-x') to the variable acc-x' at the first place,
* un-commenting acc-sx,
* replacing (wf-x' _ sx<x') with acc-sx.

The version (I) is type-checked, while for the version II it is reported
"Termination failed ...".

This contradicts to that acc-sx has the needed type Acc _<_ sx.

Is this a bug in Agda (version 2.6.0-05e8112) ?

Regards,

------
Sergei