implicit type arg vs. forall

Stream: general

[É Olive]

I'm wondering what the difference between

theorem add_right_inv {A : Type*} [ring A] : ∀ a : A, a + (-a) = 0 :=

and

theorem add_right_inv {A : Type*} [ring A] {a : A} : a + (-a) = 0 :=

I see two differences. The first is that using forall, I'm required to intro the a. This is no mystery to me, makes perfect sense. The second difference is that I can't use the latter theorem everywhere I can the former. There are some places I can use both just fine, it's not that the latter is useless, but some places it seems like only the former works. For example the following works fine with the forall version but not the implicit arg version:

theorem add_left_cancel {A : Type*} [ring A] {a b : A} (c : A) : a + c = b + c → a = b :=
begin
  intro f,
  rw ← add_right_id a,
  rw ← add_right_id b,
  rw ← add_right_inv c,
  rw add_assoc,
  rw add_assoc,
  rw f,
end

For the implicit arg version I get the error:

function expected at
  add_right_id
term has type
  ?m_1
state:
A : Type u_1,
_inst_1 : ring A,
a b c : A,
f : a + c = b + c
⊢ a = b

This is mostly jibberish to me, but u_1 and ?m_1 clue me in that this might be a universe issue? This seems similar to the difference between data type parameters and data type indices in Agda, which is rather subtle and not something I can claim to understand 100% anyway.

So what is the difference between between the two that causes this, and how can I predict which version of a theorem I should write?

(Right stream this time)

[Eric Wieser]

∀ a : A, is short for ∀ (a : A),, but you can use ∀ {a : A}, there too

[É Olive]

Using : ∀ {a : A}, seems to produce the same error as using {a : A} :, do you mean those two are the same? If the difference is just in mandatory vs optional arguments then why does it make a difference to the proof when I provide the argument either way?

[Mario Carneiro]

From the point of view of downstream users of the theorem, there is no difference between : ∀ {a : A}, and {a : A} :. However it makes a difference in the proof. The binder notation left of the colon is sugar for a pi in the type and a lambda in the proof, meaning that it saves you having to intro a but otherwise they are the same.

[Eric Rodriguez]

Wasn't there a more specific difference? I know there definitely is with an inductive, but : ∀ {a : α} [...] := λ a, "=" {a : α} : [...] :=

[Mario Carneiro]

There are asterisks on that statement; that's the cliff notes version. In inductive it is not the same (it changes the type of the local constant inside the definition, and the shape of the recursor for downstream uses), in equation compiler definitions it also affects the type of the local constant and the compilation strategy, and there is also an interaction with instance binders, which are not added to the typeclass cache if you use lambda but are if you put the argument left of the colon.