Empty typeclasses and / or instances

Stream: lean4

[cognivore]

Hi. Sometimes I just want to

class Bijection (β : Type u) (α : outParam (Type u)) where

But Lean 4 says no. So I have to

class Bijection (β : Type u) (α : outParam (Type u)) where
  comp : Type u := α
  atom : Type u := β

But ok. Then I would like to at least be able to

instance [Iterable α β] : Bijection β α

But I have to still

instance [Iterable α β] : Bijection β α where
  comp := α

[Henrik Böving]

one could make an argument here that your typeclass isn't exactly what you want, realistically speaking just knowing that beta and alpha have bijections via type class inference is useless, anyone can declare an instance for this (like you are doing above) without proof and without even providing the bijectin itself in the first place which might also be an interesting thing to do depending on your application.

Regarding defining instances that can be completely filled via default fields you can just:

instance : Bijection β α := {}

and Lean will be happy

[Reid Barton]

The empty class works fine for me here (with or without where)

[Mario Carneiro]

I would support an RFC to make all of these where lists 0+ instead of 1+