# Zulip Chat Archive

## Stream: new members

### Topic: Why can't infer instance

#### Sebastián Galkin (Aug 17 2020 at 22:42):

I have an instance of a class, with a name and all, and yet infer_instance/apply_instance can't find it

```
instance my_foo_category : category Foo := {...}
instance has_hom_foo : has_hom Foo := infer_instance
instance tac_str_foo : category_struct Foo := infer_instance
instance categor_foo : category Foo := my_foo_category
# following line fails
# instance categor_foo' : category Foo := infer_instance
```

All lines but the last one succeed.

Why can't `infer_instance`

find an instance that is right there? What can I change to make it work?

#### Kevin Buzzard (Aug 17 2020 at 22:50):

Can you post a #mwe? It's difficult for me to reproduce your error.

#### Reid Barton (Aug 17 2020 at 22:52):

Without any information my guess would be that `Foo`

really has some implicit arguments that cannot be inferred

#### Reid Barton (Aug 17 2020 at 22:52):

though, now I'm confused why the second and third lines would work then

#### Sebastián Galkin (Aug 17 2020 at 23:02):

Here it is, not sure if it's very "m" but I'm trying to include every definition that could be relevant. I think you can ignore the `magma_homs`

section, bun not sure.

```
import category_theory.category
import category_theory.concrete_category.bundled
namespace magma
open category_theory
class magma (carrier: Type*) extends has_mul carrier
def Magma := bundled magma
instance mag_has_mul (m: Magma) : has_mul m.α := ⟨ m.str.mul ⟩
section magma_homs
structure magma_hom (A: Magma) (B: Magma) :=
(to_fun : A.α → B.α)
(preserves : ∀ x y : A.α, to_fun (x * y) = to_fun x * to_fun y)
infixr ` m→ `:25 := magma_hom
variables {A B C: Magma}
instance : has_coe_to_fun (A m→ B) := ⟨_, magma_hom.to_fun⟩
lemma to_fun_eq_coe (f : A m→ B) : f.to_fun = f := rfl
@[simp]
lemma coe_mk (f : A.α → B.α) (pre) : ⇑(magma_hom.mk f pre) = f := rfl
lemma coe_inj ⦃f g : A m→ B⦄ (h : (f : A.α → B.α) = g) : f = g :=
begin
cases f; cases g; cases h; refl,
end
@[ext]
lemma magma_hom_ext ⦃f g : A m→ B⦄ (h : ∀ x, f x = g x) : f = g :=
coe_inj (funext h)
def magma_id : A m→ A := ⟨id, by simp⟩
def magma_hom_comp (f: A m→ B) (g: B m→ C) : A m→ C :=
{
to_fun := g.to_fun ∘ f.to_fun,
preserves := by {
intros x y,
simp,
rw f.preserves,
rw g.preserves
}
}
end magma_homs
instance magmas_has_hom: has_hom Magma :=
{ hom := λ m n, m m→ n }
instance magmas_category_struct: category_struct Magma :=
{ id := @magma_id, comp := @magma_hom_comp }
instance magmas_category_xxx : category Magma := {}
instance : has_hom Magma := infer_instance
instance : category_struct Magma := infer_instance
instance : category Magma := infer_instance
end magma
```

#### Kevin Buzzard (Aug 18 2020 at 00:01):

don't worry about a 72 line example. Yeah, I dunno. I am suprised that the instance ends up protected -- this may have something to do with it but I don't know why it's happening.

#### Reid Barton (Aug 18 2020 at 02:01):

This is an interesting example. For some reason, the universe level in `magmas_category_xxx`

gets inferred as `max u_1 u_2`

(where `u_1`

and `u_2`

are universe level parameters of the instance) and this makes it unsuitable for matching.

#### Reid Barton (Aug 18 2020 at 02:02):

The reliable way to fix it is to write `instance magmas_category_xxx : category Magma.{u} := {}`

where `u`

is a declared universe variable

#### Reid Barton (Aug 18 2020 at 02:02):

I've seen behavior like this before, but never tracked down exactly why it was occurring.

#### Sebastián Galkin (Aug 18 2020 at 02:12):

Thank you so much! That definitely fixes it. Now I'll try to understand why, and what the `.{u}`

syntax means.

#### Johan Commelin (Aug 18 2020 at 03:47):

@Sebastián Galkin It means "hey Lean there are some "universe *variables*" in the definition of `Magma`

... please make sure that the first one is set equal to `u`

for this use case"

Last updated: Dec 20 2023 at 11:08 UTC