Weird behaviour of reduction of coq terms

[FissoreD]

Minimal example with the error:

From elpi Require Import elpi.

Elpi Tactic A.

Section S.

  Inductive Foo (N : Type) (N : Type).
  Context (A : Type).

  Elpi Accumulate  lp:{{
    solve (goal Ctx _ (prod _ T Bo) _ _) _ :- !,
      @pi-decl `A` T x\ solve (goal Ctx _ (Bo x) _ _) _.
    solve (goal _ _ T _ _) _ :- 
      % ====> I expect that T1 is the same term as T
      @redflags! coq.redflags.nored => coq.reduction.lazy.norm T T1,
      std.assert! (T = T1) "should be equal".
  }}.
  Elpi Typecheck.

  Goal forall a, Foo A a.
    elpi A.
  Abort.

End S.

Error message due to std.assert!:

should be equal: app [global (indt «Foo»), global (const «A»), c0] = app [global (indt «Foo»), c0, c0]

Note that the first argument of Foo in the result is not A but c0 Similar APIs like coq.reduction.lazy.whd give the same problem Moreover, the same error happens for any kind of reduction passed to @redflags!, e.g. @redflags! coq.redflags.beta => coq.reduction.lazy.whd T T1 is also broken

[gares]

The problem is the section variable, if you quantify A in the theorem, then things work. The program can be fully declared outside the section, no change.

Clearly a bug.

[gares]

There is a very silly bug, apparently if you name the @pi-decl something other than A (that clashes with the section variable A) then there is no confusion... what a shame :-/

[gares]

I probably force free names without looking at the section... I mean, if A is quantified in the statement, then the code avoids the collision. So I check the proof env, without looking at the section env

[FissoreD]

Yes, you are right. I have modified my class solver so that pi-decl takes a _ as name, avoiding the bug of this issue. This allows me to enterily compile stdpp with the fix related to the double compilation of instances in the context.