Element type constraints for sequence enumerations

[brianhuffman]

When you write a finite list enumeration like [5 .. 10], the result has a polymorphic type:

Cryptol> :t [5..10]
[5 .. 10] : {a} (Literal 10 a) => [6]a

It would be nice if we could put a type ascription for the element type inside the brackets, like [5 .. 10:[8]]. But currently this doesn't work:

Cryptol> [5 .. 10:[8]]

Parse error at <interactive>:1:7--1:13
  The boundaries of .. sequences should be valid numeric types.
The expression `10 : [8]` is not.

If you were trying to specify the width of the elements,
you may add a type annotation outside the sequence. For example:
   [ 1 .. 10 ] : [_][16]

We should add support in the parser to allow [m .. n : t] (and also [m : t .. n]) as special syntactic forms. They would both desugar to fromTo`{first=m, last=n, a=t}.

We should similarly add support for fromThenTo enumerations, like [a, b .. c : t].

[brianhuffman]

Pull request #628 implements the type-annotation-on-list-bounds feature mentioned above. We should probably also document the feature before closing the ticket.

[brianhuffman]

We might also consider extending this feature so that, e.g. ['a' .. 'z'] (see #622) gets its element type constrained to [8]. The idea is that on the value level, 'a' is basically syntactic sugar for 97:[8], so maybe it should work like that as a list enumeration bound. Similarly, a hex number like 0x1000 is basically sugar for 4096:[16], so maybe [0x1000..0x17ff] should be constrained to an element type of [16]. What does everyone think?

[robdockins]

We should probably actually document this somewhere before the 2.9.0 release.