429734c02f
This PR modifies the error message for type synthesis failure for the case where the type class in question is potentially derivable using a `deriving` command. Also changes the error explanation for type class instance synthesis failure with an illustration of this pattern. ## Example ```lean4 inductive MyColor where | chartreuse | sienna | thistle def forceColor (oc : Option MyColor) := oc.get! ``` Before this PR, this gives the potentially confusing impression that Lean may have decided that `MyColor` is _not_ inhabited — people used to Rust may be especially inclined towards this confusion. ``` failed to synthesize instance of type class Inhabited MyColor Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. ``` After this PR, a targeted hint suggests precisely the command that will fix the issue: ``` error: failed to synthesize instance of type class Inhabited MyColor Hint: Adding the command `deriving instance Inhabited for MyColor` may allow Lean to derive the missing instance. ``` |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||