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

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 以n ~ 0在Just Refl分支中引入约束。这允许将类型系列F n m解析为m ~ 0. 请注意，我已经删除了无关紧要的KnownNat约束；这有点重要，因为@chi 的回答表明，如果您有一个KnownNat m在g的类型签名中可用约束。毕竟，如果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 自然色可以解决这个问题：

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 ncase 分支将约束引入范围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提供了一个值小于或等于另一个值的适当类型级证据。它可能看起来像作弊，但如果将其与 的定义sameNat进行比较，您会发现这是一种常见的作弊。