Inconsistency.v

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

(* Because of strict positivity, the `X` in `funWrap` cannot be instantiated
   with `Wrap A`? *)