Structure fields as instances?

Stream: lean4

[Joey Eremondi]

Is there a way to have certain structure fields automatically registered as instances in lean? For example, if I've got a type that packages a type with its Category instance, I want to have the typeclass search know that there is a Category instance for each packaged type.

import Mathlib.CategoryTheory.Category.Basic

open CategoryTheory

structure ExCat : Type 1 where
  C : Type
  catInst : Category.{0} C

def GoodHom (x : ExCat) : x.C -> x.C -> Type :=
  x.catInst.Hom

def BadHom (x : ExCat) : x.C -> x.C -> Type :=
  Quiver.Hom -- Failed to synthesize instance Quiver x.C

Basically, is there a way I can make BadHomcompile by changing the definition of ExCat?

In Agda, I can declare catInst as an instance field, so that the typeclass search will see the Category instance for any x.C that show up during type checking. Is there an equivalent in Lean?

[Patrick Massot]

You can add the line attribute [instance] ExCat.catInst after the definition of ExCat.

[Patrick Massot]

I don’t think we have syntax to decorate the definition with that attribute.

[Kyle Miller]

Conversely, if you write

structure ExCat : Type 1 where
  C : Type
  [catInst : Category.{0} C]

then Lean can synthesize that field using typeclass inference, but you need to do attribute [instance] to make the projection participate in typeclass inference.