refactor: move isMonad? to AppBuilder.lean

src/Lean/Elab/Term.lean

@@ -625,31 +625,6 @@ private def isTypeApp? (type : Expr) : TermElabM (Option (Expr × Expr)) := do
   | Expr.app m α _ => pure (some ((← instantiateMVars m), (← instantiateMVars α)))
   | _              => pure none
 
-/-
-private def isMonad? (type : Expr) : TermElabM (Option IsMonadResult) := do
-  let type ← withReducible $ whnf type
-  match type with
-  | Expr.app m α _ =>
-    try
-      let monadType ← mkAppM `Monad #[m]
-      let result    ← trySynthInstance monadType
-      match result with
-      | LOption.some inst => pure (some { m := m, α := α, inst := inst })
-      | _                 => pure none
-    catch _ => pure none
-  | _ => pure none
--/
-
-private def isMonad? (m : Expr) : TermElabM (Option Expr) :=
-  try
-    let monadType ← mkAppM `Monad #[m]
-    let result    ← trySynthInstance monadType
-    match result with
-    | LOption.some inst => pure inst
-    | _                 => pure none
-  catch _ =>
-    pure none
-
 def synthesizeInst (type : Expr) : TermElabM Expr := do
   let type ← instantiateMVars type
   match (← trySynthInstance type) with

src/Lean/Meta/AppBuilder.lean

@@ -445,6 +445,17 @@ def mkImpCongrCtx (h₁ h₂ : Expr) : MetaM Expr :=
 def mkForallCongr (h : Expr) : MetaM Expr :=
   mkAppM ``forallCongr #[h]
 
+/-- Return instance for `[Monad m]` if there is one -/
+def isMonad? (m : Expr) : MetaM (Option Expr) :=
+  try
+    let monadType ← mkAppM `Monad #[m]
+    let result    ← trySynthInstance monadType
+    match result with
+    | LOption.some inst => pure inst
+    | _                 => pure none
+  catch _ =>
+    pure none
+
 /-- Return `(n : type)`, a numeric literal of type `type`. The method fails if we don't have an instance `OfNat type n` -/
 def mkNumeral (type : Expr) (n : Nat) : MetaM Expr := do
   let u ← getDecLevel type