RFC: expected type diffing

Proposal

The goal is to provide colored diffs between expected type vs and actual type in VSCode InfoView for type mismatch errors.

• User Experience: It usually happens that the term proposed for a proof is slightly different (e.g. because of a typo) to the correct one. When this leads to a type mismatch error, it is sometimes difficult to find the differences between expected and actual types. Highlighting the differences using two background colors as in Gitt diffs (say, red background in actual type and green background in the expected type), can make it easier to find the mistake in the proposed term.

• Beneficiaries: This is specially targeted for users building proofs, but people using Lean as a programming language who also have to work with lengthy types will find this useful.

• Maintainability: This feature should be independent of other matters, so I believe in will only require maintenance related to the diffing utilities and the VSCode extension.

Community Feedback

Discussion took place at this topic from Zulip.

@kmill suggested that pretty-print should allow to diff implicit arguments as well. @eric-wieser commented that the infrastructure for the creating the diff at the InfoView most probably exists already, to which Damiano Testa answered by recalling Lean.Widget.exprDiff.

Disclaimer. I do not have the programming experience yet to present a PR for this, but I've seen other people from the community getting this kind of thing in production in a few hours! So perhaps it is easy to implement.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reading Lean.Widget.exprDiff and investigating the existing diff infrastructure in the VSCode InfoView, as referenced in the discussion. Determine how expected and actual types are rendered and whether pretty-printing can include implicit arguments. Done means type mismatch errors show colored diffs for both types in the InfoView.