Reject record projection when there is a field type mismatch

[Gabriella439]

Fixes #1020

This also includes small fixes to the MissingField error message,
which I found along the way.

[sjakobi]

Good stuff!

Should this wait for #1023 and possibly even dhall-lang/dhall-lang#601 though!?

[sjakobi]

Great explanation! 👍

I was dreading to write one myself!

[sjakobi]

Ah, I thought we'd need to pass put nf_t instead of t to ProjectionTypeMismatch to ensure that both diff arguments are Records. I hadn't seen that prettyDiff normalizes the expressions.

I'm wondering whether the code would actually be easier to understand if we didn't have the prettyDiff alias and used Dhall.Diff.diffNormalized directly?!

[sjakobi]

LGTM! :)

[Gabriella439]

@sjakobi: prettyDiff used to be a more complex function and the alias is just scar tissue that we forgot to remove:

dhall-haskell/src/Dhall/TypeCheck.hs

Lines 887 to 899 in 3c05125

	prettyDiff :: (Eq a, Pretty a) => Expr s a -> Expr s a -> Builder
	prettyDiff exprL exprR = builder
	where
	doc =
	fmap Dhall.Pretty.annToAnsiStyle (Dhall.Diff.diffNormalized exprL exprR)
	opts = Pretty.LayoutOptions { Pretty.layoutPageWidth = Pretty.Unbounded }
	stream = Pretty.layoutPretty opts doc
	lazyText = Pretty.renderLazy stream
	builder = Builder.fromLazyText lazyText