Sequence over heterogeneous list in Haskell

Question

Consider following definition of a HList:

infixr 5 :>
data HList (types :: [*]) where
  HNil :: HList '[]
  (:>) :: a -> HList l -> HList (a:l)

And a type family Map to map over typelevel lists:

type family Map (f :: * -> *) (xs :: [*]) where
    Map f '[] = '[]
    Map f (x ': xs) = (f x) ': xs

Now I would like to define sequence equivalence for HLists. My attempt looks like

hSequence :: Applicative m => HList (Map m ins) -> m (HList ins)
hSequence HNil = pure HNil
hSequence (x :> rest) = (:>) <$> x <*> hSequence rest

But I get errors like this:

Could not deduce: ins ~ '[]
       from the context: Map m ins ~ '[]
         bound by a pattern with constructor: HNil :: HList '[]

For me it looks like the compiler isn't sure that if Map m returns [] on some list then the list is empty. Sadly, I don't see any way to convince it to that fact. What should I do in this situation?

---

I am using GHC 8.6.5 with following extensions:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

Answer 1

First, there's an error here:

type family Map (f :: * -> *) (xs :: [*]) where
    Map f '[] = '[]
    Map f (x ': xs) = (f x) ': Map f xs
                             --^^^^^-- we need this

After that is fixed, the issue here is that we need to proceed by induction on ins, not on Map f ins. To achieve that, we need a singleton type:

data SList :: [*] -> * where
    SNil  :: SList '[] 
    SCons :: SList zs -> SList ( z ': zs )

and then an additional argument:

hSequence :: Applicative m => SList ins -> HList (Map m ins) -> m (HList ins)
hSequence SNil         HNil        = pure HNil
hSequence (SCons ins') (x :> rest) = (:>) <$> x <*> hSequence ins' rest

This now compiles. Matching on SNil / SCons refines ins to either '[] or z ': zs, so Map m ins can be unfolded one step as well. This allows us to make the recursive call.

As usual, we can remove the additional singleton argument through a suitable typeclass. I'm reasonably sure that some of this can be automated exploiting the singletons library.

class SingList ins where
    singList :: SList ins

instance SingList '[] where
    singList = SNil

instance SingList zs => SingList (z ': zs) where
    singList = SCons singList

hSequence2 :: (Applicative m, SingList ins)
              => HList (Map m ins) -> m (HList ins)
hSequence2 = hSequence singList