Server error in inductives

Stream: lean4

[Mario Carneiro]

inductive Foo
| mk : (a b : Bar) → Foo

There is an error over the word Bar with unknown identifier 'Bar' as expected, but hovering over it causes a server error:

Request textDocument/hover failed.
  Message: type expected
  b
  Code: -32603

[Sebastian Ullrich]

On current master I do get a hover, with funny universes

[Mario Carneiro]

I am on Lean (version 4.0.0-nightly-2021-06-23, commit 8454102fc4b0, Release)

[Mario Carneiro]

it was a little finicky to get a reproducer, so I might have missed something

[Mario Carneiro]

do you know how I can test it from the command line?

[Sebastian Ullrich]

See tests/lean/interactive/hover.lean. Use lean --run run.lean hover.lean to run such a file.

[Mario Carneiro]

okay, that works. inductiveTypeExpected.lean:

inductive Foo
| mk : (a b : Bar) → Foo
            --^ textDocument/hover

$ lean --version
Lean (version 4.0.0-nightly-2021-06-23, commit 8454102fc4b0, Release)

$ lean --run run.lean inductiveTypeExpected.lean
{"textDocument": {"uri": "file://inductiveTypeExpected.lean"},
 "position": {"line": 1, "character": 14}}
uncaught exception: unexpected message {"jsonrpc": "2.0",
 "id": 2,
 "error": {"message": "type expected\n  b", "code": -32603}}
Watchdog error: Cannot read LSP message: Stream was closed

[Sebastian Ullrich]

Oh wow, I can reproduce iff this is the first declaration in the file

[Sebastian Ullrich]

Must be some issue with error recovery during elaboration, not the actual hover