This PR improves the error message encountered in the case of a type
class instance resolution failure, and adds an error explanation that
discusses the common new-user case of binary operation overloading and
points to the `trace.Meta.synthInstance` option for advanced debugging.
## Example
```lean4
def f (x : String) := x + x
```
Before:
```
failed to synthesize
HAdd String String ?m.5
Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
```
After:
```
failed to synthesize instance of type class
HAdd String String ?m.5
Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.
Error code: lean.failedToSynthesizeTypeclassInstance
[View explanation](https://lean-lang.org/doc/reference/latest/find/?domain=Manual.errorExplanation&name=lean.failedToSynthesizeTypeclassInstance)
```
The error message is changed in three important ways:
* Explains *what* failed to synthesize, using the "type class"
terminology that's more likely to be recognized than the "instance"
terminology
* Points to the `trace.Meta.synthInstance` option which is otherwise
nearly undiscoverable but is quite powerful (see also
leanprover/reference-manual#663 which is adding commentary on this
option)
* Gives an error explanation link (which won't actually work until the
next release after this is merged) which prioritizes the common-case
explanation of using the wrong binary operation
This PR improves the “expected type mismatch” error message by omitting
the type's types when they are defeq, and putting them into separate
lines when not.
I found it rather tediuos to parse the error message when the expected
type is long, because I had to find the `:` in the middle of a large
expression somewhere. Also, when both are of sort `Prop` or `Type` it
doesn't add much value to print the sort (and it’s only one hover away
anyways).
This PR makes functions defined by well-founded recursion use an
`opaque` well-founded proof by default. This reliably prevents kernel
reduction of such definitions and proofs, which tends to be
prohibitively slow (fixes#2171), and which regularly causes
hard-to-debug kernel type-checking failures. This changes renders
`unseal` ineffective for such definitions. To avoid the opaque proof,
annotate the function definition with `@[semireducible]`.
This PR adds an addition newline before the "Additional diagnostic
information may be available using the `set_option ... true` command."
messages, to provide better visual separation from the main error
message.
Adds a mechanism where when an autoparam tactic fails to synthesize a
parameter, the associated parameter name or field name for the autoparam
is reported in an error.
Examples:
```text
could not synthesize default value for parameter 'h' using tactics
could not synthesize default value for field 'inv' of 'S' using tactics
```
Notes:
* Autoparams now run their tactics without any error recovery or
error-to-sorry enabled. This enables catching the error and reporting
the contextual information. This is justified on the grounds that
autoparams are not interactive.
* Autoparams for applications now cleanup the autoParam annotation,
bringing it in line with autoparams for structure fields.
* This preserves the old behavior that autoparams leave terminfo, but we
will revisit this after some imminent improvements to the unused
variable linter.
Closes#2950
Defines `mergeSort`, a naive stable merge sort algorithm, replaces it
via a `@[csimp]` lemma with something faster at runtime, and proves the
following results:
* `mergeSort_sorted`: `mergeSort` produces a sorted list.
* `mergeSort_perm`: `mergeSort` is a permutation of the input list.
* `mergeSort_of_sorted`: `mergeSort` does not change a sorted list.
* `mergeSort_cons`: proves `mergeSort le (x :: xs) = l₁ ++ x :: l₂` for
some `l₁, l₂`
so that `mergeSort le xs = l₁ ++ l₂`, and no `a ∈ l₁` satisfies `le a
x`.
* `mergeSort_stable`: if `c` is a sorted sublist of `l`, then `c` is
still a sublist of `mergeSort le l`.
