LinearMap.restrictScalars prints weirdly

Stream: mathlib4

[Yaël Dillies]

Why is docs#LinearMap.restrictScalars tagged as coe? This leads to the following mumble-jumble when pretty-printing:

import Mathlib.Algebra.Module.LinearMap.Defs
import Mathlib.Data.Real.Basic

-- ↑ℝ : (?m.6 →ₗ[?m.5] ?m.7) → ?m.6 →ₗ[ℝ] ?m.7
#check LinearMap.restrictScalars ℝ

[Anne Baanen]

Since the coercion docs#LinearMap.coeIsScalarTower is defined as restrictScalars, our default rule would be to tag restrictScalars as @[coe]. But I am not sure whether that coercion is even a good idea, since docs#CoeHTCT is an implementation detail that we shouldn't have instances for...

[Eric Wieser]

Personally I think this instance is a bad idea and we should just write restrictScalars out in full

[Eric Wieser]

If that's really too long, we could introduced a scoped notation

[Junyan Xu]

I'm observing some simp timeout if I don't get rid of a certain restrictScalars. Could it be related?