Solver is too weak to solve wd constraints

[fxdpntthm]

consider

data m @ a => T m a = {.. }

and a top level definition

qqqq :: T m a -> ... 
qqqq (T f) = ...

now we have the following equations:

T @ m ~ ()
T m @ a ~ m @ a

Use of T will give rise to a m @ a constraint and elaboration of T m a will give us T @ m, T m @ a
however GHC solver is not smart enough to figure out that m @ a can be solved using T m @ a
This means we need to give an explicit v @ a constraint in qqqq for it to typecheck