feat: dotParam widget to control dot notation

This PR introduces the `dotParam` marker to indicate which parameter should be used for generalized field notation ("dot notation"). Example:
```
class A (α : Type _) where
  a : α → Nat

def A.get {α : Type _} [A α] (self : dotParam α) : Nat := a self

structure B where
  b : Nat

instance : A B := ⟨B.b⟩

namespace B
export A (get)
end B

#check fun (b : B) => b.get
-- b.get : Nat
```
The pretty printing code is modified to support the `export`-resolved dot notation introduced in leanprover#6189.

Closes leanprover#1629, closes leanprover#5482

src/Init/Prelude.lean

@@ -599,6 +599,12 @@ A binder like `(x : α := default)` in a declaration is syntax sugar for
 -/
 @[reducible] def optParam (α : Sort u) (default : α) : Sort u := α
 
+/--
+Gadget for dot notation support. A binder like `(x : dotParam α)` in a declaration will be used for generalized field notation,
+overriding the normal rule that the first argument with a relevant type will be used.
+-/
+@[reducible] def dotParam (α : Sort u) : Sort u := α
+
 /--
 Gadget for marking output parameters in type classes.
 

src/Lean/Elab/App.lean

@@ -14,6 +14,7 @@ import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.Arg
 import Lean.Elab.RecAppSyntax
+import Lean.Expr
 
 namespace Lean.Elab.Term
 open Meta
@@ -1322,14 +1323,20 @@ where
     let mut argIdx := argIdx
     let mut remainingNamedArgs := remainingNamedArgs
     let mut unusableNamedArgs := unusableNamedArgs
-    for x in xs, bInfo in bInfos do
+    let mut dotParamIdx? ← xs.findIdxM? fun x => return (← x.mvarId!.getDecl).type.isDotParam
+    let isDotParam (idx : Nat) (argType : Expr) : MetaM Bool := do
+      if let some dotParamIdx := dotParamIdx? then
+        return dotParamIdx == idx
+      else
+        typeMatchesBaseName argType baseName
+    for x in xs, bInfo in bInfos, i in [0:xs.size] do
       let xDecl ← x.mvarId!.getDecl
       if let some idx := remainingNamedArgs.findFinIdx? (·.name == xDecl.userName) then
         /- If there is named argument with name `xDecl.userName`, then it is accounted for and we can't make use of it. -/
         remainingNamedArgs := remainingNamedArgs.eraseIdx idx
       else
-        if ← typeMatchesBaseName xDecl.type baseName then
-          /- We found a type of the form (baseName ...), or we found the first explicit argument in useFirstExplicit mode.
+        if ← isDotParam i xDecl.type then
+          /- We found a type of the form (baseName ...), or if there's a dotParam, we've reached it.
              First, we check if the current argument is one that can be used positionally,
              and if the current explicit position "fits" at `args` (i.e., it must be ≤ arg.size) -/
           if h : argIdx ≤ args.size ∧ (explicit || bInfo.isExplicit) then

src/Lean/Expr.lean

@@ -1594,6 +1594,10 @@ def isOptParam (e : Expr) : Bool :=
 def isAutoParam (e : Expr) : Bool :=
   e.isAppOfArity ``autoParam 2
 
+/-- Return `true` if `e` is of th eform `dotParam _` -/
+def isDotParam (e : Expr) : Bool :=
+  e.isAppOfArity ``dotParam 1
+
 /--
 Remove `outParam`, `optParam`, and `autoParam` applications/annotations from `e`.
 Note that it does not remove nested annotations.
@@ -1605,7 +1609,7 @@ Examples:
 partial def consumeTypeAnnotations (e : Expr) : Expr :=
   if e.isOptParam || e.isAutoParam then
     consumeTypeAnnotations e.appFn!.appArg!
-  else if e.isOutParam || e.isSemiOutParam then
+  else if e.isOutParam || e.isSemiOutParam || e.isDotParam then
     consumeTypeAnnotations e.appArg!
   else
     e

src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean

@@ -5,6 +5,7 @@ Authors: Kyle Miller
 -/
 prelude
 import Lean.Meta.InferType
+import Lean.Meta.WHNF
 import Lean.PrettyPrinter.Delaborator.Attributes
 import Lean.PrettyPrinter.Delaborator.Options
 import Lean.Structure
@@ -47,16 +48,26 @@ returns the field name and the index for the argument to be used as the object o
 Otherwise it fails.
 -/
 private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name × Nat) := do
-  let .str _ field := c | failure
+  let .str baseName field := c | failure
   let field := Name.mkSimple field
-  let baseName := c.getPrefix
   guard <| !baseName.isAnonymous
   -- Disallow `Function` since it is used for pi types.
   guard <| baseName != `Function
   let info ← getConstInfo c
-  -- Search for the first argument that could be used for field notation
-  -- and make sure it is the first explicit argument.
+  -- Search for the first argument that could be used for field notation.
   forallBoundedTelescope info.type args.size fun params _ => do
+    -- First, look for a `dotParam`.
+    for h : i in [0:params.size] do
+      let type ← params[i].fvarId!.getType
+      if type.isDotParam then
+        -- We need to be sure that name resolution would find this function. If it wouldn't, then fail.
+        let .const structName _ := (← whnfCore <| ← inferType args[i]!).consumeMData.getAppFn | failure
+        let candidates := ResolveName.resolveGlobalName (← getEnv) Name.anonymous (← getOpenDecls) (structName ++ field)
+          |>.filter (fun (_, fieldList) => fieldList.isEmpty)
+          |>.map Prod.fst
+        guard <| candidates == [c]
+        return (field, i)
+    -- Second, look for a matching type. Make sure it is the first explicit argument.
     for h : i in [0:params.size] do
       let fvarId := params[i].fvarId!
       -- If there is a motive, we will treat this as a sort of control flow structure and so we won't use field notation.
@@ -68,7 +79,7 @@ private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name ×
         -- We require an exact match for the base name.
         -- While `Lean.Elab.Term.resolveLValLoop` is able to unfold the type and iterate, we do not attempt to exploit this feature.
         -- (To get it right, we would need to check that each relevant namespace does not contain a declaration named `field`.)
-        guard <| (← instantiateMVars <| ← inferType args[i]!).consumeMData.isAppOf baseName
+        guard <| (← whnfCore <| ← inferType args[i]!).consumeMData.isAppOf baseName
         return (field, i)
       else
         -- We only use the first explicit argument for field notation.

tests/lean/run/1629.lean

@@ -0,0 +1,65 @@
+/-!
+# `dotParam` for controlling which parameter recieves the object of dot notation
+https://github.com/leanprover/lean4/issues/1629
+https://github.com/leanprover/lean4/issues/5482
+-/
+
+/-!
+Example: normally `γ` would receive the object of dot notation, but we override it to the useful parameter.
+-/
+
+def Function.swap' {α β} {γ : α → β → Sort _} (f : dotParam <| (a : α) → (b : β) → γ a b)
+  (b : β) (a : α) : γ a b := f a b
+
+/-- info: 0 -/
+#guard_msgs in #eval Nat.div.swap' 10 2
+/-- info: 5 -/
+#guard_msgs in #eval Nat.div.swap' 2 10
+
+/-!
+Example from https://github.com/leanprover/lean4/issues/5482
+-/
+
+class A (α : Type _) where
+  a : α → Nat
+
+def A.get {α : Type _} [A α] (self : dotParam α) : Nat := a self
+
+structure B where
+  b : Nat
+
+instance : A B := ⟨B.b⟩
+
+namespace B
+export A (get)
+end B
+
+variable (b : B)
+
+/-- info: b.get : Nat -/
+#guard_msgs in #check b.get
+
+/-!
+Zulip example
+https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Function.20dot.20notation.20error/near/296865418
+-/
+class HasMem (α : outParam $ Type _) (β : Type _) where
+  mem : α → β → Prop
+
+infix:50 " ∈ " => HasMem.mem
+
+def HasMem.Nonempty [HasMem α β] (self : dotParam β) : Prop :=
+  ∃ x, x ∈ self
+
+def Set (α : Type _) := α → Prop
+
+instance : HasMem α (Set α) where
+  mem x s := s x
+
+namespace Set
+export HasMem (Nonempty)
+end Set
+
+variable (s : Set α)
+/-- info: s.Nonempty : Prop -/
+#guard_msgs in #check s.Nonempty