feat: add elabTypeOf and elabEnsureTypeOf

src/Lean/Elab/Term.lean

@@ -520,19 +520,18 @@ if hasCDot stx then do
 else
   pure none
 
+def mkTypeMismatchError (e : Expr) (eType : Expr) (expectedType : Expr) (header : String := "type mismatch") : MessageData :=
+header ++ indentExpr e
+++ Format.line ++ "has type" ++ indentExpr eType
+++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType
+
 def throwTypeMismatchError {α} (expectedType : Expr) (eType : Expr) (e : Expr)
     (f? : Option Expr := none) (extraMsg? : Option MessageData := none) : TermElabM α :=
 let extraMsg : MessageData := match extraMsg? with
   | none          => Format.nil
   | some extraMsg => Format.line ++ extraMsg;
 match f? with
-| none =>
-  let msg : MessageData :=
-    "type mismatch" ++ indentExpr e
-    ++ Format.line ++ "has type" ++ indentExpr eType
-    ++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType
-    ++ extraMsg;
-  throwError msg
+| none   => throwError $ mkTypeMismatchError e eType expectedType ++ extraMsg
 | some f => Meta.throwAppTypeMismatch f e extraMsg
 
 @[inline] def withoutMacroStackAtErr {α} (x : TermElabM α) : TermElabM α :=
@@ -1277,6 +1276,23 @@ fun stx _ =>
   | some val => pure $ toExpr val
   | none     => throwIllFormedSyntax
 
+@[builtinTermElab typeOf] def elabTypeOf : TermElab :=
+fun stx _ => do
+  e ← elabTerm (stx.getArg 1) none;
+  inferType e
+
+@[builtinTermElab ensureTypeOf] def elabEnsureTypeOf : TermElab :=
+fun stx expectedType? =>
+  match (stx.getArg 2).isStrLit? with
+  | none     => throwIllFormedSyntax
+  | some msg => do
+    refTerm ← elabTerm (stx.getArg 1) none;
+    refTermType ← inferType refTerm;
+    e ← elabTerm (stx.getArg 3) expectedType?;
+    eType ← inferType e;
+    unlessM (isDefEq eType refTermType) $ throwError $ mkTypeMismatchError e eType refTermType msg;
+    pure e
+
 private def mkSomeContext : Context :=
 { fileName      := "<TermElabM>",
   fileMap       := arbitrary _,

tests/lean/typeOf.lean

@@ -0,0 +1,26 @@
+new_frontend
+
+def f1 (x : Nat) (b : Bool) : typeOf! x :=
+let r : typeOf! (x+1) := x+1;
+r + 1
+
+theorem ex1 : f1 1 true = 3 :=
+rfl
+
+def f2 (x : Nat) (b : Bool) : typeOf! x :=
+let r : typeOf! b := x+1; -- error
+r + 1
+
+def f3 (x : Nat) (b : Bool) : typeOf! b :=
+let r (x!1 : typeOf! x) : typeOf! b := x > 1;
+r x
+
+def f4 (x : Nat) : Nat :=
+let y : Nat := x
+let y := ensureTypeOf! y "invalid reassignment" y == 1 -- error
+y + 1
+
+def f5 (x : Nat) : Nat :=
+let y : Nat := x
+let y := ensureTypeOf! y "invalid reassignment" (y+1)
+y + 1

tests/lean/typeOf.lean.expected.out

@@ -0,0 +1,36 @@
+typeOf.lean:11:21: error: application type mismatch
+  HasAdd.add x
+argument
+  x
+has type
+  Nat
+but is expected to have type
+  Bool
+failed to synthesize instance
+  CoeT Nat x Bool
+typeOf.lean:12:0: error: application type mismatch
+  HasAdd.add r
+argument
+  r
+has type
+  Bool
+but is expected to have type
+  Nat
+failed to synthesize instance
+  CoeT Bool r Nat
+typeOf.lean:20:9: error: invalid reassignment
+  y == 1
+has type
+  Bool
+but it is expected to have type
+  Nat
+typeOf.lean:21:0: error: application type mismatch
+  HasAdd.add y
+argument
+  y
+has type
+  Bool
+but is expected to have type
+  Nat
+failed to synthesize instance
+  CoeT Bool y Nat