Overloaded abs causing issues

Stream: general

[Keefer Rowan]

I think overloading abs for ordered group and complex numbers is causing issues. Here's an example:

import data.complex.basic

open complex
example (a : ℂ) : a.abs = abs (a.re) := sorry

It throws:

ambiguous overload, possible interpretations
  abs a.re
  ↑(a.re).abs
Additional information:
c:\Users\keefe\OneDrive\Documents\Lean\mathlib\src\test.lean:4:26: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because it failed to disambiguate overload using the expected type
  ℝ
the following overloaded terms were applicable
  abs
  abs

I'm not sure how to deal with this, as writing example (a : ℂ) : a.abs = abs (a.re : ℝ) := sorry doesn't help. My best guess is it has to do type class inference for ordered_group and for coercion to $\mathbb{C}$ and they have the same priority, or something like that. I don't know how to work around (a suggestion on that would be helpful), but it also seems like this is a problem worth fixing in mathlib too. Perhaps renaming complex abs, making it protected, or changing priorities? Since complex abs is a norm, it seems like we should make it protected and then canonically use the norm notation outside of the basic file. Thoughts?

[Reid Barton]

Not an expert on this part of mathlib, but all your suggestions sound reasonable. As a local workaround, you can use open complex (hiding abs) which would simulate it being protected.

[Reid Barton]

Oh, I overlooked "renaming complex abs"--I don't think that one sounds reasonable :upside_down:
Since dot notation a.abs unambiguously gives you complex.abs, making it protected should be pretty much strictly better.

[Keefer Rowan]

Ok, didn't know that dot notation works for protected so figured protecting was on equal footing with renaming. That's good to know!

[Patrick Massot]

The current mathlib handling of abs and norm is not optimal. We should probably study what the mathcomp people did. They explain it in https://hal.inria.fr/hal-02463336

[Yury G. Kudryashov]

Do we need complex.abs Why not use has_norm?