Hi Timotej, A KnownNat constraint gets desugared into an Integer parameter by GHC, so it seems difficult to get rid of the conversion altogether. If you mimic the KnownNat type class, for Word instead of Integer: newtype Tagged n a = Tagged a class KnownWord n where word :: Tagged n Word then you can push out the Integer -> Word conversions to the boundaries of your application. I mean that internally, you need only to pass Words around, and your internal functions would look like: internalFunction :: (KnownWord n, KnownWord m) => ... But on the outside, you may still have to do a conversion. instance (KnownNat n, n <= MaxWord) => KnownWord n where word = Tagged (integerToWord (natVal (Proxy :: Proxy n))) externalFunction :: (KnownNat n, KnownNat m, n <= MaxWord, m <= MaxWord) => ... externalFunction = internalFunction There are also a few GHC-specific tricks to help work with such a type class without GHC plugins; the constraints[1] package gives some examples (in particular, see the Data.Constraint.Nat module); this involves unsafeCoerce. You can avoid Integer -> Word conversions by instead getting the Word from a runtime value. In particular, it is possible to write the following: someWord :: Word -> SomeWord -- or some variants, depending on the extensions available, specifically AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables. data SomeWord where SomeWord :: KnownWord n => SomeWord You can also reflect type-level operations with operations on Word (as opposed to having to do everything with Integers first), and even provide tools for reasoning about these operations, all of that without getting out of the compiler, as opposed to plugins. plusWord :: (KnownWord n, KnownWord m) :- KnownWord (n + m) -- maybe with (n + m <= MaxWord) on the left hand side too As I mentioned earlier, this requires internal use of unsafeCoerce, but it is possible to keep it contained and expose a safe interface. Regards, Li-yao [1] http://hackage.haskell.org/package/constraints

FWIW. In GHC-8.2 the `natVal` from GHC.TypeNats (not TypeLits!) will return `Natural`. - Oleg On 13.05.2017 13:53, Timotej Tomandl wrote:

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

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.