fix: make sure anonymous dot notation works with pi-type-valued type synonyms #4818
Conversation
When resolving anonymous dot notation (`.ident x y z`), it would reduce the expected type to whnf. Now, it unfolds definitions step-by-step, even if the type synonym is for a pi type like so ```lean def Foo : Prop := ∀ a : Nat, a = a protected theorem Foo.intro : Foo := sorry example : Foo := .intro ```
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added
the
builds-mathlib
|
Mathlib CI status (docs):
|
kmill
changed the title
| @@ -1354,9 +1354,17 @@ private partial def resolveDotName (id : Syntax) (expectedType? : Option Expr) : | |||
| tryPostponeIfNoneOrMVar expectedType? | |||
| let some expectedType := expectedType? | |||
| | throwError "invalid dotted identifier notation, expected type must be known" | |||
| forallTelescopeReducing expectedType fun _ resultType => do | |||
There was a problem hiding this comment.
Just curious: Could we have used forallTelescope if we had a TransparencyMode none?
Or would using withReducible do the right thing here! Or do we want people to use dot notation with reducible terms (I guess we do, commonly with abbrev, right?)
There was a problem hiding this comment.
This made it mirroring how Lean.Elab.Term.consumeImplicits works (for x.f dot notation resolution), which also uses whnfCore and manual definition unfolding. It would be nice to have a version of forallTelescope where you can supply your own reduction function — that's something I was thinking about, but didn't want to touch that core meta code for this.
Supposing reducible transparency was ok here, a problem with withReducible is that it applies to the entire computation (plus the continuation!), where we just want to delimit it to the internal mechanism of forallTelescopeReducing.
There was a problem hiding this comment.
Yeah, two continuation-style functions don't compose well. Could be a ReducibilityMode option to forallTelescopeReducing. (Not important)
There was a problem hiding this comment.
Yeah, it could be, but better would be reduction function rather than configuration, since we do want whnfCore here rather than whnf. Without measuring, I worry a bit about the performance impact though since the function won't be specialized to whnf, and forallTelescope(Reducing) is used everywhere.
There was a problem hiding this comment.
On second thought, there's no need to adjust forallTelescopeReducingAuxAux itself, since you can use the pattern in this PR. I don't think there are really any optimizations from inserting a custom whnf function into it.
(This PR also continues on with whnfCore of the body, vs forallTelescopeReducing which gives you the unreduced body if it didn't reduce to a forall.)
When resolving anonymous dot notation (
.ident x y z), it would reduce the expected type to whnf. Now, it unfolds definitions step-by-step, even if the type synonym is for a pi type like soCloses #4761