Auto param issue

Stream: general

[Adam Topaz]

Here's something strange:

import algebra

class zero_add_eq_zero (A : Type*) [has_add A] [has_zero A] :=
(thing : A)
(zero_add {x : A} : 0 + x = x . obviously)

class zero_add_eq_zero' (A : Type*) [has_add A] [has_zero A] :=
(thing : A)
(zero_add : ∀ {x : A}, 0 + x = x . obviously)

instance bar {A : Type*} [ring A] : zero_add_eq_zero A :=
{ thing := 1,
  zero_add := by tidy } -- Works

instance baz {A : Type*} [ring A] : zero_add_eq_zero' A :=
{ thing := 1 } -- Works

instance foo {A : Type*} [ring A] : zero_add_eq_zero A :=
{ thing := 1 } -- Fails

/-
invalid structure value { ... }, field 'zero_add' was not provided
-/

What's going on? (This came up as part of the discussion about #3762 )
Ping @Scott Morrison

[Adam Topaz]

It doesn't seem to be an issue with "obviously" itself:

meta def thing := `[simp]

class zero_add_eq'' (A : Type*) [has_add A] [has_zero A] :=
(zero_add {x : A} : 0 + x = x . thing)
class zero_add_eq''' (A : Type*) [has_add A] [has_zero A] :=
(zero_add : ∀ {x : A}, 0 + x = x . thing)

instance foo' {A : Type*} [ring A] : zero_add_eq'' A := {} -- Fails
instance foo'' {A : Type*} [ring A] : zero_add_eq''' A := {} -- Works