Failed to synthesize Union

Stream: new members

[Iocta]

What is this and how to fix?

import Mathlib

variable {α : Type} (a b : Finset α)
#check a ∪ b
failed to synthesize
  Union (Finset α)

#check insert b ({a} : Finset (Finset α))
failed to synthesize
  Insert (Finset α) (Finset (Finset α))

[Matt Diamond]

the instances require DecidableEq, so just use the classical tactic beforehand or add an assumption

[Matt Diamond]

or open Classical in, etc.

[Iocta]

What's the clue that should tip me off that I need classical?

[Matt Diamond]

not sure... honestly I just looked up docs#Union in the mathlib docs, opened the Instances list, saw docs#Finset.instUnion, clicked through, and saw the DecidableEq requirement

[Matt Diamond]

it would be cool if the instance search had some way of telling the user "I almost found an instance but it was missing this one typeclass requirement"

[Matt Diamond]

actually you can do this:

import Mathlib

variable {α : Type}

set_option diagnostics true

#synth Union (Finset α)

and there's some more info there