Bug or feature?

[Ryan Scott]

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