Instance attribute not being found

Stream: new members

[Fernando Chu]

Could someone please explain why sanity_check is not working below? I thought attribute [instance] IsSkeletonOf'.eqv were the magic words to make this work.

import Mathlib
namespace CategoryTheory
open Category

universe v₁ v₂ v₃ u₁ u₂ u₃
variable (C : Type u₁) [Category.{v₁} C]
variable (D : Type u₂) [Category.{v₂} D]

structure IsSkeletonOf' (F : D ⥤ C) : Prop where
  skel : Skeletal D
  eqv : F.IsEquivalence := by infer_instance

attribute [instance] IsSkeletonOf'.eqv

theorem sanity_check
    (F : D ⥤ C) (skF : IsSkeletonOf' C D F) : F.IsEquivalence := by infer_instance

[Kyle Miller]

Taking a look at the type of this projection,

CategoryTheory.IsSkeletonOf'.eqv.{v₁, v₂, u₁, u₂} {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂}
  [Category.{v₂, u₂} D] {F : D ⥤ C} (self : IsSkeletonOf' C D F) : F.IsEquivalence

the self argument is not determined by F.IsEquivalence, so Lean can't find it.

If IsSkeletonOf' were a class, then it would work.

I think you're running into a known bug that causes instance to not report the fact the instance can never apply.

[Fernando Chu]

Oh, that makes sense, thank you!