haskell - 断言类型类适用于类型族应用程序的所有结果

Question

我有一个类型族定义如下:

type family Vec a (n :: Nat) where
  Vec a Z = a
  Vec a (S n) = (a, Vec a n)

我想断言应用此类型系列的结果始终满足 SBV 包中的 SymVal 类约束:

forall a . (SymVal a) => SymVal (Vec a n)

有 SymVal实例 a,b , 所以每当 SymVal a成立，然后 SymVal (Vec a n)对于 n 的任何值，应该成立.如何确保 GHC 看到 SymVal总是为类型族应用程序的结果实现？

但是，我不知道如何表达这一点。我写一个实例吗？派生条款？我不是在创建新类型，只是将数字映射到现有类型。

还是我完全走错了路？我应该使用数据系列还是功能依赖项？

Answer 1

做不到。你只需要把约束放在任何地方。这是一个真正的无赖。