feat: dot notation and aliases

This commit addresses the issue raised at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Namespace-based.20overloading.20does.20not.20find.20exports/near/282946185

RELEASES.md

@@ -1,6 +1,21 @@
 Unreleased
 ---------
 
+* Improve dot notation and aliases interaction. See discussion on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Namespace-based.20overloading.20does.20not.20find.20exports/near/282946185) for additional details.
+  Example:
+  ```lean
+  def Set (α : Type) := α → Prop
+  def Set.union (s₁ s₂ : Set α) : Set α := fun a => s₁ a ∨ s₂ a
+  def FinSet (n : Nat) := Fin n → Prop
+
+  namespace FinSet
+    export Set (union) -- FinSet.union is now an alias for `Set.union`
+  end FinSet
+
+  example (x y : FinSet 10) : FinSet 10 :=
+    x.union y -- Works
+  ```
+
 * `ext` and `enter` conv tactics can now go inside let-declarations. Example:
   ```lean
   example (g : Nat → Nat) (y : Nat) (h : let x := y + 1; g (0+x) = x) : g (y + 1) = y + 1 := by
@@ -55,7 +70,7 @@ Unreleased
 
 * [`let/if` indentation in `do` blocks in now supported.](https://github.com/leanprover/lean4/issues/1120)
 
-* Updated Lake to v3.1.1. See the [v3.1.0 release note](https://github.com/leanprover/lake/releases/tag/v3.1.0) for detailed changes.
+* Update Lake to v3.1.1. See the [v3.1.0 release note](https://github.com/leanprover/lake/releases/tag/v3.1.0) for detailed changes.
 
 * Add unnamed antiquotation `$_` for use in syntax quotation patterns.
 

src/Lean/Elab/App.lean

@@ -527,7 +527,8 @@ private def throwLValError (e : Expr) (eType : Expr) (msg : MessageData) : TermE
 /-- `findMethod? env S fName`.
     1- If `env` contains `S ++ fName`, return `(S, S++fName)`
     2- Otherwise if `env` contains private name `prv` for `S ++ fName`, return `(S, prv)`, o
-    3- Otherwise for each parent structure `S'` of  `S`, we try `findMethod? env S' fname` -/
+    3- Otherwise for each parent structure `S'` of  `S`, we try `findMethod? env S' fname`
+-/
 private partial def findMethod? (env : Environment) (structName fieldName : Name) : Option (Name × Name) :=
   let fullName := structName ++ fieldName
   match env.find? fullName with
@@ -542,6 +543,23 @@ private partial def findMethod? (env : Environment) (structName fieldName : Name
       else
         none
 
+/--
+  Return `some (structName', fullName)` if `structName ++ fieldName` is an alias for `fullName`, and
+  `fullName` is of the form `structName' ++ fieldName`.
+
+  TODO: if there is more than one applicable alias, it returns `none`. We should consider throwing an error or
+  warning.
+-/
+private def findMethodAlias? (env : Environment) (structName fieldName : Name) : Option (Name × Name) :=
+  let fullName := structName ++ fieldName
+  let aliasesCandidates := getAliases env fullName |>.filterMap fun alias =>
+    match alias.eraseSuffix? fieldName with
+    | none => none
+    | some structName' => some (structName', alias)
+  match aliasesCandidates with
+  | [r] => some r
+  | _   => none
+
 private def throwInvalidFieldNotation (e eType : Expr) : TermElabM α :=
   throwLValError e eType "invalid field notation, type is not of the form (C ...) where C is a constant"
 
@@ -574,9 +592,11 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
   | some structName, LVal.fieldName _ fieldName _ _ =>
     let env ← getEnv
     let searchEnv : Unit → TermElabM LValResolution := fun _ => do
-      match findMethod? env structName (Name.mkSimple fieldName) with
-      | some (baseStructName, fullName) => return LValResolution.const baseStructName structName fullName
-      | none   =>
+      if let some (baseStructName, fullName) := findMethod? env structName fieldName then
+        return LValResolution.const baseStructName structName fullName
+      else if let some (structName', fullName) := findMethodAlias? env structName fieldName then
+        return LValResolution.const structName' structName' fullName
+      else
         throwLValError e eType
           m!"invalid field '{fieldName}', the environment does not contain '{Name.mkStr structName fieldName}'"
     -- search local context first, then environment

tests/lean/run/DVec.lean

@@ -0,0 +1,44 @@
+/-- A `Vec` is just a `List α` of statically known size -/
+def Vec (α : Type _) (n : Nat) : Type _
+  := Fin n → α
+
+abbrev TypeVec : Nat → Type _
+  := Vec (Type _)
+
+/-- A dependent vector is a heterogenous list of statically known size -/
+def DVec {n : Nat} (αs : TypeVec n) : Type _
+  := (i : Fin n) → (αs i)
+
+/-- A vector that repeats a single element `a` -/
+def Vec.const {α : Type _} (a : α) (n : Nat) : Vec α n
+  := fun _ => a
+
+/- `Vec` is defeq to a `DVec` with constant type -/
+unif_hint (α : Type _) (n : Nat) where
+  |- Vec α n =?= DVec (Vec.const α n)
+
+namespace DVec
+  def hd {n : Nat} {αs : TypeVec (n+1)} (v : DVec αs) : (αs 0)
+    := v 0
+end DVec
+
+namespace Vec
+  export DVec (hd)
+end Vec
+
+def ts : TypeVec 1 := Vec.const Nat 1
+
+-- works
+example (v : DVec ts) : Nat :=
+  v.hd
+
+-- works
+example (v : Vec Nat 1) : Nat :=
+  DVec.hd v
+
+-- Vec.hd exists
+#check @Vec.hd
+
+-- works
+example (v : Vec Nat 1) : Nat :=
+  v.hd

tests/lean/run/alias.lean

@@ -0,0 +1,16 @@
+def Set (α : Type) := α → Prop
+
+def Set.union (s₁ s₂ : Set α) : Set α :=
+  fun a => s₁ a ∨ s₂ a
+
+def FinSet (n : Nat) := Fin n → Prop
+
+namespace FinSet
+  export Set (union)
+end FinSet
+
+example (x y : FinSet 10) : FinSet 10 :=
+  FinSet.union x y
+
+example (x y : FinSet 10) : FinSet 10 :=
+  x.union y