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