Index into an HList by another

Ix.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnicodeSyntax #-}


import           GHC.TypeLits
import           GHC.Types

data Ix i where
  Z ∷     x → Ix (x : xs)
  S ∷ Ix xs → Ix (x : xs)

data Ixee t where
  Cons ∷ x → Ixee xs → Ixee (x : xs)
  Nil  ∷ Ixee '[]

type family Index ixee ix where
  Index (Ixee (x:_))  (Ix (y:'[])) = x
  Index (Ixee (_:xs)) (Ix (_:ys))  = Index (Ixee xs) (Ix ys)

index ∷    Ixee xs
  →                  Ix ys
  → Index (Ixee xs) (Ix ys)
index (Cons x _)           (Z _)  = x
index (Cons _ (Cons x xs)) (S ss) = index (Cons x xs) ss

--
-- Fails (due to stuck type families) with:
--
Ix.hs:26:37: error:
    • Could not deduce: Index (Ixee (x : xs1)) (Ix (x1 : xs2)) ~ x
      from the context: xs ~ (x : xs1)
        bound by a pattern with constructor:
                   Cons :: forall x (xs :: [*]). x -> Ixee xs -> Ixee (x : xs),
                 in an equation for ‘index’
        at Ix.hs:26:8-15
      or from: ys ~ (x1 : xs2)
        bound by a pattern with constructor:
                   Z :: forall x (xs :: [*]). x -> Ix (x : xs),
                 in an equation for ‘index’
        at Ix.hs:26:29-31
      ‘x’ is a rigid type variable bound by
        a pattern with constructor:
          Cons :: forall x (xs :: [*]). x -> Ixee xs -> Ixee (x : xs),
        in an equation for ‘index’
        at Ix.hs:26:8-15
      Expected type: Index (Ixee xs) (Ix ys)
        Actual type: x
    • In the expression: x
      In an equation for ‘index’: index (Cons x _) (Z _) = x
    • Relevant bindings include x :: x (bound at Example.hs:26:13)
   |
26 | index (Cons x _)           (Z _)  = x
   |                                     ^

Ix.hs:27:37: error:
    • Could not deduce: Index (Ixee (x1 : xs2)) (Ix xs3)
                        ~ Index (Ixee (x : x1 : xs2)) (Ix (x2 : xs3))
      from the context: xs ~ (x : xs1)
        bound by a pattern with constructor:
                   Cons :: forall x (xs :: [*]). x -> Ixee xs -> Ixee (x : xs),
                 in an equation for ‘index’
        at Ix.hs:27:8-25
      or from: xs1 ~ (x1 : xs2)
        bound by a pattern with constructor:
                   Cons :: forall x (xs :: [*]). x -> Ixee xs -> Ixee (x : xs),
                 in an equation for ‘index’
        at Ix.hs:27:16-24
      or from: ys ~ (x2 : xs3)
        bound by a pattern with constructor:
                   S :: forall (xs :: [*]) x. Ix xs -> Ix (x : xs),
                 in an equation for ‘index’
        at Ix.hs:27:29-32
      Expected type: Index (Ixee xs) (Ix ys)
        Actual type: Index (Ixee (x1 : xs2)) (Ix xs3)
      NB: ‘Index’ is a non-injective type family
    • In the expression: index (Cons x xs) ss
      In an equation for ‘index’:
          index (Cons _ (Cons x xs)) (S ss) = index (Cons x xs) ss
    • Relevant bindings include
        ss :: Ix xs3 (bound at Ix.hs:27:31)
        xs :: Ixee xs2 (bound at Ix.hs:27:23)
        x :: x1 (bound at Ix.hs:27:21)
   |
27 | index (Cons _ (Cons x xs)) (S ss) = index (Cons x xs) ss
   |                                     ^^^^^^^^^^^^^^^^^^^^