Wait this is valid?

Stream: lean4

[Sofia]

Uhh.. Stumbled upon this between ideas while representing some data.. Noticed Lean didn't complain. How is this valid?

inductive Foo : List Foo -> Type
| x : Foo []

[Wojciech Nawrocki]

It looks like an unfortunate interaction with the autoImplicit feature. Try #check Foo.mk (Foo := Nat) :)
And

set_option autoImplicit false in
inductive Foo : List Foo → Type
  | x : Foo []

[Sofia]

Ah ! That explains it. Thanks.

[Jakob von Raumer]

Would be good if the syntax highlighting distinguished the two

[Sofia]

Or injected a verbosity layer, like some editors do with type hints. Ex. let x := 1 -> let x : Nat := 1 where the : Nat annotation is grayed out because it isn't really in the code, it was merely inferred and displayed as if it were. Don't know if any editors which do this allow you to make that code, to lock in the type, but that'd be nice too.

[Siddhartha Gadgil]

In scala on VS code (with `metals) the inferred types are shown and can be added, so the editor clearly supports this.