Let’s assume you have this code:

```
data HList :: [*] -> * where
Cons :: p -> HList a -> HList (p ': a)
End :: HList '[]
-- convinience to not write explicit signature
class CBottom
type CSat = () :: Constraint
type CNSat = CBottom
type ConstStr = '[Char]
data Pair a b where
MkPair :: a -> b -> Pair a b
-- Check if hlist have all elements of type Pair '[Char] Type
type family RecurseAndCheck a (b :: HList t) where
RecurseAndCheck a End = CSat
RecurseAndCheck a (Cons (b :: a) r) = RecurseAndCheck a r
RecurseAndCheck a (Cons (b :: m) r) = CNSat
-- Any hlist that is constructed from Pairs of (ConstStr, Type) is a TypeClass
class (forall t p (a :: HList t) . RecurseAndCheck (Pair ConstStr p) a)
=> TypeClass a where
retrieve :: a -> (s :: ConstStr) -> Pair a s
```

Unfortunately, compiler shows me a horrible error:

`Occurs check: cannot construct the infinite kind: t ~ a : t • In the second argument of ‘RecurseAndCheck’, namely ‘(Cons (b :: a) r)’`

So two questions:

- What can I do to vanquish the error?
- Do you see anything awkward in this code?