Ambient variables and inductive types

Stream: lean4

[Francisco Giordano]

I find it really unintuitive that an ambient variable used in an inductive constructor is added as a parameter to the inductive family rather than the constructor.

variable {α : Type}
inductive Foo : Type -> Prop where
  | mk : Foo α
#check Foo -- Foo {α : Type} (a : Type) : Prop
#check Foo.mk -- Foo.mk {α : Type} : Foo α α

What I would expect here is:

#check Foo -- Foo (a : Type) : Prop
#check Foo.mk -- Foo.mk {α : Type} : Foo α

Am I thinking about this wrong? My intuition is that the mk line is a definition of the mk constructor so I expect variables to be scoped to that definition.

[Junyan Xu]

You want:

variable {α : Type}
inductive Foo : Type -> Prop where
  | mk {α} : Foo α