FYI, your Q2 (with no tyfam) is well-typed because of #15009 On Mon, May 20, 2019, 11:01 Iavor Diatchki <[email protected]> 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 <[email protected]> > 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 > > [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 > > [email protected] > > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > _______________________________________________ > ghc-devs mailing list > [email protected] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
