Make `length` return the dedicated type

Clarification and motivation

There is an acknowledged issue (I heard at least two mentions, one is here) that length returns exactly Int - too often we want a different type and have to convert explicitly. In #423 (closed) this problem has raised with new rigor, Unsafe.fromIntegral @Int @a . length got a de-facto common pattern.

I suggest to re-implement length in morley-prelude package as follows:

newtype Len = Len Int

type instance IntBaseType Len = FixedWordTag 29  -- think which number to put here

length :: (Container t, IsIntSubType Len l ~ 'True) => t -> l 

and probably Len should be assumed to be of 29-bytes. We can assume that length of any container is not larger, and casting to wider types is safe (currently a similar assumption is made anyway - length returns Int).

The only perfect solution would be to make length return Natural, but I suspect we don't want to go there. In either way, if lists turns to be larger than we expected, the solution above allows making the restriction on length's return type stricter (allowing only larger values) anytime.

Also, in this issue I propose to look at usages of take and drop - whether are they often used with an explicit cast, and probably update them as well (in their case, I think we could even accept an arbitrary Integral number).

Acceptance criteria

  • length is updated so that the following explicit fromIntegral is necessary only when the target type is too narrow.
  • Whether take and drop (and maybe other similar functions) are worth making accept various numeric types - is considered.
Edited by Konstantin Ivanov