Store argument well formed-ness constraints in Data constructor representation type

[fxdpntthm]

Consider our favorite data Ord a => BST a :: L | N a (T a) (T a)
And a wrapper datatype data WD a = MkWD (BST a)

we currently store MkWD :: BST a -> WD a but in ideal world we would like to store MkWD :: BST @ a => BST a -> WD a. This will potentially enable short circuiting the solver to reuse the dictionaries eg:

f :: Ord a => a -> T a -> T a
f a (MkWD t)= MkWD (insert a t) 

[fxdpntthm]

Possible issue with engineering.
datacon context, type arguments are all knot tied, so elaborating it will be troublesome.
Currently we use the stupid_theta route, were we just drop them while compiling to core.