feature request: improved char type

[Chris-Hawblitzel]

Dafny's char type predates the newtype facility and is very limited compared to newtypes. It would be useful if char behaved more like a newtype. For example, this would allow programmers to convert between char types and other integral types, which would help when writing parsers and printers that convert between strings and integers. For example, with newtypes, you can write:

newtype mychar = x:int | 0 <= x < 0x10000

function method digitAsChar(i:int):mychar
  requires 0 <= i < 10
{
  mychar(48 + i)
}

This is difficult to do with the current char type.