<div dir="ltr"><div style="font-size:12.8px"><div>Hi,<br></div>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<br><br><div style="margin-left:40px">type MaxConstraint a=a<=MaxNat<br></div><div style="margin-left:40px">toNatural :: forall n. (MaxConstraint n,KnownNat n)=>Natural n<br></div><div style="margin-left:40px">toNatural = Natural (integerToWord (natVal (Proxy :: Proxy n)))<br></div><br></div><div style="font-size:12.8px">where MaxNat is the hard-coded value of maxBound :: Word for now,<br><br><div style="margin-left:40px">type MaxNat=18446744073709551615<br></div> <br>My data type and the constrained constructor for Natural are<br><br><div style="margin-left:40px">data Natural (x::Nat) where<br></div><div style="margin-left:40px">     Natural :: (MaxConstraint x)=>{-# UNPACK #-} !Word# -> Natural x<br></div><br></div><div style="font-size:12.8px">I have tried to eliminate the integerToWord cast from toNatural, yet I have failed at doing so.<br></div><div style="font-size:12.8px">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.<br><br></div><div style="font-size:12.8px">Timo</div></div>