Adde:
Thanks, using pattern matching to avoid mentioning the type didn't even cross my mind. You are correct in assuming that I thought I could get away with "getConnection :: Connection c => Transaction c". To be honest, I still don't understand why it's too polymorphic. To me it says that it'll return a Transaction parameterised by a type confirming to the Connection interface, even though the concrete type is long lost.
That's not quite right. Replace "a type" with "any type" in that statement, and you'll be closer to the truth. There is an implicit "forall" (which can also be read as "for any") in front of any type with a free type variable, so you actually have: getConnection :: forall c. Connection c => Transaction c Universally ("forall")-quantified type variables are resolved through unification with the context (in this case, by the caller of getConnection). If we had an "exists" quantifier, then you might be able to read an existentially-quantified type variable as a placeholder for some type that you know exists, but where you don't know the concrete type. This seems to be the way you are reading the type you want to give to getConnection. If you still don't see the difference between universal and existstential quantification, try substituting "any type the caller wants" in place of "a type" in your statement about the type. Of course, we can't give the caller any type it wants, even if the caller is limited to types conforming to the Connection class. We would only be able to give it the concrete type that was originally wrapped in the TransactionT, except for the fact we've forgotten what that type is. Since we don't have an "exists" quantifier, there is a common transformation used to convert to "forall" quantification. Martin demonstrated the transformation with his "withConnection". What Martin didn't mention is that "withConnection" is rank-2 polymorphic, and that can be a whole world of fun of its own. :-)