GHC.TypeLits.Compare

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.

<= and <=?

data (:<=?) :: Nat -> Nat -> * where

Constructors

LE :: ((m <=? n) :~: True) -> m :<=? n

NLE :: ((m <=? n) :~: False) -> ((n <=? m) :~: True) -> m :<=? n

(%<=?) :: (KnownNat m, KnownNat n) => p m -> q n -> m :<=? n

Convenience functions

isLE :: (KnownNat m, KnownNat n) => p m -> q n -> Maybe ((m <=? n) :~: True)

isNLE :: (KnownNat m, KnownNat n) => p m -> q n -> Maybe ((m <=? n) :~: False)

CmpNat

data SCmpNat :: Nat -> Nat -> * where

Constructors

CLT :: (CmpNat m n :~: LT) -> SCmpNat m n

CEQ :: (CmpNat m n :~: EQ) -> (m :~: n) -> SCmpNat m n

CGT :: (CmpNat m n :~: GT) -> SCmpNat m n

cmpNat :: (KnownNat m, KnownNat n) => p m -> q n -> SCmpNat m n

Manipulating witnesses

flipCmpNat :: SCmpNat m n -> SCmpNat n m

cmpNatEq :: (CmpNat m n :~: EQ) -> m :~: n

eqCmpNat :: (m :~: n) -> CmpNat m n :~: EQ

reflCmpNat :: (m :~: n) -> SCmpNat m n

Interfacing with <=?

cmpNatLE :: SCmpNat m n -> m :<=? n