elaboration of `show type from value`

Stream: lean4

[Aaron Liu]

Currently, show type from value elaborates to

have this : type := value
this

I think this is a bit confusing, for example if I have something like

/--
error: type mismatch
  this
has type
  Int : Type
but is expected to have type
  Nat : Type
---
info: id
  (have this := 0;
  sorry) : Nat
-/
#guard_msgs in
#check @id Nat (show Int from 0)

the error message here is a bit hard to interpret. Also, docs#Lean.Meta.mkExpectedTypeHint returns @id type value, which does give better error messages

/--
error: Application type mismatch: In the application
  id (id 0)
the argument
  id 0
has type
  Int : Type
but is expected to have type
  Nat : Type
---
info: id sorry : Nat
-/
#guard_msgs in
#check @id Nat (@id Int 0)

Can we change show to do this instead?

[Robin Arnez]

I think the reason is that have reduces under with_reducible (through zeta reduction) but id doesn't.

[Eric Wieser]

Could this be handled with mdata and a pretty printer?

[Robin Arnez]

You could certainly just check for the particular pattern and delab like this:

import Lean

open Lean PrettyPrinter Delaborator
@[delab letE]
def delabShow : Delab := do
  let Expr.letE _ t v (.bvar 0) true ← SubExpr.getExpr | failure
  let t ← delab t
  let v ← delab v
  `(show $t from $v)

/-- info: show Nat from 5 : Nat -/
#guard_msgs in
#check show Nat from 5

But to make sure the error message changes meaningfully, you'd need an elaborator (not keep this a macro):

import Lean

open Lean PrettyPrinter Delaborator in
@[delab letE]
def delabShow : Delab := do
  let Expr.letE _ t v (.bvar 0) true ← SubExpr.getExpr | failure
  let t ← delab t
  let v ← delab v
  `(show $t from $v)

/-- info: show Nat from 5 : Nat -/
#guard_msgs in
#check show Nat from 5

open Lean Meta Elab Term in
elab_rules : term | `(show $t from $v) => do
  let type ← elabType t
  let value ← elabTerm v type
  return .letE `this type value (.bvar 0) true

/--
error: Application type mismatch: The argument
  show Int from 0
has type
  Int
but is expected to have type
  Nat
in the application
  id (show Int from 0)
---
info: id sorry : Nat
-/
#guard_msgs in
#check @id Nat (show Int from 0)