FYI, your Q2 (with no tyfam) is well-typed because of #15009 On Mon, May 20, 2019, 11:01 Iavor Diatchki 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 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-outs...

...

[2] https://gitlab.haskell.org/ghc/ghc/issues/10651 [3] https://gitlab.haskell.org/ghc/ghc/issues/14921 [4] https://gitlab.haskell.org/ghc/ghc/issues/15649 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

---

ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

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 On Behalf Of Nicolas Frisby Sent: 21 May 2019 00:58 To: Iavor S. S. Diatchki Cc: ghc-devs@haskell.org; Ryan Scott 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-eqs2018https://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 mailto:nicolas.frisby@gmail.com> wrote: FYI, your Q2 (with no tyfam) is well-typed because of #15009 On Mon, May 20, 2019, 11:01 Iavor Diatchki mailto:iavor.diatchki@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 mailto:ryan.gl.scott@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-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