我正在尝试使用类型族来生成依赖于某种类型级别的自然约束数字这里有这样一个函数：
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
| ^^^^^^^
模式匹配不产生任何约束的主要原因是您在不是GADT的natVal (Proxy @n) :: Integer上进行大小写匹配。根据@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事例分支将约束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的定义进行比较，你会发现这是常见的作弊。