Dear 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. But given that this is the place where I know many GHC devs look at, I'll just try :)

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.

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe