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.