The following code fails to compile:

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

data family Sing (a :: k)

data instance Sing (a :: Maybe k) where
  SNothing :: Sing 'Nothing
  SJust :: Sing b -> Sing ('Just b)

The error is

    Data constructor `SNothing' returns type `Sing
                                                (Maybe k0) ('Nothing k0)'
      instead of an instance of its parent type `Sing (Maybe k) a'
    In the definition of data constructor `SNothing'
    In the data instance declaration for `Sing'

It seems that the k kind parameter is not being allowed to generalize over other kind parameters. The following (seemingly equivalent) formulation compiles:

{-# LANGUAGE ..., ExistentialQuantification #-}

data instance Sing (a :: Maybe k) =
    a ~ 'Nothing => SNothing
  | forall b. a ~ 'Just b => SJust (Sing b)

This was tested on 7.5.20120420.