type class error with mk_fintype_instance

Stream: general

[Floris van Doorn]

I'm trying to show that some class is a fintype. The derive handler doesn't quite work, because I need to also assume decidable_eq, so I tried to do it with docs#tactic.mk_fintype_instance. However, I get a weird error:

import tactic.derive_fintype

class my_class (M : Type*) :=
(one : M)
(eq_one : ∀ x : M, x = one)

variable {M : Type*}
instance [fintype M] [decidable_eq M] : fintype (my_class M) :=
begin
  haveI : fintype (Σ' (one : M) (eq_one : ∀ (x : M), x = one), unit) :=
  by apply_instance,
  tactic.mk_fintype_instance,
end

This gives

failed to synthesize type class instance for
M : Type u_1,
_inst_1 : fintype M,
_inst_2 : decidable_eq M,
_inst : fintype (Σ' (one : M) (eq_one : ∀ (x : M), x = one), unit)
⊢ fintype (Σ' (one : M) (eq_one : ∀ (x : M), x = one), unit)

even though the haveI shows that this instance can be synthesized. Any ideas what goes wrong? @Mario Carneiro

[Kevin Buzzard]

When this exact same thing happened to me (not with fintype, with some other typeclass which was in the instance cache) it turned out the problem was that there was another typeclass instance hidden in the goal which was not the one being picked up by type class inference (it was a classical v decidable eq one in my case). No idea if this is your problem but thought it was a funny coincidence that this also happened to me today.

[Kevin Buzzard]

indeed,

begin
  haveI : fintype (Σ' (one : M) (eq_one : ∀ (x : M), x = one), unit) :=
  by apply_instance,
  classical,
  tactic.mk_fintype_instance,
end

works so it was the same problem in some sense

[Mario Carneiro]

The two fintype expressions are not alpha equal. I will look at this more later but it looks like the terms being constructed by hand in mk_finset are not type correct, I think some unique names got messed up

[Mario Carneiro]

#7581