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
.

Compute
inferred = qtvs \\ psig_tvs
, where\\
denotes setsubtraction. 
Compute
final_qtvs = scopedSort (inferred ++ psig_tvs)
. That is, we seedscopedSort
with the correct ordering. And we suggest that theinferred
should go first. 
Check that the ordering of the
psig_tvs
withinfinal_qtvs
is as expected. (That is,psig_tvs
should be a subsequence offinal_qtvs
.) If not, error. 
Label the qtvs correctly as
Specified
orInferred
(perhaps this can be done while doing step 3).
And off you go!