《Thinking With Types》中HList的Eq实例报错问题求助

问题背景 #

在Sandy Maguire所著《Thinking With Types》第69页的代码中，尝试为HList实现Eq实例时遇到编译错误。

原始代码 #

HList定义：

data HList (ts :: [Type]) where
  HNil :: HList '[]
  (:#) :: t -> HList ts -> HList (t ': ts)
infixr 5 :#

尝试实现的Eq实例：

{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE InstanceSigs #-}

instance (Eq t, Eq (HList ts)) => Eq (HList (t ': ts)) where 
  (a :# as) == (b :# bs) = a == b && as == bs 

第一次编译错误 #

• Couldn't match expected type ‘t1’ with actual type ‘t2’
      ‘t2’ is a rigid type variable bound by
        a pattern with constructor:
          :# :: forall t (ts :: [Type]) t'.
                t -> HList ts -> HList ((':) @Type t' ts),
        in an equation for ‘==’
        at src/Types/ChapterFive.hs:41:17-23
      ‘t1’ is a rigid type variable bound by
        a pattern with constructor:
          :# :: forall t (ts :: [Type]) t'.
                t -> HList ts -> HList ((':) @Type t' ts),
        in an equation for ‘==’
        at src/Types/ChapterFive.hs:41:4-10
    • In the second argument of ‘(==)’, namely ‘b’
      In the first argument of ‘(&&)’, namely ‘a == b’
      In the expression: a == b && as == bs
    • Relevant bindings include
        b :: t2 (bound at src/Types/ChapterFive.hs:41:17)
        a :: t1 (bound at src/Types/ChapterFive.hs:41:4)
   |
41 |   (a :# as) == (b :# bs) = a == b && as == bs 

添加显式签名后的错误 #

修改后的代码：

instance (Eq t, Eq (HList ts)) => Eq (HList (t ': ts)) where 
  (==) :: forall t (ts :: [Type]).(Eq t, Eq (HList ts)) => HList ((':) @Type t ts) -> HList ((':) @Type t ts) -> Bool
  (a :# as) == (b :# bs) = a == b && as == bs 

错误信息：

Operator applied to too few arguments: :
   |
41 |   (==) :: forall t (ts :: [Type]).(Eq t, Eq (HList ts)) => HList ((':) @Type t ts) -> HList ((':) @Type t ts) -> Bool

再次修改后的错误 #

修改代码为：

instance (Eq t, Eq (HList ts)) => Eq (HList (t ': ts)) where 
  (==) :: forall t (ts :: [Type]).(Eq t, Eq (HList ts)) => HList ((:#) @Type t ts) -> HList ((:#) @Type t ts) -> Bool
  (a :# as) == (b :# bs) = a == b && as == bs 

错误信息：

src/Types/ChapterFive.hs:41:107: error:
    • Expected kind ‘HList ts1’, but ‘ts’ has kind ‘[Type]’
    • In the third argument of ‘(:#)’, namely ‘ts’
      In the first argument of ‘HList’, namely ‘((:#) @Type t ts)’
      In the type signature:
        (==) :: forall t (ts :: [Type]). (Eq t, Eq (HList ts)) =>
                                         HList ((:#) @Type t ts) -> HList ((:#) @Type t ts) -> Bool
   |
41 |   (==) :: forall t (ts :: [Type]).(Eq t, Eq (HList ts)) => HList ((:#) @Type t ts) -> HList ((:#) @Type t ts) -> Bool

错误原因 #

1. 首次错误核心：GHC无法关联两个:#模式中的类型变量t——GADT模式匹配会引入独立的刚性类型变量，默认无法确认它们是同一类型。
2. 显式签名错误：
   • 第一种错误是类型语法误用，(':) @Type t ts写法冗余且易触发语法解析问题，正确类型列表写法应为t ': ts。
   • 第二种错误混淆了值构造器:#和类型构造器(:)，:#是值层面的构造器，不能用于类型表达式。

解决方法 #

方案1：带InstanceSigs的正确实现 #

启用ScopedTypeVariables绑定实例的类型变量，确保模式匹配的类型一致性：

{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE InstanceSigs #-}

-- 先定义空列表的Eq实例
instance Eq (HList '[]) where
  HNil == HNil = True

-- 带作用域类型变量的实例
instance forall t ts. (Eq t, Eq (HList ts)) => Eq (HList (t ': ts)) where 
  (==) :: HList (t ': ts) -> HList (t ': ts) -> Bool
  (a :# as) == (b :# bs) = a == b && as == bs

方案2：无InstanceSigs的简化实现 #

去掉InstanceSigs，依赖GHC自动推断类型，同样需要ScopedTypeVariables：

{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

instance Eq (HList '[]) where
  HNil == HNil = True

instance (Eq t, Eq (HList ts)) => Eq (HList (t ': ts)) where 
  (a :# as) == (b :# bs) = a == b && as == bs

关键说明 #

• 必须先定义HList '[]的Eq实例，作为递归终止条件。
• ScopedTypeVariables让实例头部的t和ts能在方法中被引用，确保两个:#模式的t是同一类型，解决类型不匹配问题。
• 使用InstanceSigs时，方法签名无需重复forall和约束，实例头部已提供这些信息。

内容的提问来源于stack exchange，提问作者Michael Litchard