The following inductive definition of U is accepted by Coq because it can see that the occurrences of U in M.T U -> U are strictly positive.
Module M.
Definition T (A : Type) : Type := unit -> A.
End M.
Module N.
Inductive U : Type :=
| c : M.T U -> U.
End N.
On the other hand, the following inductive definition of U is not accepted by Coq because, depending on the definition of M.T, it might have non-strictly positive occurrences.
Module Type S.
Parameter T : Type -> Type.
End S.
Module N (M : S).
Fail Inductive U : Type :=
| c : M.T U -> U.
End N.
How can I specify in the signature S that the parameter of T should only have strictly negative occurrences? Thus preventing any non-strictly positive occurrences of U in its definition.
This U type can be seen as the least fixed point of M.T. Another common encoding is
Definition Mu (T : Type -> Type) := forall A, (T A -> A) -> A.
Definition U := Mu M.T.
Provided that T is a functor (which strict positivity would imply, maybe?):
Parameter map : forall A B, (A -> B) -> T A -> T B. (* in module M *)
we have a constructor and destructor:
Definition c : M.T U -> U := fun x A f =>
f (M.map _ _ (fun y => y _ f) x).
Definition d : U -> M.T U := fun y => y _ (fun x => M.map _ _ c x).
Showing they are inverses requires parametricity, so there is no direct way to prove it. If you don't want to axiomatize it, you can probably enrich T and U to carry evidence of parametricity.
Essentially, the requirement above that T be a functor is a semantic replacement/approximation of the strict positivity condition, which is syntactic.
It is also possible to switch off positivity checking with this new plugin: