overloaded names can slow down elaboration

Stream: lean4

[Jovan Gerbscheid]

I noticed that in Mathlib/Geometry/Euclidean/SignedDist.lean, elaboration of

noncomputable def signedInfDist : P →ᵃ[ℝ] ℝ :=
  (innerₗ V (‖p -ᵥ orthogonalProjection s p‖⁻¹ • (p -ᵥ orthogonalProjection s p))).toAffineMap.comp
    (AffineMap.id ℝ P -ᵥ s.subtype.comp (orthogonalProjection s))

is sped up by about 40% if we replace orthogonalProjection with EuclideanGeometry.orthogonalProjection. Even though we have used open EuclideanGeometry, Lean still attempts to elaborate orthogonalProjection in the root namespace before it tries it in the EuclideanGeometry namespace.

Is this kind of behaviour expected? I hadn't expected that Lean attempts to elaborate constants in multiple different ways. And is there a way to change the order in which these are attempted? I feel like writing open X should give priority to constants in the X namespace over those in the root namespace.

[Kyle Miller]

Have you verified your hypothesis that it attempts one of the names before another? I thought that the way it worked is that it tries all interpretations simultaneously. The "ambiguous interpretation" error is when elaboration errors don't winnow down the list.

[Jovan Gerbscheid]

I discovered it by looking at the profiler trace: it was unsuccesfully trying to find some weird coercion. This turned out to come from trying the wrong orthogonalProjection. Fully specifying the name got rid of this.

[Kyle Miller]

That's consistent with trying all interpretations simultaneously, right?

[Jovan Gerbscheid]

Yes that's right. I first thought you meant it was doing parallel computation

[Kyle Miller]

Oh no, sorry, I mean more like concurrently (but without any multiplexing). It saves the elaborator state and attempts all interpretations of the constant.

[Kyle Miller]

This is know behavior, and it's a reason why it can be good to choose different names for things even if they're in different namespaces.

[Kyle Miller]

Since you've been looking at this case, I'm idly wondering whether there are any heuristics that we might consider in the app elaborator to be able to fail fast on _root_.orthogonalProjection. (The heuristic needs to have no false negatives.) Does anything pop out to you?

[Jovan Gerbscheid]

I don't think there is a way to make it fail particularly fast; it has to attempt coercions to make sure the elaboration fails.

[Yury G. Kudryashov]

Should we just move it to Submodule.orthogonalProjection?

[Yury G. Kudryashov]

(and the other one to AffineSubspace.orthogonalProjection)

[Jovan Gerbscheid]

#24247 does the rename to Submodule.orthogonalProjection

[Jireh Loreaux]

Should we rename docs#HasOrthogonalProjection to Submodule.OrthogonalProjection (note the lack of Has)?

[Jovan Gerbscheid]

I'm not too sure about the naming conventions. This class doesn't contain data, just a proof that there exists some orthogonal projection, so it is a bit different form classes like Add that give an add function. So I think the Has might describe to this?

[Jireh Loreaux]

Aha, so it should be Is, except Is doesn't make any sense, so it's Has. Sure, I agree with this logic.