Why does lean add implicit variables to lemmas from eq?

Question

The following code has a strange behavior

variable (toto : Type)
check eq.symm  --output: eq.symm : ?a toto = ?b toto → ?b toto = ?a toto

I would expect check to not take into account the irrelevant implicit variable toto when showing me the type of eq.symm. Is this really intended?

Answer 1

I got the answer from github issues here.

This is actually a bug referenced here which can be worked around by doing either

print eq.symm -- theorem eq.symm : ∀ {A : Type} {a b : A}, a = b → b = a :=
          -- λ A a, eq.rec (eq.refl a)

check @eq.symm -- eq.symm : ∀ {A} {a b}, a = b → b = a