From 246e0a55320ea7beaf5eea9e6e2daffb587f67b6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 11 Jan 2020 12:01:12 -0800 Subject: [PATCH] fix: propagate type before `synthesizeSyntheticMVars` --- src/Init/Lean/Elab/Definition.lean | 4 ++-- tests/lean/run/termParserAttr.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) 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 |⟩