The following example, using inhabited types, motivates the potential interest for allowing coercions to leverage typeclass inference. I wonder if there would be obstacles to supporting it. Set Implicit Arguments. Class Inhab (A:Type) : Prop := { inhab: exists (x:A), True }. Record IType : Type…

Generalizing coercions to infer typeclass arguments

mattam82 April 11, 2021, 3:36pm 5

That sounds like a good plan!

1 Like