小编Sti*_*rpo的帖子

我正在尝试使用类型系列来生成依赖于某种类型级别自然数的约束。这是一个这样的函数：

type family F (n :: Nat) (m :: Nat) :: Constraint where
  F 0 m = ()
  F n m = (m ~ 0)

然后我有一个具有此约束的函数。

f :: forall n m. (KnownNat n, KnownNat m, m ~ 0) => ()
f = ()

当我尝试在我的类型系列应该产生这个约束的模式匹配中使用这个函数时，ghc 说它不能推断出约束

下面是一个例子：

g :: forall n m. (KnownNat n, KnownNat m, F n m) => ()
g =
  case (natVal (Proxy @n)) of
    0 -> ()
    n -> f @n @m

它产生错误

• Could not deduce: …