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