Canonical Trivial Typeclass?

Stream: new members

[Oskar Goldhahn]

I'm writing something that is generic over typeclasses. Is there a Canonical Trivial Typeclass that I can use as the default? Something like: class Any (_: Type u)?

[Eric Wieser]

Generalizing over type classes doesn't really work very well in lean; is this perhaps an #xy problem?

[Oskar Goldhahn]

It's for #Is there code for X? > Restricted Monads.

[Oskar Goldhahn]

In what way does generalizing over type classes not work well?

[Eric Wieser]

Well, your generalization won't work for docs#star_ring for instance

[Eric Wieser]

Because it has too many arguments

[Oskar Goldhahn]

I'm fine with requiring a shim that uncurries the typeclasses.

[Eric Wieser]

At that point you could consider uncurrying the typeclasses elsewhere too, and bundle them in the types themselves

[Eric Wieser]

That's what things like docs#Group are

[Oskar Goldhahn]

I see. I can give that a try.

[Eric Wieser]

That pretty much amounts to what Scott suggested in the other thread, of course...