Improve error messages from conversion checking

[BinderDavid]

We also report the subexpression which is different if we compare two complex expressions. For example, if we compare List(Bool) and List(Nat) we additionally point out the difference between Bool and Nat.

[codecov]

Codecov Report

Attention: Patch coverage is 54.42177% with 67 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
...aborator/src/typechecker/type_info_table/lookup.rs	0.00%	20 Missing ⚠️
lang/elaborator/src/normalizer/eval.rs	6.66%	14 Missing ⚠️
lang/elaborator/src/conversion_checking/unify.rs	75.60%	10 Missing ⚠️
lang/elaborator/src/result.rs	33.33%	4 Missing ⚠️
lang/elaborator/src/typechecker/exprs/mod.rs	20.00%	4 Missing ⚠️
lang/elaborator/src/typechecker/decls/mod.rs	50.00%	3 Missing ⚠️
.../elaborator/src/typechecker/exprs/local_comatch.rs	50.00%	3 Missing ⚠️
...ng/elaborator/src/typechecker/exprs/local_match.rs	0.00%	3 Missing ⚠️
...ang/elaborator/src/typechecker/decls/codatatype.rs	0.00%	2 Missing ⚠️
lang/elaborator/src/typechecker/decls/datatype.rs	0.00%	2 Missing ⚠️
... and 2 more

Files with missing lines	Coverage Δ
lang/ast/src/exp/hole.rs	77.08% <ø> (ø)
lang/driver/src/codespan.rs	17.02% <ø> (ø)
lang/driver/src/database.rs	78.76% <100.00%> (ø)
lang/elaborator/src/conversion_checking/mod.rs	100.00% <100.00%> (ø)
lang/elaborator/src/normalizer/normalize.rs	100.00% <100.00%> (ø)
lang/elaborator/src/typechecker/ctx.rs	80.00% <100.00%> (-1.16%)	⬇️
lang/miette_util/src/codespan.rs	30.00% <ø> (ø)
lang/elaborator/src/typechecker/exprs/hole.rs	84.21% <0.00%> (ø)
lang/elaborator/src/typechecker/util.rs	93.33% <0.00%> (ø)
...ang/elaborator/src/typechecker/decls/codatatype.rs	86.66% <0.00%> (-1.97%)	⬇️
... and 9 more

[timsueberkrueb]

I'm wondering if we should use Markdown ticks when referencing terms in error messages? Rust does that.