Why can't I get this code to work, typed verbatim from "Thinking With Types"

In Sandy Maguire’s "Thinking With Types", Page 69, there is the following code

{-# 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

The definition of HList is

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

The above instance produces the following error

    • 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

So, I tried giving it an explicit type

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

But this produces a new error

    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

I tried changing the code as follows

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

This yielded the following error

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

>Solution :

I get this working when writing the GADT as:

data HList (ts :: [*]) where
  HNil :: HList '[]
  (:#) :: t-> HList ts -> HList(t ': ts)  -- 🖘 space between t and ':
infixr 5 :#

otherwise it is probably interpreted as t' followed by :.

In order to let this work, you should also makes HNil an instance of Eq:

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

Leave a Reply