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

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

(* 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多态性对第二个定义没有帮助。