id in classes

Stream: general

[Sebastien Gouezel]

I don't really remember if having useless id in typeclasses can be bad for typeclass inference or not. For instance in

#print power_series.ring

@[instance]
protected noncomputable def power_series.ring : Π {α : Type u_1} [_inst_1 : ring α], ring (power_series α) :=
λ {α : Type u_1} [_inst_1 : ring α], id mv_power_series.ring

Thoughts?

[Reid Barton]

It does have a (probably bad) effect, yes.

[Reid Barton]

Namely, if this instance power_series.ring itself appears in the type of an instance search problem (maybe for a class like class fancy_ring (A : Type) [ring A] := ..., although this is not so common in the algebraic hierarchy, I suppose), then instance search will not be able to see that power_series.ring is actually equal to mv_power_series.ring so it won't apply instances that are declared for the latter.

[Patrick Massot]

Isn't hiding stuff the goal of such an instance?

[Mario Carneiro]

I don't think id has instance reducibility

[Mario Carneiro]

it is as opaque as a regular definition

[Mario Carneiro]

I think this comes up when you are trying to prove that some defeq diamond commutes

[Reid Barton]

It's not easy to come up with an example where it would matter here because I guess power_series must be defined by something like def power_series := mv_power_series unit, and this def also doesn't have instance reducibility.

[Mario Carneiro]

it shouldn't hamper regular instance search

[Mario Carneiro]

A recent norm_num bug had to do with a problem of this form, where int.has_sub is defeq to algebra_has_sub but the defeq is only if you unfold semireducible definitions so lean prefers to unfold something else

[Gabriel Ebner]

The typical way this burns you is if you have a second ring instance for power_series, like:

instance : comm_ring (power_series α) := mv_power_series.comm_ring

[Sebastien Gouezel]

You have, among many instances,

instance [semiring α]        : semiring        (power_series α) := by delta power_series; apply_instance
instance [comm_semiring α]   : comm_semiring   (power_series α) := by delta power_series; apply_instance
instance [ring α]            : ring            (power_series α) := by delta power_series; apply_instance
instance [comm_ring α]       : comm_ring       (power_series α) := by delta power_series; apply_instance

[Johan Commelin]

O.ooo... did I create a mess?

[Sebastien Gouezel]

#3033 (not sure it is really useful, but I don't think it can hurt).

[Gabriel Ebner]

It's typically not a problem because type-class instances usually occur in implicit arguments (and implicit arguments are unified with a higher transparency setting, i.e., semireducible). The last time I've seen this issue is with the bundled structure from the category theory library (where the type-class instance is explicit). Maybe the conclusion here is to make bundled.str instance-implicit.

[Mario Carneiro]

The clean tactic is intended for just this purpose

[Mario Carneiro]

it removes identity functions inserted to the term by tactics that do definitional reduction