Unexpected type in elaboration

Stream: lean4

[Jovan Gerbscheid]

Quiz question: What is the type of this function in Lean?

def test (_ : Int) (_ : Float) :=
  (fun x =>
  let m := _
  match x with
  | (a) => (a : m)) 5

#check test

Answer

test : Int → Float → Float

[Edward van de Meent]

that's whack... but the example seems contrived too...

[Edward van de Meent]

bad code does weird things... what else is new.