To work with certain network protocols, I used GHC.TypeLits to implement fixed-sized bit vectors in the form of wrapped integers with tags of type Nat .
newtype W (n :: Nat) = W { getW :: Integer }
Along with instances for all classes (Integral, Num, Bits, etc.), I defined a function for combining them:
(>+<) :: forall n m. (KnownNat m, KnownNat n, KnownNat (m + n)) => W m -> W n -> W (m + n) (W x) >+< (W y) = fromInteger $ x + shift y (natValInt (Proxy :: Proxy m))
I have problems in this next part. I am trying to create an application that leads to a W n from one, which leads to a W m , where m is a divisor of n . For example, using attoparsec, you should be able to write:
anyWord128 :: Parser (W 128) anyWord128 = assemble $ fmap (fromIntegral :: Word8 -> W 8) anyWord8
Here is my attempt:
class (KnownNat d, KnownNat n) => d :|: n where assemble :: forall f. Applicative f -> f (W d) -> f (W n) instance KnownNat n => n :|: n where assemble = id instance (KnownNat n, CmpNat nd ~ GT, d :|: n', (d + n') ~ n) => d :|: n where assemble f = liftA2 (>+<) f (assemble f)
Compiling the code (with many language extensions, including -XOverlappingInstances, all of which are in the actual source listed below), downloading the assemble example, makes GHCi tell me that there are overlapping instances for 8 :|: 8 , I assume that either because I don’t know what I am doing, or because the GHC type of verification limits computational capabilities (or both).
Do you have any of you GHC wizards to correctly define this class?
Edit
Fixed type in assembly definition - thanks kosmikus.
In addition, the full one is presented here ( :|: defined on line 159).