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

Question

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

Compilation Snd.hsworks, but compilation NoSnd.hsgives

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.hsand NoSnd.hsis that in the latter case, instead of defining a type family, SndI try to directly destroy types. This happens in two places: definition MapSndand type (to parameter) hmap2.

Two questions: can someone explain a type error; and is there a way to write hmap2without defining a type family Snd?

Thank.

Answer 1

Statement

exists a. x ~ '(a, b)

a little stronger than a statement

b ~ Snd x

For example, given

type family Any :: (*, *) where {}

,

Snd Any ~ Snd Any

exists a. Any ~ '(a, Snd Any)

Any .

HList , (*,*), , '(a,b), , . , , , , , . , , . () , . . , f, . !