David Christiansen requested this, and I want to record it so I don't forget. What he wants to be able to do is say things like this in signatures:

signature A where

data T
data S
type family F a

instance T ~ S
instance F Int ~ S

This is currently rejected by GHC because you are not allowed to define instances of type equality. But really all this is saying is that the type equality must hold when we eventually implement the module; easy to check.