Enable --lossy-unification globally?

[fredrik-bakke]

Should we consider setting the --lossy-unification flag globally for the library? Degrading performance due to not enabling this flag is a recurring issue that new contributors face and lose a lot of time to, and potentially get frustrated by, especially in elementary-number-theory and real-numbers.

[EgbertRijke]

When we discussed this last time I thought we came to the conclusion that lossy unification doesn't speed up type checking globally, and the real gain is obtained on a case by case basis. Perhaps things have changed since the new Agda release came out, so we'd have to check again.

[fredrik-bakke]

The main benefit I see of enabling the flag globally is not about whether the overall type checking time would decrease, but rather that it lowers the bar for people who want to contribute to the library, and avoids unnecessary frustration and time-waste in the beginner phase.