chore: revert "feat: make isRfl lazy"

This reverts commit 39b64ddc92 due to
unclear Mathlib fallout.

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -110,8 +110,8 @@ where
       return false
 
 private def useImplicitDefEqProof (thm : SimpTheorem) : SimpM Bool := do
-  if (← getConfig).implicitDefEqProofs then
-    thm.getRfl
+  if thm.rfl then
+    return (← getConfig).implicitDefEqProofs
   else
     return false
 
@@ -218,7 +218,7 @@ where
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.1.priority > e₂.1.priority
       for (thm, numExtraArgs) in candidates do
-        unless inErasedSet thm || (rflOnly && !(← thm.getRfl)) do
+        unless inErasedSet thm || (rflOnly && !thm.rfl) do
           if let some result ← tryTheoremWithExtraArgs? e thm numExtraArgs then
             trace[Debug.Meta.Tactic.simp] "rewrite result {e} => {result.expr}"
             return some result
@@ -236,7 +236,7 @@ where
     else
       let candidates := candidates.insertionSort fun e₁ e₂ => e₁.priority > e₂.priority
       for thm in candidates do
-        unless inErasedSet thm || (rflOnly && !(← thm.getRfl)) do
+        unless inErasedSet thm || (rflOnly && !thm.rfl) do
           let result? ← withNewMCtxDepth do
             let val  ← thm.getValue
             let type ← inferType val
@@ -352,7 +352,7 @@ def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (Option Result) :=
 def simpMatchCore (matcherName : Name) (e : Expr) : SimpM Step := do
   for matchEq in (← Match.getEquationsFor matcherName).eqnNames do
     -- Try lemma
-    match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rflTask := (← isRflTheorem matchEq) }) with
+    match (← withReducible <| Simp.tryTheorem? e { origin := .decl matchEq, proof := mkConst matchEq, rfl := (← isRflTheorem matchEq) }) with
     | none   => pure ()
     | some r => return .visit r
   return .continue
@@ -433,7 +433,7 @@ def sevalGround : Simproc := fun e => do
     -- `declName` has equation theorems associated with it.
     for eqn in eqns do
       -- TODO: cache SimpTheorem to avoid calls to `isRflTheorem`
-      if let some result ← Simp.tryTheorem? e { origin := .decl eqn, proof := mkConst eqn, rflTask := (← isRflTheorem eqn) } then
+      if let some result ← Simp.tryTheorem? e { origin := .decl eqn, proof := mkConst eqn, rfl := (← isRflTheorem eqn) } then
         trace[Meta.Tactic.simp.ground] "unfolded, {e} => {result.expr}"
         return .visit result
     return .continue

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -122,56 +122,45 @@ structure SimpTheorem where
     It is also viewed an `id` used to "erase" `simp` theorems from `SimpTheorems`.
   -/
   origin      : Origin
-  /-- True if `proof` is by `Eq.refl` or `rfl`. Lazy so `[simp]` doesn't block the main thread. -/
-  rflTask     : Task Bool
+  /-- `rfl` is true if `proof` is by `Eq.refl` or `rfl`. -/
+  rfl         : Bool
   deriving Inhabited
 
-def SimpTheorem.getRfl (t : SimpTheorem) : CoreM Bool :=
-  traceBlock "SimpTheorem.getRfl" t.rflTask
-
 mutual
-  partial def isRflProofCore (env : Environment) (type : Expr) (proof : Expr) : Task Bool :=
+  partial def isRflProofCore (type : Expr) (proof : Expr) : CoreM Bool := do
     match type with
     | .forallE _ _ type _ =>
       if let .lam _ _ proof _ := proof then
-        isRflProofCore env type proof
+        isRflProofCore type proof
       else
-        .pure false
+        return false
     | _ =>
       if type.isAppOfArity ``Eq 3 then
         if proof.isAppOfArity ``Eq.refl 2 || proof.isAppOfArity ``rfl 2 then
-          .pure true
+          return true
         else if proof.isAppOfArity ``Eq.symm 4 then
           -- `Eq.symm` of rfl theorem is a rfl theorem
-          isRflProofCore env type proof.appArg! -- small hack: we don't need to set the exact type
+          isRflProofCore type proof.appArg! -- small hack: we don't need to set the exact type
         else if proof.getAppFn.isConst then
           -- The application of a `rfl` theorem is a `rfl` theorem
           -- A constant which is a `rfl` theorem is a `rfl` theorem
-          isRflTheoremCore env proof.getAppFn.constName!
+          isRflTheorem proof.getAppFn.constName!
         else
-          .pure false
+          return false
       else
-        .pure false
+        return false
 
-  partial def isRflTheoremCore (env : Environment) (declName : Name) : Task Bool := Id.run do
-    env.findTask declName |>.bind (sync := true) fun
-      | none => .pure false
-      | some aconst => aconst.constInfo.bind (sync := true) fun
-        | .thmInfo info => isRflProofCore env info.type info.value
-        | _             => .pure false
+  partial def isRflTheorem (declName : Name) : CoreM Bool := do
+    let { kind := .thm, constInfo, .. } ← getAsyncConstInfo declName | return false
+    let .thmInfo info ← traceBlock "isRflTheorem theorem body" constInfo | return false
+    isRflProofCore info.type info.value
 end
 
-def isRflProof (proof : Expr) : MetaM (Task Bool) := do
-  let env ← getEnv
+def isRflProof (proof : Expr) : MetaM Bool := do
   if let .const declName .. := proof then
-    return isRflTheoremCore env declName
+    isRflTheorem declName
   else
-    let type ← inferType proof
-    return isRflProofCore env type proof
-
-def isRflTheorem (declName : Name) : MetaM (Task Bool) := do
-  let env ← getEnv
-  return isRflTheoremCore env declName
+    isRflProofCore (← inferType proof) proof
 
 instance : ToFormat SimpTheorem where
   format s :=
@@ -412,7 +401,7 @@ private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array
       match type.eq? with
       | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs noIndexAtArgs, ← isPerm lhs rhs)
       | none => throwError "unexpected kind of 'simp' theorem{indentExpr type}"
-    return { origin, keys, perm, post, levelParams, proof, priority := prio, rflTask := (← isRflProof proof) }
+    return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl := (← isRflProof proof) }
 
 private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool) (prio : Nat) : MetaM (Array SimpTheorem) := do
   let cinfo ← getConstVal declName

src/Lean/Meta/Tactic/Split.lean

@@ -51,7 +51,7 @@ where
       let simpTheorem := {
         origin := .decl matchEqDeclName
         proof := mkConst matchEqDeclName
-        rflTask := (← isRflTheorem matchEqDeclName)
+        rfl := (← isRflTheorem matchEqDeclName)
       }
       match (← withReducible <| Simp.tryTheorem? e simpTheorem) with
       | none => return .continue

src/Lean/Meta/Tactic/Unfold.lean

@@ -22,7 +22,7 @@ def unfold (e : Expr) (declName : Name) : MetaM Simp.Result := do
     return { expr  := (← deltaExpand e (· == declName)) }
 where
   pre (unfoldThm : Name) (e : Expr) : SimpM Simp.Step := do
-    match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm, proof := mkConst unfoldThm, rflTask := (← isRflTheorem unfoldThm) }) with
+    match (← withReducible <| Simp.tryTheorem? e { origin := .decl unfoldThm, proof := mkConst unfoldThm, rfl := (← isRflTheorem unfoldThm) }) with
     | none   => pure ()
     | some r => match (← reduceMatcher? r.expr) with
       | .reduced e' => return .done { r with expr := e' }