安全的Agda是否支持无尺寸类型的共感应?

Question

我最近决定在阿格达玩弄共感应，发现"共模式"机制相当脆弱。我决定切入正题并定义M类型，它们或多或少地概括了所有归纳类型(将归纳-递归放在一边(。我的希望是完全避开整个共模式混乱，但令我惊讶的是，似乎协模式无法处理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

这是一个错误。计划对 agda 2.6.1 进行修复。