<div dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="gmail_default" style="font-family:tahoma,sans-serif">
3.1: OK, so if the case branch introduces type-class constraints,
but not equality constraints, then the unification variables from
an outer level are still touchable? Presumably because the
type-class constraints don't interact with the equality
constraints?
</div></blockquote><div><br></div><div style="font-family:tahoma,sans-serif" class="gmail_default">Yes, but the check is a bit conservative. Look at `inert_given_eqs` in `InertCans`, and `updateGivenEqs`.</div><div style="font-family:tahoma,sans-serif" class="gmail_default"><br></div><div style="font-family:tahoma,sans-serif" class="gmail_default"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><p>* implication constraints like (a ~ Int ==> a ~ Int) are never
created.</p></blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div>
I may be assuming that GHC runs the solver for each GADT pattern
match before creating implication constraints. <br></div></blockquote>
</div><div style="font-family:tahoma,sans-serif" class="gmail_default"></div><div style="font-family:tahoma,sans-serif" class="gmail_default">That's not right. They can be created, but then get solved, by solving the Wanted from the Given.</div><div style="font-family:tahoma,sans-serif" class="gmail_default"><br></div><div style="font-family:tahoma,sans-serif" class="gmail_default">
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><p>3.3: Also, is there a standard way to pretty-print implication
constraints? The OutsideIn paper uses LaTeX \supset I think, but
there isn't an obvious ASCII character to use to for \supset...</p></blockquote><div><br></div><div>Well there is a `Outputable` instance. It uses `=>`.</div><div><br></div><div>Simon <br></div>
</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 15 Aug 2022 at 20:00, Benjamin Redelings <<a href="mailto:benjamin.redelings@gmail.com">benjamin.redelings@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div>
<p>Thanks a bunch for this!</p>
<div>On 8/4/22 3:45 PM, Simon Peyton Jones
wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr">
<div class="gmail_default" style="font-family:tahoma,sans-serif">
<p>QUESTION 1: Are there any obviously important resources
that I've overlooked?</p>
</div>
<div class="gmail_default" style="font-family:tahoma,sans-serif">That's
a good list. Ningning's thesis <a href="https://xnning.github.io/" target="_blank">https://xnning.github.io/</a>
is also good stuff.</div>
</div>
</blockquote>
<p>Thanks!</p>
<p><br>
</p>
<blockquote type="cite">
<div dir="ltr">
<div class="gmail_default" style="font-family:tahoma,sans-serif">QUESTION
2: if my quick scan is correct, none of the papers mention the
GHC technique of determining untouchability by assigning
"levels" to type variables. Is there any written paper
(outside the GHC sources) that discusses type levels?
</div>
<div class="gmail_default" style="font-family:tahoma,sans-serif">It
is disgracefully undocumented, I'm afraid. Sorry. Didier
Remy used similar ideas, in some INRIA papers I think.</div>
</div>
</blockquote>
<p>OK, that was my impression, just checking. I think I get the
basic idea...<br>
</p>
<p><br>
</p>
<blockquote type="cite">
<div dir="ltr">
<div class="gmail_default" style="font-family:tahoma,sans-serif">QUESTION
3: My impression is that: <br>
<p style="margin-left:40px">(a) type variable levels were
introduced in order to clarify which MetaTyVars are
"untouchable", but</p>
<div style="margin-left:40px"> </div>
<p style="margin-left:40px">(b) levels now also check that
type variables do not escape their quantification scope.</p>
<div style="margin-left:40px"> </div>
<p style="margin-left:40px">(c) levels can also be used to
figure out which variables are free in the type environment,
and therefore should not be generalized over.<br>
</p>
<p>Does this sound right? I suspect that I might be wrong
about the last one...</p>
<p><br>
</p>
<p>Correct about all three.</p>
</div>
</div>
</blockquote>
Good to know! <br>
<br>
<blockquote type="cite">
<div dir="ltr">
<div class="gmail_default" style="font-family:tahoma,sans-serif">
<p> Except that a unification variable is only untouchable if
it comes from an outer level *and* there are some
intervening Given equalities. If there are no equalities
it's not untouchable. E.b.</p>
f = \x -> case x of</div>
<div class="gmail_default" style="font-family:tahoma,sans-serif">
<div style="margin-left:120px">Just y -> 3::Int<br>
</div>
<p>Here the (3::Int) can affect the result type of the
function because the Just pattern match does not bind any
Given equalities (in a GADT like way).</p>
</div>
</div>
</blockquote>
<p>3.1: OK, so if the case branch introduces type-class constraints,
but not equality constraints, then the unification variables from
an outer level are still touchable? Presumably because the
type-class constraints don't interact with the equality
constraints?<br>
</p>
<p>3.2: The OutsideIn paper talks about creating implication
constraints, which then bubble UP to the level where the solver is
applied. Maybe only at the outermost level? <br>
</p>
<p>However, it sounds like GHC pushes given constraints from a GADT
pattern match DOWN into the case branch. Implication constraints
would only be created if the wanted constraints bubble up to a
GADT pattern match, and are not entailed by the givens. So<br>
</p>
<p>* implication constraints like (a ~ Int ==> a ~ Int) are never
created.</p>
<p>* however, implication constraints like (a ~ Int ==> b ~ Int)
could be created.</p>
<p>I may be assuming that GHC runs the solver for each GADT pattern
match before creating implication constraints.<br>
</p>
<p>Does that sound right?<br>
</p>
<p>3.3: Also, is there a standard way to pretty-print implication
constraints? The OutsideIn paper uses LaTeX \supset I think, but
there isn't an obvious ASCII character to use to for \supset...</p>
<p><br>
</p>
<blockquote type="cite">
<div dir="ltr">
<div class="gmail_default" style="font-family:tahoma,sans-serif">
<p>I keep meaning to write an updated version of <a href="https://www.microsoft.com/en-us/research/publication/practical-type-inference-for-arbitrary-rank-types/" target="_blank">Practical type inference for
arbitrary rank types</a>, but failing to get around to it!</p>
</div>
</div>
</blockquote>
<p>That would be great, if you find the time! Are you thinking of
adding practical steps for handling equality constraints to it?
Or, removing the deep-subsumption language? Or something else?
It has already been quite helpful.<br>
</p>
<p>-BenRI</p>
<br>
</div>
</blockquote></div>