Are panics Lean bugs?

Stream: lean4

[Mac]

Does a panic imply a bug in Lean or can it just be user error? For example, I am currently getting the following panic:

PANIC at Lean.MetavarContext.isLevelAssignable Lean.MetavarContext:430:14: unknown universe metavariable

I assumed this just due some bugs on my part, but I just wanted to verify.

[Leonardo de Moura]

Yes, this is usually due to a bug in Lean.
Could you please create an issue on GitHub with a (small) example that exposes this problem?

[Mac]

Unfortunately, this is an incredibly difficult bug to localize. There is a large amount of code in my project between the root cause of the error and its eventual panic spot. However, I was able to generate the same panic through a more compact example (though I am not sure it is the same code path to the error):

universe u
#check fun {T : Sort u} (a : T) => a + 0

I will go make an issue about it ASAP.