refactor: rfl tactic: do not use Kernel.isDefEq (#3772)

Sebastian mentioned that the use of the kernel defeq was to work around
a performance issue that was fixed since. Let's see if we can do
without.

This is also a semantic change: Ground terms (no free vars, no mvars)
are reduced at
“all” transparency even if the the transparency setting is default. This
was the case
even before 03f6b87647 switched to the
kernel defeq
checking for performance. It seems that this is rather surprising
behavior from the user
point of view. The fallout on batteries and mathlib is rather limited,
only a few
`rfl` proofs seem to have (inadvertently or not) have relied on this.

The speedcenter reports no significant regressions on core or mathlib.

src/Lean/Meta/Tactic/Refl.lean

@@ -10,12 +10,6 @@ import Lean.Meta.Tactic.Apply
 
 namespace Lean.Meta
 
-private def useKernel (lhs rhs : Expr) : MetaM Bool := do
-  if lhs.hasFVar || lhs.hasMVar || rhs.hasFVar || rhs.hasMVar then
-    return false
-  else
-    return (← getTransparency) matches TransparencyMode.default | TransparencyMode.all
-
 /--
 Close given goal using `Eq.refl`.
 -/
@@ -27,10 +21,7 @@ def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do
       throwTacticEx `rfl mvarId m!"equality expected{indentExpr targetType}"
     let lhs ← instantiateMVars targetType.appFn!.appArg!
     let rhs ← instantiateMVars targetType.appArg!
-    let success ← if (← useKernel lhs rhs) then
-      ofExceptKernelException (Kernel.isDefEq (← getEnv) {} lhs rhs)
-    else
-      isDefEq lhs rhs
+    let success ← isDefEq lhs rhs
     unless success do
       throwTacticEx `rfl mvarId m!"equality lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
     let us := targetType.getAppFn.constLevels!

tests/lean/run/4644.lean

@@ -10,9 +10,17 @@ termination_by a.size - i
 def check_sorted [x: LE α] [DecidableRel x.le] (a: Array α): Bool :=
   sorted_from_var a 0
 
--- works (because `rfl` of closed terms resorts to kernel defeq, see #3772)
-example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] := by
-  rfl
+/--
+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 reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
+⊢ check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] = true
+-/
+#guard_msgs in
+example: check_sorted #[0, 3, 3, 5, 8, 10, 10, 10] = true := by
+  rfl -- fails because `rfl` uses `.default` transparency, and `sorted_from_var` is marked as irreducible
 
 /--
 error: tactic 'decide' failed for proposition

tests/lean/run/ack.lean

@@ -25,17 +25,3 @@ set_option diagnostics.threshold 500 in
 set_option diagnostics true in
 theorem ex : ack 3 2 = 29 :=
   rfl
-
-
-/--
-info: [kernel] unfolded declarations (max: 1193, num: 4):
-  [kernel] Nat.casesOn ↦ 1193
-  [kernel] Nat.rec ↦ 1065
-  [kernel] Eq.ndrec ↦ 973
-  [kernel] Eq.rec ↦ 973use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
--/
-#guard_msgs in
-set_option diagnostics true in
-set_option diagnostics.threshold 800 in
-theorem ack_3_2_eq_29 : ack 3 2 = 29 := by
-  rfl -- uses kernel defeq checker, so only kernel diags shown

tests/lean/run/treeNode.lean

@@ -37,5 +37,5 @@ theorem length_treeToList_eq_numNames (t : TreeNode) : (treeToList t).length = n
 where
   helper (cs : List TreeNode) : (cs.map treeToList).join.length = numNamesLst cs := by
     match cs with
-    | [] => rfl
+    | [] => simp [List.join, numNamesLst]
     | c::cs' => simp [List.join, List.map, numNamesLst, length_treeToList_eq_numNames c, helper cs']

tests/lean/run/wfirred.lean

@@ -29,7 +29,15 @@ but is expected to have type
 #guard_msgs in
 example : foo (n+1) = foo n := rfl
 
--- This succeeding is a bug or misfeature in the rfl tactic, using the kernel defeq check
+-- also for closed terms
+/--
+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 reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
+`exact HEq.rfl` etc.
+⊢ foo 0 = 0
+-/
 #guard_msgs in
 example : foo 0 = 0 := by rfl