refactor: do not try rfl in mkEqnTypes in WF.mkEqns (#4047)

when dealing with well-founded recursive definitions, `tryURefl` isn't
going to be that useful and possibly slow. So disable that code path
when doing well-founded recursion.

(This is a variant of #4025 where I tried using `with_reducible` to
limit the impact of slow unfolding, but if we can get away with
disabling it complete, then even better.)

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -228,20 +228,23 @@ private def shouldUseSimpMatch (e : Expr) : MetaM Bool := do
             throwThe Unit ()
   return (← (find e).run) matches .error _
 
-partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
+partial def mkEqnTypes (tryRefl : Bool) (declNames : Array Name) (mvarId : MVarId) : MetaM (Array Expr) := do
   let (_, eqnTypes) ← go mvarId |>.run { declNames } |>.run #[]
   return eqnTypes
 where
   go (mvarId : MVarId) : ReaderT Context (StateRefT (Array Expr) MetaM) Unit := do
     trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}"
-    if (← tryURefl mvarId) then
-      saveEqn mvarId
-      return ()
+    if tryRefl then
+      if (← tryURefl mvarId) then
+        saveEqn mvarId
+        return ()
 
     if let some mvarId ← expandRHS? mvarId then
       return (← go mvarId)
---  The following `funext?` was producing an overapplied `lhs`. Possible refinement: only do it if we want to apply `splitMatch` on the body of the lambda
-/-    if let some mvarId ← funext? mvarId then
+
+    --  The following `funext?` was producing an overapplied `lhs`. Possible refinement: only do it
+    --  if we want to apply `splitMatch` on the body of the lambda
+    /- if let some mvarId ← funext? mvarId then
         return (← go mvarId) -/
 
     if (← shouldUseSimpMatch (← mvarId.getType')) then

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -62,7 +62,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst info.declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
-    mkEqnTypes #[info.declName] goal.mvarId!
+    mkEqnTypes (tryRefl := true) #[info.declName] goal.mvarId!
   let baseName := info.declName
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -114,7 +114,8 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
     let us := info.levelParams.map mkLevelParam
     let target ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
     let goal ← mkFreshExprSyntheticOpaqueMVar target
-    mkEqnTypes info.declNames goal.mvarId!
+    withReducible do
+      mkEqnTypes (tryRefl := false) info.declNames goal.mvarId!
   let mut thmNames := #[]
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]!