Type family evaluation in dependent kind signature

Question

Consider the following:

type Nat :: Type
data Nat = Z | S Nat

type Fin :: Nat -> Type
data Fin n
  where
  FZ :: Fin ('S n)
  FS :: Fin n -> Fin ('S n)

type Length :: [k] -> Nat
type family Length xs
  where
  Length '[] = 'Z
  Length (_ ': xs) = Length xs

Given all this, it seems like it should be possible to define a type level function that maps a type level list and an index smaller than its length to the type stored at the corresponding position.

type Get :: forall k. forall (l :: [k]) -> Fin (Length l) -> k
type family Get l i
  where
  Get (x ': xs) 'FZ = x
  Get (_ ': xs) ('FS i) = Get xs i

But this blows up with the following error:

• Illegal type synonym family application ‘Length @k xs’ in instance:
    Get @k ((':) @k x xs) ('FZ @(Length @k xs))
• In the equations for closed type family ‘Get’
  In the type family declaration for ‘Get’

So it seems GHC is not happy with the evaluation of the Length type family in the dependent kind signature. Is there some way to convince GHC that it's OK to define such a function? Alternatively, is there some workaround I can use to describe the dependently-kinded operation of indexing into a type level list?

Answer 1

I'm personally not aware of a way to make this work (hoping someone else is). That said, we can work around the need to evaluate a type family in the kind signature if we absorb Length into the definition of Fin. In other words, we can create a special purpose indexing type for lists that mirrors Fin (Length l):

type Index :: [k] -> Type
data Index xs
  where
  Head :: Index (x ': xs)
  Next :: Index xs -> Index (x ': xs)

Now we can use that to write a variation of Get:

type Get :: forall k. forall (l :: [k]) -> Index l -> k
type family Get l i
  where
  Get (x ': xs) 'Head = x
  Get (_ ': xs) ('Next i) = Get xs i

Which seems to work:

type Test = Get '[Int, String, Bool] (Next (Next Head))

> :k! Test
Test :: *
= Bool

This approach is kind of gross and anti-compositional, but I suppose it works.