如何使用Haskell类型类表达<=约束实现长度索引向量take函数

需求 #

编写适配长度索引向量的take函数，约束待提取的元素个数小于等于向量自身长度。

初始实现代码 #

data Nat where
    Zero :: Nat
    Succ :: Nat -> Nat

data SNat (n :: Nat) where
    SZero :: SNat Zero
    SSucc :: SNat n -> SNat (Succ n)

data Vec (n :: Nat) (a :: Type) where
    Nil  :: Vec Zero a
    Cons :: a -> Vec n a -> Vec (Succ n) a

class (m :: Nat) >= (n :: Nat)
instance m >= Zero
instance m >= n => (Succ m >= Succ n)

take :: (m >= n) => SNat n -> Vec m a -> Vec n a
take (SZero  ) _         = Nil
take (SSucc n) (x `Cons` xs) = x `Cons` (take n xs)

编译报错 #

编译上述代码时抛出如下错误：

* Could not deduce (n2 >= n1) arising from a use of `take'
      from the context: m >= n
        bound by the type signature for:
                   take :: forall (m :: Nat) (n :: Nat) a.
                           (m >= n) =>
                           SNat n -> Vec m a -> Vec n a
        at src\AnotherOne.hs:39:1-48
      or from: (n :: Nat) ~ ('Succ n1 :: Nat)
        bound by a pattern with constructor:
                   SSucc :: forall (n :: Nat). SNat n -> SNat ('Succ n),
                 in an equation for `take'
        at src\AnotherOne.hs:41:7-13
      or from: (m :: Nat) ~ ('Succ n2 :: Nat)
        bound by a pattern with constructor:
                   Cons :: forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a,
                 in an equation for `take'
        at src\AnotherOne.hs:41:17-27
      Possible fix:
        add (n2 >= n1) to the context of the data constructor `Cons'
    * In the second argument of `Cons', namely `(take n xs)'
      In the expression: x `Cons` (take n xs)
      In an equation for `take':
          take (SSucc n) (x `Cons` xs) = x `Cons` (take n xs

已排查现象 #

• 尝试过多种类型类的迭代写法，添加过OVERLAPS甚至INCOHERENT编译pragma，都没能修复问题
• HLS提示模式匹配不完整，指出未覆盖(SSucc SZero) Nil和(SSucc (SSucc _)) Nil两种分支
• 编写测试代码test = take (SSucc SZero) Nil时，编译器可以正确抛出Couldn't match type ‘'Zero’ with ‘'Succ 'Zero’的类型错误，说明函数对外API逻辑正确，问题仅出现在函数定义环节

已验证可行的替代方案 #

使用闭类型族实现>=约束可以正常运行，对应代码如下：

type (>=~) :: Nat -> Nat -> Bool
type family m >=~ n where
    m >=~ Zero        = True
    Succ m >=~ Succ n = m >=~ n
    _ >=~ _           = False
type m >= n = m >=~ n ~ True

目前希望通过Haskell类型类实例的方式解决该问题，同时想了解：这两种约束实现方式相比各有什么优劣？

内容的提问来源于stack exchange，提问作者Mathias Sven