宇宙不一致（由於嚴格的積極性限制？）

Question

我有以下代碼片段。

Set Implicit Arguments. 

Inductive Simple (A: Type) := simple : Simple A. 
Inductive Wrap (A: Type) := 
| wrap : A -> Wrap A 
| funWrap : forall X, Simple X -> (X -> Wrap A) -> Wrap A. 

Definition anotherWrap A : Wrap A := 
    funWrap (simple A) (fun x => wrap x). 

Fail Definition specialWrap1 A : Wrap (Wrap A) := 
    funWrap (simple (Wrap A)) (fun x => wrap x). 

Fail Definition specialWrap A : Wrap A := 
    funWrap (simple (Wrap A)) (fun x => x). 

我首先想到的是，在funWrap的X不能Wrap A被實例化，因爲歸納類型嚴格限制陽性的。是這種情況還是存在不一致的另一個原因（也可能採用不同的方法來定義功能specialWrap）？

編輯：第二個定義的解釋在所選答案的評論中給出。

Answer 1

你的第一個定義的問題是缺乏宇宙多態性，我認爲。如果你啓用Set Universe Polymorphism.它會通過。

這是因爲規則歸納定義是「宇宙單形」，所以在這種情況下，由於共享的宇宙級別，你會得到一個宇宙問題。