No local context when there is an error

Stream: lean4

[Kyle Miller]

When there's an error that triggers the error-to-sorry feature, you don't get the local context at the term that has the error.

In the following, if you move your cursor right before b, you don't see the context, but if you move right before id you do.

def a (x : Nat) : Nat := id b

But in this one, you don't get any context at all, presumably because the application elaborator gives up.

def a' (x : Nat) : Nat := id b 2

This is reflected in the terms you get:

#print a
/-
def a : Nat → Nat :=
fun x => id (sorryAx Nat true)
-/
#print a'
/-
def a' : Nat → Nat :=
fun x => sorryAx Nat true
-/

[Kyle Miller]

Does anyone know what's going on? It would be nice to be able to see the local context at the point of an error. The only workaround I know is to replace the offending subterm with _ or sorry, and then you can see the local context there.

[Kyle Miller]

(This came up in this message, where it was thought that because incomplete terms don't show the local context that it doesn't exist. It certainly exists, but it's not clear why it's not being shown.)

[Mario Carneiro]

This behavior seems consistent with error-to-sorry not producing an info node

[Mario Carneiro]

is there a reason you believe this is not the case?

[Mario Carneiro]

in the first example id _ elaborates successfully and b fails (and doesn't leave an info node), and in the second example id _ _ fails (and doesn't leave an info node)

[Mario Carneiro]

...oh. Looks like this is explicitly coded in

  if let some i := res? then
    if let .ofTermInfo ti := i.info then
      if ti.expr.isSyntheticSorry then
        return none

[Mario Carneiro]

this gets called from InfoTree.termGoalAt?which is used by the plainTermGoal request

[Kyle Miller]

Mario Carneiro said:

This behavior seems consistent with error-to-sorry not producing an info node

When I was poking around, it looked like error-to-sorry was supposed to produce an info node like anything else, but I didn't get to the point of looking at the info trees to check.

[Kyle Miller]

Mario Carneiro said:

...oh. Looks like this is explicitly coded in

Thanks for finding that. I had a suspicion it might have to do with the server, but I wasn't sure where to look.

[Kyle Miller]

Commenting out that block results in the following "expected type" infoviews with the cursors right before the ^s:

def a (x : Nat) : Nat := id b
/-                          ^
x : Nat
⊢ Nat
-/
def a' (x : Nat) : Nat := id b 2
/-                           ^
x : Nat
⊢ ?m.973
-/

[Kyle Miller]

This is when a sorry check was originally added: https://github.com/leanprover/lean4/commit/736d32c0262e8324135681f71917dceab85795ec

It looks like it might have been for parse errors originally, rather than elaboration errors.