Data Constructor promotion in GHC-7.6

You didn’t say which version of GHC 7.6 you were using or include which extensions you have on, so I’m guessing a bit.

This ticket seems to answer your question 1, although I don’t totally understand the problem myself. In your particular example, I think SSet isn’t promotable because one of its arguments (Symbol tpe) is an associated type which brings with it the SymbolSet constraint.

If I move Symbol out of the class we get the type promoted, however now we get kind mismatch errors:

{-# LANGUAGE DataKinds , TypeFamilies , GADTs , MultiParamTypeClasses #-}
class SymbolSet tpe where
  -- data Symbol tpe :: *
data Symbol tpe :: *
-- ...

I can get the whole shebang to compile by adding kind signatures to HasElem:

{-# LANGUAGE DataKinds , TypeFamilies , GADTs , MultiParamTypeClasses, FlexibleInstances  #-}
class SymbolSet tpe where
-- MOVED OUT OF CLASS:
data Symbol tpe :: *

data SSet tpe where
  Identity :: tpe -> SSet tpe
  And :: SSet tpe -> Symbol tpe -> SSet tpe

-- ADDED KIND SIGNATURES:
class HasElem (a :: SSet *) (b :: Symbol *) where

instance (SymbolSet tpe) => HasElem (And (Identity tpe) s) s
instance (HasElem sset s) => HasElem (And sset s) s

I don’t really understand your code so that may not work for you.