Agda Termination Checking

mutual

 data Simple : ℕ → Type →  Set where
   compl : Simple zero compl
   intcompl  : Simple zero (δcompl int)
   realcompl : Simple zero (δcompl real)
   lift  : ∀{n t}  → (φ : Simple n t) → (m : ℕ) → (¬Lift φ) → Simple (suc (n + m)) t
   _⇨_   : ∀{n t t′} → Simple n t  → Simple n t′ → Simple (suc n) (t ⇨ t′)

 data ¬Lift : ∀{n t} → Simple n t → Set where
   compl : ¬Lift compl
   intcompl : ¬Lift intcompl
   realcompl : ¬Lift realcompl
   _⇨_ : ∀{n t t′} → (φ : Simple n t) → (φ′ : Simple n t′) →  ¬Lift (φ ⇨ φ′)

-- Non terminating
ss' : {t : Type} → {n : ℕ} →  (φ : Simple n t) → ℕ
ss' compl = 0
ss' intcompl = 0
ss' realcompl = 0
ss' (lift φ _ _) = 0
ss' (φ ⇨ compl)    = 0
ss' (φ ⇨ intcompl) = 0
ss' (φ ⇨ realcompl)   = 0
ss' (φ ⇨ lift  _ _ _) =  ss' φ
ss' (φ ⇨ (φ′ ⇨ φ″))   =  ss' (φ′ ⇨ φ″)