## Stream: Coq users

### Topic: Non strictly positive occurrence for nested types

#### Jules Viennot (Apr 25 2024 at 11:12):

Hello, I want to verify some OCaml piece of code that doesn't require to check for strict positivity in types definition.

The code I want to write look something like this :

``````Parameter J : Type -> Type.

Inductive K (a : Type) : Type -> Type :=
| Kc {b : Type} : J a -> K (M a) b -> J a -> K a b

with L (a : Type) : Type :=
| Lc {b : Type} : K a b -> L b -> L a

with M (a : Type) : Type :=
| Mc : J a -> L (M a) -> M a.
``````

But it returns the error : 'Non strictly positive occurrence of "M" in "forall b : Type, J a -> K (M a) b -> J a -> K a b".'

I can't wrap my head around this problem, is it really a non-strictly positive occurrence of M, and in this case, how do we prove that implementing it leads to inconsistency ?

Otherwise, is there a way to work around this issue ?

#### Li-yao (Apr 25 2024 at 11:28):

If you let `J a := a -> bool` then you will find a recursive negative occurrence of `M`.

#### Jules Viennot (Apr 25 2024 at 12:21):

And if J is an inductive type of the form `Inductive J (A : Type) : Type := Jc : A -> J A. ` ?

#### Li-yao (Apr 25 2024 at 12:29):

I guess that would be fine but then you need a way smarter condition than "strict positivity" (and find someone to implement it)

#### Li-yao (Apr 25 2024 at 12:33):

In this case you're just building a stack of `M`s so you can encode this type with a `nat` parameter to avoid the recursion in parameters

``````(* iter : nat -> (A -> A) -> A -> A somewhere in the stdlib *)
Inductive Kn (n : nat) (a : Type) (b : Type) : Type := Kc : J (iter n M a) -> Kn (S n) -> J (iter n M a) -> K a b
...

Definition K := Kn 0.
``````

#### Li-yao (Apr 25 2024 at 12:34):

Ah, nvm, since M is also defined mutually recursively that's still too naive...

Last updated: Jun 23 2024 at 04:03 UTC