[Haskell-cafe] natVal straight to Word#

[Timotej Tomandl]

Hi,
I am using type-level naturals constrained to be at max the size of Word#,
as such I have found myself casting the type-level naturals first to
Integer and then to Word# like this

type MaxConstraint a=a<=MaxNat
toNatural :: forall n. (MaxConstraint n,KnownNat n)=>Natural n
toNatural = Natural (integerToWord (natVal (Proxy :: Proxy n)))

where MaxNat is the hard-coded value of maxBound :: Word for now,

type MaxNat=18446744073709551615

My data type and the constrained constructor for Natural are

data Natural (x::Nat) where
     Natural :: (MaxConstraint x)=>{-# UNPACK #-} !Word# -> Natural x

I have tried to eliminate the integerToWord cast from toNatural, yet I have
failed at doing so.
As such I would like to ask, if anyone has some insight, whether it is
possible to eliminate this one step of indirection. The only option I came
up with is writing GHC plugin to do this.

Timo
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20170513/74b3fe09/attachment.html>