• Currently only types indexed by type variables are supported. E.g. Pair (A B : Type), Functor (F : Type -> Type). While working on EVM Bytes De-/Encoding #3378, it has become evident that having indexed types by natural numbers would be useful. For instance, we would allow the type Word (numBytes : Nat).

In more detail, we would have.

type Word (bytes : Nat) := mk Nat
with
  toNat {b : Nat} : Word b -> Nat
    | (mk n) := mod n (256 * b);
  
  -- byte size is known at compile time so we don't encode the length of the word in the bytearray
  instance
  toBytes {b : Nat} : ToBytes (Word b) := ...
end;

Another useful feature would be to have the ability to constraint the index. This is usefule because Evm only supports words up to 32 bytes:

the bytearray
  instance
  toBytes {b : Nat} {{b <= 32}} : ToBytes (Word b) := ...
end;