为什么由于严格的积极性而不允许我的定义？

Question

我有以下两个定义，导致两个不同的错误消息。第一个定义由于严格的正性而被拒绝，第二个定义由于宇宙不一致而被拒绝。

(* non-strictly positive *)
Inductive SwitchNSP (A : Type) : Type :=
| switchNSP : SwitchNSP bool -> SwitchNSP A.

Fail Inductive UseSwitchNSP :=
| useSwitchNSP : SwitchNSP UseSwitchNSP -> UseSwitchNSP.

(* universe inconsistency *)
Inductive SwitchNSPI : Type -> Type :=
| switchNSPI : forall A, SwitchNSPI bool -> SwitchNSPI A.

Fail Inductive UseSwitchNSPI :=
| useSwitchNSPI : SwitchNSPI UseSwitchNSPI -> UseSwitchNSPI.

在gitter上聊天显示，首先检查了Universe（内部）一致性，即第一个定义遵循此检查，但是由于严格的正性问题而失败。

据我了解严格的积极性限制，如果Coq允许非严格的积极性数据类型定义，我可以不使用而构造非终止函数fix（这很糟糕）。

为了使之更加混乱，第一个定义在Agda中被接受，第二个定义给出了严格的正错误。

data Bool : Set where
  True : Bool
  False : Bool

data SwitchNSP (A : Set) : Set where
  switchNSP : SwitchNSP Bool -> SwitchNSP A

data UseSwitchNSP : Set where
  useSwitchNSP : SwitchNSP UseSwitchNSP -> UseSwitchNSP

data SwitchNSPI : Set -> Set where
  switchNSPI : forall A -> SwitchNSPI Bool -> SwitchNSPI A

data UseSwitchNSPI : Set where
  useSwitchNSP : SwitchNSPI UseSwitchNSPI -> UseSwitchNSPI

现在，我的问题有两个方面：首先，用上述定义可以构造的“邪恶的例子”是什么？第二，以下规则适用于上述定义？

注意1：为澄清起见，我认为我确实理解为什么不允许对第二个定义进行类型检查，但是当允许该定义时，仍然觉得这里没有“邪恶”发生。

注意2：我首先认为我的示例是该问题的一个实例，但是启用Universe多态性对第二个定义没有帮助。

Answer 1

不幸的是，这个例子并没有什么深奥的内容。正如您所指出的，Agda 接受它，而 Coq 的问题是参数缺乏统一性。例如，它接受：

Inductive SwitchNSPA (A : Type) : Type :=
| switchNSPA : SwitchNSPA A -> SwitchNSPA A.

Inductive UseSwitchNSPA :=
| useSwitchNSPA : SwitchNSPA UseSwitchNSPA -> UseSwitchNSPA.

像 Coq 使用的积极性标准并不完整，因此它们会拒绝无害的类型；支持更多类型的问题在于，它通常会使积极性检查器变得更加复杂，而这已经是内核中最复杂的部分之一。

至于为什么拒绝的具体细节，我并不能100%确定。按照手册上的规则，我认为应该接受？

编辑：手册正在更新。

具体来说，使用以下较短的名称来简化以下内容：

Inductive Inner (A : Type) : Type := inner : Inner bool -> Inner A.
Inductive Outer := outer : Inner Outer -> Outer.

1. 正确性规则

2. 积极条件
   这里，

   X = Outer
   T = forall x: Inner X, X
   

   所以我们处于第二种情况

   U = Inner X
   V = X
   

   1. V很容易，所以我们先这样做： V = (X)属于第一种情况，没有t_i，因此 X 为正
   2. 对于U： 是U = Inner X 严格正的吗X？ 这里，

      T = Inner X
      

      因此我们处于最后一种情况：T转换为(I a1)(no t_i)

      I = Inner
      a1 = X
      

      并且X不会出现在 中t_i，因为没有t_i. 构造函数的实例化类型是否满足嵌套正性条件？只有一个构造函数：
      1. inner : Inner bool -> Inner X. 这是否满足嵌套正性条件？这里，

         T = forall x: Inner bool, Inner X.
         

         所以我们处于第二种情况

         U = Inner bool
         V = Inner X
         

         1. X不会出现在 中U，因此X是严格正的 中U。
         2. 是否V满足 的嵌套正性条件X？这里，

            T = Inner X
            

            因此我们处于第一种情况：T转换为(I b1)(no u_i)

            I = Inner
            b1 = X
            

            没有u_i，因此V满足嵌套正性条件。

我已经打开了一个错误报告。手册正在修复中。

还有两件小事：

1. I can't resist pointing that your type is empty:

   Theorem Inner_empty: forall A, Inner A -> False.
   Proof. induction 1; assumption. Qed.
   

2. You wrote:

   if Coq allows non-strictly positivity data type definitions, I could construct non-terminating functions without using fix (which is pretty bad).

   That's almost correct, but not exactly: if Coq didn't enforce strict positivity, you could construct non-terminating functions period, which is bad. It doesn't matter whether they use fix or not: having non-termination in the logic basically makes it unsound (and hence Coq prevents you from writing fixpoints that do not terminate by lazy reduction).