From ecb1bc982faefeaffbea03f92ba639de13dfb145 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Dec 2019 07:23:42 -0800
Subject: [PATCH] feat: invoke `ensureHasType` at `elabArg`

---
 src/Init/Lean/Elab/Term.lean | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 500f980cbe..36908159c0 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -579,8 +579,10 @@ match arg with
 | Arg.expr val => do
   valType ← inferType ref val;
   ensureHasType ref expectedType valType val
-| Arg.stx val  =>
-  elabTerm val expectedType
+| Arg.stx val  => do
+  val ← elabTerm val expectedType;
+  valType ← inferType ref val;
+  ensureHasType ref expectedType valType val
 
 private partial def elabAppArgsAux (ref : Syntax) (args : Array Arg) (expectedType? : Option Expr) (explicit : Bool)
     : Nat → Array NamedArg → Array MVarId → Expr → Expr → TermElabM Expr
@@ -916,6 +918,12 @@ fun stx expectedType? => do
 @[builtinTermElab proj] def elabProj : TermElab := elabApp
 @[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabApp
 
+/-
+@[builtinTermElab str] def elabStr : TermElab :=
+fun stx _ => do
+  throw (arbitrary _)
+-/
+
 end Term
 
 @[init] private def regTraceClasses : IO Unit := do