Inductive type declaration UX bug involving a where typo #11853
Description
Prerequisites
- [ X ] Check that your issue is not already filed:
https://github.com/leanprover/lean4/issues - [ X ] Reduce the issue to a minimal, self-contained, reproducible test case.
Avoid dependencies to Mathlib or Batteries. - [ X ] Test your test case against the latest nightly release, for example on
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
In the following code, a typo is made when typing where on the first line. This causes a warning on the last line because Where is interpreted as a universe level variable for MyResult.
/-
The 'W' in 'Where' should be lower case. Fixing it clears the error at the bottom.
-/
inductive MyResult (α : Type) : Type Where
| Ok : α → MyResult α
| Err : String → MyResult α
instance : Monad MyResult where
pure x := .Ok x
bind := fun x f => match x with
| .Ok x => f x
| .Err s => .Err s
def myResultProg (x : Nat) : MyResult Nat := do
let a ← if x > 10 then MyResult.Ok (x-10) else MyResult.Err "x must be greater than 10"
MyResult.Ok a
/-
[error][lake][Lean 4] declaration `_eval` contains universe level metavariables at the expression
repr.{?u.23296} (myResultProg.{?u.23296} 9)
in the declaration body
repr.{?u.23296} (myResultProg.{?u.23296} 9)
-/
#eval myResultProg 9
Context
I'm a new Lean user. I encountered this while following the Monads section of the FPIL tutorial.
This was discussed briefly in a zulip topic #lean4 > Why does this typo not give me a syntax error or warning?.
Steps to Reproduce
Expected behavior: A syntax error or warning message on the inductive type declaration.
Actual behavior: A warning on the #eval line.
Versions
I encountered this while using 4.24.0 and reproduced it on lean-nightly with live.lean-lang.org.