convert

Stream: mathlib4

[Kyle Miller]

Something people have noticed during porting is that convert/convert_to is less good at elaboration, in the sense that it doesn't really make use of any information from the goal when synthesizing instances.

#6041 is an experiment to change how the term is elaborated so that it has the following properties:
1) It will try to synthesize instances when it can.
2) If it fails for any reason, it turns the instance problems into additional goals.
3) The goals can be solved for by unification during the congr! algorithm.

[Kyle Miller]

While the changes do seem to work, there are some downsides:
1) Typeclass inference failures are not errors. (This is both a positive and a negative.)
2) Ambiguous notation can't use typeclass inference to disambiguate. One example that popped up is μ[X] in probability, which is either an integral or the GetElem notation...

[Kyle Miller]

(@Matthew Ballard I think I remember you running into convert limitations a lot. Maybe you know of some good places to test this change out?)