<div dir="ltr">Hi Alejandro,<div><br></div><div>This is definitely a question for the Types forum: <span style="color:rgb(119,119,119);font-family:'normal arial',sans-serif;font-size:12px">types-list</span><span style="color:rgb(119,119,119);font-family:'normal arial',sans-serif;font-size:12px">@<a href="http://lists.seas.upenn.edu">lists.seas.upenn.edu</a></span></div>

<div>This list is research oriented, low traffic, and mostly read by people working on type theory. Threads are usually about questions in type theory papers just like yours.</div><div><br></div><div>Cheers,</div></div><div class="gmail_extra">

<br clear="all"><div>--  <br>Cp</div>
<br><br><div class="gmail_quote">On Wed, Feb 26, 2014 at 4:07 PM, Alejandro Serrano Mena <span dir="ltr"><<a href="mailto:trupill@gmail.com" target="_blank">trupill@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<div dir="ltr">Dear Haskell-café,<div>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 :)</div>



<div><br></div><div>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.</div>



<div><br></div><div>In particular, I'm playing with an example where</div><div><br></div><div>QQ (the set of axioms) = { forall. C a => D a } (where C and D are one-parameter type classes)</div><div>Q_q = { }</div>



<div>Q_w = { D Int }</div><div><br></div><div>Thus, if I apply the rule DINSTW (to be found in page 65), I get a new</div><div><br></div><div>Q_w' = { C Int }</div><div><br></div><div>Now, if the lemma 7.2 is true, it should be the case that </div>



<div><br></div><div>(1)  QQ ||- C Int <-> D Int</div><div><br></div><div>which in particular means that I have the two implications</div><div><br></div><div>(2)  { forall. C a => D a, C Int } ||- D Int</div><div>



(3)  { forall. C a => D a, D Int } ||- C Int<br></div><div><br></div><div>(2) follows easily by applying the AXIOM rule of ||- (as shown in page 54). However, I don't see how to make (3) work :(</div><div>I think that understanding this example will be key for my understanding of the whole system.</div>



<div><br></div><div>Anybody could point to the error in my reasoning or to places where I could find more information?</div><div>Thanks in advance.</div></div>
<br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br></div>