NonStrictPositivity.v

(* The following two examples fulfill the (strict) positivity condition *)

Inductive Switch (A : Type) : Type :=
| switch : Switch A -> Switch A.

Inductive UseSwitch :=
| useSwitch : Switch UseSwitch -> UseSwitch.
 

Inductive SwitchSP (A : Type) : Type :=
| switchSP : bool -> SwitchSP A.
  
Inductive UseSwitchSP :=
| useSwitchSP : SwitchSP UseSwitchSP -> UseSwitchSP.


(* this definition, however, does not --
   which rule applies for this definition?
   https://coq.inria.fr/refman/language/cic.html#strict-positivity
 *)
Inductive SwitchNSP (A : Type) : Type :=
| switchNSP : SwitchNSP bool -> SwitchNSP A.

Fail Inductive UseSwitchNSP :=
| useSwitchNSP : SwitchNSP UseSwitchNSP -> UseSwitchNSP.