Incompatibilité d'univers (en raison d'une restriction de positivité stricte?)

Question

J'ai l'extrait de code suivant.

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). 

Ma première pensée était que le X dans funWrap ne peut pas être instancié avec Wrap A, en raison de la restriction de positivité stricte pour les types inductives. Est-ce le cas ou existe-t-il une autre raison pour l'incohérence (et peut-être une approche différente pour définir la fonction specialWrap)?

Éditer: L'explication de la deuxième définition est donnée dans un commentaire de la réponse sélectionnée.

Answer 1

Le problème avec votre première définition est le manque de polymorphisme de l'univers, je pense. Si vous activez Set Universe Polymorphism., il passera. Ceci est dû au fait que la définition inductive régulière est "univers monomorphe". Dans ce cas, vous obtenez un problème d'univers dû au niveau de l'univers partagé.