Termination.agda

module Termination where

open import Data.Maybe
open import Data.Sum

data Unit : Set where
  unit : Unit

record Stream : Set where
  coinductive
  field
    step : Unit ⊎ Stream

open Stream

-- Passes the termination checker!
valid₀ : Maybe Unit → Stream
step (valid₀ x) = inj₂ (valid₀ x)

-- Failed!
invalid₀ : Maybe Unit → Stream
step (invalid₀ x) = maybe (λ _ → inj₂ (invalid₀ x)) (inj₁ unit) x

-- Simpler? Failed!
elim : {A : Set} → (Unit → A) → Unit → A
elim f unit = f unit

invalid₁ : Unit → Stream
step (invalid₁ x) = elim (λ y → inj₂ (invalid₁ y)) x

{-
/Users/emily/src/3ea3-final-project/Termination.agda:19,1-20,66
Termination checking failed for the following functions:
  invalid₀
Problematic calls:
  invalid₀ x
-}