questions about type class instance

Stream: new members

[Winston Yin]

I'm trying to do two things.

1. Define a structure containing, say, (ι : Type*), but also requiring nontrivial ι, perhaps by type class inference rather than explicit proof. E.g.

structure my_struct :=
(ι : Type*)
[nontriv_ι : nontrivial ι]
...

2. In a proof, I need to provide a term for the type Π₀ i : ι, M i. When I construct this term using an object of my_struct, Lean fails to see nontriv_ι when synthesising the nontrivial ι for the dfinsupp. How can I help Lean see the type class instance provided by nontriv_ι? Lean keeps saying "failed to synthesise type class instance".

[Kevin Buzzard]

The square brackets in the definition do not make it an instance. Try attribute [instance] my_struct.nontriv_ι after the definition and see if this fixes things.

[Eric Wieser]

I think for this specific example #lint will complain the instance is dangerous / impossible, but that might just be because you over-minimized the example