1

I recently decided to fool around with coinduction in Agda, and found the "copattern" machinery to be fairly brittle. I decided to cut to the chase and define M types, which more-or-less generalize all the coinductive types (setting coinduction-recursion aside). My hope was to sidestep the whole copattern mess entirely, but to my surprise, it seems that copatterns aren't capable of handling the M constructor:

{-# OPTIONS --safe #-}
module M {l}
  (Index : Set l)
  (Shape : Index -> Set l)
  (Position : (i : Index) -> Shape i -> Set l)
  (index : (i : Index) -> (s : Shape i) -> Position i s -> Index) where

record M (i : Index) : Set l where
  coinductive
  field shape : Shape i
  field children : (p : Position i shape) -> M (index i shape p)

open M

record MBase (Rec : Index -> Set l) (i : Index) : Set l where
  coinductive
  field shapeB : Shape i
  field childrenB : (p : Position i shapeB) -> Rec (index i shapeB p)

open MBase

unroll : (S : Index -> Set l) -> (∀ {i} -> S i -> MBase S i) -> ∀ {i} -> S i -> M i
shape (unroll S u s) = shapeB (u s)
children (unroll S u s) p = unroll S u (childrenB (u s) p)

produces:

Termination checking failed for the following functions:
  unroll
Problematic calls:
  shape (unroll S u s)
  unroll S u (childrenB (u s) p)

I tried a couple of minor variations, to no avail. Is there an incantation that causes safe agda to accept some variant of M?

For the record, I'm aware that I have a number of options available to me, including:

  • turning on --sized-types and indexing M on a size
  • turning off --safe and promising the compiler that unroll is productive
  • maybe try "old-style coinduction", which may or may not be consistent (?)

I find all of these at least mildly unpalatable, and am surprised that vanilla safe agda cannot handle this case (given that it's the one case that, if handled, leaves the user an escape hatch). Am I missing something?

4

1 回答 1

1

'twas a bug. A fix is scheduled for agda 2.6.1.

于 2020-02-07T15:43:55.653 回答