GHC gives the error:
Couldn't match expected type `T f1 f1 a' against inferred type `T f f a' In the expression: blah x In the definition of `wrapper': wrapper x = blah x
actually, GHC gives me "could not deduce Blah f a from Blah f1 a" first. It seems that desugaring type function notation into an additional constraint helps, so there's something odd going on: class Blah f a where blah :: a -> T f f a class A f where type T f :: (* -> *) -> * -> * wrapper :: forall a f tf . (Blah f a,T f~tf) => a -> tf f a wrapper x = blah x You're relying on that second f to determine the first, which then allows T f to determine tf f a. Looks a bit like cyclic programming at the type level?-) Whereas the desugared view is that we may not know the type constructor tf yet, but whatever it is, its first parameter fixes f. Yet another take on it: tf, the result of T f f a, needs to be determined by the context, rather than the type function, and type functions are traditionally bad at reasoning backwards. The extra indirection separates determining f from applying T f. I think I'd prefer if that naive desugaring of type function always worked, without such differences. Worth a ticket? Claus