`ext` on structures should use `subsingleton` instances to avoid unnecessary hypotheses

[rwbarton]

Toy example:

import tactic.ext

@[ext] structure foo (α : Type*) :=
(a : α)
(b : unit)

#check @foo.ext

The generated lemma has type foo.ext : ∀ {α : Type u_1} (x y : foo α), x.a = y.a → x.b = y.b → x = y, in which the hypothesis x.b = y.b is always satisfied; instead the lemma should only take the x.a = y.a hypothesis.

In this example, the extra hypothesis doesn't matter so much, because unit also has an extensionality lemma which will be applied by the ext tactic. But you might want to apply the foo.ext lemma by hand, and there are other subsingleton types without ext lemmas (e.g. trunc β).

[eric-wieser]

I'm not refuting the suggestion here that @[ext] should be smarter, but...

and there are other subsingleton types without ext lemmas (e.g. trunc β).

IMO these types should have ext lemmas anyway, otherwise calling ext on trunc α × β won't eliminate the trunc either.

Can we make the ext tactic perform this search for subsingletons automatically?