typeclass failure

Stream: lean4

[Kevin Buzzard]

I would expect type class inference to succeed here. I couldn't get it to work in Lean 3 either. What am I doing wrong?

class has_note (M : Type) where
  note : M

notation "♩" => has_note.note

class has_note_and_foo (M : Type) extends has_note M where
  foo : Unit -- in Lean 3 you can just extend has_note with no extra fields and the problem persists

variable {ι : Type} {N : Type} {η : ι → Type} (β : ι → Type)

structure dfinsupp [∀ i, has_note (β i)] : Type :=
(to_fun : ∀ i, β i)

instance dfinsupp.has_note {ι : Type} {β : ι → Type} [∀ i, has_note (β i)] :
  has_note (dfinsupp (λ i => β i)) := ⟨⟨λ _ => ♩⟩⟩

instance dfinsupp.has_note_and_foo [∀ i, has_note_and_foo (β i)] :
  has_note_and_foo (dfinsupp (λ i => β i)) where
  note      := ♩
  foo := ()

variable (α : Type) (M : Type)

structure finsupp [has_note M] :=
(to_fun             : α → M)

instance finsupp.has_note [has_note M] :
  has_note (finsupp α M) := ⟨⟨λ i => ♩⟩⟩

instance finsupp.has_note_and_foo [has_note_and_foo M] :
  has_note_and_foo (finsupp α M) where
  note      := ♩
  foo := ()

example [has_note_and_foo N] : has_note_and_foo (dfinsupp (λ (i : ι) => finsupp (η i) N)) :=
inferInstance -- fails

example [has_note_and_foo N] : has_note_and_foo (dfinsupp (λ (i : ι) => finsupp (η i) N)) :=
dfinsupp.has_note_and_foo _ -- works

-- in Lean 3, removing the instance attribute from `finsupp.has_note` makes inferInstance work

Supplementary questions which came up when I was making this:
(1) I know it's ridiculous but I didn't know how to make a class foo2 extend foo1 and then add no more fields (so foo2 is a copy of foo1). In Lean 3 you can do class foo2 extends foo1..
(2) In Lean 3 I could try and debug using set_option trace.class_instances true. How do you say that in Lean 4?
(3) In Lean 3 I could experiment with removing instance tags from my defs with local attribute [-instance] finsupp.has_zero (which fixes the problem). How do you say that in Lean 4?

PS here is the Lean 3 discussion, with some traces.

[Kyle Miller]

Kevin Buzzard said:

(2) In Lean 3 I could try and debug using set_option trace.class_instances true. How do you say that in Lean 4?

The equivalent seems to now be set_option trace.Meta.synthInstance true

(3) In Lean 3 I could experiment with removing instance tags from my defs with local attribute [-instance] finsupp.has_zero (which fixes the problem). How do you say that in Lean 4?

I don't know if you can remove attributes anymore, but manually removing finsupp.has_note and including it into finsupp.has_note_and_foo seems to make the inferInstance succeed:

--instance finsupp.has_note [has_note M] :
--  has_note (finsupp α M) := ⟨⟨λ i => ♩⟩⟩

instance finsupp.has_note_and_foo [has_note_and_foo M] :
  has_note_and_foo (finsupp α M) where
  note      := ⟨λ i => ♩⟩
  foo := ()

[Kyle Miller]

I'm not sure why exactly typeclass resolution doesn't work, but somehow splitting off has_foo and creating a has_note_and_foo synonym class makes it succeed. (I'm not recommending anything by posting this.)

class has_note (M : Type u) where
  note : M

notation "♩" => has_note.note

class has_foo (M : Type u) [has_note M] : Sort where
  ax : (♩ : M) = ♩ -- example axiom that has_note should satisfy

class has_note_and_foo (M : Type u) extends has_note M, has_foo M
attribute [instance] has_note_and_foo.mk

structure dfinsupp (β : ι → Type u) [(i : ι) → has_note (β i)] where
  to_fun : (i : ι) → β i

instance dfinsupp._has_note {β : ι → Type u} [(i : ι) → has_note (β i)] :
  has_note (dfinsupp β) := ⟨⟨λ _ => ♩⟩⟩

instance dfinsupp._has_foo {β : ι → Type u}
  [(i : ι) → has_note (β i)] [(i : ι) → has_foo (β i)] :
  has_foo (dfinsupp β) where
  ax := rfl

structure finsupp (α : Type u) (M : Type v) [has_note M] where
  to_fun : α → M

instance finsupp._has_note (M : Type v) [has_note M] :
  has_note (finsupp α M) where
  note := ⟨λ _ => ♩⟩

instance finsupp._has_foo (M : Type u) [has_note M] [has_foo M] :
  has_foo (finsupp α M) where
  ax := rfl

example (N : Type u) [has_note N] [has_foo N] (η : ι → Type v):
  has_note (dfinsupp (λ (i : ι) => finsupp (η i) N)) :=
inferInstance

example (N : Type u) [has_note N] [has_foo N] (η : ι → Type v):
  has_foo (dfinsupp (λ (i : ι) => finsupp (η i) N)) :=
inferInstance

example (N : Type u) [has_note N] [has_foo N] (η : ι → Type v):
  has_note_and_foo (dfinsupp (λ (i : ι) => finsupp (η i) N)) :=
inferInstance

[Kevin Buzzard]

In the Lean 3 use case, note = 0, foo = +, and finsupp and dfinsupp are finitely supported functions.

[Mario Carneiro]

(1) I know it's ridiculous but I didn't know how to make a class foo2 extend foo1 and then add no more fields (so foo2 is a copy of foo1). In Lean 3 you can do class foo2 extends foo1..

That sounds like it could be an issue on the lean 4 repo. I have noticed a number of uses of "1 or more" in the grammar where "0 or more" would be valid, useful and no harder to parse: the fields after where in this case as well as match x with arms+ come to mind. There are probably some variations of the where syntax appearing like instance ... where, def ... where, as well as let rec, mutual, variable.

[Gabriel Ebner]

I think you can do class Foo2 extends Foo1 where now.

[Gabriel Ebner]

Weirdly enough, it's impossible to extend the empty structure:

class Bar
class Foo extends Bar where
-- 'Bar' is not a structure

[Mario Carneiro]

oh, class Bar works?

[Mario Carneiro]

I'm surprised it's not class Bar where

[Gabriel Ebner]

Yes!

[Gabriel Ebner]

Wait, I don't need the where after extends either. This works:

class Bar where
  x : Nat
class Foo extends Bar

[Mario Carneiro]

Oh! I had sort of assumed Kevin tried that, since it does seem like the style we want to encourage

[Kevin Buzzard]

I am an idiot

[Kevin Buzzard]

and indeed inferInstance is still failing even with foo removal

[Sebastien Gouezel]

@Daniel Selsam , do you have an idea why typeclass inference fails on https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/typeclass.20failure/near/241318335 ?

[Kevin Buzzard]

Here's the foo-free version:

class has_note (M : Type) where
  note : M

notation "♩" => has_note.note

class has_note2 (M : Type) extends has_note M

variable {ι : Type} {N : Type} {η : ι → Type} (β : ι → Type)

structure dfinsupp [∀ i, has_note (β i)] : Type :=
(to_fun : ∀ i, β i)

instance dfinsupp.has_note {ι : Type} {β : ι → Type} [∀ i, has_note (β i)] :
  has_note (dfinsupp (λ i => β i)) := ⟨⟨λ _ => ♩⟩⟩

instance dfinsupp.has_note2 [∀ i, has_note2 (β i)] :
  has_note2 (dfinsupp (λ i => β i)) where
  note      := ♩

variable (α : Type) (M : Type)

structure finsupp [has_note M] :=
(to_fun             : α → M)

instance finsupp.has_note [has_note M] :
  has_note (finsupp α M) := ⟨⟨λ i => ♩⟩⟩

instance finsupp.has_note2 [has_note2 M] :
  has_note2 (finsupp α M) where
  note      := ♩

example [has_note2 N] : has_note2 (dfinsupp (λ (i : ι) => finsupp (η i) N)) :=
inferInstance -- fails

example [has_note2 N] : has_note2 (dfinsupp (λ (i : ι) => finsupp (η i) N)) :=
dfinsupp.has_note2 _ -- works

[Kevin Buzzard]

And here's the variant that works -- "remove finsupp.has_note and bundle it into finsupp.has_note2":

class has_note (M : Type) where
  note : M

notation "♩" => has_note.note

class has_note2 (M : Type) extends has_note M

variable {ι : Type} {N : Type} {η : ι → Type} (β : ι → Type)

structure dfinsupp [∀ i, has_note (β i)] : Type :=
(to_fun : ∀ i, β i)

instance dfinsupp.has_note {ι : Type} {β : ι → Type} [∀ i, has_note (β i)] :
  has_note (dfinsupp (λ i => β i)) := ⟨⟨λ _ => ♩⟩⟩

instance dfinsupp.has_note2 [∀ i, has_note2 (β i)] :
  has_note2 (dfinsupp (λ i => β i)) where
  note      := ♩

variable (α : Type) (M : Type)

structure finsupp [has_note M] :=
(to_fun             : α → M)

instance finsupp.has_note2 [has_note2 M] : has_note2 (finsupp α M) where
  note      := ⟨λ i => ♩⟩

example [has_note2 N] : has_note2 (dfinsupp (λ (i : ι) => finsupp (η i) N)) :=
inferInstance -- now works

[Mac]

I imagine this has to do with the fact that the original finsupp has two has_note instances, one explicit and one it implicitly acquires through its explicit has_note2 instance extending has_note. Lean might not like these kind of psuedo-diamonds.

[Kevin Buzzard]

Those instances are defeq, right? I don't think this is the issue. I think that what you describe happens all over the place in mathlib in lean 3, you make something an additive abelian group and then a ring and this is no problem at all.

[Kevin Buzzard]

I think it's something to do with the pi type in the class. You can test your hypothesis by removing the pi type and trying to get type class inference to fail without it but still having your pseudo-diamond.

[Mario Carneiro]

set_option trace.Meta.synthInstance true
#synth [has_note2 N] → has_note2 (dfinsupp (λ (i : ι) => finsupp (η i) N))

-- ...
-- [Meta.synthInstance.tryResolve] has_note2
--   (dfinsupp fun (i : ι) => finsupp (η i) N) =?= has_note2 (dfinsupp fun (i : ?m.1404) => ?m.1405 i)
-- [Meta.synthInstance.tryResolve] failure

It appears to be a unification problem involving metavariables under a lambda. It looks like a bug, or at least a regression from lean 3 behavior - here ?m.1405 i should be unified with finsupp (η i) N but this is being rejected, and the synthesis fails.

[Kevin Buzzard]

It's also failing in lean 3

[Kevin Buzzard]

Should I open an issue?

[Mario Carneiro]

Hm, if it fails in lean 3 too then that lowers the chance that it will be fixable, but it's certainly something that Daniel or Leo will want to consider, so I would say yes

[Kevin Buzzard]

lean4#509

[Daniel Selsam]

Sebastien Gouezel said:

Daniel Selsam , do you have an idea why typeclass inference fails on https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/typeclass.20failure/near/241318335 ?

Hey, was away last week. I don't have time to address this now but I took a quick look and my first guess is that it tries to unify: ((?m <something>).1 : has_note2 M) =?= (<something-else> : has_note M) and that the solution may be to add special support for unification hints for structures with a single field, i.e. making it so that x.1 =?= y would try x =?= ⟨y⟩.

[François G. Dorais]

Also, it would be nice to have such hints for structures where all but one field is a Prop.

[Daniel Selsam]

François G. Dorais said:

Also, it would be nice to have such hints for structures where all but one field is a Prop.

Can you please clarify?

[François G. Dorais]

NVM: wrong way around.

[Kevin Buzzard]

fixed in lean4#521. Thanks to the devs!

[Eric Wieser]

Does that fix actually help for the dfinsupp case? Wasn't add_zero_class relevant there, which has multiple fields?

[Daniel Selsam]

Eric Wieser said:

Does that fix actually help for the dfinsupp case? Wasn't add_zero_class relevant there, which has multiple fields?

The example with dfinsupp posted at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/typeclass.20failure/near/241455170 works now as well.

[Eric Wieser]

Is it likely it would be doable for a lean 3 expert (and obviously not an already busy lean4 dev!) to backport to lean 3? Or does the strategy used to fix this only really exist in lean 4?

[Daniel Selsam]

I don't see any obstacle. It is a reasonably local and lightweight change.

[Eric Wieser]

(deleted)