GHC 错误消息逐字引用类型族定义

Question

下面的代码会产生一条错误消息，乍一看，这似乎暗示 GHC 不理解类型系列 WrapParams 的定义：

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits( Nat, type (-) )
import Data.Kind( Type )

newtype Wrapped a = Wrapped a

-- |
-- E.g., `WrapParams 2 (Int -> String -> Bool)` is `Wrapped Int -> Wrapped String -> Bool`
--
type family WrapParams (n :: Nat) (f :: Type) where
  WrapParams 0 f = f
  WrapParams n (p -> f) = Wrapped p -> WrapParams (n - 1) f


-- |
-- E.g., `extendToWrappedParams @2 (+) (Wrapped 1) (wrapped 2)` is supposed to be 3.
--
class ExtendToWrappedParams (n :: Nat) (f :: Type)  where
  extendToWrappedParams :: f -> WrapParams n f

instance ExtendToWrappedParams 0 t where
  extendToWrappedParams t = t

instance (ExtendToWrappedParams (n - 1) f) => ExtendToWrappedParams n (p -> f) where
  extendToWrappedParams g = h
    where
      h (Wrapped p) = extendToWrappedParams @(n - 1) @f (g p)

（使用 GHC 8.10.7）：

• Couldn't match expected type ‘WrapParams n (p -> f)’
              with actual type ‘Wrapped p -> WrapParams (n - 1) f’
• In the expression: h
  In an equation for ‘extendToWrappedParams’:
      extendToWrappedParams g
        = h
        where
            h (Wrapped p) = extendToWrappedParams @(n - 1) @f (g p)
  In the instance declaration for ‘ExtendToWrappedParams n (p -> f)’

这是错误 前两行逐字引用了 WrapParams 的定义，给人的印象是 GHC 不知何故不理解它。显然，这不可能是实际发生的事情 - 那么，我错过了什么？有没有什么方法（除了诉诸unsafeCoerce）来编译上面的代码？

Answer 1

WrapParams n (p -> f) 等于 Wrapped p -> f WrapParams (n - 1) f 仅当 n 不为 0 时。在 Haskell 中没有直接的方法来表达不平等。通常的解决方法包括切换到 Peano 自然数，或分支布尔比较 (Data.Type.Equality.==)，而不是在 Nat 上进行模式匹配，这样您就可以编写 (n == 0) ~ 'False 作为约束。