<div dir="auto"><div dir="auto">Also, thanks for the concrete counter example! I tried to organize my thoughts on this kind of thing a while ago (see rambly notes at <a href="https://gitlab.haskell.org/ghc/ghc/wikis/float-more-eqs2018">https://gitlab.haskell.org/ghc/ghc/wikis/float-more-eqs2018</a> and my comments on #15009), but didn't succeed before setting it aside. Your counter example is very helpful as a conversation substrate.</div><div dir="auto"><br></div><div dir="auto"><span style="font-family:sans-serif">Disclaimer: I've only ever tested my understanding of this stuff with GHC itself (as a typechecker plugin author, with a malnourished test suite to boot), so I'm not totally confident in what follows. Excited for others to review.</span><br></div><div dir="auto"><br></div><div dir="auto">Iavor's user decl:<br><div dir="auto"><br></div><div dir="auto"><span style="color:rgb(128,0,128);font-family:sans-serif;font-size:12.8px">    data Q3 = forall a. Q3 (forall b. (F b ~ Int) => T a b)</span><br style="color:rgb(128,0,128);font-family:sans-serif;font-size:12.8px"><div dir="ltr" style="font-family:sans-serif"><br></div><div dir="ltr" style="font-family:sans-serif">Your summary of the relevant Wanted implication of the ambiguity check:</div><br><span style="color:rgb(128,0,128);font-family:sans-serif;font-size:12.8px">   forall a. forall b. (F b ~ Int) => (a ~ alpha)</span><br></div></div><div class="gmail_quote"><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">Your explanation of the "counter-example" due to the open world assumption:</div><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr"><span style="font-family:sans-serif;font-size:12.8px">type family G i a</span><br style="font-family:sans-serif;font-size:12.8px"><span style="font-family:sans-serif;font-size:12.8px">    type instance G Int a = a</span><br style="font-family:sans-serif;font-size:12.8px"><br style="font-family:sans-serif;font-size:12.8px"><span style="font-family:sans-serif;font-size:12.8px">If that were the case, then the implication constraint above would no</span><br style="font-family:sans-serif;font-size:12.8px"><span style="font-family:sans-serif;font-size:12.8px">longer have a unique solution, since there would exist another</span><br style="font-family:sans-serif;font-size:12.8px"><span style="font-family:sans-serif;font-size:12.8px">substitution [alpha |-> G (F b) a] that is incomparable with [alpha</span><br style="font-family:sans-serif;font-size:12.8px"><span style="font-family:sans-serif;font-size:12.8px">|-> a]. OutsideIn(X) was designed to only pick unique solutions …</span><br></div><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">If we write the Wanted again with explicit tyvar levels:</div><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">    forall a[1]. forall b[2]. (F b ~ Int) => (a ~ alpha[2])<br></div><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">And flatten:</div><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr"><span style="font-family:sans-serif">    forall a[1]. forall b[2]. (F b ~ fsk[2], fsk ~ Int) => (a ~ alpha[1])</span><br></div><div dir="ltr" class="gmail_attr"><span style="font-family:sans-serif"><br></span></div><div dir="ltr" class="gmail_attr"><span style="font-family:sans-serif">Then I think your counter example becomes:</span></div><div dir="ltr" class="gmail_attr"><span style="font-family:sans-serif"><br></span></div><div dir="ltr" class="gmail_attr">    the substitution mapping alpha[1] to G fsk[2] a[1]</div><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">(I'm eliding the corresponding fmv flatten skolem; irrelevant, I think.)</div><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">But that mapping is "ill-leveled", isn't it? The level 2 skolem b[2] would be escaping if a type including it were assigned to the level 1 univar alpha[1]. (I'm unsure if b's position as an argument to a tyfam <span style="font-family:sans-serif">in the RHS of alpha</span> matters -- my intuition says it does not.)<span style="font-family:sans-serif"><br></span></div><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">Could be an exciting improvement to unification under local equalities, if I'm right here and also the argument generalizes beyond this kind of example.<br></div><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">Please let me know what you think! Thanks. -Nick</div><div dir="ltr" class="gmail_attr"><br></div><div dir="ltr" class="gmail_attr">On Mon, May 20, 2019, 16:26 Nicolas Frisby <<a href="mailto:nicolas.frisby@gmail.com" target="_blank" rel="noreferrer">nicolas.frisby@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">FYI, your Q2 (with no tyfam) is well-typed because of #15009</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, May 20, 2019, 11:01 Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" rel="noreferrer noreferrer" target="_blank">iavor.diatchki@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
thanks for the detailed response---I thought something like that might<br>
be happening, which is why I thought I'd better ask before reporting a<br>
bug.<br>
<br>
I wonder how we might make the error message a little more user<br>
friendly.   One idea would be to compute a couple of examples to show,<br>
after an ambiguity check fails.<br>
<br>
-Iavor<br>
<br>
On Sat, May 18, 2019 at 7:03 AM Ryan Scott <<a href="mailto:ryan.gl.scott@gmail.com" rel="noreferrer noreferrer noreferrer" target="_blank">ryan.gl.scott@gmail.com</a>> wrote:<br>
><br>
> Hi Iavor,<br>
><br>
> This is a feature in the sense that it is an expected outcome of the<br>
> OutsideIn(X) type inference algorithm (in particular, Section 5 of the<br>
> corresponding paper [1]). I'll try to explain the issue to the best of<br>
> my understanding.<br>
><br>
> The tricky thing about the Q3 data type:<br>
><br>
>     data Q3 = forall a. Q3 (forall b. (F b ~ Int) => T a b)<br>
><br>
> Is that there is a rank-n type with a /local/ equality constraint. In<br>
> order to ensure that the type of the Q3 data constructor is never<br>
> ambiguous, GHC tries to infer that Q3's type is always a subtype of<br>
> itself. As a part of this, GHC attempts to solve the following<br>
> implication constraint:<br>
><br>
>     forall a. forall b. (F b ~ Int) => (a ~ alpha)<br>
><br>
> Where `alpha` is a unification variable. GHC tries to find a unique,<br>
> most-general substitution that solves this constraint but ultimately<br>
> gives up and reports the "untouchable" error message you observed.<br>
><br>
> This is a bit strange, however. Upon first glance, this constraint<br>
> would appear to have a unique solution: namely, [alpha |-> a]. Why<br>
> doesn't GHC just use this? Ultimately, it's because OutsideIn(X) is<br>
> conservative: there may exist constraints that admit a unique solution<br>
> which it may fail to solve. This is explained in greater depth in<br>
> Section 5.2 of the paper, but the essence of this restriction is<br>
> because of the open-world assumption for type families. Namely, it's<br>
> possible that your Q3 data type might later be linked against code<br>
> which defines the following type family:<br>
><br>
>     type family G i a<br>
>     type instance G Int a = a<br>
><br>
> If that were the case, then the implication constraint above would no<br>
> longer have a unique solution, since there would exist another<br>
> substitution [alpha |-> G (F b) a] that is incomparable with [alpha<br>
> |-> a]. OutsideIn(X) was designed to only pick unique solutions that<br>
> remain unique solutions even if more axioms (i.e., type family<br>
> equations) are added, so for these reasons it fails to solve the<br>
> implication constraint above.<br>
><br>
> See also GHC issues #10651 [2], #14921 [3], and #15649 [4], which all<br>
> involve similar issues.<br>
><br>
> -----<br>
><br>
> I'm far from an expert on type inference, so I can't really offer a<br>
> better inference algorithm that would avoid this problem. The best you<br>
> can do, as far as I can tell, is to enable AllowAmbiguousTypes and<br>
> hope for the best. Even then, you'll still run into situations where<br>
> untouchability rears its ugly head, as in your `q3` definition. When<br>
> that happens, your only available option (again, as far as I can tell)<br>
> is to make use of TypeApplications. For example, the following /does/<br>
> typecheck:<br>
><br>
>     q3 :: Q3<br>
>     q3 = Q3 @Bool t<br>
><br>
> Hope that helps,<br>
><br>
> Ryan S.<br>
> -----<br>
> [1] <a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf" rel="noreferrer noreferrer noreferrer noreferrer" target="_blank">https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf</a><br>
> [2] <a href="https://gitlab.haskell.org/ghc/ghc/issues/10651" rel="noreferrer noreferrer noreferrer noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc/issues/10651</a><br>
> [3] <a href="https://gitlab.haskell.org/ghc/ghc/issues/14921" rel="noreferrer noreferrer noreferrer noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc/issues/14921</a><br>
> [4] <a href="https://gitlab.haskell.org/ghc/ghc/issues/15649" rel="noreferrer noreferrer noreferrer noreferrer" target="_blank">https://gitlab.haskell.org/ghc/ghc/issues/15649</a><br>
> _______________________________________________<br>
> ghc-devs mailing list<br>
> <a href="mailto:ghc-devs@haskell.org" rel="noreferrer noreferrer noreferrer" target="_blank">ghc-devs@haskell.org</a><br>
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer noreferrer noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" rel="noreferrer noreferrer noreferrer" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer noreferrer noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>
</blockquote></div></div>