安全的Agda是否支持没有尺寸类型的共生？

Question

我最近决定在阿格达（Ada）进行硬币共生，并且发现“仿制”机械相当脆弱。我决定切入并定义M类型，这些类型或多或少地概括了所有共归类型（撇开coinduction-递归）。我的希望是完全避开整个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富有成效
• 也许尝试“老式的共生”，可能一致也可能不一致（？）

[我发现所有这些问题至少都不太好吃，并且令香草安全型AGDA无法处理这种情况感到惊讶（考虑到这是一种情况，如果处理后会给使用者带来逃生的危险）。我想念什么吗？

Answer 1

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