Type-level sized Word literals???

[Viktor Dukhovni]

I am working on some code where it is useful to have types indexed by a
16-bit unsigned value.

Presently, I am using type-level naturals and having to now and then
provide witnesses that a 'Nat' value I am working with is at most 65535.

Also, perhaps there's some inefficiency here, as Naturals have two
constructors, and so a more complex representation with (AFAIK) no
unboxed forms.

I was wondering what it would take to have type-level fixed-size
Words (Word8, Word16, Word32, Word64) to go along with the Nats?

It looks like some of the machinery (KnownWord16, SomeWord16, wordVal16,
etc.) can be copied straight out of GHC.TypeNats with minor changes, and
that much works, but the three major things that are't easily done seem
to be:

    - There are it seems no TypeReps for types of Kind Word16, so one can't
      have (Typeable (Foo w)) with (w :: Word16).

    - There are no literals of a promoted Word16 Kind.

        type Foo :: Word16 -> Type
        data Foo w = MkFoo Int

        -- 1 has Kind 'Natural' (a.k.a. Nat)
        x = MkFoo 13 :: Foo 1 -- Rejected, 

        -- The new ExtendedLiterals syntax does not help
        --
        x = MkFoo 13 :: Foo (W16# 1#Word16) -- Syntax error!

    - There are unsurprisingly also no built-in 'KnownWord16' instances
      for any hypothetical type-level literals of Kind Word16.

Likely the use case for type-level fixed-size words is too specialised
to rush to shoehorn into GHC, but is there something on the not too
distant horizon that would make it easier and reasonable to have
fixed-size unsigned integral type literals available?

[ I don't see a use-case for unsigned versions, they can trivially be
  represented by the unsigned value of the same width. ]

With some inconvenience, in many cases I can perhaps synthesise Proxies
for types of Kind Word16, and just never use literals directly.

--
    Viktor.