Unguarded Fixpoint becomes guarded after section closes

[anton-trunov]

Description of the problem

Consider the following snippet:

Section FooSect.

Unset Guard Checking.

Fixpoint loop (n : nat) : nat := loop n.
Print Assumptions loop.
(*
Axioms:
loop is assumed to be guarded.
*)
End FooSect.

Print Assumptions loop.
(* Closed under the global context *)

I would expect the last Print Assumptions to say "loop is assumed to be guarded".

Coq Version

8.13.2 and somewhat recent master (b78e6cf).

[ejgallego]

There is a trivial proof of False using this, so raising priority.

[SkySkimmer]

The easiest fix would be to forbid changing consistency flags inside sections.

[ejgallego]

How come the typing flags were not preserved during elaboration at section closing time?

[ejgallego]

The easiest fix would be to forbid changing consistency flags inside sections.

That would still feel a bit fragile maybe?

[SkySkimmer]

We could also stop losing the typing flags in

coq/kernel/safe_typing.ml

Line 1385 in c53190a

let cb = Term_typing.translate_recipe senv.env kn r in

However there is also a hole if you do something like

Section S.
  Unset Guard Checking.
  Let bad := fix bad (n:nat) : False := bad n.
  Set Guard Checking.
  Definition really_bad := bad 0.
End S.
Print Assumptions really_bad.

since section variables don't have attached typing flags.

[ppedrot]

IMHO the only sound way to store guardedness is to put it in the (co)Fix node. Otherwise we still have issues with reduction functions.

[ejgallego]

IMHO the only sound way to store guardedness is to put it in the (co)Fix node. Otherwise we still have issues with reduction functions.

What about other flags? This doesn't save you from having to traverse everything anyways.

I was thinking of this problem more in the line of "environment tainting", once an environment is tainted, it is not easy to have it back. Morally the sections should preserve tainting [as would typing rules if you add a tainted bit to \Gamma], so the above example once elaborated should be equivalent to:

Unset Guard Checking.
Fixpoint foo := ...
Set Guard Checking.
Definition a := foo ...
Print Assumptions a.

[ppedrot]

This doesn't save you from having to traverse everything

Yes, but Print Assumption does that anyways.

What about other flags?

It depends. Some of them would benefit from having an explicit representation in the term, notably type-in-type (with a dedicated sort). I belive that impredicative set should also be done that way. Positivity checking is better handled in the inductive block since they can't be unfolded. For the other ones it's a bit murky.

[Zimmi48]

Did everybody forget about this issue? I'm putting it in the 8.14+rc1 milestone (because otherwise the blocker label amounts to nothing). But IMHO this would deserve an 8.13.3 release (cc @gares).

[gares]

Thanks for the heads up.