我有以下两个定义，导致两个不同的错误消息。第一个定义由于严格的正性而被拒绝，第二个定义由于宇宙不一致而被拒绝。
(* 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 …我试图在Coq中建模一种不太天真的monadic编码的非确定性(比MonadPlus和常见列表更不天真),这在Haskell中经常使用; 例如,列表的编码看起来像
data List m a = Nil | Cons (m a) (m (List m a))
而Coq中的相应定义如下.
Inductive List (M: Type -> Type) (A: Type) :=
Nil: List M A
| Cons : M A -> M (List M A) -> List M A.
但是,由于归纳数据类型的"严格正"条件,Coq中不允许这种定义.
我不确定我是否打算在Haskell中针对Coq特定的答案或替代实现,我可以在Coq中形式化,但我很高兴阅读有关如何克服此问题的任何建议.