[Agda] strange termination check

[Sergei Meshveliani]

On Thu, 2013-10-10 at 21:57 +0400, Sergei Meshveliani wrote:
> Please, why the below  powerToPos  is not checked as terminating ?
> 
> 
> {-# OPTIONS --termination-depth=3 #-}
> module Report where
> open import Level    using () renaming (zero to 0ℓ)
> open import Function using (case_of_)
> open import Relation.Binary 
>             using (module Setoid; module IsEquivalence;_Preserves_⟶_)
> open import Relation.Binary.PropositionalEquality using (_≡_)
> open import Algebra    using (Semigroup; module Semigroup)
> open import Data.Empty using (⊥)
> open import Data.List  using ([]; _∷_)
> open import Data.Fin   using (Fin) renaming (zero to 0b; suc to sucB)
> open import Data.Digit using (Bit)
> open import Data.Bin   using (Bin⁺)
>           
> 1b : Bit
> 1b = sucB 0b
> 
> postulate H : Semigroup 0ℓ 0ℓ
> 
> open Semigroup H using (setoid; _≈_; _∙_)
>                        renaming (Carrier to C; isEquivalence to ≈equiv)
> open IsEquivalence ≈equiv using ()
>                  renaming (refl to ≈refl; sym to ≈sym; trans to ≈trans)
> 
> HasLast1 : Bin⁺ → Set       -- "is the bit list of a non-zero binary"
> HasLast1 []           =  ⊥
> HasLast1 (b ∷ [])     =  b ≡ 1b
> HasLast1 (_ ∷ b ∷ bs) =  HasLast1 (b ∷ bs)
> 
> powerToPos : C → (bs : Bin⁺) → HasLast1 bs → C
>
> [..]

> The recursion     (b ∷ b' ∷ bs)  -->  (b' ∷ bs)  
> 
> by the second argument is well-founded. Why does not the checker see the
> termination proof? 


Sorry, the implementation needs to be

powerToPos _ []                    ()
powerToPos x (0b      ∷ [])        ()
powerToPos x (sucB 0b ∷ [])        _   =  x
powerToPos x (sucB (sucB ()) ∷ [])

powerToPos x (b ∷ b' ∷ bs)  last1-b:b':bs =
                           case b of \ { 0b              → p ∙ p
                                       ; (sucB 0b)       → x ∙ (p ∙ p)
                                       ; (sucB (sucB ()))
                                       }
                           where
                           hl1 : HasLast1 (b' ∷ bs)
                           hl1 = last1-b:b':bs

                           p = powerToPos x (b' ∷ bs) hl1
-----------------------------------------------------------------------

And again, I do not understand why is not it checked as terminating.

Thanks,

------
Sergei