Issue with refine

[patrick-nicodemus]

I wrote an Elpi tactic to simplify the goal, I tried to follow something I found in some code in the repository.

    solve (goal _Ctx _Trigger Type _Proof _ as G) GL :-
        coq.reduction.lazy.whd Type Typea,
        not (same_term Type Typea),
        refine {{ _ : lp:Typea }} G GL.

I managed to get the following error when applying this to a goal:

File "./cat_cc.v", line 71, characters 14-29:                                                  
Error: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.                                                    
(while solving unification constraints,                                                        
 see flag "Solve Unification Constraints")

Is this to be expected, or a bug? Should I not use the lazy reduction on the goal in this context?
I can try to minimize it but I am drawing on some code from the HoTT library so it will take me a while.

Edit: The problem is not related to lazy reduction, this is a red herring.

[patrick-nicodemus]

Here is a reproducible instance of the problem, with _Coq project containing -arg -noinit
(Edited a bit to reduce dependencies and eliminate some sources of confusion)

Edit: January 30 The problem does not have to do with lazy reduction. I have edited the code sample
to remove the lazy reduction.

From elpi Require Import elpi.
Require Import Ltac.

From HoTT Require Import Basics WildCat.Core.
From HoTT Require NatTrans.

Record Fun01 (A B : Type) `{IsGraph A} `{IsGraph B} := {
  fun01_F : A -> B;
  fun01_is0functor : Is0Functor fun01_F;
}.

Coercion fun01_F : Fun01 >-> Funclass.
Existing Instance fun01_is0functor.

Instance isgraph_fun01 (A B : Type) `{IsGraph A} `{Is1Cat B} : IsGraph (Fun01 A B).
Proof.
  srapply Build_IsGraph.
  intros [F ?] [G ?].
  exact (NatTrans.NatTrans F G).
Defined.

Instance is2graph_fun01 (A B : Type) `{IsGraph A, Is1Cat B}
  : Is2Graph (Fun01 A B).
Proof.
  intros [F ?] [G ?]; apply Build_IsGraph.
  intros [alpha ?] [gamma ?].
  exact (forall a, alpha a $== gamma a).
Defined.

Elpi Tactic simplify. 
Elpi Accumulate lp:{{
    solve (goal _Ctx _Trigger Type _Proof _args as G) GL :-
      refine {{ _ : lp:Type }} G GL.
}}.

Inductive Unit := tt.
Goal Unit.
elpi simplify.


Goal forall (A B : Type) 
  `{IsGraph A} `{Is1Cat B}
  (F : Fun01 A B),
  F $-> F.
Proof.
  intros.
  apply (NatTrans.Build_NatTrans (fun a => Id (F a))).
  { 
    constructor.
    { intros. transitivity (fmap F f).
      { apply cat_idl. }
      { elpi simplify. }
    }
  }
  Admitted.

Elpi Trace Browser dumps a 2300 line text file, if you have any idea where to start looking let me know.
For some reason the VSCode Elpi trace tool is not working with this file, I cannot get the visual representation of the trace to show up.

[patrick-nicodemus]

Here are the last few lines of the trace text file. It seems the very last rule application was a success (which is just std.append [] [] []) which I think suggests that the Not_found exception is not being raised from the part of the program which is contained in the trace? I don't know if that interpretation is correct.

{"step" : 295,"kind" : ["Info"],"goal_id" : 314,"runtime_id" : 0,"name" : "user:newgoal","payload" : 
 ["evar (X127 c11 c12 c13 c14 c15 c16 c17 c18 c19 c20 c21) 
    (app [primitive (proj HoTT.WildCat.Core.Hom 1),
       app
         [c15, app [primitive (proj minimize2.fun01_F 4), c18, c19], 
      app [primitive (proj minimize2.fun01_F 4), c18, c20]], 
    app
     [primitive (proj HoTT.WildCat.Core.cat_comp 3), c16, 
      app [primitive (proj minimize2.fun01_F 4), c18, c19], 
      app [primitive (proj minimize2.fun01_F 4), c18, c20], 
      app [primitive (proj minimize2.fun01_F 4), c18, c20], 
      app
       [primitive (proj HoTT.WildCat.Core.Id 2), c16, 
        app [primitive (proj minimize2.fun01_F 4), c18, c20]], 
      app
       [primitive (proj HoTT.WildCat.Core.fmap 5), 
        app [primitive (proj minimize2.fun01_is0functor 5), c18], c19, c20, 
        c21]], 
    app
     [primitive (proj HoTT.WildCat.Core.cat_comp 3), c16, 
      app [primitive (proj minimize2.fun01_F 4), c18, c19], 
      app [primitive (proj minimize2.fun01_F 4), c18, c19], 
      app [primitive (proj minimize2.fun01_F 4), c18, c20], 
      app
       [primitive (proj HoTT.WildCat.Core.fmap 5), 
        app [primitive (proj minimize2.fun01_is0functor 5), c18], c19, c20, 
        c21], 
      app       [primitive (proj HoTT.WildCat.Core.Id 2), c16, 
        app [primitive (proj minimize2.fun01_F 4), c18, c19]]]]) 
 (X123 c11 c12 c13 c14 c15 c16 c17 c18 c19 c20 c21)"]}
{"step" : 295,"kind" : ["Info"],"goal_id" : 310,"runtime_id" : 0,"name" : "user:rule:builtin","payload" : ["success"]}
{"step" : 296,"kind" : ["Info"],"goal_id" : 305,"runtime_id" : 0,"name" : "user:curgoal","payload" : ["std.append","std.append [] [] X124"]}
{"step" : 296,"kind" : ["Info"],"goal_id" : 305,"runtime_id" : 0,"name" : "user:rule","payload" : ["backchain"]}
{"step" : 296,"kind" : ["Info"],"goal_id" : 305,"runtime_id" : 0,"name" : "user:rule:backchain:candidates","payload" : ["File \"builtin_stdlib.elpi\", line 87, column 0, characters 2841-2854:"]}
{"step" : 296,"kind" : ["Info"],"goal_id" : 305,"runtime_id" : 0,"name" : "user:rule:backchain:try","payload" : ["File \"builtin_stdlib.elpi\", line 87, column 0, characters 2841-2854:","(std.append [] A0 A0) :- ."]}
{"step" : 296,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["A0 := []"]}
{"step" : 296,"kind" : ["Info"],"goal_id" : 0,"runtime_id" : 0,"name" : "user:assign","payload" : ["X124 := []"]}
{"step" : 296,"kind" : ["Info"],"goal_id" : 305,"runtime_id" : 0,"name" : "user:rule:backchain","payload" : ["success"]}

[patrick-nicodemus]

The problem appears to be in coq.elaborate-skeleton.
One can replace the tactic above with

  solve (goal _ _ Ty _ _) _ :-
    (@keepunivs! => coq.elaborate-skeleton  {{ _ : lp:Ty}} Ty _ ok).

and get the error.

[gares]

The bug is related to the fact that, at the end of a tactic application, Elpi cleans up the evar map of unreachable evars, but the computation is wrong since it does not consider "unification constraints" as roots.

These constraints are introduced by constructor, or even simple apply NatTrans.Build_Is1Natural'.. It is a bit unclear to me why, at the moment. By helping Coq's unification with a type cast on the last argument of Build_Is1Natural' things seems ok:

refine (let HN : @NatTrans.Transformation A (fun _ : A => B) (fun _ : A => IsGraph0) (@fun01_F A B H IsGraph0 F) (@fun01_F A B H IsGraph0 F)
  :=
  fun a : A => @Id B IsGraph0 Is01Cat0 (@fun01_F A B H IsGraph0 F a) in _).

apply (@NatTrans.Build_Is1Natural' A B H IsGraph0 Is2Graph0 Is01Cat0 H0 (@fun01_F A B H IsGraph0 F) (@fun01_is0functor A B H IsGraph0 F) (@fun01_F A B H IsGraph0 F) (@fun01_is0functor A B H IsGraph0 F) HN).

generates no constraints, and then Elpi code works fine.

So, there is a bug in Coq-Elpi when the proof state contains a unification constraint (that is not referenced by the goal).