Data constructor ‘SfSwitch’ cannot be GADT-like in its *kind* arguments

FailArz.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE GADTs #-}

data Sv u where
  E :: u -> Sv u
  S :: u -> Sv u

data Sf (coupled :: Bool)
         (f :: u -> *)
         (a :: [Sv u])
         (b :: [Sv u]) :: * where

  SfSwitch
    :: Sf cp f a (E e ': b) ->
       (e -> Sf cp f a b) ->
       Sf cp f a b

-- FailArz.hs:15:3: Data constructor ‘SfSwitch’ cannot be GADT-like in its *kind* arguments
--       SfSwitch :: forall (cp :: Bool)
--                          (f :: * -> *)
--                          (a :: [Sv *])
--                          (b :: [Sv *])
--                          e.
--                   Sf cp f a ('E e : b) -> (e -> Sf cp f a b) -> Sf cp f a b
--     In the definition of data constructor ‘SfSwitch’
--     In the data declaration for ‘Sf’
-- Compilation failed.