chore: remove the coercion from String to Name

RELEASES.md

@@ -82,6 +82,10 @@ fact.def :
 ```
 
 v4.7.0
+Breaking changes:
+ * The coercion from `String` to `Name` was removed. Previously, it was `Name.mkSimple`, which does not separate strings at dots, but experience showed that this is not always the desired coercion. For the previous behavior, manually insert a call to `Name.mkSimple`.
+
+v4.7.0 (development in progress)
 ---------
 
 * `simp` and `rw` now use instance arguments found by unification,

src/Init/Meta.lean

@@ -947,6 +947,11 @@ def _root_.Substring.toName (s : Substring) : Name :=
       else
         Name.mkStr n comp
 
+/--
+Converts a `String` to a hierarchical `Name` after splitting it at the dots.
+
+`"a.b".toName` is the name `a.b`, not `«a.b»`. For the latter, use `Name.mkSimple`.
+-/
 def _root_.String.toName (s : String) : Name :=
   s.toSubstring.toName
 

src/Init/Prelude.lean

@@ -3482,20 +3482,31 @@ instance : Hashable String where
 namespace Lean
 
 /--
-Hierarchical names. We use hierarchical names to name declarations and
-for creating unique identifiers for free variables and metavariables.
+Hierarchical names consist of a sequence of components, each of
+which is either a string or numeric, that are written separated by dots (`.`).
 
-You can create hierarchical names using the following quotation notation.
+Hierarchical names are used to name declarations and for creating
+unique identifiers for free variables and metavariables.
+
+You can create hierarchical names using a backtick:
 ```
 `Lean.Meta.whnf
 ```
-It is short for `.str (.str (.str .anonymous "Lean") "Meta") "whnf"`
-You can use double quotes to request Lean to statically check whether the name
+It is short for `.str (.str (.str .anonymous "Lean") "Meta") "whnf"`.
+
+You can use double backticks to request Lean to statically check whether the name
 corresponds to a Lean declaration in scope.
 ```
 ``Lean.Meta.whnf
 ```
 If the name is not in scope, Lean will report an error.
+
+There are two ways to convert a `String` to a `Name`:
+
+ 1. `Name.mkSimple` creates a name with a single string component.
+
+ 2. `String.toName` first splits the string into its dot-separated
+    components, and then creates a hierarchical name.
 -/
 inductive Name where
   /-- The "anonymous" name. -/
@@ -3546,7 +3557,9 @@ abbrev mkNum (p : Name) (v : Nat) : Name :=
   Name.num p v
 
 /--
-Short for `.str .anonymous s`.
+Converts a `String` to a `Name` without performing any parsing. `mkSimple s` is short for `.str .anonymous s`.
+
+This means that `mkSimple "a.b"` is the name `«a.b»`, not `a.b`.
 -/
 abbrev mkSimple (s : String) : Name :=
   .str .anonymous s

src/Lean/AuxRecursor.lean

@@ -34,7 +34,7 @@ def isAuxRecursor (env : Environment) (declName : Name) : Bool :=
   || declName == ``Eq.ndrec
   || declName == ``Eq.ndrecOn
 
-def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : Name) : Bool :=
+def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : String) : Bool :=
   match declName with
   | .str _ s => s == suffix && isAuxRecursor env declName
   | _ => false

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -663,7 +663,7 @@ def emitExternCall (builder : LLVM.Builder llvmctx)
     (name : String := "") : M llvmctx (LLVM.Value llvmctx) :=
   match getExternEntryFor extData `c with
   | some (ExternEntry.standard _ extFn) => emitSimpleExternalCall builder extFn ps ys retty name
-  | some (ExternEntry.inline "llvm" _pat) => throw "Unimplemented codegen of inline LLVM"
+  | some (ExternEntry.inline `llvm _pat) => throw "Unimplemented codegen of inline LLVM"
   | some (ExternEntry.inline _ pat) => throw s!"Cannot codegen non-LLVM inline code '{pat}'."
   | some (ExternEntry.foreign _ extFn)  => emitSimpleExternalCall builder extFn ps ys retty name
   | _ => throw s!"Failed to emit extern application '{f}'."

src/Lean/CoreM.lean

@@ -219,7 +219,7 @@ def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat)
   unless max == 0 do
     let numHeartbeats ← IO.getNumHeartbeats
     if numHeartbeats - (← read).initHeartbeats > max then
-      throwMaxHeartbeat moduleName optionName max
+      throwMaxHeartbeat (.mkSimple moduleName) optionName max
 
 def checkMaxHeartbeats (moduleName : String) : CoreM Unit := do
   checkMaxHeartbeatsCore moduleName `maxHeartbeats (← read).maxHeartbeats

src/Lean/Data/Name.lean

@@ -7,8 +7,6 @@ prelude
 import Init.Data.Ord
 namespace Lean
 
-instance : Coe String Name := ⟨Name.mkSimple⟩
-
 namespace Name
 -- Remark: we export the `Name.hash` to make sure it matches the hash implemented in C++
 @[export lean_name_hash_exported] def hashEx : Name → UInt64 :=

src/Lean/Data/NameMap.lean

@@ -11,8 +11,6 @@ import Lean.Data.SSet
 import Lean.Data.Name
 namespace Lean
 
-instance : Coe String Name := ⟨Name.mkSimple⟩
-
 def NameMap (α : Type) := RBMap Name α Name.quickCmp
 
 @[inline] def mkNameMap (α : Type) : NameMap α := mkRBMap Name α Name.quickCmp

src/Lean/Elab/App.lean

@@ -1035,7 +1035,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
   if eType.isForall then
     match lval with
     | LVal.fieldName _ fieldName _ _ =>
-      let fullName := `Function ++ fieldName
+      let fullName := Name.str `Function fieldName
       if (← getEnv).contains fullName then
         return LValResolution.const `Function `Function fullName
     | _ => pure ()
@@ -1060,9 +1060,9 @@ 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
-      if let some (baseStructName, fullName) := findMethod? env structName fieldName then
+      if let some (baseStructName, fullName) := findMethod? env structName (.mkSimple fieldName) then
         return LValResolution.const baseStructName structName fullName
-      else if let some (structName', fullName) := findMethodAlias? env structName fieldName then
+      else if let some (structName', fullName) := findMethodAlias? env structName (.mkSimple fieldName) then
         return LValResolution.const structName' structName' fullName
       else
         throwLValError e eType

src/Lean/Elab/BuiltinCommand.lean

@@ -55,7 +55,7 @@ private def popScopes (numScopes : Nat) : CommandElabM Unit :=
 
 private def checkAnonymousScope : List Scope → Option Name
   | { header := "", .. } :: _ => none
-  | { header := h, .. }  :: _ => some h
+  | { header := h, .. }  :: _ => some <| .mkSimple h
   | _                         => some .anonymous -- should not happen
 
 private def checkEndHeader : Name → List Scope → Option Name
@@ -64,7 +64,7 @@ private def checkEndHeader : Name → List Scope → Option Name
     if h == s then
       (.str · s) <$> checkEndHeader p scopes
     else
-      some h
+      some <| .mkSimple h
   | _, _ => some .anonymous -- should not happen
 
 @[builtin_command_elab «namespace»] def elabNamespace : CommandElab := fun stx =>

src/Lean/Elab/Declaration.lean

@@ -95,7 +95,7 @@ private def expandDeclNamespace? (stx : Syntax) : MacroM (Option (Name × Syntax
   let scpView := extractMacroScopes name
   match scpView.name with
   | .str .anonymous _ => return none
-  | .str pre shortName => return some (pre, setDefName stx { scpView with name := shortName }.review)
+  | .str pre shortName => return some (pre, setDefName stx { scpView with name := .mkSimple shortName }.review)
   | _ => return none
 
 def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do

src/Lean/Elab/Structure.lean

@@ -302,7 +302,7 @@ private def getFieldType (infos : Array StructFieldInfo) (parentType : Expr) (fi
           let args := e.getAppArgs
           if let some major := args.get? numParams then
             if (← getNestedProjectionArg major) == parent then
-              if let some existingFieldInfo := findFieldInfo? infos subFieldName then
+              if let some existingFieldInfo := findFieldInfo? infos (.mkSimple subFieldName) then
                 return TransformStep.done <| mkAppN existingFieldInfo.fvar args[numParams+1:args.size]
       return TransformStep.done e
     let projType ← Meta.transform projType (post := visit)

src/Lean/Elab/Syntax.lean

@@ -173,7 +173,7 @@ where
           | `(stx| $sym:str) => pure sym
           | _ => return arg'
         let sym := sym.getString
-        return (← `(ParserDescr.nodeWithAntiquot $(quote sym) $(quote (`token ++ sym)) $(arg'.1)), 1)
+        return (← `(ParserDescr.nodeWithAntiquot $(quote sym) $(quote (Name.str `token sym)) $(arg'.1)), 1)
     else
       pure args'
     let (args', stackSz) := if let some stackSz := info.stackSz? then

src/Lean/Hygiene.lean

@@ -51,7 +51,7 @@ private def mkInaccessibleUserNameAux (unicode : Bool) (name : Name) (idx : Nat)
     else
       name.appendAfter ("✝" ++ idx.toSuperscriptString)
   else
-    name ++ Name.mkNum "_inaccessible" idx
+    name ++ Name.num `_inaccessible idx
 
 private def mkInaccessibleUserName (unicode : Bool) : Name → Name
   | .num p@(.str ..) idx =>

src/Lean/Meta/ArgsPacker.lean

@@ -532,7 +532,7 @@ where
   go : List Expr → Array Expr → MetaM α
   | [], acc => k acc
   | t::ts, acc => do
-    let name := if argsPacker.numFuncs = 1 then name else s!"{name}{acc.size+1}"
+    let name := if argsPacker.numFuncs = 1 then name else .mkSimple s!"{name}{acc.size+1}"
     withLocalDecl name .default t fun x => do
       go ts (acc.push x)
 

src/Lean/Meta/IndPredBelow.lean

@@ -65,8 +65,8 @@ def mkContext (declName : Name) : MetaM Context := do
 where
   motiveName (motiveTypes : Array Expr) (i : Nat) : MetaM Name :=
     if motiveTypes.size > 1
-    then mkFreshUserName s!"motive_{i.succ}"
-    else mkFreshUserName "motive"
+    then mkFreshUserName <| .mkSimple s!"motive_{i.succ}"
+    else mkFreshUserName <| .mkSimple "motive"
 
   mkHeader
       (motives : Array (Name × Expr))
@@ -315,7 +315,7 @@ where
 def mkBrecOnDecl (ctx : Context) (idx : Nat) : MetaM Declaration := do
   let type ← mkType
   let indVal := ctx.typeInfos[idx]!
-  let name := indVal.name ++ brecOnSuffix
+  let name := indVal.name ++ .mkSimple brecOnSuffix
   return Declaration.thmDecl {
     name := name
     levelParams := indVal.levelParams
@@ -337,8 +337,8 @@ where
       (motive : Name × Expr) : MetaM $ Name × (Array Expr → MetaM Expr) := do
     let name :=
       if ctx.motives.size > 1
-      then mkFreshUserName s!"ih_{idx.val.succ}"
-      else mkFreshUserName "ih"
+      then mkFreshUserName <| .mkSimple s!"ih_{idx.val.succ}"
+      else mkFreshUserName <| .mkSimple "ih"
     let ih ← instantiateForall motive.2 params
     let mkDomain (_ : Array Expr) : MetaM Expr :=
       forallTelescopeReducing ih fun ys _ => do

src/Lean/Meta/Tactic/FunInd.lean

@@ -368,7 +368,7 @@ def deduplicateIHs (vals : Array Expr) : MetaM (Array Expr) := do
 def assertIHs (vals : Array Expr) (mvarid : MVarId) : MetaM MVarId := do
   let mut mvarid := mvarid
   for v in vals.reverse, i in [0:vals.size] do
-    mvarid ← mvarid.assert s!"ih{i+1}" (← inferType v) v
+    mvarid ← mvarid.assert (.mkSimple s!"ih{i+1}") (← inferType v) v
   return mvarid
 
 
@@ -580,7 +580,7 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
     -- * the MVars are independent (so we don’t need to reorder them)
     -- * we do no need the mvars in their unassigned form later
     let e' ← Meta.withLocalDecls
-      (mvars.mapIdx (fun i mvar => (s!"case{i.val+1}", .default, (fun _ => mvar.getType))))
+      (mvars.mapIdx (fun i mv => (.mkSimple s!"case{i.val+1}", .default, (fun _ => mv.getType))))
       fun xs => do
         for mvar in mvars, x in xs do
           mvar.assign x

src/Lean/Parser.lean

@@ -49,9 +49,9 @@ builtin_initialize
   register_parser_alias andthen { stackSz? := none }
   register_parser_alias recover
 
-  registerAlias "notFollowedBy" ``notFollowedBy (notFollowedBy · "element")
-  Parenthesizer.registerAlias "notFollowedBy" notFollowedBy.parenthesizer
-  Formatter.registerAlias "notFollowedBy" notFollowedBy.formatter
+  registerAlias `notFollowedBy ``notFollowedBy (notFollowedBy · "element")
+  Parenthesizer.registerAlias `notFollowedBy notFollowedBy.parenthesizer
+  Formatter.registerAlias `notFollowedBy notFollowedBy.formatter
 
 end Parser
 

src/Lean/Parser/Extra.lean

@@ -291,7 +291,9 @@ macro_rules
   | `(register_parser_alias $[(kind := $kind?)]? $(aliasName?)? $declName $(info?)?) => do
     let [(fullDeclName, [])] ← Macro.resolveGlobalName declName.getId |
       Macro.throwError "expected non-overloaded constant name"
-    let aliasName := aliasName?.getD (Syntax.mkStrLit declName.getId.toString)
+    let aliasName := match aliasName? with
+      | some n => quote (Name.mkSimple n.getString)
+      | none => quote declName.getId
     `(do Parser.registerAlias $aliasName ``$declName $declName $(info?.getD (Unhygienic.run `({}))) (kind? := some $(kind?.getD (quote fullDeclName)))
          PrettyPrinter.Formatter.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `formatter))
          PrettyPrinter.Parenthesizer.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `parenthesizer)))

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -906,6 +906,7 @@ where
   projInfo : DelabM (Name × Nat × Bool) := do
     let .app fn _ ← getExpr | failure
     let .const c@(.str _ field) _ := fn.getAppFn | failure
+    let field := Name.mkSimple field
     let env ← getEnv
     let some info := env.getProjectionFnInfo? c | failure
     -- Don't delaborate for classes since the instance parameter is implicit.

src/Lean/Server/Completion.lean

@@ -250,7 +250,7 @@ private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName :
   else if let (.str p₁ s₁, .str p₂ s₂) := (id, declName) then
     if p₁ == p₂ then
       -- If the namespaces agree, fuzzy-match on the trailing part
-      return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (s₂, ·)
+      return fuzzyMatchScoreWithThreshold? s₁ s₂ |>.map (.mkSimple s₂, ·)
     else if p₁.isAnonymous then
       -- If `id` is namespace-less, also fuzzy-match declaration names in arbitrary namespaces
       -- (but don't match the namespace itself).
@@ -383,14 +383,14 @@ private def idCompletionCore
   let addAlias (alias : Name) (declNames : List Name) (score : Float) : M Unit := do
     declNames.forM fun declName => do
       if allowCompletion eligibleHeaderDecls env declName then
-        addUnresolvedCompletionItemForDecl alias.getString! declName score
+        addUnresolvedCompletionItemForDecl (.mkSimple alias.getString!) declName score
   -- search explicitly open `ids`
   for openDecl in ctx.openDecls do
     match openDecl with
     | OpenDecl.explicit openedId resolvedId =>
       if allowCompletion eligibleHeaderDecls env resolvedId then
         if let some score := matchAtomic id openedId then
-          addUnresolvedCompletionItemForDecl openedId.getString! resolvedId score
+          addUnresolvedCompletionItemForDecl (.mkSimple openedId.getString!) resolvedId score
     | OpenDecl.simple ns _      =>
       getAliasState env |>.forM fun alias declNames => do
         if let some score := matchAlias ns alias then
@@ -543,7 +543,7 @@ private def dotCompletion
       if ! (← isDotCompletionMethod typeName c) then
         return
       let completionKind ← getCompletionKindForDecl c
-      addUnresolvedCompletionItem c.name.getString! (.const c.name) (kind := completionKind) 1
+      addUnresolvedCompletionItem (.mkSimple c.name.getString!) (.const c.name) (kind := completionKind) 1
 
 private def dotIdCompletion
     (params        : CompletionParams)
@@ -580,7 +580,7 @@ private def dotIdCompletion
       let completionKind ← getCompletionKindForDecl c
       if id.isAnonymous then
         -- We're completing a lone dot => offer all decls of the type
-        addUnresolvedCompletionItem c.name.getString! (.const c.name) completionKind 1
+        addUnresolvedCompletionItem (.mkSimple c.name.getString!) (.const c.name) completionKind 1
         return
 
       let some (label, score) ← matchDecl? typeName id (danglingDot := false) declName | pure ()

src/Lean/Server/Rpc/Deriving.lean

@@ -70,7 +70,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr
     let ctorTy ← instantiateForall (← getConstInfoCtor ctorName).type params
     forallTelescopeReducing ctorTy fun argVars _ => do
     let .str _ ctor := ctorName | throwError m!"constructor name not a string: {ctorName}"
-    let ctorId := mkIdent ctor
+    let ctorId := mkIdent (.mkSimple ctor)
 
     -- create the constructor
     let fieldStxs ← argVars.mapM fun arg => do

src/Lean/Widget/Diff.lean

@@ -206,7 +206,7 @@ def diffHypothesesBundle (useAfter : Bool) (ctx₀  : LocalContext) (h₁ : Inte
      this indicates that something like `rewrite at` has hit it. -/
   for (ppName, fvid) in Array.zip h₁.names h₁.fvarIds do
     if !(ctx₀.contains fvid) then
-      if let some decl₀ := ctx₀.findFromUserName? ppName then
+      if let some decl₀ := ctx₀.findFromUserName? (.mkSimple ppName) then
         -- on ctx₀ there is an fvar with the same name as this one.
         let t₀ := decl₀.type
         return ← withTypeDiff t₀ h₁

src/lake/Lake/CLI/Main.lean

@@ -190,12 +190,12 @@ def verifyInstall (opts : LakeOptions) : ExceptT CliError MainM PUnit := do
 def parseScriptSpec (ws : Workspace) (spec : String) : Except CliError Script :=
   match spec.splitOn "/" with
   | [scriptName] =>
-    match ws.findScript? scriptName with
+    match ws.findScript? scriptName.toName with
     | some script => return script
     | none => throw <| CliError.unknownScript spec
   | [pkg, scriptName] => do
     let pkg ← parsePackageSpec ws pkg
-    match pkg.scripts.find? scriptName with
+    match pkg.scripts.find? scriptName.toName with
     | some script => return script
     | none => throw <| CliError.unknownScript spec
   | _ => throw <| CliError.invalidScriptSpec spec

src/lake/Lake/Load/Materialize.lean

@@ -29,7 +29,7 @@ def updateGitPkg (name : String) (repo : GitRepo) (rev? : Option String) : LogIO
     repo.checkoutDetach rev
 
 /-- Clone the Git package as `repo`. -/
-def cloneGitPkg (name : Name) (repo : GitRepo)
+def cloneGitPkg (name : String) (repo : GitRepo)
 (url : String) (rev? : Option String) : LogIO PUnit := do
   logInfo s!"{name}: cloning {url} to '{repo.dir}'"
   repo.clone url

src/lake/tests/globs/lakefile.lean

@@ -10,4 +10,4 @@ lean_lib TBA where
 
 @[default_target]
 lean_lib Test where
-  globs := #[.submodules "Test"]
+  globs := #[.submodules `Test]

stage0/src/stdlib_flags.h

@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);

tests/bench/inundation/lakefile.lean

@@ -9,7 +9,7 @@ package inundation where
 @[default_target]
 lean_lib Inundation where
   srcDir := "test"
-  roots := #[test]
+  roots := #[.mkSimple test]
 
 script nop :=
   return 0

tests/lean/interactive/run.lean

@@ -63,7 +63,7 @@ def word : Parsec String :=
 def ident : Parsec Name := do
   let head ← word
   let xs ← Parsec.many1 (Parsec.pchar '.' *> word)
-  return xs.foldl Name.mkStr $ head
+  return xs.foldl .str $ .mkSimple head
 
 partial def main (args : List String) : IO Unit := do
   let uri := s!"file:///{args.head!}"