The following code fails to compile:

{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, KindSignatures, GADTs, TypeOperators
 #-}

data Nat = Zero | Succ Nat

type family Sing (a :: k) :: k -> *

data SNat n where
  SZero :: SNat Zero
  SSucc :: SNat n -> SNat (Succ n)

data SList (a :: [k]) where
  SNil :: SList '[]
  SCons :: Sing h h -> SList t -> SList (h ': t)

type instance Sing (a :: Nat) = SNat
type instance Sing (a :: [k]) = SList

term :: SList '[ '[Zero], '[]]
term = SCons (SCons SZero SNil) (SCons SNil SNil)

The error generated is

/Users/rae/temp/Scratch.hs:27:15:
    Couldn't match type `Sing [Nat] ((':) Nat 'Zero ('[] Nat))'
                  with `SList Nat'
    Expected type: Sing
                     [Nat] ((':) Nat 'Zero ('[] Nat)) ((':) Nat 'Zero ('[] Nat))
      Actual type: SList Nat ((':) Nat 'Zero ('[] Nat))
    In the return type of a call of `SCons'
    In the first argument of `SCons', namely `(SCons SZero SNil)'
    In the expression: SCons (SCons SZero SNil) (SCons SNil SNil)

/Users/rae/temp/Scratch.hs:27:40:
    Couldn't match type `Sing [Nat] ('[] Nat)' with `SList Nat'
    Expected type: Sing [Nat] ('[] Nat) ('[] Nat)
      Actual type: SList Nat ('[] Nat)
    In the first argument of `SCons', namely `SNil'
    In the second argument of `SCons', namely `(SCons SNil SNil)'
    In the expression: SCons (SCons SZero SNil) (SCons SNil SNil)

It seems that the Sing kind-indexed type family isn't quite working. My guess is that the problem is that we really want, say, Sing '[Zero] to be SList Nat, where Nat is the implicit kind parameter to SList. But, we can't say that. I would hope that the explicit kind annotation on the result of Sing would fix the implicit kind parameter to SList, but it doesn't seem to.

This was tested on 7.5.20120420.