It is quite likely that the error that you are getting with approach 2 is because when you are constructing the `Combinator` value, there is not enough type information to figure out how to solve the constraint (and it sounds like this happens because there is not enough type information to reduce the type function). The fix depends on the concrete program but it might be something as simple as adding a type signature somewhere.

Note, again, that it is not sufficient to know that the constraint could be solved for any type of the appropriate kind: we need to actually solve the constraint so that we can determine what the program should do.

The difference between the two `data` definitions is that the second one uses a technique called _existential quantification_, which "hides" the type `s`. If this type appears nowhere else in the surrounding expressions and the constraint could not be solved, then the constraint is ambiguous. I could explain that in more detail, if it is unclear please ask.

Happy hacking,

-Iavor

On Thu, May 17, 2012 at 4:18 AM, Serguey Zefirov <sergueyz@gmail.com> wrote:

I can write something like that:

data Combinator s a where
Combinator :: Class (TypeFamExpr s) => ... -> Combinator s a

And I cannot write something like that:
data Combinator a where
Combinator :: Class (TypeFamExpr s) => .mentions s.. -> Combinator a

If my TypeFamExpr does have type variables, I get a wild type error
messages that mentions partially computed TypeFamExpr as an argument
to constraint.