Incomplete reasoning about exponentiation with respect to exhaustiveness checking

[RyanGlScott]

In certain cases, Cryptol's exhaustiveness checker for numeric constraint guards incorrectly deems sets of guards to be inexhaustive when they involve exponentiation. Here is a program with some relevant examples:

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

I would expect all of the functions above to be marked as exhaustive, but Cryptol does not do so for the functions prefixed with nonExhaustive*:

[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.

My understanding is that the typechecker's reasoning about the behavior of exponentiation is necessarily incomplete, but it does feel like we could do better in these specific examples.