(Cross-posted from Haskell-Café) I don't know if this is the best forum to ask questions about the OutsideIn(X) paper that lies below type inference in GHC. Any way, I sent it to Haskell-café and was advised to send it here also. My question related about the proof of soundness and principality, specifically Lemma 7.2 (to be found in page 67). In that lemma, it's stated that QQ and \phi' Q_q ||- \phi Q_w <-> \phi' Q_w'. I'm trying to recover the proof (which is omitted in the text), but I stumble upon a wall when trying to work out what happens in the case an axiom is applied. In particular, I'm playing with an example where QQ (the set of axioms) = { forall. C a => D a } (where C and D are one-parameter type classes) Q_q = { } Q_w = { D Int } Thus, if I apply the rule DINSTW (to be found in page 65), I get a new Q_w' = { C Int } Now, if the lemma 7.2 is true, it should be the case that (1) QQ ||- C Int <-> D Int which in particular means that I have the two implications (2) { forall. C a => D a, C Int } ||- D Int (3) { forall. C a => D a, D Int } ||- C Int (2) follows easily by applying the AXIOM rule of ||- (as shown in page 54). However, I don't see how to make (3) work :( I think that understanding this example will be key for my understanding of the whole system. Anybody could point to the error in my reasoning or to places where I could find more information? Thanks in advance.