Partial type signatures sometimes gets their ordering wrong
If I write
f1 :: forall b a. a -> b -> _ f1 x _ = x
GHC cleverly quantifies
a, allowing visible type application to work as the user might expect.
But here are two cases where GHC is not so clever:
f2 :: forall k (a :: k). k -> Proxy (a :: k) f2 _ = Proxy f3 :: forall a k. k -> Proxy (a :: _) f3 = f2
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.
f4 :: forall a b. a -> b -> _ f5 :: forall b a. a -> b -> _ f4 = f5 f5 = f4
Note that the ordering of variables in
f5 is different. Yet GHC assigns the same quantification order to both.
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
inferred = qtvs \\ psig_tvs, where
final_qtvs = scopedSort (inferred ++ psig_tvs). That is, we seed
scopedSortwith the correct ordering. And we suggest that the
inferredshould go first.
Check that the ordering of the
final_qtvsis as expected. (That is,
psig_tvsshould be a subsequence of
final_qtvs.) If not, error.
Label the qtvs correctly as
Inferred(perhaps this can be done while doing step 3).
And off you go!