Deriving equalities from inequalities produces a misleading error message

[kleinreact]

For the following example

leZeroToEqZero :: n <= 0 => (n ~ 0 => r) -> r
leZeroToEqZero x = x

GHC reports that

• Could not deduce 'n ~ 0' arising from a use of 'x'
   from the context: n <= 0

which makes it perfectly clear that GHC can't derive the equality constraint from the inequality constraint here. However, enabling the plugin turns that into

Cannot satisfy: n <= 0

which is misleading, as n <= 0 is a given constraint. Furthermore, it does not make clear that the plugin won't be able to derive the equality either (see #33).

This error message probably also caused some confusion with respect to fixes proposed by @rowanG077 in #83.

[rowanG077]

The reason this is happening is that in the core logic of the plugin a check is done to see if a constraint is a valid natural number. This is implemented for inequalites by transformingforall n p. n <= p to p - n and checking if that is a natural. For p ~ 0 this becomes 0 - n which the isNatural function wrongly reports as definitely not a natural and thus returning a type error. Even for given constraints.

So in effect you can get very wrong type errors as this issue shows.

• leZeroToEqZero :: n <= 0 => (n ~ 0 => r) -> r has the radioactive n <= 0 constraint.
• n ~ 0 cannot be outright solved so natnormalise is called by GHC to help.
• natnormalise sees the n <= 0 given constraints and says impossible.

The constraint to be solved doesn't even have to be n ~ 0 it can be any constraint such that the n <= 0 ends up in natnormalise.. It's made even worse by the fact that in simple cases GHC can outright solve the constraint if they are syntactically equal to a give. For example this is totally fine:

leZeroToEqZero :: n <= 0 => (n <= 0 => r) -> r
leZeroToEqZero x = x

Because GHC can solve the wanted n <= 0 immediately with the given n <= 0. So n <= 0 doesn't end up in the solver and everything works as expected.

leZeroToEqZero :: n <= 0 => (n + n ~ 2 * n => r) -> r
leZeroToEqZero x = x

However is broken again because n + n ~ 2 * n is not solvable by GHC. Natnormalise is invoked and n <= 0 is in the given and you get:

Cannot satisfy: n <= 0

Even though natnormalise can solve n + n ~ 2 * n from nothing. This is a nightmare to debug in non-trivial code since from a high level view it can be that you add a totally unrelated constraint somewhere and suddenly you have the type checker screaming at you about n <= 0 being impossible. And there really is no hint why this is happening.

My PR was meant to fix this. But I got all kinds of breakage.