failed to generate instance

Stream: new members

[Alex Zhang]

Why can't lean infer instance in the following cases?

import field_theory.finite.basic
example (h : ∃ (I : Type*) (inst : fintype I), true) : true :=
begin
  rcases h with ⟨I, inst⟩,
  have g : fintype (I ⊕ I),
  {apply_instance}
end

error : tactic.mk_instance failed to generate instance for fintype (I ⊕ I)

[Eric Wieser]

tactic#resetI