type-class loops in category theory

Stream: general

[Floris van Doorn]

I wrote a new linter that catches type-class loops (#8932), and I'm making some topics with some issues it found. I don't always know the best solution to fix these loops, so I'm hoping that someone who knows that part of mathlib better can fix these.

In category theory (@Scott Morrison @Bhavik Mehta @others) I found the following issues:

• docs#category_theory.adjunction.has_limit_comp_equivalence and docs#category_theory.under.category_theory.limits.has_limit loop together. See following example (which is supposed to fail)

import category_theory.adjunction.limits
import category_theory.limits.over

open category_theory

universe u

example {J : Type*} [small_category J] {C : Type*} [_inst_2 : category C]
{X : C} (F : J ⥤ under X) :
  limits.has_limit F :=
by apply_instance

• Similarly, docs#category_theory.adjunction.has_colimit_comp_equivalence and docs#category_theory.over.category_theory.limits.has_colimit loop together
• docs#category_theory.forget₂.category_theory.reflects_isomorphisms loops together with docs#category_theory.has_forget_to_Type

import category_theory.concrete_category.reflects_isomorphisms

open category_theory

universe u

variables (C : Type (u+1)) [category C] [concrete_category.{u} C]
variables (D : Type (u+1)) [category D] [concrete_category.{u} D]

example [has_forget₂ C D] : reflects_isomorphisms (forget₂ C D) :=
by apply_instance

• The instance docs#category_theory.abelian.pseudoelement.has_zero doesn't cause a loop per se, but
  whenever we are trying to find an instance for has_zero applied to any coe_sort this instance (and all category instances) are tried. Can we make this localized?

• docs#category_theory.quiver.hom.add_comm_group (and other instances on single_obj if they exist) is superfluous, since type-class inference is happy to unfold docs#category_theory.single_obj.category_struct. I don't think this really causes issues, but you could consider removing it

import category_theory.preadditive.default
import category_theory.single_obj

open category_theory

variables {α : Type*} [ring α]

def foo (X Y : single_obj α) : add_comm_group (X ⟶ Y) :=
by apply_instance
#print foo -- ring.to_add_comm_group

[Adam Topaz]

@Floris van Doorn Just double checking... do you mean docs#category_theory.limits.has_limit_equivalence_comp ? (The first link doesn't work in your message.)

[Floris van Doorn]

Oops, it's missing the category_theory prefix. I mean docs#category_theory.adjunction.has_limit_comp_equivalence

[Adam Topaz]

Ah!

[Floris van Doorn]

I fixed the links in my first message

[Scott Morrison]

Sorry this took a while to get to: #9154 #9155 #9156 #9157.

[Scott Morrison]

Thanks for writer a new linter! They are a really valuable investment.