Positivity checker

Foo.agda

module Foo where
open import Level using ( Lift )

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

elimℕ : ∀{ℓ} (P : ℕ → Set ℓ)
  (pzero : P zero)
  (psuc : (n : ℕ) → P n → P (suc n))
  (n : ℕ) → P n
elimℕ P pzero psuc zero = pzero
elimℕ P pzero psuc (suc n) = psuc n (elimℕ P pzero psuc n)

ℕ∨Xpred₁ : ∀{ℓ} (X : ℕ → Set ℓ) (n : ℕ) → Set ℓ
ℕ∨Xpred₁ X zero = Lift ℕ
ℕ∨Xpred₁ X (suc n) = X n

ℕ∨Xpred₂ : ∀{ℓ} (X : ℕ → Set ℓ) (n : ℕ) → Set ℓ
ℕ∨Xpred₂ {ℓ = ℓ} X = elimℕ (λ _ → Set ℓ) (Lift ℕ) (λ (m : ℕ) (ih : Set ℓ) → X m)

data Foo {ℓ} (n : ℕ) : Set ℓ where
  foo₁ : ℕ∨Xpred₁ Foo n → Foo n
  foo₂ : ℕ∨Xpred₂ Foo n → Foo n 
      -- elimℕ (λ _ → Set ℓ) (Lift ℕ) (λ m ih → Foo m) n → Foo n
{-
Foo is not strictly positive, because it occurs in the 4th argument
to elimℕ in the type of the constructor foo₂ in the definition of
Foo.
-}