<div dir="ltr"><div>My first go is at <a href="https://github.com/conal/hermit-extras/blob/master/src/HERMIT/Extras.hs#L1030">https://github.com/conal/hermit-extras/blob/master/src/HERMIT/Extras.hs#L1030</a> . It type-checks. I haven't tried running it yet. Comments most welcome!<br>
<br></div>-- Conal<br></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Jun 24, 2014 at 4:10 PM, Conal Elliott <span dir="ltr"><<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</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"><div>I'm glad for the interest and help. I can make an initial go of it. My current simple plan is to traverse expressions, collecting type equalities from bound coercion variables as I descend, combining them progressively with successive type unifications. The traversal is thus parametrized by a TvSubst and yields a Maybe TvSubst. The coercion variables will come from lambdas, let bindings and case alternatives. If an added equality is not unifiable given the current TvSubst, we've reached a contradiction. If the contradiction arises for one of the variables in a case alternative, then remove that alternative.<br>
<br>How does this strategy sound?<br><br>Some issues:<br><br>* Nominal vs representational type equalities.<br>* Will I want to normalize the types (with normaliseType) before unifying?<br>* How can I unify while carrying along a type substitution environment? The Unify module exports tcUnifyTy, which takes no such environment, but not unify, which does.<span class="HOEnZb"><font color="#888888"><br>
<br></font></span></div><span class="HOEnZb"><font color="#888888">-- Conal<br></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><br><div class="gmail_quote">On Tue, Jun 24, 2014 at 4:43 AM, Simon Peyton Jones <span dir="ltr"><<a href="mailto:simonpj@microsoft.com" target="_blank">simonpj@microsoft.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div link="#0563C1" vlink="#954F72" lang="EN-GB">
<div><div>
<p class="MsoNormal" style="margin-left:36.0pt"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">we need to do a bit more work to re-connect to source pattern locations and nested patterns? I can’t assess
very well yet if this is a real problem though<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
</div><p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">That is a very good point.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Nevertheless, given
<u></u><u></u></span></p>
<p><u></u><span style="font-family:Symbol;color:#1f497d"><span>·<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">the typechecked HsSyn (i.e. still in source form, but with type inference fully completed
</span><span style="font-family:"Calibri","sans-serif";color:#1f497d"><u></u><u></u></span></p>
<p><u></u><span style="font-family:Symbol;color:#1f497d"><span>·<span style="font:7.0pt "Times New Roman"">
</span></span></span><u></u><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">the independent contradiction-detector described below (which is independent of whether the contradiction problems it is
given come from HsSyn or Core)</span><span style="font-family:"Calibri","sans-serif";color:#1f497d"><u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d">it would be easy to give source-localised error messages<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d">Simon<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"" lang="EN-US">From:</span></b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"" lang="EN-US"> Dimitrios Vytiniotis
<br>
<b>Sent:</b> 24 June 2014 11:58<br>
<b>To:</b> Simon Peyton Jones; Conal Elliott; <a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<b>Cc:</b> Nikolaos S. Papaspyrou (<a href="mailto:nickie@softlab.ntua.gr" target="_blank">nickie@softlab.ntua.gr</a>); George Karachalias</span></p><div><div><br>
<b>Subject:</b> RE: Pruning GADT case alternatives with uninhabitable coercion parameters<u></u><u></u></div></div><p></p>
</div>
</div><div><div>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Yes it would be better in the sense that we don’t really want to be dealing with unification variables and evidence when we simply
use the constraint solver to detect inconsistencies in possibly missing patterns, but the concern has been that if we are already desugared and in core maybe we need to do a bit more work to re-connect to source pattern locations and nested patterns? I can’t
assess very well yet if this is a real problem though … <u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">In general I agree that a simple constraint solver for Core might be an independently useful tool for this kind of optimization.
(I think George had thought about this too). <u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">Thanks!<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d">d-<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-size:11.0pt;font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<div>
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"" lang="EN-US">From:</span></b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"" lang="EN-US"> Simon Peyton Jones
<br>
<b>Sent:</b> Tuesday, June 24, 2014 11:41 AM<br>
<b>To:</b> Conal Elliott; <a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<b>Cc:</b> Dimitrios Vytiniotis; Nikolaos S. Papaspyrou (<a href="mailto:nickie@softlab.ntua.gr" target="_blank">nickie@softlab.ntua.gr</a>); George Karachalias; Simon Peyton Jones<br>
<b>Subject:</b> RE: Pruning GADT case alternatives with uninhabitable coercion parameters<u></u><u></u></span></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d">Conal<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d">This also relates to detecting redundant or overlapped patterns in source programs. I know that Dimitrios is looking at this with Tom, Nikolas, George
who I’m cc’ing him.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d">I think their current approach may be to integrate the overlap checking with the constraint solver in the type checker. But that isn’t going to work
for optimising Core.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d">An alternative approach would be to implement a specialised constraint solver. It could be MUCH simpler than the one in the inference engine, because
(a) there are no unification variables to worry about, (b) there is no need to gather evidence. More or less it’s task could be to answer the question<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d"> Is C |- D definitely a contradiction?<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d">where C are the “given” constraints (from enclosing pattern matches) and D are the “wanted” constraints (from the current pattern match that may be
unreachable).<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d">I don’t think it would be hard to implement such a function. I’d be happy to help advise if someone wants to take it on.<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d">Dimitrios: If we had such a function, then maybe it’d be better to use it for the pattern-matching overlap detection too?<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d"><br>
Simon<u></u><u></u></span></p>
<p class="MsoNormal"><span style="font-family:"Calibri","sans-serif";color:#1f497d"><u></u> <u></u></span></p>
<div style="border:none;border-left:solid blue 1.5pt;padding:0cm 0cm 0cm 4.0pt">
<div>
<div style="border:none;border-top:solid #e1e1e1 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal"><b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"" lang="EN-US">From:</span></b><span style="font-size:11.0pt;font-family:"Calibri","sans-serif"" lang="EN-US"> ghc-devs [<a href="mailto:ghc-devs-bounces@haskell.org" target="_blank">mailto:ghc-devs-bounces@haskell.org</a>]
<b>On Behalf Of </b>Conal Elliott<br>
<b>Sent:</b> 20 June 2014 18:59<br>
<b>To:</b> <a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<b>Subject:</b> Pruning GADT case alternatives with uninhabitable coercion parameters<u></u><u></u></span></p>
</div>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:12.0pt;margin-left:0cm">
I'm looking for tips on pruning away impossible branches in `case` expressions on GADTs, due to uninhabited coercion parameter types.<br>
<br>
Here's a simple example (rendered by HERMIT) from a type-specializion of the Foldable instance a GADT for perfect leaf trees in which the tree depth is part of the type:<br>
<br>
> case ds of wild (Sum Int)<br>
> L (~# :: S (S Z) ~N Z) a1 -> f a1<br>
> B n1 (~# :: S (S Z) ~N S n1) uv -> ...<br>
<br>
Note the kind of the coercion parameter to the leaf constructor (`L`): `S (S Z) ~N Z`, i.e., 2 == 0. I think we can safely remove this branch as impossible.<br>
<br>
The reasoning gets subtler, however.<br>
After inlining and simplifying in the second (`B`) alternative, the following turns up:<br>
<br>
> case ds0 of wild0 (Sum Int)<br>
> L (~# :: n1 ~N Z) a1 -> f0 a1<br>
> B n2 (~# :: n1 ~N S n2) uv0 -> ...<br>
<br>
Now I want to remove the first `L` alternative with `n1 ~ Z`, given that the kind `S (S Z) ~N S n1` is inhabited (since we're in the first `B` alternative), so that `n1 ~ S Z`. With more inlining, more such equalities pile up. Soon we get to an impossible `B`
alternative, whose removal would then eliminate the rest of the recursive unfolding.<br>
<br>
My questions:<br>
<br>
* Does this sort of transformation already live in GHC somewhere, and if so, where?<br>
* Are there gotchas / sources of unsoundness in the transformation I'm suggesting?<br>
* Is anyone else already working on this sort of transformation?<u></u><u></u></p>
</div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
-- Conal<u></u><u></u></p>
<div>
<p class="MsoNormal" style="margin-right:0cm;margin-bottom:6.0pt;margin-left:0cm">
<u></u> <u></u></p>
</div>
</div>
</div>
</div></div></div>
</div>
</div>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>