From e8531ef4deaaed3f396e871e5487cb940d92c60d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 27 Apr 2021 16:03:27 -0700
Subject: [PATCH] fix: new type ascription elaborator

It was propating the incorrect type.
---
 src/Lean/Elab/BuiltinNotation.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index e2ad314c63..b3698486c4 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -230,7 +230,7 @@ where
     match ← expandCDot? e with
     | some e => `(($e : $type))
     | none   => Macro.throwUnsupported
-  | `(($e))         => do return (← expandCDot? e).getD e
+  | `(($e))         => return (← expandCDot? e).getD e
   | `(($e, $es,*))  => do
     let pairs ← mkPairs (#[e] ++ es)
     (← expandCDot? pairs).getD pairs
@@ -240,7 +240,7 @@ where
   match stx with
   | `(($e : $type)) =>
     let type ← withSynthesize (mayPostpone := true) <| elabType type
-    let e ← elabTerm e expectedType?
+    let e ← elabTerm e type
     ensureHasType type e
   | _ => throwUnsupportedSyntax