Why does this typo not give me a syntax error or warning?

Stream: lean4

[Christopher Lang]

New lean user here. Just got hit with this super confusing error message that was highlighting code far away from the actual error.
My expected behaviour would be and error or warning message on the inductive type declaration. I dont understand why this is even valid syntax with the upper case 'W'.

/-
 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

Lean version 4.24.0

[Henrik Böving]

There Where is interpreted as a universe level variable for MyResult, which you can tell by hovering over it or running #check MyResult. The reason for this is that the where is not obligatory and the syntax can thus also be parsed as Type Where.

This seems like quite an annoying UX bug to me, please do open an issue on lean4.

[Christopher Lang]

Issue submitted
https://github.com/leanprover/lean4/issues/11853