Bug or feature?

[Nicolas Frisby]

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> 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>
> 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
> > ghc-devs at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20190520/e722d72b/attachment.html>