Positivity cheking for type constructor applied to itself

[clarus]

Hi,

I have some troubles to deactivate the positivity checking. When I do:

From TypingFlags Require Import Loader.

Unset Guard Checking.

Inductive foo : Type :=
| bar : (foo -> unit) -> foo.

the definition of foo is indeed accepted without the following message:

Error: Non strictly positive occurrence of "foo" in "(foo -> unit) -> foo".

However, with:

Inductive foo : Type -> Type :=
| bar : foo (foo unit).

I still get:

Error: Non strictly positive occurrence of "foo" in "foo (foo unit)".

even with Unset Guard Checking.. Is this kind of positivity check covered by the flag? Tested with Coq 8.9.1. Thanks.

[SimonBoulier]

Hi @clarus, sorry for the delay. In this branch I can define your inductive: https://github.com/SimonBoulier/coq/tree/uncheck_positivity_bug

Unset Positivity Checking.

Inductive foo : Type -> Type :=
| bar : foo (foo unit).

But I don't know what we can do with it...

Do you think it is worth merging in Coq?

[clarus]

Hi,

Top, thanks, excellent news!

For our work on the crypto-currency Tezos, to formalize the OCaml code https://gitlab.com/tezos/tezos/-/blob/master/src/proto_alpha/lib_protocol/script_typed_ir.ml in Coq we would need to support such types. Indeed, this GADT describing the syntax of the smart-contracts contains such types with self-referencing. For now what we do is what we erase the type annotations, but then we need to add unsafe casts in the matchs.

So for us this would be quite useful!