Termination checker fails after abstracting the call site

Question

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

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

score 6 · Accepted Answer · answered Apr 03 '19 at 18:04

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.

Potato44 · Answer 2 · 2019-04-04T08:08:15.990

The problem is that Agda cant see that invalid₀ is productive. This is because it is both recursive and not guarded by a constructor. Agda does not look inside the definition of maybe when deciding whether this is terminating or not.

Here is an implementation that satisfies the termination checker because both branches are guarded by constructors and/or non-recursive:

okay₀ : Maybe Unit → Stream
step (okay₀ x@(just _)) = inj₂ (invalid₀ x)
step (okay₀ nothing) = inj₁ unit

The important part is the recursive just case has the constructor inj₂ as the top level of the expression.