Is type equality preserved across application in Haskell?

Question

In haskell, does s k v ~ s1 k1 v1, where s :: * -> * -> *, imply that k ~ k1, v ~ v1, or s ~ s1? If not, why doesn't it?

I encountered this when writing some experimental code, a small piece of which is:

newtype Article = Article String
newtype ArticleId = ArticleId Int
newtype Comment = Comment String
newtype CommentId = CommentId Int

data TableName k v where
    Articles :: TableName ArticleId Article
    Comments :: TableName CommentId Comment    

data CRUD k v r where
    Create :: v -> CRUD k v k
    Read :: k -> CRUD k v (Maybe v)

data Operation t r where
    Operation :: s k v -> CRUD k v r -> Operation (s k v) r        

operatesOn :: (Eq (s k v)) => s k v -> Operation (s k v) r -> Bool
operatesOn tableName1 (Operation tableName2 _) = tableName1 == tableName2 

Which doesn't compile due to the following error:

Could not deduce (v1 ~ v)
from the context (Eq (s k v))
  bound by the type signature for
             operatesOn :: Eq (s k v) => s k v -> Operation (s k v) r -> Bool
or from (s k v ~ s1 k1 v1)
  bound by a pattern with constructor
             Operation :: forall r (s :: * -> * -> *) k v.
                          s k v -> CRUD k v r -> Operation (s k v) r,
           in an equation for `operatesOn'
  `v1' is a rigid type variable bound by
       a pattern with constructor
         Operation :: forall r (s :: * -> * -> *) k v.
                      s k v -> CRUD k v r -> Operation (s k v) r,
       in an equation for `operatesOn'
       at src\Example\Error.hs:44:24
  `v' is a rigid type variable bound by
      the type signature for
        operatesOn :: Eq (s k v) => s k v -> Operation (s k v) r -> Bool
      at src\Example\Error.hs:43:15
Expected type: s k v
  Actual type: s1 k1 v1
In the second argument of `(==)', namely `tableName2'
In the expression: tableName1 == tableName2
In an equation for `operatesOn':
    operatesOn tableName1 (Operation tableName2 _)
      = tableName1 == tableName2

Answer 1

If I change the definition of Operation to

data Operation t r where
    Operation :: (t ~ s k v) => t -> CRUD k v r -> Operation t r

The operatesOn function will compile, similar to how it did for Maybe

The (t ~ s k v) => constraint(?) will still reject incorrect programs like:

doesntCompile = Operation Article $ Create $ Comment "Yo"