Partial type signatures sometimes gets their ordering wrong

If I write

f1 :: forall b a. a -> b -> _
f1 x _ = x

GHC cleverly quantifies b before a, allowing visible type application to work as the user might expect.

But here are two cases where GHC is not so clever:

Case 1:

f2 :: forall k (a :: k). k -> Proxy (a :: k)
f2 _ = Proxy

f3 :: forall a k. k -> Proxy (a :: _)
f3 = f2

Of course, f3's type is bogus: k has to come before a. And indeed GHC swizzles these around -- but it shouldn't. Better would be to reject, because the user has requested the impossible.

Case 2:

f4 :: forall a b. a -> b -> _
f5 :: forall b a. a -> b -> _
f4 = f5
f5 = f4

Note that the ordering of variables in f4 and f5 is different. Yet GHC assigns the same quantification order to both.

Solution:

Currently, the working case works because of a series of delicate dependencies, starting with code in decideQuantifiedTyVars that sets an initial (correct) order, and blindly hopes that various data structures and functions preserve the order. They do, most of the time, but not in the cases above. Yet these functions are not really concerned with ordering, and so this might change in the future.

Better would be to fix the ordering in chooseInferredQuantifiers, which happens right at the end. At this point, we have the psig_tvs, which are the tvs as the user wrote them; and the qtvs, which are the variables that simplifyInfer has indicated should be quantified over. It should always be the case that qtvs is a superset of psig_tvs.

1. Compute inferred = qtvs \\ psig_tvs, where \\ denotes set-subtraction.

2. Compute final_qtvs = scopedSort (inferred ++ psig_tvs). That is, we seed scopedSort with the correct ordering. And we suggest that the inferred should go first.

3. Check that the ordering of the psig_tvs within final_qtvs is as expected. (That is, psig_tvs should be a subsequence of final_qtvs.) If not, error.

4. Label the qtvs correctly as Specified or Inferred (perhaps this can be done while doing step 3).

And off you go!