| > Yes, (1-GHC) certainly contradicts the FD paper that Martin and I wrote. | > I think (1) should be: | > | > (1-fixed) Each assertion in the context must constrain type | > variables, and | > those type variables must all be mentioned in the head. | > | > That is, there is no requirement that the type variables should be | > distinct (they can be repeated). But they must all appear in the HEAD. | | Ah, but you added the no-repetition requirement a few weeks ago in | response to the example | | class C a b | instance C b b => C (Maybe a) b Oh yes. And in fact I now remember that this is a bug in the paper: the Basic Conditions should require *distinct* type variables. So I take back that bit. Simon