Refactor usage of `Nat`s on type-level

[TurtlePU]

Currently, we have a lot of constraints on type-level naturals sprinkled all over the codebase. Some of them seem redundant from common sense, for example:

• relations which always hold, like (n + 1) - 1 ~ n
• relations which hold in context, like 1 <= n in a context where 128 <= n
• definedness of results of type families, like KnownNat (8 * n) in a context where KnownNat n

While we wait for Dependent Haskell which will come any minute, we can do the following:

• introduce better API for some of the Vector and ByteString operations, like uncons :: Vector (1 + size) a -> (a, Vector size a) and toWords :: ByteString (m * n) c -> Vector m (ByteString n c)
• respect that type-level operations do not have any algebraic properties (e.g. type-level addition is not commutative and not associative) and restructure the way code is organized so that it doesn't matter (I was looking at splitAt3 in Vector; it actually is not used and can be removed)

In cases where the above doesn't work, we can use the trick described here: https://stackoverflow.com/questions/32839389/can-i-get-knownnat-n-to-imply-knownnat-n-3-etc. This allows us to build a library of helpers like:

withAdd :: (KnownNat m, KnownNat n) => (KnownNat (m + n) => r) -> r
withSub :: (KnownNat m, KnownNat n, n <= m) => (KnownNat (m - n) => r) -> r
withMul :: (KnownNat m, KnownNat n) => (KnownNat (m * n) => r) -> r
withDiv :: (KnownNat m, KnownNat n, 1 <= n) => (KnownNat (Div m n) => r) -> r
-- | same for log2, exp etc.

assoc :: ((m + n) + k ~ m + (n + k) => r) -> r
comm :: (m + n ~ n + m => r) -> r
trans :: (m <= n, n <= k) => (m <= k => r) -> r
-- | some more axioms for naturals

And use them to only specify constraints we really need for our dependent functions.