Declaring TC instance in section can throw anomaly on closing

[trilis]

Here is the minimal example:

From elpi Require Import elpi.
Require Import String.

Class Show (A : Type) :=
  { show : A -> string }.
Definition String_Show : Show string := {|
    show := id
|}.

Elpi Command ElpiStart.
#[synterp] Elpi Accumulate lp:{{
    main _ :-
        coq.env.begin-section "A".
}}.
Elpi Accumulate lp:{{
    main _ :-
        coq.env.begin-section "A".
}}.
Elpi Typecheck.
Elpi Export ElpiStart.

Elpi Command ElpiTCEnd.
#[synterp] Elpi Accumulate lp:{{
    main _ :-
        coq.env.end-section.
}}.
Elpi Accumulate lp:{{
    main _ :-
        coq.locate "String_Show" I,
        @global! => coq.TC.declare-instance I 0,
        coq.env.end-section.
}}.
Elpi Typecheck.
Elpi Export ElpiTCEnd.

ElpiStart.

ElpiTCEnd.

On the ending of the section, I get this anomaly:

Error: Anomaly
"File "tactics/hints.ml", line 1301, characters 6-12: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

It seems like some hints are replayed when they shouldn't.
Note that everything works fine when we do declare-instance and end-section in separate commands, or when we do everything (begin-section, declare-instance and end-section) in one command, or when we remove @global!.
Coq 8.19.1, coq-elpi 2.1.0. We definitely didn't have this issue before synterp introduction.

[gares]

It seems the bug is in Coq, file classes.ml, and that is was introduced by the parsing/execution phase split.
The code below should use Global.sections_are_opened () instead of Lib.sections_are_open () since add_instance_base is interp code (not synterp code).

let add_instance_base inst =
  let locality = match inst.locality with
  | Local -> Local
  | SuperGlobal ->
    (* i.e. in a section, declare the hint as local since discharge is managed
       by rebuild_instance which calls again add_instance_hint; don't ask hints
       to take discharge into account itself *)
    if Lib.sections_are_opened () then Local
    else SuperGlobal
  | Export ->
    (* Same as above for export *)
    if Lib.sections_are_opened () then Local
    else Export
  in
  add_instance_hint inst.instance ~locality
    inst.info

CC @Janno @rlepigre that may be impacted too.
Note that the erroneous code path is only taken if one passes @globa! (that corresponds to SuperGlobal).

I did not test a fix, so I'm only speculating, but it seems plausible.

Thanks for reporting the bug.

[gares]

I did not test a fix, so I'm only speculating, but it seems plausible.

Because I'm super busy. @trilis if you have the time to patch Coq and confirm my analysis, it would be great. Otherwise you'll have to wait (about a month I'm afraid).

[trilis]

Sure, I'll try to patch. Thanks for pointing me to the relevant code.

[trilis]

I can confirm that the anomaly in the minimized example is gone with the proposed fix. However, when trying to apply this fix to our real code, I found another anomaly: (removed from this issue, see #619)

[gares]

Could you please open another bugreport, this is about locate and not TC. The bug could be as well in Coq.
It would also be nice if you could provide your TC patch, or directly submit it to Coq.

[trilis]

Sure, I created separate bugreport and submitted PR to coq repo