Ltac unification should either ignore universe constraints, deferring them to when the proof tree is built, or should update universe constraints

[JasonGross]

I want the following code to work:

Goal Type = Type.
  match goal with |- ?x = ?x => idtac end.

I'm not sure what the behavior should be if one of the Types is replaced by Set or Prop. I'm running into a problem where rewrite fails to find the term it needs to rewrite with because of a universe mismatch, I think. (It's not quite the same as this; it's failing to unify ap10 (* Top.191 Top.191 Top.191 *) with ap10 (* Top.1863 Top.191 Top.1865 *).) It's very annoying to have to go manually fill in the arguments to the rewrite, pose the lemma, and change the variant in the goal with the variant in the hypothesis, just to rewrite. I've recently emailed coq-club about this; here is what I wrote:

I have a goal where the following succeed:

lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> let check := constr:(eq_refl : f = g) in idtac
end.
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> change f with g
end.
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> let F := eval hnf in f in let G := eval hnf in g in constr_eq F G
end.
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> pose Type as stupid;
let F := eval cbv delta [stupid] in f in let G := eval cbv delta [stupid] in g in constr_eq F G
end.
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> let T := type of f in let T' := type of g in constr_eq T T'
end.
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> let F := constr:(fun _ : Set => f) in let G := constr:(fun _ : Set => g) in constr_eq F G
end.

and the following fail:

lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?g ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> constr_eq f g
end.
(* note the lack of [g] in the following match *)
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?f ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> idtac
end.

note that match goal with |- ?G => has_evar G end fails, indicating that the problem is not evars.

Even more weirdly,

lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?f' ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> let check := constr:(idpath : f = f') in idtac
end.
lazymatch goal with |- ?f ?x0 ?x1 ?x2 ?x3 ?x4 ?x5 = ?f' ?x0 ?x1 ?x2 ?x3 ?x4' ?x5
=> progress change f with f'
end.

fails, but if I switch the order of the lazymatches, then it goes through!

What's going on here? I strongly suspect that this is a bug. (Also, what's kind of reduction does [cbv deta [foo] in bar] do when [foo] doesn't appear in [bar]?)

-Jason

P.S. The code I'm working with is available at https://github.com/JasonGross/HoTT-categories/blob/3a47db011ea7ff6f7a3fcb538fd9bcefbd6e4b0f/theories/Grothendieck/ToCat.v#L194. It only runs on top of HoTT/coq, sorry.

[mattam82]

I pushed a patch that changes the semantics by allowing to identify instances of metas ignoring universes in Ltac, but that might have unforeseen consequences. [constr_eq] does not ignore them, but the new [constr_eq_nounivs] does. [change] is up-to universes.

[JasonGross]

Thanks!

[JasonGross]

I think that Ltac matching should notice that Prop and Set are distinct; the following is the behavior I expect:

Goal Type = Type.
  match goal with |- ?x = ?x => idtac end.
Abort.

Goal Prop.
  Fail match goal with |- Type => idtac end.
Abort.

Goal Prop = Set.
  Fail match goal with |- ?x = ?x => idtac end.
Abort.

Goal Type = Prop.
  Fail match goal with |- ?x = ?x => idtac end.
Abort.

Goal Type = Set.
  Fail match goal with |- ?x = ?x => idtac end.
Abort.