Holes in constructors

Stream: new members

[Julian Berman]

"Why" does this work:

inductive Sum''' (α : Type) (β : Type) : Type where
  | inl (a : α) : Sum''' _ _
  | inr (b : β) : Sum''' _ _

#check Sum'''.inl
#check Sum'''.inr

Specifically why does Lean know I mean Sum \alpha \beta rather than assuming say Sum \alpha \alpha for inl's type (or really blowing up, which I half expected)? Does it simply try to (unify?) the most general possible interpretation of holes?

[Arthur Adjedj]

Arguments given in the left-hand side of : in inductive signatures are parameters, meaning that they're fixed in all recursive appeareances of the inductive type in its constructors, hence why Lean interprets the holes in the right way. If you instead put there arguments as indices, you'll see that Lean makes a more "general" interpretation:

inductive Sum''' : Type → Type → Type where
  | inl (a : α) : Sum''' _ _
  | inr (b : β) : Sum''' _ _

#check Sum'''.inl
#check Sum'''.inr