feat: improve inductive type parameter error messages (#8338)

This PR improves the error messages displayed in `inductive`
declarations when type parameters are invalid or absent.

Closes #2195 by improving the relevant error message.

src/Lean/Elab/Inductive.lean

@@ -138,7 +138,7 @@ private def reorderCtorArgs (ctorType : Expr) : MetaM Expr := do
     else
       let r ← mkForallFVars (bsPrefix ++ as) type
       /- `r` already contains the resulting type.
-         To be able to produce more better error messages, we copy the first `bsPrefix.size` binder names from `C` to `r`.
+         To be able to produce better error messages, we copy the first `bsPrefix.size` binder names from `C` to `r`.
          This is important when some of constructor parameters were inferred using the auto-bound implicit feature.
          For example, in the following declaration.
          ```
@@ -178,7 +178,8 @@ private def elabCtors (indFVars : Array Expr) (params : Array Expr) (r : ElabHea
           match ctorView.type? with
           | none          =>
             if indFamily then
-              throwError "constructor resulting type must be specified in inductive family declaration"
+              throwError "Missing resulting type for constructor '{ctorView.declName}': \
+                Its resulting type must be specified because it is part of an inductive family declaration"
             return mkAppN indFVar params
           | some ctorType =>
             let type ← Term.elabType ctorType
@@ -188,9 +189,9 @@ private def elabCtors (indFVars : Array Expr) (params : Array Expr) (r : ElabHea
             let type ← checkParamOccs type
             forallTelescopeReducing type fun _ resultingType => do
               unless resultingType.getAppFn == indFVar do
-                throwError "unexpected constructor resulting type{indentExpr resultingType}"
+                throwUnexpectedResultingTypeMismatch resultingType indFVar ctorView.declName ctorType
               unless (← isType resultingType) do
-                throwError "unexpected constructor resulting type, type expected{indentExpr resultingType}"
+                throwUnexpectedResultingTypeNotType resultingType ctorView.declName ctorType
             return type
         let type ← elabCtorType
         Term.synthesizeSyntheticMVarsNoPostponing
@@ -229,23 +230,62 @@ private def elabCtors (indFVars : Array Expr) (params : Array Expr) (r : ElabHea
         trace[Elab.inductive] "{ctorView.declName} : {type}"
         return { name := ctorView.declName, type }
 where
+  /--
+  Ensures that the arguments to recursive occurrences of the type family being defined match the
+  parameters from the inductive definition.
+  -/
   checkParamOccs (ctorType : Expr) : MetaM Expr :=
-    let visit (e : Expr) : MetaM TransformStep := do
+    let visit (e : Expr) : StateT (List Expr) MetaM TransformStep := do
       let f := e.getAppFn
       if indFVars.contains f then
         let mut args := e.getAppArgs
-        unless args.size ≥ params.size do
-          throwError "unexpected inductive type occurrence{indentExpr e}"
-        for h : i in [:params.size] do
-          let param := params[i]
+        -- Prefer throwing an "argument mismatch" error rather than a "missing parameter" one
+        for i in [:min args.size params.size] do
+          let param := params[i]!
           let arg := args[i]!
           unless (← isDefEq param arg) do
-            throwError "inductive datatype parameter mismatch{indentExpr arg}\nexpected{indentExpr param}"
+            let (arg, param) ← addPPExplicitToExposeDiff arg param
+            let msg := m!"Mismatched inductive type parameter in{indentExpr e}\nThe provided argument\
+              {indentExpr arg}\nis not definitionally equal to the expected parameter{indentExpr param}"
+            let noteMsg := m!"The value of parameter '{param}' must be fixed throughout the inductive \
+              declaration. Consider making this parameter an index if it must vary."
+            throwError msg ++ .note noteMsg
           args := args.set! i param
+        unless args.size ≥ params.size do
+          let expected := mkAppN f params
+          let containingExprMsg := (← get).head?.map toMessageData |>.getD m!"<missing>"
+          let msg :=
+            m!"Missing parameter(s) in occurrence of inductive type: In the expression{indentD containingExprMsg}\n\
+               found{indentExpr e}\nbut expected all parameters to be specified:{indentExpr expected}"
+          let noteMsg :=
+            m!"All occurrences of an inductive type in the types of its constructors must specify its \
+              fixed parameters. Only indices can be omitted in a partial application of the type constructor."
+          throwError msg ++ .note noteMsg
         return TransformStep.done (mkAppN f args)
       else
+        modify fun es => e :: es
         return .continue
-    transform ctorType (pre := visit)
+    let popContainingExpr (e : Expr) : StateT (List Expr) MetaM TransformStep := do
+      modify fun es => es.drop 1
+      return .done e
+    transform ctorType (pre := visit) (post := popContainingExpr) |>.run' [ctorType]
+
+  throwUnexpectedResultingTypeMismatch (resultingType indFVar : Expr) (declName : Name) (ctorType : Syntax) := do
+    let lazyAppMsg := MessageData.ofLazyM do
+      if let some fvarId := indFVar.fvarId? then
+        if let some decl := (← getLCtx).find? fvarId then
+          if (← whnfD decl.type).isForall then
+            return m!" an application of"
+      return m!""
+    throwErrorAt ctorType "Unexpected resulting type for constructor '{declName}': \
+      Expected{lazyAppMsg}{indentExpr indFVar}\nbut found{indentExpr resultingType}"
+
+  throwUnexpectedResultingTypeNotType (resultingType : Expr) (declName : Name) (ctorType : Syntax) := do
+    let lazyMsg := MessageData.ofLazyM do
+      let resultingTypeType ← inferType resultingType
+      return indentExpr resultingTypeType
+    throwErrorAt ctorType "Unexpected resulting type for constructor '{declName}': \
+      Expected a type, but found{indentExpr resultingType}\nof type{lazyMsg}"
 
 @[builtin_inductive_elab Lean.Parser.Command.inductive, builtin_inductive_elab Lean.Parser.Command.classInductive]
 def elabInductiveCommand : InductiveElabDescr where

src/Lean/Elab/MutualInductive.lean

@@ -219,7 +219,7 @@ private def checkUnsafe (rs : Array PreElabHeaderResult) : TermElabM Unit := do
   let isUnsafe := rs[0]!.view.modifiers.isUnsafe
   for r in rs do
     unless r.view.modifiers.isUnsafe == isUnsafe do
-      throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
+      throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in mutually inductive datatypes"
 
 private def checkClass (rs : Array PreElabHeaderResult) : TermElabM Unit := do
   if rs.size > 1 then

tests/lean/inductive1.lean.expected.out

@@ -20,10 +20,12 @@ inductive1.lean:80:0-80:27: error: invalid use of 'partial' in inductive declara
 inductive1.lean:81:0-81:33: error: invalid use of 'noncomputable' in inductive declaration
 inductive1.lean:82:2-82:8: error: declaration is not a definition 'T1''
 inductive1.lean:85:0-85:17: error: invalid 'private' constructor in a 'private' inductive datatype
-inductive1.lean:93:7-93:26: error: invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes
-inductive1.lean:100:0-100:4: error: constructor resulting type must be specified in inductive family declaration
+inductive1.lean:93:7-93:26: error: invalid inductive type, cannot mix unsafe and safe declarations in mutually inductive datatypes
+inductive1.lean:100:0-100:4: error: Missing resulting type for constructor 'T1.z2': Its resulting type must be specified because it is part of an inductive family declaration
 inductive1.lean:105:7-105:9: error: type expected, got
   (T1 : Nat → Type)
-inductive1.lean:108:0-108:10: error: unexpected constructor resulting type
+inductive1.lean:108:7-108:10: error: Unexpected resulting type for constructor 'T1.z1': Expected an application of
+  T1
+but found
   Nat
 inductive1.lean:118:7-118:11: error: unknown identifier 'cons'

tests/lean/run/inductiveParamMismatchError.lean

@@ -0,0 +1,151 @@
+/-! # Inductive parameter mismatch error messages
+
+Tests that appropriate error messages are shown when the fixed parameters of an inductive type
+constructor are omitted or incorrect in an `inductive` declaration.
+
+A previous version of one such error message was noted to be confusing in #2195:
+https://github.com/leanprover/lean4/issues/2195
+-/
+
+/-! ## Example from Issue #2195 -/
+
+inductive Desc where
+  | intro
+    (name: String)
+    (hash: UInt64)
+    (params: List Desc)
+  : Desc
+  deriving Repr
+
+def hash_with_name (_name: String) (_params: List Desc): UInt64 := 0 -- mock hash function
+
+def Desc.intro_func (name: String) (params: List Desc): Desc :=
+  Desc.intro
+    name
+    (hash_with_name name params)
+    params
+
+inductive Forall {α : Type u} (p : α → Prop) : List α → Prop
+  | nil  : Forall p ([] : List α)
+  | cons : ∀ {x xs}, p x → Forall p xs → Forall p (x :: xs)
+
+/--
+error: Missing parameter(s) in occurrence of inductive type: In the expression
+  Forall IsSmart params
+found
+  IsSmart
+but expected all parameters to be specified:
+  IsSmart d
+
+Note: All occurrences of an inductive type in the types of its constructors must specify its fixed parameters. Only indices can be omitted in a partial application of the type constructor.
+-/
+#guard_msgs in
+inductive IsSmart (d: Desc): Prop
+  | isSmart: ∀
+    (name: String)
+    (params: List Desc)
+    (hash: UInt64)
+    (reader: Bool),
+    d = Desc.intro name hash params
+    → hash = hash_with_name name params
+    → Forall IsSmart params
+    → IsSmart d
+
+
+/-! ## "Missing parameter" error -/
+
+abbrev NatOf (F : Type → Type) : Type := F Nat
+/--
+error: Missing parameter(s) in occurrence of inductive type: In the expression
+  NatOf T
+found
+  T
+but expected all parameters to be specified:
+  T α
+
+Note: All occurrences of an inductive type in the types of its constructors must specify its fixed parameters. Only indices can be omitted in a partial application of the type constructor.
+-/
+#guard_msgs in
+inductive T (α : Type) where
+  | mk : NatOf T → T α
+
+inductive T_OK (α : Type) : Type → Type where
+  | mk : NatOf (T_OK α) → T_OK α Nat
+
+/--
+error: Missing parameter(s) in occurrence of inductive type: In the expression
+  NatOf (T₂ α)
+found
+  T₂ α
+but expected all parameters to be specified:
+  T₂ α β
+
+Note: All occurrences of an inductive type in the types of its constructors must specify its fixed parameters. Only indices can be omitted in a partial application of the type constructor.
+-/
+#guard_msgs in
+inductive T₂ (α β : Type) : Type
+  | mk : NatOf (T₂ α) → T₂ α β
+
+abbrev InList : List (Type → Type) → Type :=
+  fun _ => Nat
+/--
+error: Missing parameter(s) in occurrence of inductive type: In the expression
+  [Foo]
+found
+  Foo
+but expected all parameters to be specified:
+  Foo α
+
+Note: All occurrences of an inductive type in the types of its constructors must specify its fixed parameters. Only indices can be omitted in a partial application of the type constructor.
+-/
+#guard_msgs in
+inductive Foo (α : Type) : Type
+  | mk : InList [Foo] → Foo α
+
+
+/-! ## "Mismatched parameter" error -/
+
+/--
+error: Mismatched inductive type parameter in
+  BadIdx α 0
+The provided argument
+  0
+is not definitionally equal to the expected parameter
+  n
+
+Note: The value of parameter 'n' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
+-/
+#guard_msgs in
+inductive BadIdx (α : Type) (n : Nat) : Type
+  | mk : BadIdx α 0
+
+/--
+error: Mismatched inductive type parameter in
+  BadIdx' α 0 k
+The provided argument
+  0
+is not definitionally equal to the expected parameter
+  n
+
+Note: The value of parameter 'n' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
+-/
+#guard_msgs in
+inductive BadIdx' (α : Type) (n k : Nat) : Type
+  | mk : BadIdx' α 0 k
+
+
+/-! ## "Mismatched parameter" preempts "missing parameter" -/
+
+/--
+error: Mismatched inductive type parameter in
+  Bar Nat
+The provided argument
+  Nat
+is not definitionally equal to the expected parameter
+  α
+
+Note: The value of parameter 'α' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
+-/
+#guard_msgs in
+inductive Bar (α β : Type) : Type
+  | mk : NatOf (Bar Nat) → Bar α β