OutsideIn(X) question

[Alejandro Serrano Mena]

(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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20140227/5e343c0c/attachment.html>