Trying to understand behavior of whd under universe polymorphism + primitive projections

[patrick-nicodemus]

Edit: Gaetan helped me narrow down the cause, see below.

I am wondering if you can help me figure out this strange behavior.
I created a Coq project with no standard library linked in and one of my dependencies is the coq-HoTT library https://github.com/HoTT/Coq-HoTT.

I have slightly different versions of the same code.

From elpi Require Import elpi.
Record A := { p : Type }.
From HoTT Require Overture.
(* Record A := { p : Type }. *)

Elpi Tactic simplify. 
Elpi Accumulate lp:{{
        
    solve (goal _Ctx _Trigger Type _Proof _ as G) GL :-
        coq.say Type,
        whd1 Type Typea,
        refine {{ _ : lp:Typea }} G GL.
}}.

Inductive Unit := tt.
Definition a : A := {| p := Unit |}.
Goal p a.
Proof.
    elpi simplify.

The tactic elpi simplify works in the expected way. However if I define the record after I load the HoTT library (as in the commented line) the tactic fails. Do you have any idea why this might be the case?

[SkySkimmer]

The global settings in https://github.com/HoTT/Coq-HoTT/blob/master/theories/Basics/Settings.v are possible causes. You can try each instead of the Require to see what happens.

[patrick-nicodemus]

@SkySkimmer Thanks very much, that helps a lot.

From elpi Require Import elpi.
Require Import Ltac.
Set Universe Polymorphism.
Set Primitive Projections.
Record A := { p : Type }.
Elpi Tactic simplify. 
Elpi Accumulate lp:{{
        
    solve (goal _Ctx _Trigger Type _Proof _ as G) GL :-
        coq.say Type,
        whd1 Type Typea,
        refine {{ _ : lp:Typea }} G GL.
}}.

Inductive Unit := tt.
Definition a : A := {| p := Unit |}.
Goal p a.
Proof.
    elpi simplify.

These flags both effect the behavior of the code. With just Set Universe Polymorphism, the Elpi representation of p a is

 [pglobal (const «p») «minimize.406», 
  pglobal (const «a») «minimize.406»]

and the whd is match a with | {| p := p0 |} => p0 end.

With both of the flags mentioned above, the Elpi representation of p a is

app [primitive (proj minimize.p 0), pglobal (const «a») «minimize.427»]

and whd doesn't change the term.
So I can see specifically what's causing it but I still don't really understand what's happening here. I did read the Elpi code for whd here but I don't understand what's failing.

[SkySkimmer]

p a is already the normal form when p is a primitive projection (assuming you don't want to unfold a)

[patrick-nicodemus]

Okay, that makes sense. I can understand that point of view. But, also, if I change the definition of simplify to:

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

it does simplify p a to Unit. Is this to be expected, or is lazy.whd supposed to have a different behavior?

[gares]

You could try to write Elpi Trace Browser. just before calling elpi simplify, ignore the instructions that are printed.
Once elpi simplify terminates in vscode you can open the elpi tracer panel, open /tmp/traced.tmp.json (be sure to disable syntax highlighting in the elpi-lang extension setting).

Sorry, it is a bit clumsy, but should let you see all the steps and pinpoint the problem.

If the above does not work, you can also try Elpi Trace. but the output is plain text, much harder to navigate.

[patrick-nicodemus]

@gares Thanks, I get the usage of the browser now.

As I step through the code I see that whd-indc defined for global inductives but there's no analogous clause for polymorphic global inductives. Is this intentional or an oversight?

coq-elpi/elpi/elpi-reduction.elpi

Line 52 in fd11b7a

whd-indc A GR KA :- whd A [] VA C, !, not(var VA), VA = global (indc GR), KA = C.

[gares]

An oversight.