simps fails

Stream: general

[Joël Riou]

In my homology refactor project, I have structures similar to the MWE below, where I can't get simps to generate the expected projections:

import category_theory.limits.shapes.kernels

noncomputable theory

open category_theory category_theory.limits

variables {C : Type*} [category C] [has_zero_morphisms C] {X Y : C} (f : X ⟶ Y)

structure kernel_data :=
(K : C)
(ι : K ⟶ X)
(hι₀ : ι ≫ f = 0)
(hι : is_limit (kernel_fork.of_ι ι hι₀))

@[simps]
def kernel_data.of_has_kernel [has_kernel f] :
  kernel_data f :=
{ K := kernel f,
  ι := kernel.ι f,
  hι₀ := kernel.condition f,
  hι := kernel_is_kernel f, }

The problem is with the is_limit field hι, but I do not need simps to generate any simp lemma for this field. I have tried @[simps K ι], but I always get the error message Failed to find constructor in structure category_theory.limits.is_limit.. ( set_option trace.simps.verbose true is not very helpful either.) Is there a way to fix this on a given definition, or using some initialize_simps_projections?

[Adam Topaz]

Why can't you just use docs#category_theory.limits.limit_cone for this?

[Floris van Doorn]

This is a bug in @[simps]. The problem is that projection name hι is a prefix of hι₀. As a workaround you can rename the projections (e.g. hι -> hι').

[Floris van Doorn]

It's the last item in #5489

[Joël Riou]

Thanks @Floris van Doorn!
@Adam Topaz: This is not the actual structure, this is a MWE for the problem I encountered for a more elaborate structure.