to instance or not to instance

Stream: general

[Johan Commelin]

Clearly, the following instances form a loop together. Do we have design principles that dictate which should be instance and which should be lemma?

instance {f g : arrow T} (ff : f ⟶ g) [is_iso ff.left] [is_iso ff.right] :
  is_iso ff :=
{ out := ⟨⟨inv ff.left, inv ff.right⟩,
          by { ext; dsimp; simp only [is_iso.hom_inv_id] },
          by { ext; dsimp; simp only [is_iso.inv_hom_id] }⟩ }

instance left_is_iso [is_iso sq] : is_iso sq.left :=
{ out := ⟨(inv sq).left, by simp only [← comma.comp_left, is_iso.hom_inv_id, is_iso.inv_hom_id,
    arrow.id_left, eq_self_iff_true, and_self]⟩ }

instance right_is_iso [is_iso sq] : is_iso sq.right :=
{ out := ⟨(inv sq).right, by simp only [← comma.comp_right, is_iso.hom_inv_id, is_iso.inv_hom_id,
    arrow.id_right, eq_self_iff_true, and_self]⟩ }

[Gabriel Ebner]

The first one should not be an instance because it loops (at least as far as I can see the types).

[Johan Commelin]

The first one alone doesn't loop, right?

[Johan Commelin]

But it's somehow an "extensionality instance" if that makes sense. Maybe those are "bad"? Can/should we lint against those?

[Gabriel Ebner]

Ah, because ff.left is no longer a morphism between objects in an arrow.

[Johan Commelin]

Or at least, if it is, then in a different category. (If you start with f g : arrow (arrow T))

[Reid Barton]

Ideally is_iso would not exist as a class at all (there are a lot of ways to prove that a map is an isomorphism and many of them are not "syntactic"). However, the loop-breaking rule is generally that the instance head(s) should get smaller when you apply an instance.

[Johan Commelin]

Which in thise case means that nr1 should not be an instance, and the other two are fine, right?