安全的 Agda 是否支持共同归纳 w/out 大小的类型？

Question

我最近决定在 Agda 中混用共归纳法，发现 "copattern" 机制相当脆弱。我决定开门见山地定义 M 类型，这些类型或多或少地概括了所有的余归纳类型（将余归纳递归放在一边）。我的希望是完全避开整个 copattern 混乱，但令我惊讶的是，copatterns 似乎无法处理 M 构造函数：

{-# 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)

产生：

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

我尝试了几个小的变化，但无济于事。是否存在使安全 agda 接受 M 的某些变体的咒语？

郑重声明，我知道我有很多选择，包括：

打开 --sized-types 并索引 M 尺寸
关闭 --safe 并向编译器保证 unroll 是高效的
也许可以尝试 "old-style coinduction"，这可能一致也可能不一致 (?)

我发现所有这些至少有点令人不快，并且我很惊讶香草安全的 agda 无法处理这种情况（考虑到这是一种情况，如果处理的话，会给用户留下一个逃生口）。我错过了什么吗？

Answer 1

是 bug。计划对 agda 2.6.1 进行修复。

安全的 Agda 是否支持共同归纳 w/out 大小的类型？

Does safe Agda support coinduction w/out sized-types?

agda

coinduction