Why can't infer instance

Stream: new members

[Sebastián Galkin]

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]

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

[Reid Barton]

Without any information my guess would be that Foo really has some implicit arguments that cannot be inferred

[Reid Barton]

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

[Sebastián Galkin]

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]

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]

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]

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]

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

[Sebastián Galkin]

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

[Johan Commelin]

@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"