在Haskell中使用类型级自然重叠实例

Question

为了处理某些网络协议,我一直在使用GHC.TypeLits固定大小的位向量作为带有类型类型的包装整数Nat.

newtype W (n :: Nat) = W { getW :: Integer }

除了各种类的实例(Integral,Num,Bits等)之外,我还定义了一个函数来组合它们:

(>+<) :: 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))

下一部分是我遇到麻烦的地方.我试图创建一个应用程序,导致W n一个导致a W m,其中m是除数的一个n.例如,使用attoparsec,应该可以写:

anyWord128 :: Parser (W 128)
anyWord128 = assemble $ fmap (fromIntegral :: Word8 -> W 8) anyWord8

这是我的尝试:

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 n d ~ GT, d :|: n', (d + n') ~ n) => d :|: n where
    assemble f = liftA2 (>+<) f (assemble f)

代码编译(包含许多语言扩展,包括-XOverlappingInstances,所有这些都在下面链接的实际源代码中),加载assembleGHCi原因的示例用法告诉我有重叠的实例8 :|: 8.我猜这是因为我不知道我在做什么,或者因为GHC的类型检查器的计算能力有限(或两者兼而有之).

你们中的任何一个GHC向导都能看到正确定义这个类的方法吗？

编辑

固定类型的汇编定义 - 谢谢kosmikus.
此外,这里是完整的源(:|:在第159行定义).