Undocumented bottoms in surprising places

[sjakobi]

While running the new normalizeWithMIsConsistentWithNormalize property test again with a larger maxSuccesses, I was surprised by an error from normalizeWithM which I previously believed to be total!

The problematic expression boils down to <>.x || Type. The standard requires the two arguments of || to be tested for equivalence if neither normalizes to True or False, and normalizeWithM uses judgmentallyEqual for this. judgmentallyEqual is just convEmpty and convEmpty relies on eval, which uses error in a few cases, for example <>.x.

As Haskell functions are generally expected to be total, I think it would be good to document the partiality of eval and the functions that rely on eval.

Currently the documentation of e.g. normalize even incorrectly claims totality:

dhall-haskell/dhall/src/Dhall/Core.hs

Lines 1189 to 1199 in e40e847

	{-| Reduce an expression to its normal form, performing beta reduction
	`normalize` does not type-check the expression. You may want to type-check
	expressions before normalizing them since normalization can convert an
	ill-typed expression into a well-typed expression.
	However, `normalize` will not fail if the expression is ill-typed and will
	leave ill-typed sub-expressions unevaluated.
	-}
	normalize :: Eq a => Expr s a -> Expr t a

Regarding normalizeWithM, I wonder whether it could perform the equivalence tests without using eval, since it can take care of beta-normalization on its own.

[Gabriella439]

Fix is up here: #1140

[sjakobi]

Regarding removing the use of judgmentallyEqual in normalizeWithM: I initially thought that a replacement could be as simple as

alphaEquivalent e0 e1 = alphaNormalize e0 == alphaNormalize e1

Now I see that, to compare DoubleLits, we rely on Dhall.Binary.encode, so I think that a proper equivalent function for this usecase would involve a fair amount of boilerplate – unless anyone knows a way to do this with less boilerplate?!

[Gabriella439]

@sjakobi: I wouldn't worry too much about it. I'd like to move towards less variants of core utilities. If the partial normalization really bothers people then we could always make Dhall.Eval total, but so far nobody has complained.