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:1723
‘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:410
• 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