Teach solver more about exponents

[yav]

Adding #1380 will enable us to write divide an conquer algorithms like this:

len2 : {n,a} (fin n) => [2^^n] a -> Integer
len2 x
  | (n == 0)  => 1
  | (n > 1)   => (len2 a + len2 b)
                    where (a,b) = splitAt `{2^^(n-1)} x

Unfortunately, at the moment this does not type check because we are missing some facts about the interaction between exponents and division:

[error] at test.cry:1:1--4:5:
  Failed to infer the following types:
    • ?m, type argument 'n' of 'Main::len2(n > 1)' at test.cry:1:1--4:5
  while validating user-specified signature
    in the definition of 'Main::len2', at test.cry:4:1--4:5,
    we need to show that
      for any type n, a
      assuming
        • fin n
        • n > 1
      the following constraints hold:
        • 2 ^^ n == 2 ^^ ?m
            arising from
            matching types
            at test.cry:1:1--4:5
        • fin ?m
            arising from
            use of expression Main::len2(n > 1)
            at test.cry:1:1--4:5
        • ?m > 1
            arising from
            use of expression Main::len2(n > 1)
            at test.cry:1:1--4:5
[error] at test.cry:1:1--4:5:
  Failed to validate user-specified signature.
    in the definition of 'Main::len2(n > 1)', at test.cry:4:1--4:5,
    we need to show that
      for any type n, a
      assuming
        • fin n
        • n > 1
      the following constraints hold:
        • 2 ^^ n >= 2 ^^ (n - 1)
            arising from
            matching types
            at test.cry:7:55--7:56

To get the first one to work we need a new improvement rule:

(fin n, a ^^ n == a ^^ m, a >= 2) => (n == m)

To get the second one to work we need something like:

(a <= b) => (x ^^ a <= x ^^ b)

[RyanGlScott]

See also #704.