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
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-outs...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/10651https://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/14921https://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/15649https://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@haskell.orgmailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devshttps://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@haskell.orgmailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devshttps://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