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