diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 3b96765695..c45e2af19b 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Lean.Util.FindMVar
 import Lean.Elab.Term
 import Lean.Elab.Binders
+import Lean.Elab.SyntheticMVars
 
 namespace Lean
 namespace Elab
@@ -276,9 +277,18 @@ private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermEl
     if ctx.namedArgs.isEmpty && ctx.argIdx == ctx.args.size then
       finalize ()
     else do
-      e ← tryCoeFun eType e;
-      eType ← inferType e;
-      elabAppArgsAux ctx e eType
+      -- eType may become a forallE after we synthesize pending metavariables
+      synthesizeAppInstMVars ctx.instMVars;
+      synthesizeSyntheticMVars;
+      let ctx := { ctx with instMVars := #[] };
+      -- try to normalize again.
+      eType ← whnfForall eType;
+      match eType with
+      | Expr.forallE _ _ _ _ => elabAppArgsAux ctx e eType
+      | _ => do
+        e ← tryCoeFun eType e;
+        eType ← inferType e;
+        elabAppArgsAux ctx e eType
 
 private def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg)
     (expectedType? : Option Expr) (explicit : Bool) : TermElabM Expr := do
diff --git a/tests/lean/repr_issue.lean b/tests/lean/repr_issue.lean
index 1e515b5770..4d86d2aead 100644
--- a/tests/lean/repr_issue.lean
+++ b/tests/lean/repr_issue.lean
@@ -1,3 +1,4 @@
+new_frontend
 def foo {m} [Monad m] [MonadExcept String m] [MonadState (Array Nat) m] : m Nat :=
 catch (do modify $ fun (a : Array Nat) => a.set! 0 33;
           throw "error")