Tell GHC that a <= Max a b

[leonschoorl]

By telling GHC that a <= Max a b it knows that (Max a b - a) is a valid Nat.

And you can do things like this:

-- | Overwrite either the first a of the last b bits.
overwrite :: forall a b. (KnownNat a, KnownNat b)
          => BitVector (Max a b) -> Either (BitVector a) (BitVector b) -> BitVector (Max a b)
overwrite ab (Left a) = a ++# rest
  where (_, rest) = split ab :: (BitVector a,  BitVector (Max a b - a))
overwrite ab (Right b) = rest ++# b
  where (rest, _) = split ab :: (BitVector (Max a b - b), BitVector b)

[martijnbastiaan]

Superseeded by https://github.com/clash-lang/ghc-typelits-extra/pull/20