Stream: Coq devs & plugin devs

Topic: ✔ Stack overflow during positivity checking (?)

view this post on Zulip gallais (Aug 17 2022 at 12:25):

Wondering if this is a known issue or whether I should report it on github.
Loading the following code in coqide, using coq 8.9.1 I get a stack overflow on the last line.

Definition Not (x : Type) := x -> False.

Record Apply (f : Type -> Type) (a : Type) : Type :=
  MkApply { runApply : forall b, b = a -> f b }.

Inductive Oops : Type :=
  MkOops : Apply Not Oops -> Oops.

view this post on Zulip Notification Bot (Aug 17 2022 at 12:29):

This topic was moved here from #Coq users > Stack overflow during positivity checking (?) by Karl Palmskog.

view this post on Zulip Karl Palmskog (Aug 17 2022 at 12:30):

moving to this stream where stack overflows and similar things are more frequently discussed

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2022 at 12:35):

This gives a universe inconsistency error on master, FWIW.

view this post on Zulip gallais (Aug 17 2022 at 12:35):

I also get the universe inconsistency when inlining the definition of Apply.
Edit: or rather I used to in a situation with no strict positivity issue, with the strict positivity issue I get that error first.

view this post on Zulip Notification Bot (Aug 17 2022 at 12:48):

gallais has marked this topic as resolved.

Last updated: Sep 09 2024 at 05:02 UTC