feat: improve set_option error messages (#9496)

This PR improves the error messages produced by the `set_option`
command.

src/Lean/Data/Options.lean

@@ -39,10 +39,10 @@ private builtin_initialize optionDeclsRef : IO.Ref OptionDecls ← IO.mkRef (mkN
 @[export lean_register_option]
 def registerOption (name : Name) (decl : OptionDecl) : IO Unit := do
   unless (← initializing) do
-    throw (IO.userError "failed to register option, options can only be registered during initialization")
+    throw (IO.userError "Failed to register option: Options can only be registered during initialization")
   let decls ← optionDeclsRef.get
   if decls.contains name then
-    throw $ IO.userError s!"invalid option declaration '{name}', option already exists"
+    throw $ IO.userError s!"Invalid option declaration `{name}`: Option already exists"
   optionDeclsRef.set $ decls.insert name decl
 
 def getOptionDecls : IO OptionDecls := optionDeclsRef.get
@@ -56,7 +56,7 @@ def getOptionDeclsArray : IO (Array (Name × OptionDecl)) := do
 
 def getOptionDecl (name : Name) : IO OptionDecl := do
   let decls ← getOptionDecls
-  let (some decl) ← pure (decls.find? name) | throw $ IO.userError s!"unknown option '{name}'"
+  let (some decl) ← pure (decls.find? name) | throw $ IO.userError s!"Unknown option `{name}`"
   pure decl
 
 def getOptionDefaultValue (name : Name) : IO DataValue := do

src/Lean/Elab/SetOption.lean

@@ -23,7 +23,7 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
   let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error ref ex.toString) (getOptionDecl optionName)
   pushInfoLeaf <| .ofOptionInfo { stx := id, optionName, declName := decl.declName }
   let rec setOption (val : DataValue) : m Options := do
-    unless decl.defValue.sameCtor val do throwError "type mismatch at set_option"
+    unless decl.defValue.sameCtor val do throwMistypedOptionValue optionName val decl.defValue
     return (← getOptions).insert optionName val
   match val.isStrLit? with
   | some str => setOption (DataValue.ofString str)
@@ -35,6 +35,34 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
   | Syntax.atom _ "true"  => setOption (DataValue.ofBool true)
   | Syntax.atom _ "false" => setOption (DataValue.ofBool false)
   | _ =>
-    throwError "unexpected set_option value {val}"
+    if let some ctorType := ctorType? decl.defValue then
+      throwError "Unexpected set_option value `{val}`; expected a literal of type `{ctorType}`"
+    else
+      throwUnconfigurable optionName
+where
+  throwMistypedOptionValue (optionName : Name) (found defVal : DataValue) := do
+    match ctorType? defVal with
+    | some defValType =>
+      let foundType := ctorType? found |>.get!
+      throwError "set_option value type mismatch: The value{indentD (toMessageData found)}\nhas type\
+        {indentD (toMessageData foundType)}\nbut the option `{optionName}` expects a value of type\
+        {indentExpr defValType}"
+    | _ => throwUnconfigurable optionName
+
+  throwUnconfigurable {α} (optionName : Name) : m α :=
+    throwError "Invalid `set_option` command: The option `{optionName}` cannot be configured using \
+      `set_option`"
+
+  /--
+  Returns the type corresponding to the given `DataValue`, or `none` if the corresponding type
+  cannot be specified using `set_option` notation.
+  -/
+  ctorType? : DataValue → Option Expr
+  | .ofString .. => mkConst ``String
+  | .ofNat .. => mkConst ``Nat
+  | .ofBool .. => mkConst ``Bool
+  | .ofInt .. => none
+  | .ofName .. => none
+  | .ofSyntax .. => none
 
 end Lean.Elab

tests/lean/run/setOptionErrors.lean

@@ -0,0 +1,20 @@
+/-!
+# `set_option` Errors
+
+Tests the error messages produced by the `set_option` command.
+-/
+
+/-- error: Unknown option `nonexistent_option_name` -/
+#guard_msgs in
+set_option nonexistent_option_name false
+
+/--
+error: set_option value type mismatch: The value
+  21
+has type
+  Nat
+but the option `pp.explicit` expects a value of type
+  Bool
+-/
+#guard_msgs in
+set_option pp.explicit 21