Instances for forgetful inheritance

Stream: general

[Patrick Massot]

@Daniel Selsam did you had a look at https://hal.inria.fr/hal-02463336/document? The authors somehow claim that instance resolution procedures (either unification hints or type classes) should do something special to prioritize instances that corresponding to embedded weaker structures. For instance, in mathlib we define a metric space as a structure containing a uniform_space structure as a field to_uniform_space, and an axiom uniformity_dist saying this uniform space structure has to be the determined by the other fields. Then in mathlib we mark to_uniform_space as an instance but, for reasons explained here, this instance has a low priority. However, when we want a uniform structure on a metric space, we would like that one to be found immediately. In the paper, the authors argue that unification hints allow more search control that type classes for this issue (this is the traditional claim that unification hints are more verbose but more controlled than type class). Do you have any thought about that?

[Daniel Selsam]

Unfortunately I don't have time to read these links right now, but my default Zulip typeclass answering machine message is 'wait and see if this is still a problem after tabling'. This might be a problem right now only because if the wrong instance fires first you might try to synthesize decidable_linear_ordered_field ~30,000 times. If it is really still a problem after porting, then we could consider supporting additional instance annotations.