It may be tempting to add type functions for subtraction, division, logarithms, and square roots. These are the inverses of the functions that we already have. The problem with having these operations is that they are not defined for all their inputs. I can see the following options, if we were to introduce such functions:

1. Accept some ill defined "types" like (1 - 2), or (5 / 2). They would belong to kind Nat, but are not really natural numbers.
2. Come up with a "completion" for the type function (e.g., by defining (1 - 2) ~ 0), and having division do some rounding)
3. Automatically generate additional constraints which would ensure that types are well-defined, somehow.

None of these options seem particularly attractive.

Furthermore, we can already express basically the same functionality by using (implicit or explicit) equalities.

f :: Array n Byte -> Array (n / 8) Word64           -- using division.

f :: Array (8 * n) Byte -> Array n Word64           -- using multiplication and an implicit equality constraint.

f :: (m ~ 8 * n) => Array m Byte -> Array n Word64  -- using an explicit equality constraint.

Subjectively, the second form is the most readable. The third form shows that we are essentially using a qualified type to restrict the valid instantiation of the function.