invalid {...} notation

Stream: lean4

[Winston Yin (尹維晨)]

I find that this error message doesn't make very much sense to the user:

def foo : bar where

-- invalid {...} notation, expected type is not of the form (C ...)
--   bar

First, we're using the where notation, rather than {...}, so the user is confused. Second, I personally don't understand what (C ...) means and therefore how to fix my code. Third, the problem is really that bar is undefined, not because there's something wrong with its type. What I would've liked to read is something about bar being an unknown identifier.

Even in the case of the invalid def foo : Type 1 where, why can't I get the same error message as the following:

def foo : ℕ where

-- invalid {...} notation, structure type expected
--  ℕ

({...} still should maybe instead say where or structure constructor)

[Mario Carneiro]

(C ...) means an application with a constant at the head

[Mario Carneiro]

bar is not undefined, it is an auto-bound local variable

[Mario Carneiro]

you have to turn off auto-bound locals if you want to get an error saying bar is undefined

[Mario Carneiro]

I agree the message is a bit opaque though. Perhaps something like:

Expected a structure type or a type which unfolds to a structure type, got local variable 'bar'.
note: 'bar' is an auto-bound identifier, maybe it is a typo?

[Winston Yin (尹維晨)]

Your suggestion is much clearer. Sorry that I'm just a confused end user that doesn't know things like "auto-bound local variable" but knows there's got to be a better error message. :sweat_smile: