Metaprogramming in Lean 4 example

Stream: metaprogramming / tactics

[Greg Shuflin]

I'm going through https://leanprover-community.github.io/lean4-metaprogramming-book/ and encountering the first "Building a command" example https://leanprover-community.github.io/lean4-metaprogramming-book/#building-a-command

With the #assertTypeexample code there, I'm getting "success" return from my editor (neovim) regardless of whether I give a valid or invalid type:

#assertType 4 : String
/--
failed to synthesize
  OfNat String 4
numerals are polymorphic in Lean, but the numeral `4` cannot be used in a context where the expected type is
  String
due to the absence of the instance above

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

▼ 20:1-20:23: information:
success
-/

Is this expected, or is something broken about my editor setup or the code in the example?

[Greg Shuflin]

#assertType "s" : Nat also fails but logs the string "success", so this isn't just some weirdness with numeral polymorphism

[Mirek Olšák]

So far, I can confirm it is not an editor issue -- apparently elabTermEnsuringType doesn't throw an exception, only logs an error. I suppose it should be enclosed into a function that throws an exception in case of an error but I don't remember how it is called.

[Mirek Olšák]

This works:

elab "#assertType " termStx:term " : " typeStx:term : command =>
  open Lean Lean.Elab Command Term in
  liftTermElabM
    try
      let tp ← elabType typeStx
      withoutErrToSorry <|
        discard <| elabTermEnsuringType termStx tp
      synthesizeSyntheticMVarsNoPostponing
      logInfo "success"
    catch | _ => throwError "failure"