Bug or feature?

Mon May 20 23:57:42 UTC 2019

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 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> 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>
> 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/f0eb15c8/attachment.html>