This module provides the ability to refine given KnownNat instances using GHC.TypeLits's comparison API, and also the ability to prove inequalities and upper/lower limits.

If a library function requires 1 <= n constraint, but only KnownNat n is available:

foo :: (KnownNat n, 1 <= n) => Proxy n -> Int

bar :: KnownNat n => Proxy n -> Int
bar n = case (Proxy :: Proxy 1) %<=? n of
          LE  Refl -> foo n
          NLE _    -> 0

foo requires that 1 <= n, but bar has to handle all cases of n. %<=? lets you compare the KnownNats in two Proxys and returns a :<=?, which has two constructors, LE and NLE.

If you pattern match on the result, in the LE branch, the constraint 1 <= n will be satisfied according to GHC, so bar can safely call foo, and GHC will recognize that 1 <= n.

In the NLE branch, the constraint that 1 > n is satisfied, so any functions that require that constraint would be callable.

For convenience, isLE and isNLE are also offered:

bar :: KnownNat n => Proxy n -> Int
bar n = case isLE (Proxy :: Proxy 1) n of
          Just Refl -> foo n
          Nothing   -> 0

Similarly, if a library function requires something involving CmpNat, you can use cmpNat and the SCmpNat type:

foo1 :: (KnownNat n, CmpNat 5 n ~ LT) => Proxy n -> Int
foo2 :: (KnownNat n, CmpNat 5 n ~ GT) => Proxy n -> Int

bar :: KnownNat n => Proxy n -> Int
bar n = case cmpNat (Proxy :: Proxy 5) n of
          CLT Refl -> foo1 n
          CEQ Refl -> 0
          CGT Refl -> foo2 n

You can use the Refl that cmpNat gives you with flipCmpNat and cmpNatLE to "flip" the inequality or turn it into something compatible with <=? (useful for when you have to work with libraries that mix the two methods) or cmpNatEq and eqCmpNat to get to/from witnesses for equality of the two Nats.