Homebrew TC algorithm breaks evar map invariants

[ppedrot]

While cleaning up the evar normalization algorithms, I realized that the coq-elpi TC solver messes with some invariants of the evarmap.

To reproduce the bug, one needs a patch that makes Evarutil.nf_evar throw an anomaly on missing evars and that can be found at coq/coq#18554. Note that the current function on master is more lenient as it ignores such situations, but this is still very much unsound (the evarmap is really, really needed to make sense of evar instances represented as sparse lists, so it's just producing garbage in this case).

Here is a reproducible snippet extracted from one of the tests:

From elpi.apps Require Import tc.
Elpi Override TC TC.Solver All.

Definition relation A := A -> A -> Prop.

Class Equiv A := equiv: relation A.

Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) : Prop :=
  inj x y : S (f x) (f y) -> R x y.

Inductive sum_relation {A B} (RA : relation A) (RB : relation B) : relation (A + B) :=
| inl_related x1 x2 : RA x1 x2 -> sum_relation RA RB (inl x1) (inl x2)
| inr_related y1 y2 : RB y1 y2 -> sum_relation RA RB (inr y1) (inr y2).

Declare Instance inl_inj' : forall {A : Type} {RA : relation A} {B : Type} {RB : relation B},
  Inj RA (sum_relation RA RB) inl.
Declare Instance inr_inj' : forall {A : Type} {RA : relation A} {B : Type} {RB : relation B},
  Inj RB (sum_relation RA RB) inr.

Instance sum_equiv {A : Type} {_ : Equiv A} {B : Type} {_ : Equiv B} : Equiv (A + B) := sum_relation equiv equiv.

Elpi Accumulate TC.Solver lp:{{
  shorten tc-elpi.apps.tc.tests.stdppInj.{tc-Inj}.
  % shorten tc-stdppInj.{tc-Inj}.
  tc-Inj A B RA {{@equiv (sum _ _) (@sum_equiv _ _ _ _)}} S C :-
    tc-Inj A B RA {{sum_relation _ _}} S C.
}}.
Elpi Typecheck TC.Solver.

Definition foo {A : Type} {_ : Equiv A} {B : Type} {_ : Equiv B} : Inj equiv equiv inl := _. (* OK *)
Instance bar {A : Type} {_ : Equiv A} {B : Type} {_ : Equiv B} : Inj equiv equiv inl := _. (* anomaly *)

Here is a backtrace:

Anomaly "Missing evar ?X73"
Please report at http://coq.inria.fr/bugs/.
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Evd.MiniEConstr.to_constr_gen.self in file "engine/evd.ml", line 1763, characters 18-82
Called from Evd.MiniEConstr.to_constr_gen in file "engine/evd.ml", line 1805, characters 12-23
Called from Evd.MiniEConstr.nf_evar in file "engine/evd.ml", line 1827, characters 15-50
Called from Evd.map_evar_body in file "engine/evd.ml", line 283, characters 35-40
Called from Evd.map_evar_info in file "engine/evd.ml", line 291, characters 16-45
Called from CMap.MapExt.Smart.mapi in file "clib/cMap.ml", line 276, characters 15-20
Called from CMap.MapExt.Smart.mapi in file "clib/cMap.ml", line 274, characters 15-23
Called from CMap.MapExt.Smart.mapi in file "clib/cMap.ml", line 275, characters 15-23
Called from CMap.MapExt.Smart.mapi in file "clib/cMap.ml", line 275, characters 15-23
Called from CMap.MapExt.Smart.mapi in file "clib/cMap.ml", line 275, characters 15-23
Called from Evd.raw_map in file "engine/evd.ml", line 886, characters 19-54
Called from Classes.do_instance_resolve_TC in file "vernac/classes.ml", line 430, characters 14-40
Called from Classes.do_instance in file "vernac/classes.ml", line 515, characters 24-65
Called from Classes.new_instance in file "vernac/classes.ml", line 599, characters 2-100
Called from Vernacentries.vernac_instance in file "vernac/vernacentries.ml", line 1482, characters 4-61
Called from Vernactypes.vtdefault.(fun) in file "vernac/vernactypes.ml", line 82, characters 29-33
Called from Vernacinterp.interp_typed_vernac in file "vernac/vernacinterp.ml", line 21, characters 20-113
Called from Vernacinterp.interp_control.(fun) in file "vernac/vernacinterp.ml", line 168, characters 24-126

As you can see, this happens when normalizing an evarmap, so this means that it's already too late, some info from the evarmap contains dangling evars in its body. This can probably be traced by instrumenting evar instantiation to detect this situation but it's a fairly intrusive change, and in any case this reflects a bug in coq-elpi so I don't really feel qualified to track it down.

[gares]

@FissoreD this seems a bug in the hook compiling instances. The code changed a lot, it would be nice if we could give it a try (this is on coq-master, not master... so we need to do some git gimmics).

[ppedrot]

It's easy to backport the change that makes nf_evar explode on dangling evars, if that helps you.

[ppedrot]

This particular bug seems to have been fixed on coq-elpi master (by #581 most likely). The test-suite still fails with an anomaly on undefined evars though. I'll try to minimize the bug again.

[gares]

Thanks!

[ppedrot]

I am very confused now: the same reduced example still triggers an anomaly when it is compiled from within the test folder of tc-elpi, but not when launched from the toplevel loading the coq-elpi files installed in the user-contrib repo. Those files are the same as the ones from my CI folder where coq-elpi is compiled, but somehow the loadpath seems to be an important difference.