agda/test/Bugs/NonRecursiveCoinductiveRecord.agda

-- Andreas, 2014-04-23 test case by Andrea Vezzosi
{-# OPTIONS --sized-types --copatterns #-}
-- {-# OPTIONS --show-implicit -v term:60 #-}
module _ where

open import Common.Size

-- Invalid coinductive record, since not recursive.
record ▸ (A : Size → Set) (i : Size) : Set where
  coinductive         -- This should be an error, since non-recursive.
  constructor delay_
  field
    force : ∀ {j : Size< i} → A j

open ▸

-- This fixed-point combinator should not pass the termination checker.
∞fix : ∀ {A : Size → Set} → (∀ {i} → ▸ A i → A i) → ∀ {i} → ▸ A i
force (∞fix {A} f {i}) {j} = f {j} (∞fix {A} f {j})

-- The following fixed-point combinator is not strongly normalizing!
fix : ∀ {A : Size → Set} → (∀ {i} → (∀ {j : Size< i} → A j) → A i) → ∀ {i} {j : Size< i} → A j
fix f = force (∞fix (λ {i} x → f {i} (force x)))

-- test = fix {!!}
-- C-c C-n test gives me a stack overflow