`eapply` fails where `simple eapply` succeeds (universes and primitive arrays)

[fpottier]

Description of the problem

I am writing (the beginning of) a library that is supposed to help make Rocq's primitive arrays more usable. I am using Rocq 9.1. I have run into situations where eapply fails with a unification error that involves universe levels, yet simple eapply succeeds.

I have asked for help in this Zulip thread. @Janno has been able to simplify my problem into this minimal example:

Require Import Corelib.Array.PrimArray.
Axiom P : forall A t i (a:A), get t i = a.
Axiom Q : forall A a i, @length@{length.u0} A a = i.
Lemma test : forall A a i, @length@{P.u0} A a = i.
Proof.
  intros A a i.
  Succeed refine (Q _ _ _).
  Succeed simple eapply Q.
  Fail eapply Q.
  Constraint P.u0 = length.u0.
  Succeed eapply Q.
Abort.

Apparently eapply should introduce a universe constraint but does not (and fails). This seems to be a bug.

A separate question is whether primitive arrays should be universe-polymorphic.

Small Rocq / Coq file to reproduce the bug

Version of Rocq / Coq where this bug occurs

No response

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response

[SkySkimmer]

In master I get uncaught Not_found in refine (Q _ _ _). (!)
EDIT that's fixed by #21672

[SkySkimmer]

In

rocq/pretyping/unification.ml

Line 943 in 44b2136

let constr_cmp pb env sigma flags ?nargs t u =

we compare length at different instances. This generates ULub constraints (EConstr.eq_constr_universes always generates ULub for constants) between rigid universes, so we get UniversesDiffer and this fast path fails.

Then in

rocq/pretyping/unification.ml

Line 1486 in 44b2136

match infer_conv_ustate ~pb ~ts:convflags curenv sigma m1 n1 with

we are still comparing length at different instances, infer_conv_ustate tries EConstr.leq_constr_universes which produces the same constraints so we return them and get the same exception again.

We can see the same unification error with axioms:

Polymorphic Axiom foo@{u} : nat -> Prop.

Axiom bar : forall n, foo n.

Goal foo 0.
  Succeed simple apply bar.
  Fail apply bar.

I guess there are 2 things to fix:

• constr_cmp or (EConstr.eq_constr_universes) should be checking if the constant has an actual body, not just if it's marked opaque in the transparent state (

  rocq/kernel/environ.ml

  Line 728 in 44b2136

  | Undef _ | Primitive _ | Symbol _ -> false

  , note that it considers primitives non-evaluable)
• we should call infer_conv instead of infer_conv_ustate so that if we get UniversesDiffer from the fast path we actually try full conversion (infer_conv_ustate was introduced in a1c7657, but should not be needed since 8218aa0)

Note that since primitives are considered non-evaluable this would make it a bit too eager to unify rigid universes (ie unifying @length@{u} nat [| | 0 |] == @length@{v} nat [| | 0 |] would force u = v, unless there we already have u < v or v < u to force reduction). But also note that refine/evarconv already does this:

Require Import Corelib.Array.PrimArray.

Fail Definition foo@{u v|} : length@{u} [| | 0 |] = length@{v} [| | 0 |]
  := eq_refl.
(* Universe constraints are not implied by the ones declared: u = v *)
Succeed Definition foo@{u v|u < v} : length@{u} [| | 0 |] = length@{v} [| | 0 |]
  := eq_refl.
Succeed Definition foo@{u v|v < u} : length@{u} [| | 0 |] = length@{v} [| | 0 |]
  := eq_refl.

To avoid this it seems like we should still consider univ rigidity when length could reduce.
However we can't tell if length can reduce without reducing its argument which may be costly.
I guess the full solution would be to change length to make its universe irrelevant when an argument is provided, then non-applied length can be considered rigid and applied length doesn't try to unify instances. Currently we don't have code for instance cumulativity of non inductives but IMO it could be done.
(I think we only need to require 1 argument ie the type parameter for the univ to be irrelevant, but we could also require full application)
(and of course it would need to be done for all the array primitives not just length)