Is there a way to use type-level pattern matching rather than defining a type family

Consider the following 3 Haskell files

HList.hs

{-# LANGUAGE DataKinds     #-}
{-# LANGUAGE GADTs         #-}
{-# LANGUAGE PolyKinds     #-}
{-# LANGUAGE TypeOperators #-}
module HList where

data HList :: (k -> *) -> [k] -> * where
  Nil :: HList f '[]
  (:&) :: !(f x) -> HList f xr -> HList f (x ': xr)

Snd.hs

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeOperators       #-}
module Snd where

import           HList

hmap :: forall f g xs. (forall x. f x -> g x) -> HList f xs -> HList g xs
hmap f = go

  where
    go :: HList f xs' -> HList g xs'
    go Nil       = Nil
    go (x :& xs) = f x :& go xs

type family Snd x where
  Snd '(a, b) = b

type family MapSnd xs where
  MapSnd '[] = '[]
  MapSnd (y ': ys) = Snd y ': MapSnd ys

hmap2 :: forall f g (xs :: [(*,*)]). (forall x. f x -> g (Snd x)) -> HList f xs -> HList g (MapSnd xs)
hmap2 f = go
  where
    go :: HList f xs' -> HList g (MapSnd xs')
    go Nil       = Nil
    go (x :& xs) = f x :& go xs

NoSnd.hs

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeOperators       #-}
module NoSnd where

import           HList

hmap :: forall f g xs. (forall x. f x -> g x) -> HList f xs -> HList g xs
hmap f = go
  where
    go :: HList f xs' -> HList g xs'
    go Nil       = Nil
    go (x :& xs) = f x :& go xs

type family MapSnd xs where
  MapSnd '[] = '[]
  MapSnd ('(_, y) ': ys) = y ': MapSnd ys

hmap2 :: forall f g (xs :: [(*,*)]). (forall x a b. (x ~ '(a, b)) => f x -> g b) -> HList f xs -> HList g (MapSnd xs)
hmap2 f = go
  where
    go :: HList f xs' -> HList g (MapSnd xs')
    go Nil       = Nil
    go (x :& xs) = f x :& go xs

Compiling Snd.hs works, but compiling NoSnd.hs gives

NoSnd.hs:27:20: error:
    • Could not deduce: x ~ '(a0, x0) arising from a use of ‘f’
      from the context: xs' ~ (x : xr)
        bound by a pattern with constructor:
                   :& :: forall k (a :: k -> *) (x :: k) (xr :: [k]).
                         a x -> HList a xr -> HList a (x : xr),
                 in an equation for ‘go’
        at NoSnd.hs:27:9-15
      ‘x’ is a rigid type variable bound by
        a pattern with constructor:
          :& :: forall k (a :: k -> *) (x :: k) (xr :: [k]).
                a x -> HList a xr -> HList a (x : xr),
        in an equation for ‘go’
        at NoSnd.hs:27:9
    • In the first argument of ‘(:&)’, namely ‘f x’
      In the expression: f x :& go xs
      In an equation for ‘go’: go (x :& xs) = f x :& go xs
    • Relevant bindings include x :: f x (bound at NoSnd.hs:27:9)

The difference between Snd.hs and NoSnd.hs is that, in the latter, instead of defining a type family Snd, I try to destructure types directly. This happens in two places: the definition of MapSnd and the type of (the parameter to) hmap2.

The two questions are: can someone explain the type error; and is there a way to write hmap2 without defining a Snd type family?

Thank you.