Not finding typeclass in hypotheses

Stream: general

[Eric Wieser]

What's going on in this gist?

https://gist.github.com/eric-wieser/66022bcfd708091799bc86e80404b504

Line 106 fails with:

failed to synthesize type class instance for
A : Type u_1,
_inst_1 : semiring A,
ι : Type u_2,
_inst_2 : add_comm_monoid ι,
_inst_3 : decidable_eq ι,
carriers : ι → add_submonoid A,
_inst_4 : semiring_add_gradation carriers,
x : ⨁ (i : ι), ↥(carriers i),
_inst : Π (i : ι) (x : (λ (i : ι), ↥(carriers i)) i), decidable (x ≠ 0)
⊢       Π (i : ι) (x : (λ (i : ι), ↥(carriers i)) i), decidable (x ≠ 0)

Why is it failing to synthesize an instance that is right there in the context?

[Kevin Buzzard]

I got an error with simp in the line before -- invalid simp lemma. My mathlib is a couple of weeks old though. Is it a pp.all thing?

[Anne Baanen]

My first thoughts are to diff the pp.all output, or to use letI instead of haveI.

[Kyle Miller]

For some reason this rw line works:

rw @add_monoid_hom.coe_dfinsupp_sum _ _ _ _ _ _ _ _ (λ i x', _inst i x') x,

[Kyle Miller]

but not _inst or (λ i, _inst i)

[Kevin Buzzard]

Oh yes, presumably decidable isn't a prop so it's letI

[Kyle Miller]

letI doesn't change seem to help here

[Eric Wieser]

@Kevin Buzzard, docs#add_monoid_hom.coe_dfinsupp_sum is very new

[Eric Wieser]

I wonder if changing the lemma to use {} instead of [] for that argument helps

[Eric Wieser]

Since the instance in question is already in the goal statement anyway

[Eric Wieser]

@Anne Baanen, pp.all and pp.notation continue to show a hypothesis that matches the goal

[Anne Baanen]

Eric Wieser said:

I wonder if changing the lemma to use {} instead of [] for that argument helps

That could be the solution. if there's some synthesised versus unified conflict going on, that decidable is prone to.

[Kevin Buzzard]

Why have you even got that un-whatever-its-called-reduced (beta-reduced?) lambda-term in inst? Can you dsimp everything away?

[Eric Wieser]

To try and help it pattern match β. Reducing it to Π (i : ι) (x : carriers i), decidable (x ≠ 0) doesn't help, and it makes the goal and hypothesis mismatch in a visible way.

[Eric Wieser]

Anne Baanen said:

Eric Wieser said:

I wonder if changing the lemma to use {} instead of [] for that argument helps

That could be the solution. if there's some synthesised versus unified conflict going on, that decidable is prone to.

This fixes the problem

[Eric Wieser]

But it feels like a bug that I have to do that

[Eric Wieser]

For the failing version, set_option trace.class_instances true gives

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 i x : decidable (x ≠ 0) := _inst (?x_3 i x) (?x_4 i x)
failed is_def_eq
...

But I don't know how to learn more about the metavariables

[Eric Wieser]

Eric Wieser said:

Anne Baanen, pp.all and pp.notation continue to show a hypothesis that matches the goal

Wait, this was a lie. I used set_option pp.all without the trailing true. There is a difference.

[Eric Wieser]

For the zero, the goal uses

            (@add_monoid.to_has_zero
               ((λ (i : ι),
                   @coe_sort
                     (@add_submonoid A (@add_comm_monoid.to_add_monoid A (@semiring.to_add_comm_monoid A _inst_1)))
                     (@add_submonoid.has_coe_to_sort A
                        (@add_comm_monoid.to_add_monoid A (@semiring.to_add_comm_monoid A _inst_1)))
                     (carriers i))
                  i)
               (@add_comm_monoid.to_add_monoid
                  ((λ (i : ι),
                      @coe_sort
                        (@add_submonoid A (@add_comm_monoid.to_add_monoid A (@semiring.to_add_comm_monoid A _inst_1)))
                        (@add_submonoid.has_coe_to_sort A
                           (@add_comm_monoid.to_add_monoid A (@semiring.to_add_comm_monoid A _inst_1)))
                        (carriers i))
                     i)
                  ((λ (i : ι),
                      @add_submonoid.to_add_comm_monoid A (@semiring.to_add_comm_monoid A _inst_1) (carriers i))
                     i)))))

While the hypothesis uses

            (@add_submonoid.has_zero A (@add_comm_monoid.to_add_monoid A (@semiring.to_add_comm_monoid A _inst_1))
               (carriers i))))

[Eric Wieser]

Oh, I screwed up the typeclasses on docs#add_monoid_hom.coe_dfinsupp_sum... Maybe relaxing those will fix it

[Eric Wieser]

@Alex J. Best, how far from prime-time is your "typeclass assumptions are too strict" linter?

[Alex J. Best]

@Eric Wieser not too far, maybe a week or so from prime time, I have some changes to make but I think I at least know the right algorithm now :smile:

[Eric Wieser]

Another "the typeclass is right there" situation:

import algebra.module.pi

example {α ι : Type*} [comm_ring α] : is_scalar_tower α (ι → α) (ι → α) :=
by apply_instance  -- fail

example {α ι : Type*} [comm_ring α] : is_scalar_tower α (ι → α) (ι → α) :=
pi.is_scalar_tower'  -- fail

example {α ι : Type*} [comm_ring α] : is_scalar_tower α (ι → α) (ι → α) :=
let i : ι → is_scalar_tower α α α := λ i, by apply_instance in by exactI
pi.is_scalar_tower'  -- fail, does not find `i` which exactly matches the goal state

example {α ι : Type*} [comm_ring α] : is_scalar_tower α (ι → α) (ι → α) :=
let i : ι → is_scalar_tower α α α := λ i, by apply_instance in by exactI
@pi.is_scalar_tower' _ _ _ _ _ _ _ i  -- works

Why can't lean find the i instance?

[Eric Wieser]

Adding a non-dependent version of the instance seems to fix it:

instance pi.is_scalar_tower_again {ι α β γ : Type*} [has_scalar α β] [has_scalar β γ] [has_scalar α γ]
  [is_scalar_tower α β γ] : is_scalar_tower α (ι → β) (ι → γ) :=
pi.is_scalar_tower'

I wonder if we need to do this for all instance on pi types

[Gabriel Ebner]

I have the feeling that we're running into this problem relatively often, and it's freaking me out a bit because the issue seems to be deep in the unifier and I don't really understand. It would really help if we had a small mathlib-free MWE. (We can also post the MWE on the Lean 4 bug tracker...)

[Eric Wieser]

Some more data (the missing instance is #8604):

import algebra.module.pi

-- oops, this instance is missing
instance semigroup.to_is_scalar_tower {α} [semigroup α] : is_scalar_tower α α α := ⟨mul_assoc⟩

example {α ι : Type*} [monoid α] : is_scalar_tower α (ι → α) (ι → α) :=
by apply_instance  -- fail

example {α ι : Type*} [semigroup α] : is_scalar_tower α (ι → α) (ι → α) :=
by apply_instance  -- ok

[Eric Wieser]

Here's the version without mathlib:

set_option old_structure_cmd true

variables {I : Type*} {f  : I → Type*}

section has_scalar

class has_scalar (M : Type*) (α : Type*) := (smul : M → α → α)

infixr ` • `:73 := has_scalar.smul

instance has_mul.to_has_scalar (α : Type*) [has_mul α] : has_scalar α α := ⟨(*)⟩

instance pi.has_scalar {α : Type*} [Π i, has_scalar α $ f i] :
  has_scalar α (Π i : I, f i) :=
⟨λ s x, λ i, s • (x i)⟩

instance pi.has_scalar' {g : I → Type*} [Π i, has_scalar (f i) (g i)] :
  has_scalar (Π i, f i) (Π i : I, g i) :=
⟨λ s x, λ i, (s i) • (x i)⟩

end has_scalar

section is_scalar_tower

class is_scalar_tower (M N α : Type*) [has_scalar M N] [has_scalar N α] [has_scalar M α] : Prop :=
(smul_assoc : ∀ (x : M) (y : N) (z : α), (x • y) • z = x • (y • z))

class semigroup (G : Type*) extends has_mul G :=
(mul_assoc : ∀ a b c : G, a * b * c = a * (b * c))

class mul_one_class (M : Type*) extends has_one M, has_mul M :=
(one_mul : ∀ (a : M), 1 * a = a)
(mul_one : ∀ (a : M), a * 1 = a)

class monoid (G : Type*) extends semigroup G, mul_one_class G

end is_scalar_tower

export is_scalar_tower (smul_assoc) semigroup (mul_assoc)

instance semigroup.to_is_scalar_tower {α} [semigroup α] : is_scalar_tower α α α := ⟨mul_assoc⟩

instance pi.is_scalar_tower' {g : I → Type*} {α : Type*}
  [Π i, has_scalar α $ f i] [Π i, has_scalar (f i) (g i)] [Π i, has_scalar α $ g i]
  [Π i, is_scalar_tower α (f i) (g i)] : is_scalar_tower α (Π i : I, f i) (Π i : I, g i) :=
⟨λ x y z, funext $ λ i, smul_assoc x (y i) (z i)⟩

-- change `monoid` to `semigroup` and the below work

example {α ι : Type*} [monoid α] : is_scalar_tower α (ι → α) (ι → α) :=
by apply_instance  -- fail

example {α ι : Type*} [monoid α] : is_scalar_tower α (ι → α) (ι → α) :=
pi.is_scalar_tower'  -- fail

example {α ι : Type*} [monoid α] : is_scalar_tower α (ι → α) (ι → α) :=
let i : ι → is_scalar_tower α α α := λ i, by apply_instance in begin
  tactic.unfreeze_local_instances,
  tactic.freeze_local_instances,
  exact pi.is_scalar_tower'  -- fail, does not find `i` which exactly matches the goal state
end

example {α ι : Type*} [monoid α] : is_scalar_tower α (ι → α) (ι → α) :=
let i : ι → is_scalar_tower α α α := λ i, by apply_instance in by exact
@pi.is_scalar_tower' _ _ _ _ _ _ _ i  -- works

[Gabriel Ebner]

Good news: in the straightforward Lean 4 translation of this MWE, all examples work!

[Daniel Selsam]

Gabriel Ebner said:

Good news: in the straightforward Lean 4 translation of this MWE, all examples work!

They do now :) Please consider PRing your translation as a "run" test so they always do.

[Sebastien Gouezel]

Isn't it https://github.com/leanprover/lean4/issues/509 ? (I think it was said at the time that it was possible to backport this in Lean 3)

[Sebastien Gouezel]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/typeclass.20failure/near/242412905