Bug or feature?
Simon Peyton Jones
simonpj at microsoft.com
Tue May 21 08:23:00 UTC 2019
Let me have a quick stab at Nick’s idea. Consider
forall b[2]. (a ~ Int) => alpha[1] ~ Maybe a
Then we don’t want to unify alpha := Maybe a, because an equally good way to solve the constraint would be alpha := Maybe Int. And constraints elsewhere might force one or the other to be the “right” one.
But suppose none of the given constraints involve ‘a’ in any way, shape, or form. For example:
forall b[2]. (b ~ Int) => alpha[1] ~ Maybe a
Well then, we have no local constraints on a, so we can’t get any ambiguity. Aha – this is covered by the current “local equalities” story. Note [Let-bound skolems] in TcSMonad.
But what about this:
forall b[2]. (F b ~ G b) => alpha[1] ~ Maybe a
That is *not* covered by the current local-equalities story, but I think is equally immune to producing a local constraint on ‘a’. And Iavor’s example is just such a case.
So here is a possible refinement:
1. An implication is considered to “bind local equalities” iff it has at least one given equality whose free variables are not all bound by the same implication.
That loosens up Note [Let-bound skolems] in TcSMonad, perhaps significantly.
Could we go further?
1. An equality (t1~t2) can float out of an implication (forall as. C => blah) iff, assuming fvs(t1,t2) = FV
* The ‘as’ are disjoint from FV obviously.
* None of the equality constraints in C mentions any of the variables in FV
This is a bit looser because in
forall c[2]. (b ~ Int) => alpha[1] ~ a
it would allow the equality alpha~a to float even though there is a real local equality (b~Int).
I’m a bit worried about (B) however. Suppose we had a Given equality (a ~ b). Then suddenly that local Given (b ~ Int) does actually constrain a after all. Can we have Givens we didn’t “see” before? Yes, via superclasses or outer unifications.
So I would be rather cautious about (B). But (A) looks sound to me. I think it would address Iavor’s example, but perhaps not Nick’s.
Simon
From: ghc-devs <ghc-devs-bounces at haskell.org> On Behalf Of Nicolas Frisby
Sent: 21 May 2019 00:58
To: Iavor S. S. Diatchki <iavor.diatchki at gmail.com>
Cc: ghc-devs at haskell.org; Ryan Scott <ryan.gl.scott at gmail.com>
Subject: Re: Bug or feature?
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 https://gitlab.haskell.org/ghc/ghc/wikis/float-more-eqs2018<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fwikis%2Ffloat-more-eqs2018&data=02%7C01%7Csimonpj%40microsoft.com%7C8541805315cb456e1eef08d6dd7f00c0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636939934881644934&sdata=usdD49rcTG38IxnbKbH5veEodq%2BcHhBmjw19y5SWzUQ%3D&reserved=0> and my comments on #15009), but didn't succeed before setting it aside. Your counter example is very helpful as a conversation substrate.
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.
Iavor's user decl:
data Q3 = forall a. Q3 (forall b. (F b ~ Int) => T a b)
Your summary of the relevant Wanted implication of the ambiguity check:
forall a. forall b. (F b ~ Int) => (a ~ alpha)
Your explanation of the "counter-example" due to the open world assumption:
type family G i a
type instance G Int a = a
If that were the case, then the implication constraint above would no
longer have a unique solution, since there would exist another
substitution [alpha |-> G (F b) a] that is incomparable with [alpha
|-> a]. OutsideIn(X) was designed to only pick unique solutions …
If we write the Wanted again with explicit tyvar levels:
forall a[1]. forall b[2]. (F b ~ Int) => (a ~ alpha[2])
And flatten:
forall a[1]. forall b[2]. (F b ~ fsk[2], fsk ~ Int) => (a ~ alpha[1])
Then I think your counter example becomes:
the substitution mapping alpha[1] to G fsk[2] a[1]
(I'm eliding the corresponding fmv flatten skolem; irrelevant, I think.)
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 in the RHS of alpha matters -- my intuition says it does not.)
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.
Please let me know what you think! Thanks. -Nick
On Mon, May 20, 2019, 16:26 Nicolas Frisby <nicolas.frisby at gmail.com<mailto:nicolas.frisby at gmail.com>> wrote:
FYI, your Q2 (with no tyfam) is well-typed because of #15009
On Mon, May 20, 2019, 11:01 Iavor Diatchki <iavor.diatchki at gmail.com<mailto:iavor.diatchki at gmail.com>> wrote:
Hi,
thanks for the detailed response---I thought something like that might
be happening, which is why I thought I'd better ask before reporting a
bug.
I wonder how we might make the error message a little more user
friendly. One idea would be to compute a couple of examples to show,
after an ambiguity check fails.
-Iavor
On Sat, May 18, 2019 at 7:03 AM Ryan Scott <ryan.gl.scott at gmail.com<mailto:ryan.gl.scott at gmail.com>> wrote:
>
> Hi Iavor,
>
> This is a feature in the sense that it is an expected outcome of the
> OutsideIn(X) type inference algorithm (in particular, Section 5 of the
> corresponding paper [1]). I'll try to explain the issue to the best of
> my understanding.
>
> The tricky thing about the Q3 data type:
>
> data Q3 = forall a. Q3 (forall b. (F b ~ Int) => T a b)
>
> Is that there is a rank-n type with a /local/ equality constraint. In
> order to ensure that the type of the Q3 data constructor is never
> ambiguous, GHC tries to infer that Q3's type is always a subtype of
> itself. As a part of this, GHC attempts to solve the following
> implication constraint:
>
> forall a. forall b. (F b ~ Int) => (a ~ alpha)
>
> Where `alpha` is a unification variable. GHC tries to find a unique,
> most-general substitution that solves this constraint but ultimately
> gives up and reports the "untouchable" error message you observed.
>
> This is a bit strange, however. Upon first glance, this constraint
> would appear to have a unique solution: namely, [alpha |-> a]. Why
> doesn't GHC just use this? Ultimately, it's because OutsideIn(X) is
> conservative: there may exist constraints that admit a unique solution
> which it may fail to solve. This is explained in greater depth in
> Section 5.2 of the paper, but the essence of this restriction is
> because of the open-world assumption for type families. Namely, it's
> possible that your Q3 data type might later be linked against code
> which defines the following type family:
>
> type family G i a
> type instance G Int a = a
>
> If that were the case, then the implication constraint above would no
> longer have a unique solution, since there would exist another
> substitution [alpha |-> G (F b) a] that is incomparable with [alpha
> |-> a]. OutsideIn(X) was designed to only pick unique solutions that
> remain unique solutions even if more axioms (i.e., type family
> equations) are added, so for these reasons it fails to solve the
> implication constraint above.
>
> See also GHC issues #10651 [2], #14921 [3], and #15649 [4], which all
> involve similar issues.
>
> -----
>
> I'm far from an expert on type inference, so I can't really offer a
> better inference algorithm that would avoid this problem. The best you
> can do, as far as I can tell, is to enable AllowAmbiguousTypes and
> hope for the best. Even then, you'll still run into situations where
> untouchability rears its ugly head, as in your `q3` definition. When
> that happens, your only available option (again, as far as I can tell)
> is to make use of TypeApplications. For example, the following /does/
> typecheck:
>
> q3 :: Q3
> q3 = Q3 @Bool t
>
> Hope that helps,
>
> Ryan S.
> -----
> [1] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp-outsidein.pdf<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.microsoft.com%2Fen-us%2Fresearch%2Fwp-content%2Fuploads%2F2016%2F02%2Fjfp-outsidein.pdf&data=02%7C01%7Csimonpj%40microsoft.com%7C8541805315cb456e1eef08d6dd7f00c0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636939934881644934&sdata=tLMnhJGSfmhl5ENnluDF1A7xSy9JBaAMTN9tMFVPvVU%3D&reserved=0>
> [2] https://gitlab.haskell.org/ghc/ghc/issues/10651<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fissues%2F10651&data=02%7C01%7Csimonpj%40microsoft.com%7C8541805315cb456e1eef08d6dd7f00c0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636939934881654927&sdata=4k3SxYqoriadeXMvOf2AsWIPJHfOATzIAzDOmRxodAA%3D&reserved=0>
> [3] https://gitlab.haskell.org/ghc/ghc/issues/14921<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fissues%2F14921&data=02%7C01%7Csimonpj%40microsoft.com%7C8541805315cb456e1eef08d6dd7f00c0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636939934881654927&sdata=z8or8qyebl7pTm4zbxe8ZYM6%2FFRwoAST0v27kh0IMy4%3D&reserved=0>
> [4] https://gitlab.haskell.org/ghc/ghc/issues/15649<https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgitlab.haskell.org%2Fghc%2Fghc%2Fissues%2F15649&data=02%7C01%7Csimonpj%40microsoft.com%7C8541805315cb456e1eef08d6dd7f00c0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636939934881654927&sdata=GER2%2BvIIMNCyQmlSohkkZxV9PdbMX9QLV1PL7a8tMzc%3D&reserved=0>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org<mailto:ghc-devs at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs<https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01%7Csimonpj%40microsoft.com%7C8541805315cb456e1eef08d6dd7f00c0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636939934881664921&sdata=vafMrsPPVbBzZeTLYPREXBgfclzb9yYbE29SFqIB99k%3D&reserved=0>
_______________________________________________
ghc-devs mailing list
ghc-devs at haskell.org<mailto:ghc-devs at haskell.org>
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs<https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01%7Csimonpj%40microsoft.com%7C8541805315cb456e1eef08d6dd7f00c0%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636939934881664921&sdata=vafMrsPPVbBzZeTLYPREXBgfclzb9yYbE29SFqIB99k%3D&reserved=0>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190521/f29c38d7/attachment-0001.html>
More information about the ghc-devs
mailing list