KnownNats的类型级别归纳：重叠实例

Question

我试图弄清楚如何在KnownNats上进行类型级归纳。一个玩具示例，将vector-sized中的大小向量相加：

{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE TypeFamilies, TypeApplications, TypeOperators #-}
{-# LANGUAGE RankNTypes, DataKinds #-}

module Main where

import GHC.TypeNats
import qualified Data.Vector.Sized as V

class KnownNat d => SumVectorSized d where
  sumVS :: V.Vector d Int -> Int

instance SumVectorSized 0 where
  sumVS _ = 0

instance (SumVectorSized d, KnownNat d', d' ~ (1+d)) => SumVectorSized d' where
  sumVS vec = V.head vec + sumVS (V.tail vec)

main = do
  let Just vec = V.fromList @4 [1..4]
  print $ sumVS vec
编译时，会出现错误：

• Overlapping instances for SumVectorSized 0
    arising from a use of ‘sumVS’
  Matching instances:
    instance SumVectorSized 0 -- Defined at src/Main.hs:14:10
    instance (SumVectorSized d, KnownNat d', d' ~ (1 + d)) =>
             SumVectorSized d'
      -- Defined at src/Main.hs:17:10
I think

问题在于，GHC不知道（1 + d）对于任何d都不为0。我如何才能知道实例不重叠？还是有另一种方法可以进行这种归纳？

我试图弄清楚如何在KnownNats上进行类型级归纳。一个玩具示例，将向量大小的向量相加：{-＃LANGUAGE FlexibleInstances，UndecidableInstances＃-} {-＃LANGUAGE ...

Answer 1

我认为问题在于GHC不知道（1 + d）对于任何d都不为0。

Answer 2

您可以像这样在KnownNat上实现匹配