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

只有当 n 不是 0 时，

WrapParams n (p -> f) 才等于 Wrapped p -> WrapParams (n - 1) f。 Haskell 中没有直接表达不等式的方法。通常的解决方法包括切换到 Peano naturals，或在 Nat 上分支布尔比较 (Data.Type.Equality.==) 而不是 pattern-matching，因此您可以将 (n == 0) ~ 'False 写为约束。

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

GHC error message quotes type family definition verbatim

haskell

ghc

type-families