feat: relax auto-implicit restrictions

The new options `relaxedAutoBoundImplicitLocal` can be used to
disable this feature.

closes #1011

RELEASES.md

@@ -21,3 +21,5 @@ theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)]
 * Various improvements to go-to-definition & find-all-references accuracy.
 
 * Auto generated congruence lemmas with support for casts on proofs and `Decidable` instances (see [whishlist](https://github.com/leanprover/lean4/issues/988)).
+
+* [Relax auto-implicit restrictions](https://github.com/leanprover/lean4/pull/1011). The command `set_option relaxedAutoBoundImplicitLocal false` disables the relaxations.

src/Lean/Elab/AutoBound.lean

@@ -11,9 +11,15 @@ namespace Lean.Elab
 
 register_builtin_option autoBoundImplicitLocal : Bool := {
     defValue := true
-    descr    := "Unbound local variables in declaration headers become implicit arguments if they are a lower case or greek letter followed by numeric digits. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}."
+    descr    := "Unbound local variables in declaration headers become implicit arguments. In \"relaxed\" mode (default), any atomic identifier is eligible, otherwise only a lower case or greek letter followed by numeric digits are eligible. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}."
   }
 
+register_builtin_option relaxedAutoBoundImplicitLocal : Bool := {
+    defValue := true
+    descr    := "When \"relaxed\" mode is enabled, any atomic nonempty identifier is eligible for auto bound implicit locals (see optin `autoBoundImplicitLocal`."
+  }
+
+
 private def isValidAutoBoundSuffix (s : String) : Bool :=
   s.toSubstring.drop 1 |>.all fun c => c.isDigit || isSubScriptAlnum c || c == '_' || c == '\''
 
@@ -31,14 +37,14 @@ When, we try again, a `x` with a new macro scope is created and this process kee
 Therefore, we do consider identifier with macro scopes anymore.
 -/
 
-def isValidAutoBoundImplicitName (n : Name) : Bool :=
+def isValidAutoBoundImplicitName (n : Name) (relaxed : Bool) : Bool :=
   match n with
-  | Name.str Name.anonymous s _ => s.length > 0 && (isGreek s[0] || s[0].isLower) && isValidAutoBoundSuffix s
+  | Name.str Name.anonymous s _ => s.length > 0 && (relaxed || ((isGreek s[0] || s[0].isLower) && isValidAutoBoundSuffix s))
   | _ => false
 
-def isValidAutoBoundLevelName (n : Name) : Bool :=
+def isValidAutoBoundLevelName (n : Name) (relaxed : Bool) : Bool :=
   match n with
-  | Name.str Name.anonymous s _ => s.length > 0 && s[0].isLower && isValidAutoBoundSuffix s
+  | Name.str Name.anonymous s _ => s.length > 0 && (relaxed || (s[0].isLower && isValidAutoBoundSuffix s))
   | _ => false
 
 end Lean.Elab

src/Lean/Elab/Level.lean

@@ -72,7 +72,7 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do
   else if kind == identKind then
     let paramName := stx.getId
     unless (← get).levelNames.contains paramName do
-      if (← read).autoBoundImplicit && isValidAutoBoundLevelName paramName then
+      if (← read).autoBoundImplicit && isValidAutoBoundLevelName paramName (relaxedAutoBoundImplicitLocal.get (← read).options) then
         modify fun s => { s with levelNames := paramName :: s.levelNames }
       else
         throwError "unknown universe level '{paramName}'"

src/Lean/Elab/Term.lean

@@ -1418,7 +1418,7 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List Stri
     throw ex
 where process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do
   if candidates.isEmpty then
-    if (← read).autoBoundImplicit && isValidAutoBoundImplicitName n then
+    if (← read).autoBoundImplicit && isValidAutoBoundImplicitName n (relaxedAutoBoundImplicitLocal.get (← getOptions)) then
       throwAutoBoundImplicitLocal n
     else
       throwError "unknown identifier '{Lean.mkConst n}'"

tests/lean/1011.lean

@@ -0,0 +1,5 @@
+def f (x : A) := x
+
+set_option relaxedAutoBoundImplicitLocal false
+
+def g (x : A) := x

tests/lean/1011.lean.expected.out

@@ -0,0 +1 @@
+1011.lean:5:11-5:12: error: unknown identifier 'A'

tests/lean/autoBoundImplicits1.lean

@@ -1,5 +1,5 @@
 def myid (a : α) := a -- works
-
+set_option relaxedAutoBoundImplicitLocal false
 #check myid 10
 #check myid true
 

tests/lean/autoBoundImplicits2.lean

@@ -1,6 +1,6 @@
 def f [Add α] (a : α) : α :=
   a + a
-
+set_option relaxedAutoBoundImplicitLocal false
 def BV (n : Nat) := { a : Array Bool // a.size = n }
 
 def allZero (bv : BV n) : Prop :=

tests/lean/interactive/533.lean

@@ -1,3 +1,4 @@
+set_option relaxedAutoBoundImplicitLocal false
 inductive Foo where
  | bar : F
         --^ textDocument/completion

tests/lean/interactive/533.lean.expected.out

@@ -1,5 +1,5 @@
 {"textDocument": {"uri": "file://533.lean"},
- "position": {"line": 1, "character": 10}}
+ "position": {"line": 2, "character": 10}}
 {"items":
  [{"label": "False", "kind": 22, "detail": "Prop"},
   {"label": "Fin", "kind": 22, "detail": "Nat → Type"},

tests/lean/interactive/hoverException.lean

@@ -1,3 +1,4 @@
+set_option relaxedAutoBoundImplicitLocal false
 inductive Foo
 | mk : (a b : Bar) → Foo
             --^ textDocument/hover

tests/lean/interactive/hoverException.lean.expected.out

@@ -1,3 +1,3 @@
 {"textDocument": {"uri": "file://hoverException.lean"},
- "position": {"line": 1, "character": 14}}
+ "position": {"line": 2, "character": 14}}
 null

tests/lean/structSorryBug.lean

@@ -1,3 +1,4 @@
+set_option relaxedAutoBoundImplicitLocal false
 instance has_arr : HasArr Preorder := { Arr := Function }
 
 def foo : Nat := { first := 10 }

tests/lean/structSorryBug.lean.expected.out

@@ -1,3 +1,3 @@
-structSorryBug.lean:1:19-1:25: error: unknown identifier 'HasArr'
-structSorryBug.lean:3:17-3:32: error: invalid {...} notation, structure type expected
+structSorryBug.lean:2:19-2:25: error: unknown identifier 'HasArr'
+structSorryBug.lean:4:17-4:32: error: invalid {...} notation, structure type expected
   Nat