inferType in delaborator

Stream: lean4

[Alexander Bentkamp]

I am trying to use inferType in a delaborator. This causes Lean to crash when I type constants that are undefined, such as test below:

import Lean

namespace Lean.PrettyPrinter.Delaborator
open SubExpr
open Meta

@[delab app]
partial def delabMinimization : Delab := do
  let ty ← inferType $ ← getExpr
  failure

end Lean.PrettyPrinter.Delaborator

set_option pp.rawOnError true

#check test
/-
[Error - 6:06:45 PM] Request textDocument/hover failed.
  Message: unknown constant '[Error pretty printing expression: unknown constant 'test'. Falling back to raw printer.]
test'
  Code: -32603
-/

Do I first need to test whether ← getExpr is actually a valid expression? How can I do that?

[Mac]

(deleted)

[Sebastian Ullrich]

That is definitely not expected (and the error message is hilarious).

[Daniel Selsam]

@Sebastian Ullrich Maybe just remove the mkConst from https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/Term.lean#L1504? Since we know the constant does not exist, I don't see a point in having the message view it as an expression rather than as a name.

[Leonardo de Moura]

The mkConst is there to make sure the name is not treated as a regular Name object, but as an Expr.
The delaborator should tolerate type incorrect terms.

[Alexander Bentkamp]

So how can I check if a term is not type correct?

[Daniel Selsam]

Alexander Bentkamp said:

So how can I check if a term is not type correct?

Delaborators should not assume that inferType will succeed in general. In your example, you could just wrap the inferType with try/catch. It is perhaps surprising though that the delaborator outer-loop will not recover from the exception -- it might make sense to put a try/catch here as well: https://github.com/leanprover/lean4/blob/master/src/Lean/PrettyPrinter/Delaborator/Basic.lean#L226

[Alexander Bentkamp]

Ok, thanks!