coq - 为什么我的定义因为严格的积极性而不允许？

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 (in) 一致性，即第一个定义遵循此检查，但由于严格的正性问题而失败。
据我了解严格正数限制，如果 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

现在我的问题有两个方面:首先，我可以用上述定义构建的“邪恶例子”是什么？二、哪个 the rules适用于上述定义？
一些注意事项:

澄清一下，我认为我确实理解为什么不允许在类型检查方面使用第二个定义，但仍然觉得当允许定义时，这里没有任何“邪恶”发生。

我一开始以为我的例子是this question的一个实例，但启用 Universe 多态性对第二个定义没有帮助。

我可以使用一些“技巧”来调整我的定义以便 Coq 接受它吗？

Answer 1

我有以下两个定义会导致两个不同的错误消息。第一个定义因为严格的正性而被拒绝，第二个定义因为宇宙不一致而被拒绝。
(* 非严格正数 *)
电感式 SwitchNSP (A : Type) : Type :=
| switchNSP : SwitchNSP bool -> SwitchNSP A。
失败感应 UseSwitchNSP :=
| useSwitchNSP : SwitchNSP UseSwitchNSP -> UseSwitchNSP。
(* 宇宙不一致 *)
电感式开关NSPI:类型 -> 类型:=
| switchNSPI :对于所有 A，SwitchNSPI bool -> SwitchNSPI A。
失败感应 UseSwitchNSPI :=
| useSwitchNSPI : SwitchNSPI UseSwitchNSPI -> UseSwitchNSPI。