Problem

I have a simple coinductive record with a single field of a sum type. Unit gives us a simple type to play with.

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

Works

valid passes the termination checker:

valid : Maybe Unit → Stream
step (valid x) = inj₂ (valid x)

Breaks

But say I want to eliminate the Maybe Unit member and only recurse when I have a just.

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

Now the termination checker is unhappy!

Termination checking failed for the following functions:
  invalid₀
Problematic calls:
  invalid₀ x

Why does this not satisfy the termination checker? Is there a way around this or is my conceptual understanding incorrect?

Background

agda --version yields Agda version 2.6.0-7ae3882. I am compiling only with the default options.

The output of -v term:100 is here: https://gist.github.com/emilyhorsman/f6562489b82624a5644ed78b21366239

Attempted Solutions

1. Use Agda version 2.5.4.2. Does not fix.
2. Use --termination-depth=10. Does not fix.

You could make use of sized types here.

open import Data.Maybe
open import Data.Sum
open import Size

data Unit : Set where
  unit : Unit

record Stream {i : Size} : Set where
  coinductive
  field
    step : {j : Size< i} → Unit ⊎ Stream {j}

open Stream

valid : Maybe Unit → Stream
step (valid x) = inj₂ (valid x)

invalid₀ : {i : Size} → Maybe Unit → Stream {i}
step (invalid₀ x) = maybe (λ _ → inj₂ (invalid₀ x)) (inj₁ unit) x

_ : step (invalid₀ (nothing)) ≡ inj₁ unit
_ = refl

_ : step (invalid₀ (just unit)) ≡ inj₂ (invalid₀ (just unit))
_ = refl

Being more explicit about the Size arguments in the definition of invalid₀:

step (invalid₀ {i} x) {j} = maybe (λ _ → inj₂ (invalid₀ {j} x)) (inj₁ unit) x

where j has type Size< i, so the recursive call to invalid₀ is on a “smaller” Size.

Notice that valid, which didn't need any “help” to pass termination checking, doesn't need to reason about Size's at all.