open import Agda.Builtin.Nat

data D : Set where
  c : Nat → Nat → D

mutual
  f : D → Set
  f (c (suc n) 0) = g (c n)
  f (c n (suc m)) = f (c (suc n) m)

  g : (Nat → D) → Set
  g h = f (h 42)

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

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

data D : Set where
  c : Nat → Nat → D

mutual
  f : (x : D) → Nat
  f (c (suc n) 0) = g (c n)
  f (c n (suc (suc m))) = f (c (suc n) m)
  f _ = zero

  g : (h : Nat → D) → Nat
  g h = f (h 2)

loop : f (c 1 0) ≡ zero
loop = refl

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

data ⊥ : Set where
record ⊤ : Set where

data Nat : Set where
  zero : Nat
  suc  : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

data _≡_ (A : Set) : Set → Set₁ where
  refl : A ≡ A

cast : ∀{A B : Set} → A ≡ B → A → B
cast refl x = x

cast⁻¹ : ∀{A B : Set} → A ≡ B → B → A
cast⁻¹ refl x = x

-- Exploit the termination checker bug to prove ⊥.

data D : Set where
  _,_ : Nat → Nat → D

P : D → Set
P (suc _ , _)           = ⊥
P (_     , suc (suc _)) = ⊥
P (0 , 0) = ⊤
P (0 , 1) = ⊤

-- This does not hold definitionally (no exact split), so prove it.
lem : ∀ n {m} → P (n , suc (suc m)) ≡ ⊥
lem 0       = refl
lem (suc n) = refl

mutual
  f : (x : D) → P x
  -- The loop:
  f (suc n , _)           = cast   (lem n) (g (n ,_))       -- this call to g is fishy!
  f (n     , suc (suc m)) = cast⁻¹ (lem n) (f (suc n , m))
  -- Base cases:
  f (0 , 0) = record{}
  f (0 , 1) = record{}

  g : (h : Nat → D) → P (h 2)
  g h = f (h 2)

loop : ⊥
loop = f (1 , 0)