Defaulting for `[]`

[yav]

Ticket #875 points out that the new defaulting rules lead to a different behavior when you write [0x10] @@ [].
This has type {a} Integral a => [] [8]. In this case we don't default the a because there is no literal that causes the ambiguity.

I am not sure how useful this example is in real Cryptol code but it does appear in the book.

Since I doubt that this would appear very often in actual code, perhaps we should solve this by being more aggressive in the REPL defaulting rules, and use Integral a as a potential hint for defaulting.

[yav]

On #875 @weaversa points out that a similar thing happens if you just type []. In that case we don't have any constraints, which could also warrant a special REPL defaulting rule.