diff --git a/src/Init/Lean/Elab/Definition.lean b/src/Init/Lean/Elab/Definition.lean
index 2cbfcc1814..bb36ff76dd 100644
--- a/src/Init/Lean/Elab/Definition.lean
+++ b/src/Init/Lean/Elab/Definition.lean
@@ -83,11 +83,11 @@ withUsedWhen ref vars xs e dummyExpr cond k
 def mkDef (view : DefView) (declName : Name) (explictLevelNames : List Name) (vars : Array Expr) (xs : Array Expr) (type : Expr) (val : Expr)
     : TermElabM (Option Declaration) := do
 let ref := view.ref;
+valType ← Term.inferType view.val val;
+val     ← Term.ensureHasType ref type valType val;
 Term.synthesizeSyntheticMVars false;
 type    ← Term.instantiateMVars ref type;
 val     ← Term.instantiateMVars view.val val;
-valType ← Term.inferType view.val val;
-val     ← Term.ensureHasType ref type valType val;
 if view.kind.isExample then pure none
 else withUsedWhen ref vars xs val type view.kind.isDefOrOpaque $ fun vars => do
   type ← Term.mkForall ref xs type;
diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean
index 49a81255a6..e3710d841c 100644
--- a/tests/lean/run/termParserAttr.lean
+++ b/tests/lean/run/termParserAttr.lean
@@ -63,7 +63,7 @@ def fooParser (rbp : Nat := 0) : Parser := categoryParser (mkNameSimple "foo") r
 @[termParser] def tst3 := parser! symbol "FOO " 0 >> fooParser 0
 
 @[termElab tst3] def elabTst3 : TermElab :=
-fun (stx : Syntax) expected? =>
+fun stx expected? =>
   elabTerm ((stx.getArg 1).getArg 1) expected?
 
 #check FOO ⟨| id 1 |⟩