surprising implicit declaration in inductive

Stream: lean4

[Mario Carneiro]

inductive Foo : Nat → Prop
  | mk : Foo _

#print Foo
-- inductive Foo : Nat → Prop
-- number of parameters: 1
-- constructors:
-- Foo.mk : ∀ {a : Nat}, Foo a

This seems... surprising, I was expecting to get an error on the _ saying it couldn't infer the value. This is not an autoImplicit issue, it happens with or without that setting.