diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 7fe52d329a..704e4aae7d 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -7,6 +7,7 @@ prelude import Lean.Util.FindMVar import Lean.Util.CollectFVars import Lean.Parser.Term +import Lean.Meta.Hint import Lean.Meta.KAbstract import Lean.Meta.Tactic.ElimInfo import Lean.Elab.Term @@ -1289,6 +1290,36 @@ private partial def findMethod? (structName fieldName : Name) : MetaM (Option (N private def throwInvalidFieldNotation (e eType : Expr) : TermElabM α := throwLValError e eType "Invalid field notation: Type is not of the form `C ...` where C is a constant" +/-- +If it seems that the user may be attempting to project out the `n`th element of a tuple, or that the +nesting behavior of n-ary products is otherwise relevant, generates a corresponding hint; otherwise, +produces an empty message. +-/ +private partial def mkTupleHint (eType : Expr) (idx : Nat) (ref : Syntax) : TermElabM MessageData := do + let arity := prodArity eType + if arity > 1 then + let numComps := arity + 1 + if idx ≤ numComps && ref.getHeadInfo matches .original .. then + let ordinalSuffix := match idx % 10 with + | 1 => "st" | 2 => "nd" | 3 => "rd" | _ => "th" + let mut projComps := List.replicate (idx - 1) "2" + if idx < numComps then projComps := projComps ++ ["1"] + let proj := ".".intercalate projComps + let sug := { suggestion := proj, span? := ref, + toCodeActionTitle? := some (s!"Change projection `{idx}` to `{·}`") } + MessageData.hint m!"n-tuples in Lean are actually nested pairs. To access the \ + {idx}{ordinalSuffix} component of this tuple, use the projection `.{proj}` instead:" #[sug] + else + return MessageData.hint' m!"n-tuples in Lean are actually nested pairs. For example, to access the \ + \"third\" component of `(a, b, c)`, write `(a, b, c).2.2` instead of `(a, b, c).3`." + else + return MessageData.nil +where + prodArity (type : Expr) := + match type.prod? with + | none => 0 + | some (_, p2) => prodArity p2 + 1 + private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do if eType.isForall then match lval with @@ -1312,7 +1343,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L | .fieldIdx _ i => (m!"projection", m!"projection `{i}`") throwError "Invalid {kind}: Type of{indentExpr e}\nis not known; cannot resolve {name}" match eType.getAppFn.constName?, lval with - | some structName, LVal.fieldIdx _ idx => + | some structName, LVal.fieldIdx ref idx => if idx == 0 then throwError "Invalid projection: Index must be greater than 0" let env ← getEnv @@ -1335,8 +1366,10 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L (m!"field", m!"the only valid index is 1") else (m!"fields", m!"it must be between 1 and {numFields}") + let tupleHint ← mkTupleHint eType idx ref throwError m!"Invalid projection: Index `{idx}` is invalid for this structure; {bounds}" ++ .note m!"The expression{inlineExpr e}has type{inlineExpr eType}which has only {numFields} {fields}" + ++ tupleHint | some structName, LVal.fieldName _ fieldName _ fullRef => let env ← getEnv if isStructure env structName then @@ -1385,7 +1418,7 @@ private partial def consumeImplicits (stx : Syntax) (e eType : Expr) (hasArgs : | _ => return (e, eType) | _ => return (e, eType) -private partial def resolveLValLoop (lval : LVal) (e eType : Expr) (previousExceptions : Array Exception) (hasArgs : Bool) : TermElabM (Expr × LValResolution) := do +private partial def resolveLValLoop (lval : LVal) (e eType : Expr) (hasArgs : Bool) : TermElabM (Expr × LValResolution) := do let (e, eType) ← consumeImplicits lval.getRef e eType hasArgs tryPostponeIfMVar eType /- If `eType` is still a metavariable application, we try to apply default instances to "unblock" it. -/ @@ -1399,15 +1432,13 @@ private partial def resolveLValLoop (lval : LVal) (e eType : Expr) (previousExce | ex@(Exception.error _ _) => let eType? ← unfoldDefinition? eType match eType? with - | some eType => resolveLValLoop lval e eType (previousExceptions.push ex) hasArgs - | none => - previousExceptions.forM fun ex => logException ex - throw ex + | some eType => resolveLValLoop lval e eType hasArgs + | none => throw ex | ex@(Exception.internal _ _) => throw ex private def resolveLVal (e : Expr) (lval : LVal) (hasArgs : Bool) : TermElabM (Expr × LValResolution) := do let eType ← inferType e - resolveLValLoop lval e eType #[] hasArgs + resolveLValLoop lval e eType hasArgs private partial def mkBaseProjections (baseStructName : Name) (structName : Name) (e : Expr) : TermElabM Expr := do let env ← getEnv diff --git a/tests/lean/run/invalidProjection.lean b/tests/lean/run/invalidProjection.lean index 975e67a752..8b2303a237 100644 --- a/tests/lean/run/invalidProjection.lean +++ b/tests/lean/run/invalidProjection.lean @@ -21,6 +21,9 @@ example (h1 : P n h) (h2 : P m h') := h1.1 = h2.2 error: Invalid projection: Index `3` is invalid for this structure; it must be between 1 and 2 Note: The expression `x` has type `Nat × Nat × Nat` which has only 2 fields + +Hint: n-tuples in Lean are actually nested pairs. To access the 3rd component of this tuple, use the projection `.2.2` instead: + 3̵2̲.̲2̲ -/ #guard_msgs in example (x : Nat × Nat × Nat) := x.3 diff --git a/tests/lean/run/invalidTupleProjHints.lean b/tests/lean/run/invalidTupleProjHints.lean new file mode 100644 index 0000000000..c5ea180dcc --- /dev/null +++ b/tests/lean/run/invalidTupleProjHints.lean @@ -0,0 +1,70 @@ +/-! +# Hints for invalid tuple projections + +These tests assess hints for invalid projections that may be incorrectly attempting to project the +`n`th element from a tuple where `n > 2`. +-/ + +def p : Nat × Nat × Nat := (3, 4, 5) +/-- +error: Invalid projection: Index `3` is invalid for this structure; it must be between 1 and 2 + +Note: The expression `p` has type `Nat × Nat × Nat` which has only 2 fields + +Hint: n-tuples in Lean are actually nested pairs. To access the 3rd component of this tuple, use the projection `.2.2` instead: + 3̵2̲.̲2̲ +-/ +#guard_msgs in +#check p.3 + +/-- +error: Invalid projection: Index `17` is invalid for this structure; it must be between 1 and 2 + +Note: The expression `p` has type `Nat × Nat × Nat` which has only 2 fields + +Hint: n-tuples in Lean are actually nested pairs. For example, to access the "third" component of `(a, b, c)`, write `(a, b, c).2.2` instead of `(a, b, c).3`. +-/ +#guard_msgs in +#check p.17 + +/-- +error: Invalid projection: Index `3` is invalid for this structure; it must be between 1 and 2 + +Note: The expression `p` has type `Nat × Nat × Nat` which has only 2 fields + +Hint: n-tuples in Lean are actually nested pairs. To access the 3rd component of this tuple, use the projection `.2.2` instead: + 3̵2̲.̲2̲ +-/ +#guard_msgs in +#check p.3.succ + +/- +In prior versions of Lean, the below would erroneously produce two error messages: "structure type +expected" on the first lval resolution iteration (prior to unfolding `MyProd`), then (correctly) +"invalid index" on the second, post-unfolding iteration +-/ +abbrev MyProd := Nat × Nat × Nat × Nat × Nat +def mp : MyProd := (1, 2, 3, 4, 5) +/-- +error: Invalid projection: Index `4` is invalid for this structure; it must be between 1 and 2 + +Note: The expression `mp` has type `Nat × Nat × Nat × Nat × Nat` which has only 2 fields + +Hint: n-tuples in Lean are actually nested pairs. To access the 4th component of this tuple, use the projection `.2.2.2.1` instead: + 4̵2̲.̲2̲.̲2̲.̲1̲ +-/ +#guard_msgs in +#eval mp.4 + +-- Ensure we don't produce hints for synthetic syntax +macro "illegally_project_from_a_tuple" : term => `((true, true, false).3) + +/-- +error: Invalid projection: Index `3` is invalid for this structure; it must be between 1 and 2 + +Note: The expression `(true, true, false)` has type `Bool × Bool × Bool` which has only 2 fields + +Hint: n-tuples in Lean are actually nested pairs. For example, to access the "third" component of `(a, b, c)`, write `(a, b, c).2.2` instead of `(a, b, c).3`. +-/ +#guard_msgs in +#check illegally_project_from_a_tuple