在不同的模式匹配情况下推导不同的类型类约束

Question

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

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: m ~ 0 arising from a use of ‘f’
      from the context: (KnownNat n, KnownNat m, F n m)
        bound by the type signature for:
                   g :: forall (n :: Nat) (m :: Nat).
                        (KnownNat n, KnownNat m, F n m) =>
                        ()
    ‘m’ is a rigid type variable bound by
        the type signature for:
          g :: forall (n :: Nat) (m :: Nat).
               (KnownNat n, KnownNat m, F n m) =>
               ()
 • In the expression: f @n @m
      In a case alternative: n -> f @n @m
      In the expression:
        case (natVal (Proxy @n)) of
          0 -> ()
          n -> f @n @m
    |
168 |     n -> f @n @m
    |          ^^^^^^^

Answer 1

您的模式匹配不产生任何约束的主要原因是您在natVal (Proxy @n) :: Integer 上进行大小写匹配，这不是 GADT。根据@chi 的回答，您需要在 GADT 上进行匹配才能将类型信息纳入范围。

对于您的类型系列的略微修改版本：

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

你要做到这一点的方式是：

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

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

此案例匹配 GADT 以在 Just Refl 分支中引入约束 n ~ 0。这允许将类型族F n m 解析为m ~ 0。请注意，我已经删除了无关的 KnownNat 约束；这有点重要，因为@chi 的回答表明，如果g 的类型签名中有KnownNat m 约束可用，您的问题很容易解决。毕竟如果m是已知的，那么你可以直接判断它是否是0，而F m n约束是多余的，不管m和n的值如何。

不幸的是，对于条件翻转的原始类型族：

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

事情变得更加困难。类型族是使用非常简单的“正向求解器”解析的，因为没有更好的术语，因此对于您的 F 版本，类型表达式 F n m 只能针对特定的 n 解析，例如 0或5。没有约束表示n 是除0 之外的未指定类型，您可以以某种方式使用它来解析F n m = (m ~ 0)。所以，你可以写：

g :: forall n m. (KnownNat n, F n m) => ()
g = case sameNat (Proxy @n) (Proxy @1) of
      Just Refl -> f @n @m
      Nothing -> ()

它使用了在Just Refl -> 分支中，约束n ~ 1 在允许F n m 被解析的范围内。但似乎没有办法让它适用于任意非零n。

有几种方法可行。改用 Peano naturals 可以解决问题：

data Nat = Z | S Nat
data SNat n where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)
class KnownNat n where
  natSing :: SNat n
instance KnownNat Z where natSing = SZ
instance KnownNat n => KnownNat (S n) where natSing = SS natSing

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

f :: forall n m. (m ~ Z) => ()
f = ()

g :: forall n m. (KnownNat n, F n m) => ()
g = case natSing @n of
  SZ -> ()
  SS n -> f @n @m

这里，SS n case 分支将约束 n ~ S n1 引入范围，确实表达了 n 是除 Z 之外的未指定自然值这一事实，允许我们解决类型族F n m = (m ~ Z)。

您还可以使用类型级别的条件来表示 F 约束：

type F n m = If (1 <=? n) (m ~ 0) (() :: Constraint)

然后写：

import Data.Kind
import Data.Proxy
import Data.Type.Equality
import Data.Type.Bool
import GHC.TypeLits
import Unsafe.Coerce

type F n m = If (1 <=? n) (m ~ 0) (() :: Constraint)

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

g :: forall n m. (KnownNat n, F n m) => ()
g = case leqNat (Proxy @1) (Proxy @n) of
  Just Refl -> f @n @m
  Nothing -> ()

leqNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe ((a <=? b) :~: True)
leqNat x y | natVal x <= natVal y = Just (unsafeCoerce Refl)
           | otherwise            = Nothing

这里，函数leqNat 提供了适当的类型级别证据，证明一个值小于或等于另一个值。它可能看起来像作弊，但如果你将它与definition of sameNat 进行比较，你会发现这是一种常见的作弊。