RFC: A single rfl tactic implementation

[nomeata]

I noticed (while #3299 passed by) that rfl produces a rather unhelpful error message:

import Std
example (P : Prop) : P := by rf

gives

type mismatch
  HEq.rfl
has type
  HEq ?m.10 ?m.10 : Prop
but is expected to have type
  P : Prop

This is not a good UX for a tactic that early users will be exposed to early (and also not great later on).

Looking at what happens I found that there are four different implementations registered (using macro/macro_rules) for rfl:

• Wrapping Lean.MVarId.refl, for Eq.
• exact HEq.rfl
• exact Iff.rfl
• https://leanprover-community.github.io/mathlib4_docs/Std/Tactic/Relation/Rfl.html#Lean.MVarId.applyRfl, which supports any relation with a suitable @[refl] lemma.

Unfortunately, it seems that using macro_rules to extend tactics doesn’t give great control over which error message is shown if all fail.

Assuming we want @[refl] in core, I propose that, after upstreaming Std.Tactic.Relation.Rfl, we back the rlf tactic by a single function that combines Lean.MVarId.refl and Lean.MVarId.applyRfl, possibly still with a special path for Eq (should that be needed, TBD), and with good error messages for the various failure modes.

With a suitable @[refl] attribute, this should allow us to remove the extra exact ….rfl macro rules.

Community Feedback

This was escalated from a discussion on zulip.

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[nomeata]

Having a closer look. One issue is that the order of parameters in HEq makes it ineligible to the @[refl] machinery:

HEq.refl.{u} {α : Sort u} (a : α) : @HEq α a α a

(it would have to be @HEq α α a a).

If one still wants to persue the goal of a macro_rules-free implementation to get good control over the error messages, I see these plausible options:

• Hard-coding HEq.refl in the tactic implementation

• Changing the order of parameters on HEq

  I personally would have expected

  inductive HEq : {α : Sort u} → {β : Sort u} → α → β → Prop where

  ~~but there may be a good reason for the other order that I don’t know (if there is we should put a comment on the code).~~

  Even if there is no such good reason, not wanting to break existing code may be a reason.

  (See explanation below)

• Drop HEq support from the rfl tactic, and expect people to write exact HEq.rfl. Maybe that’s the best option, given that HEq is a rather special case anyways and it doesn’t hurt to be explicit here.

[digama0]

• Changing the order of parameters on HEq I personally would have expected

  inductive HEq : {α : Sort u} → {β : Sort u} → α → β → Prop where

  but there may be a good reason for the other order that I don’t know (if there is we should put a comment on the code).

There is: In Eq and HEq, the left argument is a parameter and the right one is an index of the inductive type. Lean strictly enforces that parameters come before indices in the inductive type, so interchanging the arguments would make (a : α) argument an index as well, which changes the type of HEq.rec considerably (try it and see), in a less than helpful direction.

[digama0]

There is another option you did not list:

• Make the @[rfl] attribute support relations that have dependencies on both sides.

This would be desirable for other reasons as well; I recall something similar coming up with being able to use calc for arrows in a category or something like that, where the type signature of Trans wasn't general enough to handle the implicit arguments. (I forget whether this concerns the current or a previous version of Trans though, I'd have to look up the details.)

In short, the issue here is not unique to HEq, so I would advise against something that special cases it.

[nomeata]

Ah, yes, parameter vs. index makes sense, thanks.

True, extending rfl is an option. I disregarded it as too complex initially, but if we find more examples then that might eventually be the best course of action. I also vaguely remember the Trans issues.

[digama0]

I think keeping apply HEq.refl as a special extra case in the meantime (but in an elab rather than using macro_rules alternation so that you can control the error message better) would be a way to not regress rfl while figuring out how to handle the general case.

Another reason you probably want rfl to work on HEq goals even though they are discouraged: HEq goals / hypotheses are generated by congr and cases in order to reason about telescope equalities, and rfl is used to close those goals when they are trivial. It's possible that there is some eq_of_heq inserted that will save you but I wouldn't be surprised if either some tactic is skipping that step or if there is some weird metavariable condition under which eq_of_heq won't apply because the types are not yet known to be equal and as a result rfl is given a HEq goal anyway.

[nomeata]

(Just for my own record: I attempted this refactoring, but got stuck in what’s either a boostrapping maze or a misunderstanding of how things works, and ran out of time today. Putting this back on the stack of things to look at when I have some extra time to spare. If someone else does tackles before I do then of course I don’t mind.)

(Update: #3714 has the tactic as I think it could be, it doesn’t swap it out for rfl yet.)

[leodemoura]

The new message is

error: The rfl tactic failed. Possible reasons:
- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
- The arguments of the relation are not equal.
Try using the reflexivitiy lemma for your relation explicitly, e.g. `exact Eq.rfl`.
P : Prop
⊢ P

Marking it as closing soon

[nomeata]

3714 and #3718 contain further improvements, including even better error messages, by having a single implementation, but I got stalled there because of the different transparency levels the current tactics work at. Might revisit that later, but I have the draft PRs to recall, so happy to close this issue.

[nomeata]

I actually picked up the work on these PRs. So reopening this, so that merging them can close it properly :-D