Exhaustiveness-checking warnings printed in descending order of source positions

[RyanGlScott]

Consider this program (taken from #1796, which is a separate issue):

module Bug where

exhaustive1 : {w} [2 ^^ (2 ^^ w)] -> [2 ^^ (2 ^^ w)]
exhaustive1 x
  | (2 ^^ (2 ^^ w)) < 2 => x
  | (2 ^^ (2 ^^ w)) == 2 => ~ x
  | (2 ^^ (2 ^^ w)) > 2 => x

// This should be exhaustive, as it simply reorders the guards found in the
// `exhaustive1` function, but Cryptol deems it non-exhaustive.
nonExhaustive1 : {w} [2 ^^ (2 ^^ w)] -> [2 ^^ (2 ^^ w)]
nonExhaustive1 x
  | (2 ^^ (2 ^^ w)) == 2 => ~ x
  | (2 ^^ (2 ^^ w)) < 2 => x
  | (2 ^^ (2 ^^ w)) > 2 => x

// This should be exhaustive, as it simply reorders the guards found in the
// `exhaustive1` function, but Cryptol deems it non-exhaustive.
nonExhaustive2 : {w} [2 ^^ (2 ^^ w)] -> [2 ^^ (2 ^^ w)]
nonExhaustive2 x
  | (2 ^^ (2 ^^ w)) == 2 => ~ x
  | (2 ^^ (2 ^^ w)) > 2 => x
  | (2 ^^ (2 ^^ w)) < 2 => x

// Note that `(2 ^^ w) >= 1`, which means that there is no need for a
// `(2 ^^ w) < 1` guard below.
exhaustive2 : {w} [2 ^^ w] -> [2 ^^ w]
exhaustive2 x
  | (2 ^^ w) == 1 => ~ x
  | (2 ^^ w) > 1 => x

// This should be exhaustive, as it is a slight variation on the same idea used
// in `exhaustive2`—namely, that `(2 ^^ (2 ^^ w)) >= 2`. Despite this, Cryptol
// deems this function non-exhaustive.
nonExhaustive3 : {w} [2 ^^ (2 ^^ w)] -> [2 ^^ (2 ^^ w)]
nonExhaustive3 x
  | (2 ^^ (2 ^^ w)) == 2 => ~ x
  | (2 ^^ (2 ^^ w)) > 2 => x

If you load this into Cryptol, it will print the following warnings:

[warning] at Bug.cry:36:1--36:15:
  Could not prove that the constraint guards used in defining Bug::nonExhaustive3 were exhaustive.
[warning] at Bug.cry:20:1--20:15:
  Could not prove that the constraint guards used in defining Bug::nonExhaustive2 were exhaustive.
[warning] at Bug.cry:12:1--12:15:
  Could not prove that the constraint guards used in defining Bug::nonExhaustive1 were exhaustive.

There are two unfortunate oddities here:

1. The warnings are printed in descending order of the definitions' source positions, whereas most warnings are printed in ascending order. That is to say, I would have expected the warnings to be printed in order of nonExhaustive1, then nonExhaustive2, and then nonExhaustive3, but they are instead printed in the opposite order.
2. The source spans for each warning do not actually include the constraint guards mentioned in the warning. For instance, Bug.cry:12:1--12:15 only encompasses the word "nonExhaustive1" on line 12, and it does not include any of the guards.

[danmatichuk]

For 2, should the source span include the entire declaration, or just the guards?

[RyanGlScott]

A good question. My inclination would be the guards, since that would mirror the behavior of GHC's exhaustiveness warnings. I don't feel strongly, however—either would be better than the status quo.