Make `Literal val1 a` constraints imply `Literal val2 a` for all `val2 <= val1`

[RyanGlScott]

Cryptol uses the Literal class to denote numeric literals: if you have a Literal val a constraint, then you can construct a value of type a that represents the number val. For instance, the expression 1 gives rise to Literal 1 a, the expression 2 gives rise to Literal 2 a, and so on.

In practice, there appears to be a sort of subtyping relationship between Literal constraints. To see what I mean, consider the type of [1, 2]:

Cryptol> :type [1, 2]
[1, 2] : {a} (Literal 2 a) => [2]a

If I put both numbers into a sequence, then the overall sequence gives rise to a single Literal 2 a constraint. This would suggest that Literal 2 a suffices to produce both 1 and 2 literals, which makes a certain kind of sense: if a type is "large enough" to fit the value 2, then it surely ought to be large enough to fit the value 1. The reason that this expression gives rise to a single Literal constraint rather than two separate (Literal 1 a, Literal 2 a) constraints is because of this special case in insertGoal, which simplifies (Literal val1 a, Literal val2 a) to Literal (max val1 val2) a.

Surprisingly, however, the Literal 2 a constraint does not imply Literal 1 a. Suppose I try to define this function:

f : {a} (Literal 2 a) => a
f = 1

This fails to typecheck:

[error] at Main.cry:2:1--2:6:
  Failed to validate user-specified signature.
    in the definition of 'Main::f', at Main.cry:2:1--2:2,
    we need to show that
      for any type a
      assuming
        • Literal 2 a
      the following constraints hold:
        • Literal 1 a
            arising from
            use of literal or demoted expression
            at Main.cry:2:5--2:6

I think it would make sense to add such an implication. Namely, I think that Literal val1 a should imply Literal val2 a for all val2 <= val1. Some other implications that might make sense to add:

• LiteralLessThan val1 a should imply LiteralLessThan val2 a for all val2 <= val1.
• Literal val1 a should imply LiteralLessThan val2 a for all val2 <= val1.
• LiteralLessThan val1 a should imply Literal val2 a for all val2 < val1.