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

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。请注意，我已经删除了无关的KnonNat约束；这有点重要，因为@chi的答案表明，如果您在g的类型签名中有一个KnonNat m约束，您的问题很容易解决。毕竟，如果已知m，那么您可以直接确定它是否为0，并且无论m和n的值如何，F 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，您可以用它来解析fnnm=（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 -> ()

它使用的事实是，在<代码>只是Refl-

有几种方法可以奏效。改用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 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的定义进行比较，你会发现这是常见的作弊。