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