Quantified constraints which specify associated type instances

I have come across a situation which I believe could benefit from the ability to refine quantified constraints by adding constraints on the associated type instance declarations. For instance, consider a class with an associated type:

class C a where
  type T a :: Type
  ...

From what I understand, a quantified constraint of the form ( forall a. C a => C (f a) ) will be soluble when there is an instance of the form

instance forall a. C a => C (f a)

My suggestion is to provide the ability to specify quantified constraints which restrict the associated type family instance declarations. In this case, we might want to insist upon the equation type T (f a) = f (T a). One possible notation would use tuple and equality constraints (mirroring how one would encode this using Dict):

forall a. C a => ( C (f a), T (f a) ~ f (T a) )

In solving this quantified constraint, we would discard all class instances which are not of the following form:

instance forall a. C a => C (f a) where
  type T (f a) = f (T a)

(I don't know how flexible we can afford to be in verifying this property, e.g. if the type family instance equations are not exactly as specified by the equality constraint but are equivalent to them, say after applying substitutions or using other equality constraints that might be available.)

Example

To illustrate, I was working with the Syntactic type class

class Syntactic a where
  type Internal a
  toAST :: a -> AST (Internal a)
  fromAST :: AST (Internal a) -> a

and I wanted to restrict attention to functors F that are compatible with this type class, i.e. which have an instance declaration of the form

instance Syntactic a => Syntactic (F a) where
  type Internal (F a) = F (Internal a)

However, while I can write a quantified constraint forall a. Syntactic a => Syntactic (f a), I cannot specify the additional requirement on the associated type family instance equation, so GHC will complain at use-sites:

* Could not deduce: Internal (f a) ~ f (Internal a)

This can be worked around using Dict ( Syntactic (f a), Internal (f a) ~ f (Internal a) ), unfortunately forgoing the use of quantified constraints and introducing indirections (requiring matching on Dict to make the instances visible to GHC). Other than that I don't know of any tricks to bypass this limitation, but I may well be missing something (quite likely, as I don't have much experience with quantified constraints).