tracing typeclass resolution

Stream: general

[Kevin Buzzard]

A MWE using mathlib3 :

import category_theory.limits.filtered_colimit_commutes_finite_limit

universe v

open category_theory

namespace category_theory.limits

variables {K J : Type v} [small_category J] [small_category K] [is_filtered K] [fin_category J]

instance colimit_limit_to_limit_colimit_cone_iso' (F : J ⥤ K ⥤ Type v) :
  is_iso (colimit_limit_to_limit_colimit_cone F) :=
begin
  haveI : is_iso (colimit_limit_to_limit_colimit_cone F).hom,
  { dsimp only [colimit_limit_to_limit_colimit_cone],
    -- START HERE
    -- apply is_iso.comp_is_iso, -- goals accomplished
    -- refine @is_iso.comp_is_iso _ _ _ _ _ _ _ _ _, -- goals accomplished
    show_term {apply_instance}, -- exact is_iso.comp_is_iso
  },
  apply cones.cone_iso_of_hom_iso,
end

end category_theory.limits

I was interested in seeing explicitly how typeclass inference solved this goal (whilst debugging during a port). show_term only told me it was comp_is_iso of some more instances, but I couldn't figure out how to explicitly capture the instances as goals in tactic mode again. How can I do this?

[Anne Baanen]

I don't know of an automatic way, but one trick to prevent refine from filling in instances is to replace _ with (id _).

[Eric Rodriguez]

There's also (_ : _) which does the same.