chore: fix apply? error reporting when out of heartbeats

This PR fixes a bug where structural recursion did not work when indices
of the recursive argument appeared as function parameters in a different
order than in the argument's type's definition.

Fixes #6015.

src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean

@@ -243,7 +243,7 @@ def tryAllArgs (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
     recArgInfoss := recArgInfoss.push recArgInfos
   -- Put non-indices first
   recArgInfoss := recArgInfoss.map nonIndicesFirst
-  trace[Elab.definition.structural] "recArgInfoss: {recArgInfoss.map (·.map (·.recArgPos))}"
+  trace[Elab.definition.structural] "recArgInfos:{indentD (.joinSep (recArgInfoss.flatten.toList.map (repr ·)) Format.line)}"
   -- Inductive groups to consider
   let groups ← inductiveGroups recArgInfoss.flatten
   trace[Elab.definition.structural] "inductive groups: {groups}"

src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean

@@ -27,7 +27,7 @@ constituents.
 structure IndGroupInfo where
   all       : Array Name
   numNested : Nat
-deriving BEq, Inhabited
+deriving BEq, Inhabited, Repr
 
 def IndGroupInfo.ofInductiveVal (indInfo : InductiveVal) : IndGroupInfo where
   all       := indInfo.all.toArray
@@ -56,7 +56,7 @@ mutual structural recursion on such incompatible types.
 structure IndGroupInst extends IndGroupInfo where
   levels    : List Level
   params    : Array Expr
-deriving Inhabited
+deriving Inhabited, Repr
 
 def IndGroupInst.toMessageData (igi : IndGroupInst) : MessageData :=
   mkAppN (.const igi.all[0]! igi.levels) igi.params

src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean

@@ -23,9 +23,9 @@ structure RecArgInfo where
   fnName       : Name
   /-- the fixed prefix of arguments of the function we are trying to justify termination using structural recursion. -/
   numFixed     : Nat
-  /-- position of the argument (counted including fixed prefix) we are recursing on -/
+  /-- position (counted including fixed prefix) of the argument we are recursing on -/
   recArgPos    : Nat
-  /-- position of the indices (counted including fixed prefix) of the inductive datatype indices we are recursing on -/
+  /-- position (counted including fixed prefix) of the indices of the inductive datatype we are recursing on -/
   indicesPos   : Array Nat
   /-- The inductive group (with parameters) of the argument's type -/
   indGroupInst : IndGroupInst
@@ -34,20 +34,23 @@ structure RecArgInfo where
   If `< indAll.all`, a normal data type, else an auxiliary data type due to nested recursion
   -/
   indIdx       : Nat
-deriving Inhabited
+deriving Inhabited, Repr
 
 /--
 If `xs` are the parameters of the functions (excluding fixed prefix), partitions them
 into indices and major arguments, and other parameters.
 -/
 def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array Expr × Array Expr) := Id.run do
+  -- First indices and major arg, using the order they appear in `info.indicesPos`
   let mut indexMajorArgs := #[]
+  let indexMajorPos := info.indicesPos.push info.recArgPos
+  for j in indexMajorPos do
+    assert! info.numFixed ≤ j && j - info.numFixed < xs.size
+    indexMajorArgs := indexMajorArgs.push xs[j - info.numFixed]!
+  -- Then the other arguments, in the order they appear in `xs`
   let mut otherArgs := #[]
   for h : i in [:xs.size] do
-    let j := i + info.numFixed
-    if j = info.recArgPos || info.indicesPos.contains j then
-      indexMajorArgs := indexMajorArgs.push xs[i]
-    else
+    unless indexMajorPos.contains (i + info.numFixed) do
       otherArgs := otherArgs.push xs[i]
   return (indexMajorArgs, otherArgs)
 

src/Lean/Elab/Syntax.lean

@@ -236,8 +236,9 @@ where
     -- Pretty-printing instructions shouldn't affect validity
     let s := s.trim
     !s.isEmpty &&
-    (s.front != '\'' || s == "''") &&
+    (s.front != '\'' || "''".isPrefixOf s) &&
     s.front != '\"' &&
+    !(isIdBeginEscape s.front) &&
     !(s.front == '`' && (s.endPos == ⟨1⟩ || isIdFirst (s.get ⟨1⟩) || isIdBeginEscape (s.get ⟨1⟩))) &&
     !s.front.isDigit &&
     !(s.any Char.isWhitespace)

src/Lean/Elab/Tactic/LibrarySearch.lean

@@ -40,7 +40,7 @@ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireCl
     | some suggestions =>
       if requireClose then throwError
         "`exact?` could not close the goal. Try `apply?` to see partial suggestions."
-      reportOutOfHeartbeats `library_search ref
+      reportOutOfHeartbeats `apply? ref
       for (_, suggestionMCtx) in suggestions do
         withMCtx suggestionMCtx do
           addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)

src/Lean/Meta/ExprDefEq.lean

@@ -939,6 +939,29 @@ def check (hasCtxLocals : Bool) (mctx : MetavarContext) (lctx : LocalContext) (m
 
 end CheckAssignmentQuick
 
+/--
+Auxiliary function used at `typeOccursCheckImp`.
+Given `type`, it tries to eliminate "dependencies". For example, suppose we are trying to
+perform the assignment `?m := f (?n a b)` where
+```
+?n : let k := g ?m; A -> h k ?m -> C
+```
+If we just perform occurs check `?m` at the type of `?n`, we get a failure, but
+we claim these occurrences are ok because the type `?n a b : C`.
+In the example above, `typeOccursCheckImp` invokes this function with `n := 2`.
+Note that we avoid using `whnf` and `inferType` at `typeOccursCheckImp` to minimize the
+performance impact of this extra check.
+
+See test `typeOccursCheckIssue.lean` for an example where this refinement is needed.
+The test is derived from a Mathlib file.
+-/
+private partial def skipAtMostNumBinders (type : Expr) (n : Nat) : Expr :=
+  match type, n with
+  | .forallE _ _ b _, n+1 => skipAtMostNumBinders b n
+  | .mdata _ b,       n   => skipAtMostNumBinders b n
+  | .letE _ _ v b _,  n   => skipAtMostNumBinders (b.instantiate1 v) n
+  | type,             _   => type
+
 /-- `typeOccursCheck` implementation using unsafe (i.e., pointer equality) features. -/
 private unsafe def typeOccursCheckImp (mctx : MetavarContext) (mvarId : MVarId) (v : Expr) : Bool :=
   if v.hasExprMVar then
@@ -959,36 +982,9 @@ where
     -- this function assumes all assigned metavariables have already been
     -- instantiated.
     go.run' mctx
-  /--
-    Given `type`, it tries to eliminate "dependencies". For example, suppose we are trying to
-    perform the assignment `?m := f (?n a b)` where
-    ```
-    ?n : let k := g ?m; A -> h k ?m -> C
-    ```
-    If we just perform occurs check `?m` at the type of `?n`, we get a failure, but
-    we claim these occurrences are ok because the type `?n a b : C`.
-    In the example above, `typeOccursCheckImp` invokes this function with `n := 2`.
-    Note that we avoid using `whnf` and `inferType` at `typeOccursCheckImp` to minimize the
-    performance impact of this extra check.
-
-    See test `typeOccursCheckIssue.lean` for an example where this refinement is needed.
-    The test is derived from a Mathlib file.
-
-    Remark: note that we perform `occursCheck` at the type and value of a let-declaration.
-    See test `typeOccursCheckIssue2.lean`.
-    -/
-  skipAtMostNumBinders? (type : Expr) (n : Nat) : Option Expr :=
-    match type, n with
-    | .forallE _ _ b _, n+1 => skipAtMostNumBinders? b n
-    | .mdata _ b,       n   => skipAtMostNumBinders? b n
-    | .letE _ t v b _,  n   => if occursCheck t && occursCheck v then skipAtMostNumBinders? b n else none
-    | type,             _   => some type
   visitMVar (mvarId' : MVarId) (numArgs : Nat := 0) : Bool :=
     if let some mvarDecl := mctx.findDecl? mvarId' then
-      if let some b := skipAtMostNumBinders? mvarDecl.type numArgs then
-        occursCheck b
-      else
-        false
+      occursCheck (skipAtMostNumBinders mvarDecl.type numArgs)
     else
       false
   visitApp (e : Expr) : StateM (PtrSet Expr) Bool :=

tests/lean/6013.lean

@@ -1,3 +0,0 @@
-def test (a : String) : String :=
-  let x : String → String := _
-  have : x = 10 := by rfl

tests/lean/6013.lean.expected.out

@@ -1,5 +0,0 @@
-6013.lean:4:0: error: unexpected end of input
-6013.lean:2:29-2:30: error: don't know how to synthesize placeholder
-context:
-a : String
-⊢ String → String

tests/lean/run/atomValidation.lean

@@ -0,0 +1,138 @@
+import Lean.Elab.Command
+import Lean.Elab.Syntax
+
+open Lean.Elab.Term.toParserDescr (isValidAtom)
+open Lean Elab Command
+
+/-!
+Test various classes of atoms that should be allowed or not.
+-/
+
+def test (expected : Bool) (strings : List String) : CommandElabM Unit := Id.run do
+  let mut wrong : List String := []
+  for s in strings do
+    if isValidAtom s != expected then
+      wrong := s :: wrong
+    if isValidAtom (" " ++ s) != expected then
+      wrong := s!"{s} (with leading whitespace)" :: wrong
+    if isValidAtom (s ++ " ") != expected then
+      wrong := s!"{s} (with trailing whitespace)" :: wrong
+    if isValidAtom (" " ++ s ++ " ") != expected then
+      wrong := s!"{s} (with leading and trailing whitespace)" :: wrong
+
+  if wrong.isEmpty then
+    logInfo <| "All " ++ if expected then "accepted" else "rejected"
+  else
+    logError <|
+      s!"The following atoms should be {if expected then "" else "in"}valid but are not:\n" ++
+      String.join (wrong.reverse.map (s! " * {·}\n"))
+
+
+syntax "#test_valid" term : command
+syntax "#test_invalid" term : command
+
+macro_rules
+  | `(#test_valid%$tok $t) => `(#eval%$tok test true $t)
+  | `(#test_invalid%$tok $t) => `(#eval%$tok test false $t)
+
+
+/-!
+# No Empty Atoms
+-/
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid [""]
+
+
+/-!
+# Preventing Character Literal Confusion
+
+Atoms are required to be suitably unlike character literals. This means that if they start with a
+single quote, the next character must also be a single quote.
+
+Two single quotes (and variations on it) has long-term usage as an infix operator in Mathlib.
+-/
+
+/-- info: All accepted -/
+#guard_msgs in
+#test_valid ["if", "''", "''ᵁ", "if'", "x'y'z", "x''y"]
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid ["'x'", "'ᵁ", "'c", "'no'", "'"]
+
+
+/-!
+# No Internal Whitespace
+-/
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid ["open mixed", "open   mixed"]
+
+
+/-!
+# No Confusion with String Literals
+
+Internal double quotes are allowed.
+-/
+
+/-- info: All accepted -/
+#guard_msgs in
+#test_valid ["what\"string\"is_this?"]
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid ["\"","\"\"", "\"f\""]
+
+/-!
+# No Confusion with Escaped Identifiers
+
+This doesn't confuse the parser, but it may confuse a user if they can define an atom that can never
+be parsed.
+-/
+
+/-- info: All accepted -/
+#guard_msgs in
+#test_valid ["prefix«", "prefix«test", "prefix«test»", "prefix«test»foo"]
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid ["«", "«test", "«test»", "«test»foo"]
+
+
+/-!
+# No Confusion with Name Literals
+
+The first two characters of an atom may not be a valid start of a name literal
+-/
+
+/-- info: All accepted -/
+#guard_msgs in
+#test_valid ["``", "`!", "x`"]
+
+/-!
+The next set all begin with U0x2035, REVERSED PRIME, rather than back-tick, and are thus accepted.
+-/
+/-- info: All accepted -/
+#guard_msgs in
+#test_valid ["‵", "‵x", "‵«", "‵xyz", "‵«x.y", "‵«x.y.z»"]
+
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid ["`", "`x", "`«", "`xyz", "`«x.y", "`«x.y.z»"]
+
+
+/-!
+# No Leading Digits
+-/
+
+/-- info: All accepted -/
+#guard_msgs in
+#test_valid ["prefix5", "prefix22test", "prefix1test0", "prefix8test8foo"]
+
+/-- info: All rejected -/
+#guard_msgs in
+#test_invalid ["0", "1test", "0test3"]

tests/lean/run/issue6015.lean

@@ -0,0 +1,21 @@
+private axiom test_sorry : ∀ {α}, α
+
+inductive Tyₛ (l : List Unit): Type
+| U : Tyₛ l
+open Tyₛ
+
+inductive Varₚ (d : Unit): List Unit → Type
+| vz : Varₚ d [d']
+| vs : Varₚ d l → Varₚ d (Bₛ :: l)
+
+inductive Tmₛ {l : List Unit}: Tyₛ l → Unit → Type 1
+| arr   : (T : Type) → Tmₛ A d → Tmₛ A d
+| param : Varₚ d l → Tmₛ A d → Tmₛ (@U l) d
+
+def TmₛA {l : List Unit} {d : Unit} (nonIndex : Bool) {Aₛ : Tyₛ l} (t : Tmₛ Aₛ d): Type :=
+match t with
+  | .arr dom cd =>
+    let cd := TmₛA nonIndex cd
+    dom → cd
+  | _ => test_sorry
+termination_by structural t