feat(frontends/lean/elaborator): add support for definitions such as monad_run.run

cc @Kha

library/init/lean/ir/elim_phi.lean

@@ -16,11 +16,10 @@ we put `x`, `y_1`, ... `y_n` in the same equivalence class.
 Then, we select a representative from each equivalence class and replace each
 variable with its representative.
 -/
-
 @[reducible] def elim_phi_m (α : Type) := state_t (disjoint_set var) id α
 
 def elim_phi_m.run {α} (a : elim_phi_m α) : α :=
-(a.run (mk_disjoint_set var)).1
+(run a (mk_disjoint_set var)).1
 
 def merge (x y : var) : elim_phi_m unit :=
 modify $ λ s, s.merge x y

library/init/lean/ir/ssa_check.lean

@@ -59,7 +59,7 @@ def decl.var2blockid (d : decl) : except format var2blockid :=
 @[reducible] def ssa_valid_m := except_t format (reader_t var2blockid (state_t var_set id))
 
 def ssa_valid_m.run {α} (a : ssa_valid_m α) (m : var2blockid) : except format α :=
-((a.run.run m).run mk_var_set).1
+(run a m mk_var_set).1
 
 /- Mark `x` as a variable defined in the current basic block. -/
 def var.define (x : var) : ssa_valid_m unit :=
@@ -158,7 +158,7 @@ do m ← d.var2blockid,
 except_t format (state blockid_set)
 
 def blockid_check_m.run {α} (a : blockid_check_m α) : except format α :=
-(a.run.run mk_blockid_set).1
+(run a mk_blockid_set).1
 
 def block.declare (b : block) : blockid_check_m unit :=
 do s ← get,

library/init/lean/ir/type_check.lean

@@ -79,7 +79,7 @@ match op with
 @[reducible] def type_checker_m := except_t format (reader_t (environment × list result) (state_t context id))
 
 def type_checker_m.run {α} (a : type_checker_m α) (env : environment) (r : list result) : except format α :=
-((a.run.run (env, r)).run mk_context).1
+(run a (env, r) mk_context).1
 
 def match_type (x : var) (t expected : type) : type_checker_m unit :=
 unless (t = expected) $

src/frontends/lean/elaborator.cpp

@@ -1536,12 +1536,49 @@ expr elaborator::visit_base_app_simple(expr const & _fn, arg_mask amask, buffer<
                 /* See comment above at first type_before_whnf assignment */
                 type_before_whnf = instantiate(binding_body(type), new_arg);
                 type             = whnf(type_before_whnf);
-            } else if (i < args.size()) {
-                expr new_fn = mk_app(fn, new_args.size(), new_args.data());
-                new_args.clear();
-                fn = ensure_function(new_fn, ref);
-                type_before_whnf = infer_type(fn);
-                type = whnf(type_before_whnf);
+           } else if (i < args.size()) {
+                bool progress = false;
+                /* If type is of the form `?m ...`, we may try to synthesize pending type class problems,
+                   and check whether `?m` has been instantiated or not.
+
+                   We need this trick to handle `monad_run.run`. This function has type
+                   ```
+                   run : Π {out m : Type u_1 → Type u_2} [c : monad_run out m] {α : Type u_1}, m α → out α
+                   ```
+                   The resultant type `out α` depends on resolving the type class resolution problem `monad_run out m`
+                   since `out` is marked as an `out_param`.
+
+                   Without this approach, we would have to write
+                   ```
+                   @[reducible] def type_checker_m := except_t format (reader_t (environment × list result) (state_t context id))
+
+                   def type_checker_m.run {α} (a : type_checker_m α) (env : environment) (r : list result) : except format α :=
+                   (run a (env, r) mk_context).1
+                   ```
+                   as
+                   ```
+                   @[reducible] def type_checker_m := except_t format (reader_t (environment × list result) (state_t context id))
+
+                   def type_checker_m.run {α} (a : type_checker_m α) (env : environment) (r : list result) : except format α :=
+                   let tmp := run a in
+                   (tmp (env, r) mk_context).1
+                   ```
+                   or completely avoid `run`. */
+                if (is_meta(type)) {
+                    synthesize_type_class_instances();
+                    expr new_type = instantiate_mvars(type);
+                    if (new_type != type) {
+                        type = new_type;
+                        progress = true;
+                    }
+                }
+                if (!progress) {
+                    expr new_fn = mk_app(fn, new_args.size(), new_args.data());
+                    new_args.clear();
+                    fn = ensure_function(new_fn, ref);
+                    type_before_whnf = infer_type(fn);
+                    type = whnf(type_before_whnf);
+                }
             } else {
                 lean_assert(i == args.size());
                 break;