Add warning about ordinals

src/Lean/Elab/SyntheticMVars.lean

@@ -208,6 +208,98 @@ private def synthesizeUsingDefault : TermElabM Bool := do
       return true
   return false
 
+/--
+Translate zero-based indexes (0, 1, 2, ...) to ordinals ("first", "second",
+"third", ...). Not appropriate for numbers that could conceivably be larger
+than 19 in real examples.
+-/
+private def toOrdinalString : Nat -> String
+  | 0 => "first"
+  | 1 => "second"
+  | 2 => "third"
+  | 3 => "fourth"
+  | 4 => "fifth"
+  | n => s!"{n+1}th"
+
+/-- Make an oxford-comma-separated list of strings. -/
+private def toOxford : List String -> String
+  | [] => ""
+  | [a] => a
+  | [a, b] => a ++ " and " ++ b
+  | [a, b, c] => a ++ ", " ++ b  ++ ", and " ++ c
+  | a :: as => a ++ ", " ++ toOxford as
+
+/- Give alternative forms of a string if the `count` is 1 or not. -/
+private def _root_.Nat.plural (count : Nat) (singular : String) (plural : String) :=
+  if count = 1 then
+    singular
+  else
+    plural
+
+def explainStuckTypeclassProblem (typeclassProblem : Expr) : TermElabM (Option MessageData) := do
+
+  -- Gather the type arguments and locate the root of the typeclass
+  let mut args := []
+  let mut ty := typeclassProblem
+  while ty.isApp do
+    match ty with
+    | .app fn arg =>
+      ty := fn
+      args := arg :: args
+    | _ => return .none -- Precluded by loop guard
+
+  -- Find the typeclass's type constructor (e.g. `HAdd`) and look up its classifying type
+  let .const name _ := ty
+    | return .none -- Typeclass problem has unexpected structure; fall back to default error
+  let .some defn := (← getEnv).findConstVal? name
+    | return .none
+  let mut kind := defn.type
+
+  /-
+  Simultaneously traverse the typeclass arguments (e.g. `#[_?, Nat, _?]` if
+  our stuck typeclass problem is `HAdd _?, Nat, _?`) and the classifier (e.g.
+  `Type → Type → outParam Type → Type`) and come up with the input positions
+  that are stuck (e.g. `[0]` if only the first type argument is stuck).
+  -/
+  let mut ord := 0
+  let mut stuckArguments := #[]
+  let mut simpleMVars := true
+  for arg in args do
+    match kind with
+    | .forallE _ argType rest _ =>
+      kind := rest
+      if !(argType.isOutParam || argType.isSemiOutParam) then
+        let arg ← instantiateExprMVars arg
+        if let .mvar _ := arg then
+          stuckArguments := stuckArguments.push ord
+        else if (arg.collectMVars {}).result.size > 0 then
+          stuckArguments := stuckArguments.push ord
+          simpleMVars := false
+    | _ => return .none -- Unexpected type structure; fall back to default error
+    ord := ord + 1
+
+  let .sort _ := kind
+    | return .none -- Unexpected type structure; fall back to default error
+  let nStuck := stuckArguments.size
+  if nStuck = 0 then
+    return .none -- This is not a simple inputs-have-metavariables issue
+
+  -- Formulate error message
+  let containMVars :=
+    if simpleMVars then
+      nStuck.plural "is a metavariable" "are metavariables"
+    else
+      nStuck.plural "contains metavariables" "contain metavariables"
+
+  let theTypeArguments :=
+    if args.length = 1 then
+      "the type argument"
+    else
+      s!"the {toOxford (stuckArguments.toList.map toOrdinalString)} type {nStuck.plural "argument" "arguments"}"
+
+  return .some (.note m!"Lean will not try to resolve this typeclass instance problem because {theTypeArguments} to `{.ofConstName name}` {containMVars}. {nStuck.plural "This argument" "These arguments"} must be fully determined before Lean will try to resolve the typeclass."
+    ++ .hint' m!"Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `{MessageData.ofConstName ``Nat}`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.")
+
 /--
 We use this method to report typeclass (and coercion) resolution problems that are "stuck".
 That is, there is nothing else to do, and we don't have enough information to synthesize them using TC resolution.
@@ -222,7 +314,9 @@ def reportStuckSyntheticMVar (mvarId : MVarId) (ignoreStuckTC := false) : TermEl
         mvarId.withContext do
           let mvarDecl ← getMVarDecl mvarId
           unless (← MonadLog.hasErrors) do
-            throwError "typeclass instance problem is stuck, it is often due to metavariables{indentExpr mvarDecl.type}{extraErrorMsg}"
+            let .some note ← explainStuckTypeclassProblem mvarDecl.type
+              | throwError "typeclass instance problem is stuck, it is often due to metavariables{indentExpr mvarDecl.type}{extraErrorMsg}"
+            throwError m!"typeclass instance problem is stuck{indentExpr mvarDecl.type}{note}{extraErrorMsg}"
     | .coe header expectedType e f? mkErrorMsg? =>
       mvarId.withContext do
         if let some mkErrorMsg := mkErrorMsg? then

tests/lean/353.lean.expected.out

@@ -1,2 +1,7 @@
-353.lean:13:26-13:50: error: typeclass instance problem is stuck, it is often due to metavariables
+353.lean:13:26-13:50: error: typeclass instance problem is stuck
   Arr.{?u, ?u + 1} (@?m a₁ a₂) (Sort ?u)
+
+Note: Lean will not try to resolve this typeclass instance problem because the first type argument to `Arr.{u1,
+  u2}` contains metavariables. This argument must be fully determined before Lean will try to resolve the typeclass.
+
+Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.

tests/lean/defaultInstance.lean.expected.out

@@ -2,5 +2,9 @@ defaultInstance.lean:20:20-20:23: error: failed to synthesize
   Foo Bool (?m x)
 
 Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
-defaultInstance.lean:22:35-22:38: error: typeclass instance problem is stuck, it is often due to metavariables
+defaultInstance.lean:22:35-22:38: error: typeclass instance problem is stuck
   Foo Bool (?m x)
+
+Note: Lean will not try to resolve this typeclass instance problem because the second type argument to `Foo` contains metavariables. This argument must be fully determined before Lean will try to resolve the typeclass.
+
+Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.

tests/lean/run/due_to_metavariables.lean

@@ -0,0 +1,72 @@
+/--
+error: typeclass instance problem is stuck
+  HMul ?m.9 ?m.9 String
+
+Note: Lean will not try to resolve this typeclass instance problem because the first and second type arguments to `HMul` are metavariables. These arguments must be fully determined before Lean will try to resolve the typeclass.
+
+Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
+-/
+#guard_msgs in
+def f1 x := (x * x : String)
+
+/--
+error: typeclass instance problem is stuck
+  HMul String ?m.8 (?m.3 x)
+
+Note: Lean will not try to resolve this typeclass instance problem because the second type argument to `HMul` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.
+
+Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
+-/
+#guard_msgs in
+def f2 x := "huh" * x
+
+/--
+error: typeclass instance problem is stuck
+  HMul (Option ?m.4) ?m.9 (?m.3 x)
+
+Note: Lean will not try to resolve this typeclass instance problem because the first and second type arguments to `HMul` contain metavariables. These arguments must be fully determined before Lean will try to resolve the typeclass.
+
+Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
+-/
+#guard_msgs in
+def f3 x := Option.none * x
+
+/--
+error: typeclass instance problem is stuck
+  LT ?m.6
+
+Note: Lean will not try to resolve this typeclass instance problem because the type argument to `LT` is a metavariable. This argument must be fully determined before Lean will try to resolve the typeclass.
+
+Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
+-/
+#guard_msgs in
+def f4 x := x < x
+
+/--
+error: typeclass instance problem is stuck
+  LT (Option ?m.4)
+
+Note: Lean will not try to resolve this typeclass instance problem because the type argument to `LT` contains metavariables. This argument must be fully determined before Lean will try to resolve the typeclass.
+
+Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
+-/
+#guard_msgs in
+def f4 x := Option.none < Option.none
+
+class Many (a b c d e: Type) where
+instance : Many Nat Nat Nat Nat Nat where
+def test [Many a b c d e] (_x1 : a) (_x2 : b) (_x3 : c) (_x4 : d) (_x5 : e) :=
+  3
+
+/--
+error: typeclass instance problem is stuck
+  Many ?m.1 Nat ?m.1 ?m.1 ?m.1
+
+Note: Lean will not try to resolve this typeclass instance problem because the first, third, fourth, and fifth type arguments to `Many` are metavariables. These arguments must be fully determined before Lean will try to resolve the typeclass.
+
+Hint: Adding type annotations and supplying implicit arguments to functions can give Lean more information for typeclass resolution. For example, if you have a variable `x` that you intend to be a `Nat`, but Lean reports it as having an unresolved type like `?m`, replacing `x` with `(x : Nat)` can get typeclass resolution un-stuck.
+-/
+#guard_msgs in
+
+
+def f x := test x 3 x x x