Why does `Eq.rec` treat the first index as a parameter?

Stream: general

[Sabrina Jewson]

If we look at the definition of Eq, we see that unlike in Lean 3 it uses two indices of type α:

inductive Eq : α → α → Prop where
  | refl (a : α) : Eq a a

However, if we check the type of Eq.rec we see that the first index is in fact treated as if that it were a parameter:

-- The type of Eq.rec
example : ∀
  {a : α}
  {motive : (b : α) → Eq a b → Sort v}
  (_ : motive a (Eq.refl a))
  {b : α}
  (t : Eq a b), motive b t := @Eq.rec α

-- What we would “expect” from two indices
example : ∀
  {motive : ∀ a b : α, Eq a b → Sort v}
  (_ : ∀ a, motive a a (Eq.refl a))
  {a b : α}
  (t : Eq a b), motive a b t := sorry

So my question is twofold:

1. I’m assuming this is a quality-of-life feature introduced in Lean 4. Is there any documentation on this — when will Lean decide to transform indices into parameters?
2. It is trivial to show that the single-indexed recursor can be used to construct the double-indexed recursor. I assume the reverse is not possible, because otherwise Lean4 wouldn’t have introduced this feature. In that case, what would be the semantics of the hypothetically double-indexed type? Is there any mental model I can have to understand why it exists? It seems strange to me that such an object might exist which is strictly worse than another.

[Mario Carneiro]

It is possible to construct the double indexed type, but lean's elaborator prefers to make things parameters when possible because they are generally more convenient

[Mario Carneiro]

The two inductives are equivalent for a suitably loose sense of equivalent

[Mario Carneiro]

an easy way to get the double-indexed inductive is

inductive Eq' : α → α → Prop where
  | refl (a : α) : Eq' (id a) a

[Mario Carneiro]

it occurs to me that one advantage of this feature is that you can set the binder mode on the argument to refl, which is not something you can do when writing the parameter left of the colon

[Mario Carneiro]

inductive Foo : Nat → Nat → Prop where
  | one (a : Nat) : Foo a 1
  | two {a : Nat} : Foo a 2
#print Foo
-- inductive Foo : Nat → Nat → Prop
-- number of parameters: 1
-- constructors:
-- Foo.one : ∀ (a : Nat), Foo a 1
-- Foo.two : ∀ {a : Nat}, Foo a 2

[Sabrina Jewson]

The two inductives are equivalent for a suitably loose sense of equivalent

Thanks, you’re right, I didn’t try hard enough with my proof. For future reference, here is the single-indexed recursor constructed from the double-indexed inductive type:

inductive Eq' : α → α → Prop where
  | refl (a : α) : Eq' (id a) a

theorem Eq'.rec' : ∀
  {a : α}
  {motive : (b : α) → Eq' a b → Sort v}
  (_ : motive a (Eq'.refl a))
  {b : α}
  (t : Eq' a b), motive b t :=
    λ {_} {_} refl {_} t => t.rec
      (motive := λ a b t => ∀ {motive : ∀ b : α, Eq' a b → Sort v}, motive a (Eq'.refl a) → motive b t)
      (λ _ _ => id)
      refl