Agda: Termination checking failed after updating Agda version

[chirsz-ever]

The code caused problem is(need the standard library):

module TerminationTest where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s)
open import Data.Nat.Properties using (+-suc)

data Bin : Set where
  nil : Bin
  x0_ : Bin → Bin
  x1_ : Bin → Bin

inc : Bin → Bin
inc nil    = x1 nil
inc (x0 t) = x1 t
inc (x1 t) = x0 (inc t)

ℕtoBin : ℕ → Bin
ℕtoBin zero    = x0 nil
ℕtoBin (suc n) = inc (ℕtoBin n)

2n-eq-x0 : ∀ (n) → 1 ≤ n → ℕtoBin (n + n) ≡ x0 (ℕtoBin n)
2n-eq-x0 zero ()
2n-eq-x0 (suc zero) (s≤s z≤n) = refl
2n-eq-x0 (suc (suc n)) (s≤s z≤n) rewrite +-suc n (suc n)
                                       | 2n-eq-x0 (suc n) (s≤s z≤n) = refl

The code was no problem with Agda 2.6.0.1, but rejected by Agda 2.6.1.

[nad]

I think this is related to the fix of #3604.

[gallais]

Note that {-# OPTIONS --termination-depth=2 #-} (it tells Agda to work a bit
harder at tracking how smaller things get) makes the error go away.

[chirsz-ever]

Note that {-# OPTIONS --termination-depth=2 #-} (it tells Agda to work a bit
harder at tracking how smaller things get) makes the error go away.

Thanks, it works.