A function `nat2Word# :: KnownNat n => Proxy# n -> Word#`

It would be nice if there were the function (perhaps in GHC.Prim) nat2Word# :: KnownNat n => Proxy# n -> Word# that was essentially (\ W# w# -> w#) . fromInteger . natVal, except that it produces the Word# at compile-time rather than runtime and that it works with Proxy# (for its no-runtime-representation, totally-free nature) instead of Proxy.

This would enable compile-time computations on Nats to produce a literal Word# without any runtime expense at all, which seems nice if you're dealing with primitives because you want to avoid runtime expense.

Motivating example

I'm learning primitive types and type-level arithmetic by making a simple set of fixed-width integer types where the type contains a Nat for the number of bits in the fixed-width integer.

Going from the following Nats to their corresponding Word#s at compile time even when optimizations are turned off during development would be very nice:

`Div (n + 63) 64` \\\\=	the highest index we should try to access via `indexWordArray#`
`Mod (n - 1) 64 + 1` \\\\=	except when `n == 0`, the number of bits actually used in the \\\\ most-significant word
`2^(Mod (n + 63) 64 + 1) - 1` \\\\=	the unsigned integer narrowing bitmask to use on the \\\\ most-significant word

Trac metadata

Trac field	Value
Version	8.4.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture