Kill varSetElemsWellScoped in quantifyTyVars

varSetElemsWellScoped introduces unnecessary non-determinism in
inferred type signatures.
Removing this instance required changing the representation of
TcDepVars to use deterministic sets.
This is the last occurence of varSetElemsWellScoped, allowing me to
finally remove it.

Test Plan:
./validate
I will update the expected outputs when commiting, some reordering
of type variables in types is expected.

Reviewers: goldfire, simonpj, austin, bgamari

Reviewed By: simonpj

Subscribers: thomie, simonmar

Differential Revision: https://phabricator.haskell.org/D2135

GHC Trac Issues: #4012

49 files changed, 216 insertions, 216 deletions

diff --git a/testsuite/tests/ado/ado004.stderr b/testsuite/tests/ado/ado004.stderr
index c6c5e3544d..6a39e6d142 100644
--- a/testsuite/tests/ado/ado004.stderr
+++ b/testsuite/tests/ado/ado004.stderr
@@ -2,29 +2,29 @@ TYPE SIGNATURES
   test1 ::
     forall (f :: * -> *). Applicative f => (Int -> f Int) -> f Int
   test2 ::
-    forall (f :: * -> *) b t.
+    forall t b (f :: * -> *).
     (Applicative f, Num t, Num b) =>
     (t -> f b) -> f b
   test2a ::
-    forall (f :: * -> *) b t.
+    forall t b (f :: * -> *).
     (Num t, Num b, Functor f) =>
     (t -> f b) -> f b
   test2b ::
     forall (m :: * -> *) a t. (Num t, Monad m) => (t -> a) -> m a
   test3 ::
-    forall (m :: * -> *) a t t1.
-    (Num t, Monad m) =>
-    (t -> m t1) -> (t1 -> t1 -> m a) -> m a
+    forall a t (m :: * -> *) t1.
+    (Num t1, Monad m) =>
+    (t1 -> m t) -> (t -> t -> m a) -> m a
   test4 ::
-    forall (m :: * -> *) a a1 t.
+    forall a a1 (m :: * -> *) t.
     (Num t, Monad m) =>
     (t -> m a1) -> (a1 -> a1 -> m a) -> m a
   test5 ::
-    forall (m :: * -> *) a a1 t.
+    forall a a1 (m :: * -> *) t.
     (Num t, Monad m) =>
     (t -> m a1) -> (a1 -> a1 -> m a) -> m a
   test6 ::
-    forall t (m :: * -> *) a.
+    forall a (m :: * -> *) t.
     (Num (m a), Monad m) =>
     (m a -> m (m a)) -> t -> m a
 TYPE CONSTRUCTORS
diff --git a/testsuite/tests/dependent/should_fail/T11334b.stderr b/testsuite/tests/dependent/should_fail/T11334b.stderr
index 8f4251b0cd..4fcc593f80 100644
--- a/testsuite/tests/dependent/should_fail/T11334b.stderr
+++ b/testsuite/tests/dependent/should_fail/T11334b.stderr
@@ -1,7 +1,7 @@
 
 T11334b.hs:8:14: error:
     • Cannot default kind variable ‘f0’
-      of kind: k0 -> *
+      of kind: k10 -> *
       Perhaps enable PolyKinds or add a kind signature
     • In an expression type signature: Proxy Compose
       In the expression: Proxy :: Proxy Compose
@@ -9,7 +9,7 @@ T11334b.hs:8:14: error:
 
 T11334b.hs:8:14: error:
     • Cannot default kind variable ‘g0’
-      of kind: k10 -> k0
+      of kind: k0 -> k10
       Perhaps enable PolyKinds or add a kind signature
     • In an expression type signature: Proxy Compose
       In the expression: Proxy :: Proxy Compose
@@ -17,7 +17,7 @@ T11334b.hs:8:14: error:
 
 T11334b.hs:8:14: error:
     • Cannot default kind variable ‘a0’
-      of kind: k10
+      of kind: k0
       Perhaps enable PolyKinds or add a kind signature
     • In an expression type signature: Proxy Compose
       In the expression: Proxy :: Proxy Compose
diff --git a/testsuite/tests/driver/werror.stderr b/testsuite/tests/driver/werror.stderr
index 398d885438..8f2e6035db 100644
--- a/testsuite/tests/driver/werror.stderr
+++ b/testsuite/tests/driver/werror.stderr
@@ -18,7 +18,7 @@ werror.hs:10:1: warning: [-Wunused-top-binds (in -Wextra, -Wunused-binds)]
 
 werror.hs:10:1: warning: [-Wmissing-signatures (in -Wall)]
     Top-level binding with no type signature:
-      f :: forall t t1. [t] -> [t1]
+      f :: forall t t1. [t1] -> [t]
 
 werror.hs:10:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr
index bc14bf1c51..797fd0ba4d 100644
--- a/testsuite/tests/gadt/gadt13.stderr
+++ b/testsuite/tests/gadt/gadt13.stderr
@@ -1,17 +1,17 @@
 
 gadt13.hs:15:13: error:
-    • Couldn't match expected type ‘t1’
+    • Couldn't match expected type ‘t’
                   with actual type ‘String -> [Char]’
-        ‘t1’ is untouchable
-          inside the constraints: t ~ Int
+        ‘t’ is untouchable
+          inside the constraints: t1 ~ Int
           bound by a pattern with constructor: I :: Int -> Term Int,
                    in an equation for ‘shw’
           at gadt13.hs:15:6-8
-      ‘t1’ is a rigid type variable bound by
-        the inferred type of shw :: Term t -> t1 at gadt13.hs:15:1
+      ‘t’ is a rigid type variable bound by
+        the inferred type of shw :: Term t1 -> t at gadt13.hs:15:1
       Possible fix: add a type signature for ‘shw’
     • Possible cause: ‘(.)’ is applied to too many arguments
       In the expression: ("I " ++) . shows t
       In an equation for ‘shw’: shw (I t) = ("I " ++) . shows t
     • Relevant bindings include
-        shw :: Term t -> t1 (bound at gadt13.hs:15:1)
+        shw :: Term t1 -> t (bound at gadt13.hs:15:1)
diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index 8219bee032..35c8e10363 100644
--- a/testsuite/tests/gadt/gadt7.stderr
+++ b/testsuite/tests/gadt/gadt7.stderr
@@ -1,20 +1,20 @@
 
 gadt7.hs:16:38: error:
-    • Couldn't match expected type ‘t2’ with actual type ‘t’
-        ‘t2’ is untouchable
-          inside the constraints: t1 ~ Int
+    • Couldn't match expected type ‘t’ with actual type ‘t1’
+        ‘t’ is untouchable
+          inside the constraints: t2 ~ Int
           bound by a pattern with constructor: K :: T Int,
                    in a case alternative
           at gadt7.hs:16:33
-      ‘t2’ is a rigid type variable bound by
-        the inferred type of i1b :: T t1 -> t -> t2 at gadt7.hs:16:1
       ‘t’ is a rigid type variable bound by
-        the inferred type of i1b :: T t1 -> t -> t2 at gadt7.hs:16:1
+        the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1
+      ‘t1’ is a rigid type variable bound by
+        the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1
       Possible fix: add a type signature for ‘i1b’
     • In the expression: y1
       In a case alternative: K -> y1
       In the expression: case t1 of { K -> y1 }
     • Relevant bindings include
-        y1 :: t (bound at gadt7.hs:16:16)
-        y :: t (bound at gadt7.hs:16:7)
-        i1b :: T t1 -> t -> t2 (bound at gadt7.hs:16:1)
+        y1 :: t1 (bound at gadt7.hs:16:16)
+        y :: t1 (bound at gadt7.hs:16:7)
+        i1b :: T t2 -> t1 -> t (bound at gadt7.hs:16:1)
diff --git a/testsuite/tests/ghci.debugger/scripts/break026.stdout b/testsuite/tests/ghci.debugger/scripts/break026.stdout
index 90c1f2ee9e..260ef49124 100644
--- a/testsuite/tests/ghci.debugger/scripts/break026.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/break026.stdout
@@ -1,8 +1,8 @@
 Stopped in Test.foldl, break026.hs:5:16-22
 _result :: Integer = _
 c :: Integer = 0
-go :: Integer -> [t1] -> Integer = _
-xs :: [t1] = _
+go :: Integer -> [t] -> Integer = _
+xs :: [t] = _
 Stopped in Test.foldl.go, break026.hs:7:23-35
 _result :: Integer = _
 c :: Integer = 0
@@ -10,17 +10,17 @@ f :: Integer -> Integer -> Integer = _
 x :: Integer = 1
 xs :: [Integer] = _
 Stopped in Test.foldl.go, break026.hs:7:23-35
-_result :: t = _
-c :: t = _
-f :: t -> Integer -> t = _
+_result :: t1 = _
+c :: t1 = _
+f :: t1 -> Integer -> t1 = _
 x :: Integer = 2
 xs :: [Integer] = _
 c = 1
 Stopped in Test.foldl, break026.hs:5:16-22
 _result :: Integer = _
 c :: Integer = 0
-go :: Integer -> [t1] -> Integer = _
-xs :: [t1] = _
+go :: Integer -> [t] -> Integer = _
+xs :: [t] = _
 Stopped in Test.foldl.go, break026.hs:7:23-35
 _result :: Integer = _
 c :: Integer = 0
@@ -28,9 +28,9 @@ f :: Integer -> Integer -> Integer = _
 x :: Integer = 1
 xs :: [Integer] = _
 Stopped in Test.foldl.go, break026.hs:7:23-35
-_result :: t = _
-c :: t = _
-f :: t -> Integer -> t = _
+_result :: t1 = _
+c :: t1 = _
+f :: t1 -> Integer -> t1 = _
 x :: Integer = 2
 xs :: [Integer] = _
 Stopped in Test.foldl.go, break026.hs:7:27-31
diff --git a/testsuite/tests/ghci/scripts/T11524a.stdout b/testsuite/tests/ghci/scripts/T11524a.stdout
index 91d51d3d14..0a9dddbaec 100644
--- a/testsuite/tests/ghci/scripts/T11524a.stdout
+++ b/testsuite/tests/ghci/scripts/T11524a.stdout
@@ -31,7 +31,7 @@ pattern Pue :: forall {t}. () => forall {a}. t -> a -> (t, Ex)
   	-- Defined at <interactive>:19:1
 pattern Pur :: forall {a}. (Num a, Eq a) => a -> [a]
   	-- Defined at <interactive>:20:1
-pattern Purp :: forall {a} {t}. (Num a, Eq a) => Show t => a
+pattern Purp :: forall {t} {a}. (Num a, Eq a) => Show t => a
                                                            -> t -> ([a], UnivProv t)
   	-- Defined at <interactive>:21:1
 pattern Pure :: forall {a}. (Num a, Eq a) => forall {a1}. a
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index 5964262843..f06760eed7 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -42,7 +42,7 @@
         (i.e. ones independent of the class type variables)
         must be distinct type variables
       Expected: PolyKindVarsF '[]
-      Actual:   PolyKindVarsF '[]
+        Actual: PolyKindVarsF '[]
       Use -fprint-explicit-kinds to see the kind arguments
     • In the type instance declaration for ‘PolyKindVarsF’
       In the instance declaration for ‘PolyKindVarsC '[]’
@@ -59,7 +59,7 @@
     Kind variable ‘k’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
-      forall k (a :: k) (b :: k).
+      forall k (b :: k) (a :: k).
         Fc a b = Int -- Defined at <interactive>:64:15
 
 <interactive>:68:15: error:
@@ -68,7 +68,7 @@
     cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
-      forall k (a :: k) (b :: k).
+      forall k (b :: k) (a :: k).
         Gc a b = Int -- Defined at <interactive>:68:15
 
 <interactive>:81:15: error:
diff --git a/testsuite/tests/ghci/scripts/T7587.stdout b/testsuite/tests/ghci/scripts/T7587.stdout
index 776eb6d223..975ad8f9a5 100644
--- a/testsuite/tests/ghci/scripts/T7587.stdout
+++ b/testsuite/tests/ghci/scripts/T7587.stdout
@@ -1 +1 @@
-A :: k -> k1 -> *
+A :: k1 -> k -> *
diff --git a/testsuite/tests/ghci/scripts/T7730.stdout b/testsuite/tests/ghci/scripts/T7730.stdout
index fcf9e4c1d2..94837b47cc 100644
--- a/testsuite/tests/ghci/scripts/T7730.stdout
+++ b/testsuite/tests/ghci/scripts/T7730.stdout
@@ -1,7 +1,7 @@
 type role A phantom phantom
-data A (x :: k) (y :: k1)
+data A (x :: k1) (y :: k)
   	-- Defined at <interactive>:2:1
-A :: k -> k1 -> *
+A :: k1 -> k -> *
 type role T phantom
 data T (a :: k) where
   MkT :: forall k (a :: k) a1. a1 -> T a
diff --git a/testsuite/tests/ghci/scripts/T7939.stdout b/testsuite/tests/ghci/scripts/T7939.stdout
index 2b2c8b73ad..0b41ebb2c6 100644
--- a/testsuite/tests/ghci/scripts/T7939.stdout
+++ b/testsuite/tests/ghci/scripts/T7939.stdout
@@ -16,12 +16,12 @@ H :: Bool -> Bool
 type family J (a :: [k]) :: Bool
   where
     [k] J k '[] = 'False
-    [k, (h :: k), (t :: [k])] J k (h : t) = 'True
+    [k, (t :: [k]), (h :: k)] J k (h : t) = 'True
   	-- Defined at T7939.hs:17:1
 J :: [k] -> Bool
 type family K (a1 :: [a]) :: Maybe a
   where
     [a] K a '[] = 'Nothing
-    [a, (h :: a), (t :: [a])] K a (h : t) = 'Just h
+    [a, (t :: [a]), (h :: a)] K a (h : t) = 'Just h
   	-- Defined at T7939.hs:21:1
 K :: [a] -> Maybe a
diff --git a/testsuite/tests/ghci/scripts/T8776.stdout b/testsuite/tests/ghci/scripts/T8776.stdout
index 937a270963..d0d9bd5240 100644
--- a/testsuite/tests/ghci/scripts/T8776.stdout
+++ b/testsuite/tests/ghci/scripts/T8776.stdout
@@ -1,2 +1,2 @@
-pattern P :: () => (Num t, Eq t1) => A t t1
+pattern P :: () => (Num t1, Eq t) => A t1 t
   	-- Defined at T8776.hs:6:1
diff --git a/testsuite/tests/indexed-types/should_compile/T3017.stderr b/testsuite/tests/indexed-types/should_compile/T3017.stderr
index 3000395aa2..bedb722475 100644
--- a/testsuite/tests/indexed-types/should_compile/T3017.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T3017.stderr
@@ -4,7 +4,7 @@ TYPE SIGNATURES
   emptyL :: forall a. ListColl a
   insert :: forall c. Coll c => Elem c -> c -> c
   test2 ::
-    forall c t t1. (Elem c ~ (t, t1), Coll c, Num t1, Num t) => c -> c
+    forall t t1 c. (Elem c ~ (t, t1), Coll c, Num t1, Num t) => c -> c
 TYPE CONSTRUCTORS
   class Coll c where
     type family Elem c :: * open
diff --git a/testsuite/tests/indexed-types/should_compile/T8889.stderr b/testsuite/tests/indexed-types/should_compile/T8889.stderr
index b93be8cc36..81359b291c 100644
--- a/testsuite/tests/indexed-types/should_compile/T8889.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T8889.stderr
@@ -1,6 +1,6 @@
 
 T8889.hs:12:1: warning: [-Wmissing-signatures (in -Wall)]
     Top-level binding with no type signature:
-      f :: forall (f :: * -> *) a b.
+      f :: forall (f :: * -> *) b a.
            (C f, C_fmap f a) =>
            (a -> b) -> f a -> f b
diff --git a/testsuite/tests/indexed-types/should_fail/T7354.stderr b/testsuite/tests/indexed-types/should_fail/T7354.stderr
index b56db1398f..0332181394 100644
--- a/testsuite/tests/indexed-types/should_fail/T7354.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7354.stderr
@@ -1,11 +1,11 @@
 
 T7354.hs:28:11: error:
     • Occurs check: cannot construct the infinite type:
-        t1 ~ Base t (Prim [t1] t1)
-      Expected type: Prim [t1] t1 -> Base t (Prim [t1] t1)
-        Actual type: Prim [t1] t1 -> t1
+        t ~ Base t1 (Prim [t] t)
+      Expected type: Prim [t] t -> Base t1 (Prim [t] t)
+        Actual type: Prim [t] t -> t
     • In the first argument of ‘ana’, namely ‘alg’
       In the expression: ana alg
       In an equation for ‘foo’: foo = ana alg
     • Relevant bindings include
-        foo :: Prim [t1] t1 -> t (bound at T7354.hs:28:1)
+        foo :: Prim [t] t -> t1 (bound at T7354.hs:28:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T8518.stderr b/testsuite/tests/indexed-types/should_fail/T8518.stderr
index 037bb76bbe..a152f55f25 100644
--- a/testsuite/tests/indexed-types/should_fail/T8518.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8518.stderr
@@ -18,9 +18,9 @@ T8518.hs:14:18: error:
         callCont :: c -> Z c -> B c -> Maybe (F c) (bound at T8518.hs:14:1)
 
 T8518.hs:16:9: error:
-    • Couldn't match type ‘F t1’ with ‘Z t1 -> B t1 -> F t1’
-      Expected type: t -> t1 -> F t1
-        Actual type: t -> t1 -> Z t1 -> B t1 -> F t1
+    • Couldn't match type ‘F t’ with ‘Z t -> B t -> F t’
+      Expected type: t1 -> t -> F t
+        Actual type: t1 -> t -> Z t -> B t -> F t
     • In an equation for ‘callCont’:
           callCont c z b
             = rpt (4 :: Int) c z b
@@ -28,4 +28,4 @@ T8518.hs:16:9: error:
                 rpt 0 c' z' b' = fromJust (fst <$> (continue c' z' b'))
                 rpt i c' z' b' = let ... in rpt (i - 1) c''
     • Relevant bindings include
-        rpt :: t -> t1 -> F t1 (bound at T8518.hs:16:9)
+        rpt :: t1 -> t -> F t (bound at T8518.hs:16:9)
diff --git a/testsuite/tests/module/mod71.stderr b/testsuite/tests/module/mod71.stderr
index 9480e92271..d02aac28fa 100644
--- a/testsuite/tests/module/mod71.stderr
+++ b/testsuite/tests/module/mod71.stderr
@@ -1,12 +1,12 @@
 
 mod71.hs:4:9: error:
-    • Found hole: _ :: t
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of f :: Num t1 => (t -> t1 -> t2) -> t2
+    • Found hole: _ :: t1
+      Where: ‘t1’ is a rigid type variable bound by
+               the inferred type of f :: Num t => (t1 -> t -> t2) -> t2
                at mod71.hs:4:1
     • In the first argument of ‘x’, namely ‘_’
       In the expression: x _ 1
       In an equation for ‘f’: f x = x _ 1
     • Relevant bindings include
-        x :: t -> t1 -> t2 (bound at mod71.hs:4:3)
-        f :: (t -> t1 -> t2) -> t2 (bound at mod71.hs:4:1)
+        x :: t1 -> t -> t2 (bound at mod71.hs:4:3)
+        f :: (t1 -> t -> t2) -> t2 (bound at mod71.hs:4:1)
diff --git a/testsuite/tests/module/mod72.stderr b/testsuite/tests/module/mod72.stderr
index 69246edb76..f546dc8139 100644
--- a/testsuite/tests/module/mod72.stderr
+++ b/testsuite/tests/module/mod72.stderr
@@ -1,2 +1,2 @@
 
-mod72.hs:3:7: error: Variable not in scope: g :: t -> t1
+mod72.hs:3:7: error: Variable not in scope: g :: t1 -> t
diff --git a/testsuite/tests/parser/should_compile/read014.stderr b/testsuite/tests/parser/should_compile/read014.stderr
index 4b324b1b2a..d7c43e53f2 100644
--- a/testsuite/tests/parser/should_compile/read014.stderr
+++ b/testsuite/tests/parser/should_compile/read014.stderr
@@ -1,7 +1,7 @@
 
 read014.hs:4:1: warning: [-Wmissing-signatures (in -Wall)]
     Top-level binding with no type signature:
-      ng1 :: forall t a. Num a => t -> a -> a
+      ng1 :: forall a t. Num a => t -> a -> a
 
 read014.hs:4:5: warning: [-Wunused-matches (in -Wextra)]
     Defined but not used: ‘x’
diff --git a/testsuite/tests/parser/should_fail/readFail003.stderr b/testsuite/tests/parser/should_fail/readFail003.stderr
index e837eeedd1..963bc50d72 100644
--- a/testsuite/tests/parser/should_fail/readFail003.stderr
+++ b/testsuite/tests/parser/should_fail/readFail003.stderr
@@ -1,7 +1,7 @@
 
 readFail003.hs:4:27: error:
     • Occurs check: cannot construct the infinite type:
-        t ~ (t, [a], [a1])
+        t ~ (t, [a1], [a])
     • In the expression: a
       In a pattern binding:
         ~(a, b, c)
@@ -12,5 +12,5 @@ readFail003.hs:4:27: error:
               nullity = null
     • Relevant bindings include
         a :: t (bound at readFail003.hs:4:3)
-        b :: [a] (bound at readFail003.hs:4:5)
-        c :: [a1] (bound at readFail003.hs:4:7)
+        b :: [a1] (bound at readFail003.hs:4:5)
+        c :: [a] (bound at readFail003.hs:4:7)
diff --git a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
index c34b1396c7..ee31ed289c 100644
--- a/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/ExtraConstraints3.stderr
@@ -1,28 +1,28 @@
 TYPE SIGNATURES
   !! :: forall a. [a] -> Int -> a
-  $ :: forall a b. (a -> b) -> a -> b
-  $! :: forall a b. (a -> b) -> a -> b
+  $ :: forall b a. (a -> b) -> a -> b
+  $! :: forall b a. (a -> b) -> a -> b
   && :: Bool -> Bool -> Bool
   * :: forall a. Num a => a -> a -> a
   ** :: forall a. Floating a => a -> a -> a
   + :: forall a. Num a => a -> a -> a
   ++ :: forall a. [a] -> [a] -> [a]
   - :: forall a. Num a => a -> a -> a
-  . :: forall b c a. (b -> c) -> (a -> b) -> a -> c
+  . :: forall a c b. (b -> c) -> (a -> b) -> a -> c
   / :: forall a. Fractional a => a -> a -> a
   /= :: forall a. Eq a => a -> a -> Bool
   < :: forall a. Ord a => a -> a -> Bool
   <= :: forall a. Ord a => a -> a -> Bool
   =<< ::
-    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
+    forall (m :: * -> *) b a. Monad m => (a -> m b) -> m a -> m b
   == :: forall a. Eq a => a -> a -> Bool
   > :: forall a. Ord a => a -> a -> Bool
   >= :: forall a. Ord a => a -> a -> Bool
-  >> :: forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
+  >> :: forall b (m :: * -> *) a. Monad m => m a -> m b -> m b
   >>= ::
-    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
-  ^ :: forall a b. (Num a, Integral b) => a -> b -> a
-  ^^ :: forall a b. (Integral b, Fractional a) => a -> b -> a
+    forall b (m :: * -> *) a. Monad m => m a -> (a -> m b) -> m b
+  ^ :: forall b a. (Num a, Integral b) => a -> b -> a
+  ^^ :: forall b a. (Integral b, Fractional a) => a -> b -> a
   abs :: forall a. Num a => a -> a
   acos :: forall a. Floating a => a -> a
   acosh :: forall a. Floating a => a -> a
@@ -39,22 +39,22 @@ TYPE SIGNATURES
   atan2 :: forall a. RealFloat a => a -> a -> a
   atanh :: forall a. Floating a => a -> a
   break :: forall a. (a -> Bool) -> [a] -> ([a], [a])
-  ceiling :: forall a b. (RealFrac a, Integral b) => a -> b
+  ceiling :: forall b a. (RealFrac a, Integral b) => a -> b
   compare :: forall a. Ord a => a -> a -> Ordering
   concat :: forall (t :: * -> *) a. P.Foldable t => t [a] -> [a]
   concatMap ::
-    forall (t :: * -> *) a b. P.Foldable t => (a -> [b]) -> t a -> [b]
-  const :: forall a b. a -> b -> a
+    forall (t :: * -> *) b a. P.Foldable t => (a -> [b]) -> t a -> [b]
+  const :: forall b a. a -> b -> a
   cos :: forall a. Floating a => a -> a
   cosh :: forall a. Floating a => a -> a
-  curry :: forall a b c. ((a, b) -> c) -> a -> b -> c
+  curry :: forall c a b. ((a, b) -> c) -> a -> b -> c
   cycle :: forall a. [a] -> [a]
   decodeFloat :: forall a. RealFloat a => a -> (Integer, Int)
   div :: forall a. Integral a => a -> a -> a
   divMod :: forall a. Integral a => a -> a -> (a, a)
   drop :: forall a. Int -> [a] -> [a]
   dropWhile :: forall a. (a -> Bool) -> [a] -> [a]
-  either :: forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
+  either :: forall b c a. (a -> c) -> (b -> c) -> Either a b -> c
   elem ::
     forall (t :: * -> *) a. (P.Foldable t, Eq a) => a -> t a -> Bool
   encodeFloat :: forall a. RealFloat a => Integer -> Int -> a
@@ -68,28 +68,28 @@ TYPE SIGNATURES
   exponent :: forall a. RealFloat a => a -> Int
   fail :: forall (m :: * -> *) a. Monad m => String -> m a
   filter :: forall a. (a -> Bool) -> [a] -> [a]
-  flip :: forall a b c. (a -> b -> c) -> b -> a -> c
+  flip :: forall c b a. (a -> b -> c) -> b -> a -> c
   floatDigits :: forall a. RealFloat a => a -> Int
   floatRadix :: forall a. RealFloat a => a -> Integer
   floatRange :: forall a. RealFloat a => a -> (Int, Int)
-  floor :: forall a b. (RealFrac a, Integral b) => a -> b
+  floor :: forall b a. (RealFrac a, Integral b) => a -> b
   fmap ::
-    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
+    forall (f :: * -> *) b a. Functor f => (a -> b) -> f a -> f b
   foldl ::
-    forall (t :: * -> *) b a.
+    forall (t :: * -> *) a b.
     P.Foldable t =>
     (b -> a -> b) -> b -> t a -> b
   foldl1 ::
     forall (t :: * -> *) a. P.Foldable t => (a -> a -> a) -> t a -> a
   foldr ::
-    forall (t :: * -> *) a b.
+    forall (t :: * -> *) b a.
     P.Foldable t =>
     (a -> b -> b) -> b -> t a -> b
   foldr1 ::
     forall (t :: * -> *) a. P.Foldable t => (a -> a -> a) -> t a -> a
   fromEnum :: forall a. Enum a => a -> Int
   fromInteger :: forall a. Num a => Integer -> a
-  fromIntegral :: forall a b. (Num b, Integral a) => a -> b
+  fromIntegral :: forall b a. (Num b, Integral a) => a -> b
   fromRational :: forall a. Fractional a => Rational -> a
   fst :: forall a b. (a, b) -> a
   gcd :: forall a. Integral a => a -> a -> a
@@ -114,21 +114,21 @@ TYPE SIGNATURES
   lines :: String -> [String]
   log :: forall a. Floating a => a -> a
   logBase :: forall a. Floating a => a -> a -> a
-  lookup :: forall a b. Eq a => a -> [(a, b)] -> Maybe b
-  map :: forall a b. (a -> b) -> [a] -> [b]
+  lookup :: forall b a. Eq a => a -> [(a, b)] -> Maybe b
+  map :: forall b a. (a -> b) -> [a] -> [b]
   mapM ::
-    forall (t :: * -> *) (m :: * -> *) a b.
+    forall (t :: * -> *) (m :: * -> *) b a.
     (P.Traversable t, Monad m) =>
     (a -> m b) -> t a -> m (t b)
   mapM_ ::
-    forall (t :: * -> *) (m :: * -> *) a b.
+    forall (t :: * -> *) (m :: * -> *) b a.
     (P.Foldable t, Monad m) =>
     (a -> m b) -> t a -> m ()
   max :: forall a. Ord a => a -> a -> a
   maxBound :: forall t. Bounded t => t
   maximum ::
     forall (t :: * -> *) a. (P.Foldable t, Ord a) => t a -> a
-  maybe :: forall b a. b -> (a -> b) -> Maybe a -> b
+  maybe :: forall a b. b -> (a -> b) -> Maybe a -> b
   min :: forall a. Ord a => a -> a -> a
   minBound :: forall t. Bounded t => t
   minimum ::
@@ -148,7 +148,7 @@ TYPE SIGNATURES
   product ::
     forall (t :: * -> *) a. (P.Foldable t, Num a) => t a -> a
   properFraction ::
-    forall a b. (RealFrac a, Integral b) => a -> (b, a)
+    forall b a. (RealFrac a, Integral b) => a -> (b, a)
   putChar :: Char -> IO ()
   putStr :: String -> IO ()
   putStrLn :: String -> IO ()
@@ -162,20 +162,20 @@ TYPE SIGNATURES
   readParen :: forall a. Bool -> ReadS a -> ReadS a
   reads :: forall a. Read a => ReadS a
   readsPrec :: forall a. Read a => Int -> ReadS a
-  realToFrac :: forall a b. (Real a, Fractional b) => a -> b
+  realToFrac :: forall b a. (Real a, Fractional b) => a -> b
   recip :: forall a. Fractional a => a -> a
   rem :: forall a. Integral a => a -> a -> a
   repeat :: forall a. a -> [a]
   replicate :: forall a. Int -> a -> [a]
   return :: forall (m :: * -> *) a. Monad m => a -> m a
   reverse :: forall a. [a] -> [a]
-  round :: forall a b. (RealFrac a, Integral b) => a -> b
+  round :: forall b a. (RealFrac a, Integral b) => a -> b
   scaleFloat :: forall a. RealFloat a => Int -> a -> a
-  scanl :: forall b a. (b -> a -> b) -> b -> [a] -> [b]
+  scanl :: forall a b. (b -> a -> b) -> b -> [a] -> [b]
   scanl1 :: forall a. (a -> a -> a) -> [a] -> [a]
-  scanr :: forall a b. (a -> b -> b) -> b -> [a] -> [b]
+  scanr :: forall b a. (a -> b -> b) -> b -> [a] -> [b]
   scanr1 :: forall a. (a -> a -> a) -> [a] -> [a]
-  seq :: forall a b. a -> b -> b
+  seq :: forall b a. a -> b -> b
   sequence ::
     forall (t :: * -> *) (m :: * -> *) a.
     (P.Traversable t, Monad m) =>
@@ -210,8 +210,8 @@ TYPE SIGNATURES
   toEnum :: forall a. Enum a => Int -> a
   toInteger :: forall a. Integral a => a -> Integer
   toRational :: forall a. Real a => a -> Rational
-  truncate :: forall a b. (RealFrac a, Integral b) => a -> b
-  uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
+  truncate :: forall b a. (RealFrac a, Integral b) => a -> b
+  uncurry :: forall c b a. (a -> b -> c) -> (a, b) -> c
   undefined :: forall t. t
   unlines :: [String] -> String
   until :: forall a. (a -> Bool) -> (a -> a) -> a -> a
@@ -221,11 +221,11 @@ TYPE SIGNATURES
   userError :: String -> IOError
   words :: String -> [String]
   writeFile :: FilePath -> String -> IO ()
-  zip :: forall a b. [a] -> [b] -> [(a, b)]
-  zip3 :: forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
-  zipWith :: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
+  zip :: forall b a. [a] -> [b] -> [(a, b)]
+  zip3 :: forall c b a. [a] -> [b] -> [c] -> [(a, b, c)]
+  zipWith :: forall c b a. (a -> b -> c) -> [a] -> [b] -> [c]
   zipWith3 ::
-    forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
+    forall d c b a. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
   || :: Bool -> Bool -> Bool
 TYPE CONSTRUCTORS
 COERCION AXIOMS
diff --git a/testsuite/tests/partial-sigs/should_compile/NamedTyVar.stderr b/testsuite/tests/partial-sigs/should_compile/NamedTyVar.stderr
index 88cf133f15..3e0743702f 100644
--- a/testsuite/tests/partial-sigs/should_compile/NamedTyVar.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/NamedTyVar.stderr
@@ -1,7 +1,7 @@
 TYPE SIGNATURES
-  foo :: forall b a. (a, b) -> (a, b)
+  foo :: forall a b. (a, b) -> (a, b)
 TYPE CONSTRUCTORS
 COERCION AXIOMS
 Dependent modules: []
 Dependent packages: [base-4.9.0.0, ghc-prim-0.5.0.0,
-                     integer-gmp-1.0.0.0]
+                     integer-gmp-1.0.0.1]
diff --git a/testsuite/tests/partial-sigs/should_compile/SkipMany.stderr b/testsuite/tests/partial-sigs/should_compile/SkipMany.stderr
index 5b94077eb0..6209498942 100644
--- a/testsuite/tests/partial-sigs/should_compile/SkipMany.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/SkipMany.stderr
@@ -2,7 +2,7 @@ TYPE SIGNATURES
   SkipMany.GenParser ::
     forall tok st a. tok -> st -> a -> GenParser tok st a
   skipMany ::
-    forall tok st a. GenParser tok st a -> GenParser tok st ()
+    forall a tok st. GenParser tok st a -> GenParser tok st ()
   skipMany' ::
     forall tok st a. GenParser tok st a -> GenParser tok st ()
 TYPE CONSTRUCTORS
diff --git a/testsuite/tests/partial-sigs/should_compile/T10438.stderr b/testsuite/tests/partial-sigs/should_compile/T10438.stderr
index 3871a6345e..0742250be3 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10438.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10438.stderr
@@ -24,5 +24,5 @@ T10438.hs:7:22: warning: [-Wpartial-type-signatures (in -Wdefault)]
         x :: t2 (bound at T10438.hs:8:17)
         r :: t2 (bound at T10438.hs:6:11)
         g :: t2 -> t2 (bound at T10438.hs:6:9)
-        f :: t (bound at T10438.hs:5:5)
-        foo :: t -> forall t1. t1 -> t1 (bound at T10438.hs:5:1)
+        f :: t1 (bound at T10438.hs:5:5)
+        foo :: t1 -> forall t. t -> t (bound at T10438.hs:5:1)
diff --git a/testsuite/tests/partial-sigs/should_compile/UncurryNamed.stderr b/testsuite/tests/partial-sigs/should_compile/UncurryNamed.stderr
index 58116f8b16..2ff8d3da3f 100644
--- a/testsuite/tests/partial-sigs/should_compile/UncurryNamed.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/UncurryNamed.stderr
@@ -1,5 +1,5 @@
 TYPE SIGNATURES
-  unc :: forall t a b. (a -> b -> t) -> (a, b) -> t
+  unc :: forall a b t. (a -> b -> t) -> (a, b) -> t
 TYPE CONSTRUCTORS
 COERCION AXIOMS
 Dependent modules: []
diff --git a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
index 7013696580..b5268acb60 100644
--- a/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/WarningWildcardInstantiations.stderr
@@ -1,5 +1,5 @@
 TYPE SIGNATURES
-  bar :: forall t t1. t1 -> (t1 -> t) -> t
+  bar :: forall t t1. t -> (t -> t1) -> t1
   foo :: forall a. (Show a, Enum a) => a -> String
 TYPE CONSTRUCTORS
 COERCION AXIOMS
@@ -30,37 +30,37 @@ WarningWildcardInstantiations.hs:5:30: warning: [-Wpartial-type-signatures (in -
         foo :: a -> String (bound at WarningWildcardInstantiations.hs:6:1)
 
 WarningWildcardInstantiations.hs:8:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘t1’
-      Where: ‘t1’ is a rigid type variable bound by
-               the inferred type of bar :: t1 -> (t1 -> t) -> t
+    • Found type wildcard ‘_’ standing for ‘t’
+      Where: ‘t’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> t1) -> t1
                at WarningWildcardInstantiations.hs:9:1
     • In the type signature:
         bar :: _ -> _ -> _
     • Relevant bindings include
-        bar :: t1 -> (t1 -> t) -> t
+        bar :: t -> (t -> t1) -> t1
           (bound at WarningWildcardInstantiations.hs:9:1)
 
 WarningWildcardInstantiations.hs:8:13: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘t1 -> t’
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of bar :: t1 -> (t1 -> t) -> t
+    • Found type wildcard ‘_’ standing for ‘t -> t1’
+      Where: ‘t1’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> t1) -> t1
                at WarningWildcardInstantiations.hs:9:1
-             ‘t1’ is a rigid type variable bound by
-               the inferred type of bar :: t1 -> (t1 -> t) -> t
+             ‘t’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> t1) -> t1
                at WarningWildcardInstantiations.hs:9:1
     • In the type signature:
         bar :: _ -> _ -> _
     • Relevant bindings include
-        bar :: t1 -> (t1 -> t) -> t
+        bar :: t -> (t -> t1) -> t1
           (bound at WarningWildcardInstantiations.hs:9:1)
 
 WarningWildcardInstantiations.hs:8:18: warning: [-Wpartial-type-signatures (in -Wdefault)]
-    • Found type wildcard ‘_’ standing for ‘t’
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of bar :: t1 -> (t1 -> t) -> t
+    • Found type wildcard ‘_’ standing for ‘t1’
+      Where: ‘t1’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> t1) -> t1
                at WarningWildcardInstantiations.hs:9:1
     • In the type signature:
         bar :: _ -> _ -> _
     • Relevant bindings include
-        bar :: t1 -> (t1 -> t) -> t
+        bar :: t -> (t -> t1) -> t1
           (bound at WarningWildcardInstantiations.hs:9:1)
diff --git a/testsuite/tests/partial-sigs/should_fail/T10045.stderr b/testsuite/tests/partial-sigs/should_fail/T10045.stderr
index 42218b5fe9..d6a3a5ac37 100644
--- a/testsuite/tests/partial-sigs/should_fail/T10045.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/T10045.stderr
@@ -1,10 +1,10 @@
 
 T10045.hs:6:18: error:
-    • Found type wildcard ‘_’ standing for ‘t1 -> Bool -> t2’
-      Where: ‘t2’ is a rigid type variable bound by
-               the inferred type of copy :: t1 -> Bool -> t2 at T10045.hs:7:10
-             ‘t1’ is a rigid type variable bound by
-               the inferred type of copy :: t1 -> Bool -> t2 at T10045.hs:7:10
+    • Found type wildcard ‘_’ standing for ‘t2 -> Bool -> t1’
+      Where: ‘t1’ is a rigid type variable bound by
+               the inferred type of copy :: t2 -> Bool -> t1 at T10045.hs:7:10
+             ‘t2’ is a rigid type variable bound by
+               the inferred type of copy :: t2 -> Bool -> t1 at T10045.hs:7:10
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
         copy :: _
@@ -20,6 +20,6 @@ T10045.hs:6:18: error:
                 copy w from = copy w True
               in copy ws1 False
     • Relevant bindings include
-        copy :: t1 -> Bool -> t2 (bound at T10045.hs:7:10)
+        copy :: t2 -> Bool -> t1 (bound at T10045.hs:7:10)
         ws1 :: () (bound at T10045.hs:5:11)
         foo :: Meta -> t (bound at T10045.hs:5:1)
diff --git a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
index ff18935c8d..63058a9781 100644
--- a/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/WildcardInstantiations.stderr
@@ -25,40 +25,40 @@ WildcardInstantiations.hs:5:30: error:
         foo :: a -> String (bound at WildcardInstantiations.hs:6:1)
 
 WildcardInstantiations.hs:8:8: error:
-    • Found type wildcard ‘_’ standing for ‘t1’
-      Where: ‘t1’ is a rigid type variable bound by
-               the inferred type of bar :: t1 -> (t1 -> t) -> t
+    • Found type wildcard ‘_’ standing for ‘t’
+      Where: ‘t’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> t1) -> t1
                at WildcardInstantiations.hs:9:1
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
         bar :: _ -> _ -> _
     • Relevant bindings include
-        bar :: t1 -> (t1 -> t) -> t
+        bar :: t -> (t -> t1) -> t1
           (bound at WildcardInstantiations.hs:9:1)
 
 WildcardInstantiations.hs:8:13: error:
-    • Found type wildcard ‘_’ standing for ‘t1 -> t’
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of bar :: t1 -> (t1 -> t) -> t
+    • Found type wildcard ‘_’ standing for ‘t -> t1’
+      Where: ‘t1’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> t1) -> t1
                at WildcardInstantiations.hs:9:1
-             ‘t1’ is a rigid type variable bound by
-               the inferred type of bar :: t1 -> (t1 -> t) -> t
+             ‘t’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> t1) -> t1
                at WildcardInstantiations.hs:9:1
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
         bar :: _ -> _ -> _
     • Relevant bindings include
-        bar :: t1 -> (t1 -> t) -> t
+        bar :: t -> (t -> t1) -> t1
           (bound at WildcardInstantiations.hs:9:1)
 
 WildcardInstantiations.hs:8:18: error:
-    • Found type wildcard ‘_’ standing for ‘t’
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of bar :: t1 -> (t1 -> t) -> t
+    • Found type wildcard ‘_’ standing for ‘t1’
+      Where: ‘t1’ is a rigid type variable bound by
+               the inferred type of bar :: t -> (t -> t1) -> t1
                at WildcardInstantiations.hs:9:1
       To use the inferred type, enable PartialTypeSignatures
     • In the type signature:
         bar :: _ -> _ -> _
     • Relevant bindings include
-        bar :: t1 -> (t1 -> t) -> t
+        bar :: t -> (t -> t1) -> t1
           (bound at WildcardInstantiations.hs:9:1)
diff --git a/testsuite/tests/patsyn/should_compile/T11213.stderr b/testsuite/tests/patsyn/should_compile/T11213.stderr
index 88d8f84a53..7a0af54b67 100644
--- a/testsuite/tests/patsyn/should_compile/T11213.stderr
+++ b/testsuite/tests/patsyn/should_compile/T11213.stderr
@@ -19,7 +19,7 @@ T11213.hs:23:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
 
 T11213.hs:24:1: warning: [-Wmissing-pattern-synonym-signatures (in -Wall)]
     Top-level binding with no type signature:
-      Purp :: forall a t.
+      Purp :: forall t a.
               (Num a, Eq a) =>
               Show t => a -> t -> ([a], UnivProv t)
 
diff --git a/testsuite/tests/polykinds/T7438.stderr b/testsuite/tests/polykinds/T7438.stderr
index d3ed001879..12d93fcf0f 100644
--- a/testsuite/tests/polykinds/T7438.stderr
+++ b/testsuite/tests/polykinds/T7438.stderr
@@ -1,19 +1,19 @@
 
 T7438.hs:6:14: error:
-    • Couldn't match expected type ‘t3’ with actual type ‘t2’
-        ‘t3’ is untouchable
-          inside the constraints: t1 ~ t
+    • Couldn't match expected type ‘t2’ with actual type ‘t3’
+        ‘t2’ is untouchable
+          inside the constraints: t ~ t1
           bound by a pattern with constructor:
                      Nil :: forall k (a :: k). Thrist a a,
                    in an equation for ‘go’
           at T7438.hs:6:4-6
-      ‘t3’ is a rigid type variable bound by
-        the inferred type of go :: Thrist t t1 -> t2 -> t3 at T7438.hs:6:1
       ‘t2’ is a rigid type variable bound by
-        the inferred type of go :: Thrist t t1 -> t2 -> t3 at T7438.hs:6:1
+        the inferred type of go :: Thrist t1 t -> t3 -> t2 at T7438.hs:6:1
+      ‘t3’ is a rigid type variable bound by
+        the inferred type of go :: Thrist t1 t -> t3 -> t2 at T7438.hs:6:1
       Possible fix: add a type signature for ‘go’
     • In the expression: acc
       In an equation for ‘go’: go Nil acc = acc
     • Relevant bindings include
-        acc :: t2 (bound at T7438.hs:6:8)
-        go :: Thrist t t1 -> t2 -> t3 (bound at T7438.hs:6:1)
+        acc :: t3 (bound at T7438.hs:6:8)
+        go :: Thrist t1 t -> t3 -> t2 (bound at T7438.hs:6:1)
diff --git a/testsuite/tests/polykinds/T7524.stderr b/testsuite/tests/polykinds/T7524.stderr
index 2340ce1aa6..c096719735 100644
--- a/testsuite/tests/polykinds/T7524.stderr
+++ b/testsuite/tests/polykinds/T7524.stderr
@@ -2,5 +2,5 @@
 T7524.hs:5:15: error:
     Conflicting family instance declarations:
       forall k2 (a :: k2). F a a = Int -- Defined at T7524.hs:5:15
-      forall k2 k1 (a :: k1) (b :: k2).
+      forall k2 k1 (b :: k2) (a :: k1).
         F a b = Bool -- Defined at T7524.hs:6:15
diff --git a/testsuite/tests/rename/should_fail/T2993.stderr b/testsuite/tests/rename/should_fail/T2993.stderr
index 4cae65ae88..4baecc277b 100644
--- a/testsuite/tests/rename/should_fail/T2993.stderr
+++ b/testsuite/tests/rename/should_fail/T2993.stderr
@@ -1,4 +1,4 @@
 
 T2993.hs:7:13: error:
-    • Variable not in scope: (<**>) :: t -> (b -> b) -> t1
+    • Variable not in scope: (<**>) :: t1 -> (b -> b) -> t
     • Perhaps you meant ‘<*>’ (imported from Prelude)
diff --git a/testsuite/tests/typecheck/should_compile/T10971a.stderr b/testsuite/tests/typecheck/should_compile/T10971a.stderr
index 0702b32384..72c675aa8c 100644
--- a/testsuite/tests/typecheck/should_compile/T10971a.stderr
+++ b/testsuite/tests/typecheck/should_compile/T10971a.stderr
@@ -11,7 +11,7 @@ T10971a.hs:7:11: warning: [-Wtype-defaults (in -Wall)]
 
 T10971a.hs:8:1: warning: [-Wmissing-signatures (in -Wall)]
     Top-level binding with no type signature:
-      g :: forall a b. (a -> b) -> [a] -> [b]
+      g :: forall b a. (a -> b) -> [a] -> [b]
 
 T10971a.hs:8:6: warning: [-Wname-shadowing (in -Wall)]
     This binding for ‘f’ shadows the existing binding
diff --git a/testsuite/tests/typecheck/should_compile/tc141.stderr b/testsuite/tests/typecheck/should_compile/tc141.stderr
index 15bdad80c3..49a26d6363 100644
--- a/testsuite/tests/typecheck/should_compile/tc141.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc141.stderr
@@ -35,7 +35,7 @@ tc141.hs:13:13: error:
         in v
 
 tc141.hs:15:18: error:
-    • Couldn't match expected type ‘a1’ with actual type ‘t1’
+    • Couldn't match expected type ‘a1’ with actual type ‘t’
         because type variable ‘a1’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
@@ -50,5 +50,5 @@ tc141.hs:15:18: error:
         in v
     • Relevant bindings include
         v :: a1 (bound at tc141.hs:15:14)
-        b :: t1 (bound at tc141.hs:13:5)
-        g :: t -> t1 -> forall a. a (bound at tc141.hs:13:1)
+        b :: t (bound at tc141.hs:13:5)
+        g :: t1 -> t -> forall a. a (bound at tc141.hs:13:1)
diff --git a/testsuite/tests/typecheck/should_compile/tc168.stderr b/testsuite/tests/typecheck/should_compile/tc168.stderr
index 16ba4b0446..5bcce5b457 100644
--- a/testsuite/tests/typecheck/should_compile/tc168.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc168.stderr
@@ -9,4 +9,4 @@ tc168.hs:17:1: error:
     • In the ambiguity check for the inferred type for ‘g’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       When checking the inferred type
-        g :: forall a b a1. C a1 (a, b) => a1 -> a
+        g :: forall b a a1. C a1 (a, b) => a1 -> a
diff --git a/testsuite/tests/typecheck/should_compile/tc231.stderr b/testsuite/tests/typecheck/should_compile/tc231.stderr
index dd5624849a..daa77b3313 100644
--- a/testsuite/tests/typecheck/should_compile/tc231.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc231.stderr
@@ -2,7 +2,7 @@ TYPE SIGNATURES
   Node :: forall s a chain. s -> a -> chain -> Q s a chain
   Z :: forall a. a -> Z a
   foo ::
-    forall s b chain.
+    forall chain s b.
     Zork s (Z [Char]) b =>
     Q s (Z [Char]) chain -> ST s ()
   huh ::
diff --git a/testsuite/tests/typecheck/should_fail/T5853.stderr b/testsuite/tests/typecheck/should_fail/T5853.stderr
index d9a8244483..c95dc53d1c 100644
--- a/testsuite/tests/typecheck/should_fail/T5853.stderr
+++ b/testsuite/tests/typecheck/should_fail/T5853.stderr
@@ -1,23 +1,23 @@
 
 T5853.hs:15:46: error:
-    • Could not deduce: Subst t1 (Elem t2) ~ t2
+    • Could not deduce: Subst t (Elem t2) ~ t2
         arising from a use of ‘<$>’
-      from the context: (F t,
-                         Elem t ~ Elem t,
-                         Elem t2 ~ Elem t2,
-                         Subst t (Elem t2) ~ t2,
-                         Subst t2 (Elem t) ~ t,
-                         F t1,
+      from the context: (F t1,
                          Elem t1 ~ Elem t1,
+                         Elem t2 ~ Elem t2,
+                         Subst t1 (Elem t2) ~ t2,
+                         Subst t2 (Elem t1) ~ t1,
+                         F t,
                          Elem t ~ Elem t,
-                         Subst t1 (Elem t) ~ t,
-                         Subst t (Elem t1) ~ t1)
+                         Elem t1 ~ Elem t1,
+                         Subst t (Elem t1) ~ t1,
+                         Subst t1 (Elem t) ~ t)
         bound by the RULE "map/map" at T5853.hs:15:2-57
       ‘t2’ is a rigid type variable bound by
         the RULE "map/map" at T5853.hs:15:2
     • In the expression: (f . g) <$> xs
       When checking the transformation rule "map/map"
     • Relevant bindings include
-        f :: Elem t -> Elem t2 (bound at T5853.hs:15:19)
-        g :: Elem t1 -> Elem t (bound at T5853.hs:15:21)
-        xs :: t1 (bound at T5853.hs:15:23)
+        f :: Elem t1 -> Elem t2 (bound at T5853.hs:15:19)
+        g :: Elem t -> Elem t1 (bound at T5853.hs:15:21)
+        xs :: t (bound at T5853.hs:15:23)
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index c20c9ecc89..3bd6b40a82 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -79,7 +79,7 @@ T6018fail.hs:66:15: error:
     Kind variable ‘k’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
-      forall k (a :: k) (b :: k).
+      forall k (b :: k) (a :: k).
         Fc a b = Int -- Defined at T6018fail.hs:66:15
 
 T6018fail.hs:70:15: error:
@@ -88,7 +88,7 @@ T6018fail.hs:70:15: error:
     cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
-      forall k (a :: k) (b :: k).
+      forall k (b :: k) (a :: k).
         Gc a b = Int -- Defined at T6018fail.hs:70:15
 
 T6018fail.hs:74:15: error:
@@ -145,7 +145,7 @@ T6018fail.hs:118:15: error:
     cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
-      forall k a b (c :: k).
+      forall k (c :: k) b a.
         G7 a b c = [G7a a b c] -- Defined at T6018fail.hs:118:15
 
 T6018fail.hs:129:1: error:
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
index 6cc0c3700e..7a0146d7d7 100644
--- a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
@@ -24,11 +24,11 @@ T6018failclosed.hs:19:5: error:
 
 T6018failclosed.hs:25:5: error:
     • Type family equation violates injectivity annotation.
-      Type and kind variables ‘k’, ‘b’
+      Type and kind variables ‘k1’, ‘b’
       cannot be inferred from the right-hand side.
       Use -fprint-explicit-kinds to see the kind arguments
       In the type family equation:
-        forall k k1 (b :: k) (c :: k1).
+        forall k k1 (c :: k) (b :: k1).
           JClosed Int b c = Char -- Defined at T6018failclosed.hs:25:5
     • In the equations for closed type family ‘JClosed’
       In the type family declaration for ‘JClosed’
@@ -90,7 +90,7 @@ T6018failclosed.hs:66:5: error:
       Kind variable ‘k’ cannot be inferred from the right-hand side.
       Use -fprint-explicit-kinds to see the kind arguments
       In the type family equation:
-        forall k (a :: k) (b :: k).
+        forall k (b :: k) (a :: k).
           Gc a b = Int -- Defined at T6018failclosed.hs:66:5
     • In the equations for closed type family ‘Gc’
       In the type family declaration for ‘Gc’
diff --git a/testsuite/tests/typecheck/should_fail/T7453.stderr b/testsuite/tests/typecheck/should_fail/T7453.stderr
index bcb2df84c8..6b8e920004 100644
--- a/testsuite/tests/typecheck/should_fail/T7453.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7453.stderr
@@ -28,14 +28,14 @@ T7453.hs:9:15: error:
         cast1 :: t -> a (bound at T7453.hs:7:1)
 
 T7453.hs:15:15: error:
-    • Couldn't match type ‘t’ with ‘t2’
+    • Couldn't match type ‘t1’ with ‘t2’
         because type variable ‘t2’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
           z :: () -> t2
         at T7453.hs:14:11-22
       Expected type: () -> t2
-        Actual type: () -> t
+        Actual type: () -> t1
     • In the expression: aux
       In an equation for ‘z’:
           z = aux
@@ -50,13 +50,13 @@ T7453.hs:15:15: error:
                   where
                       aux = const v
     • Relevant bindings include
-        aux :: forall b. b -> t (bound at T7453.hs:16:21)
+        aux :: forall b. b -> t1 (bound at T7453.hs:16:21)
         z :: () -> t2 (bound at T7453.hs:15:11)
-        v :: t (bound at T7453.hs:13:7)
-        cast2 :: t -> t1 (bound at T7453.hs:13:1)
+        v :: t1 (bound at T7453.hs:13:7)
+        cast2 :: t1 -> t (bound at T7453.hs:13:1)
 
 T7453.hs:21:15: error:
-    • Couldn't match expected type ‘t2’ with actual type ‘t’
+    • Couldn't match expected type ‘t2’ with actual type ‘t1’
         because type variable ‘t2’ would escape its scope
       This (rigid, skolem) type variable is bound by
         the type signature for:
@@ -76,7 +76,7 @@ T7453.hs:21:15: error:
                   where
                       aux = const v
     • Relevant bindings include
-        aux :: forall b. b -> t (bound at T7453.hs:22:21)
+        aux :: forall b. b -> t1 (bound at T7453.hs:22:21)
         z :: t2 (bound at T7453.hs:21:11)
-        v :: t (bound at T7453.hs:19:7)
-        cast3 :: t -> forall t1. t1 (bound at T7453.hs:19:1)
+        v :: t1 (bound at T7453.hs:19:7)
+        cast3 :: t1 -> forall t. t (bound at T7453.hs:19:1)
diff --git a/testsuite/tests/typecheck/should_fail/T7734.stderr b/testsuite/tests/typecheck/should_fail/T7734.stderr
index 1b1716bfc5..8553fdb888 100644
--- a/testsuite/tests/typecheck/should_fail/T7734.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7734.stderr
@@ -1,18 +1,18 @@
 
 T7734.hs:4:13: error:
-    • Occurs check: cannot construct the infinite type: t1 ~ t1 -> t2
+    • Occurs check: cannot construct the infinite type: t2 ~ t2 -> t1
     • In the first argument of ‘x’, namely ‘x’
       In the expression: x x
       In an equation for ‘f’: x `f` y = x x
     • Relevant bindings include
-        x :: t1 -> t2 (bound at T7734.hs:4:1)
-        f :: (t1 -> t2) -> t -> t2 (bound at T7734.hs:4:3)
+        x :: t2 -> t1 (bound at T7734.hs:4:1)
+        f :: (t2 -> t1) -> t -> t1 (bound at T7734.hs:4:3)
 
 T7734.hs:5:13: error:
-    • Occurs check: cannot construct the infinite type: t1 ~ t1 -> t2
+    • Occurs check: cannot construct the infinite type: t2 ~ t2 -> t1
     • In the first argument of ‘x’, namely ‘x’
       In the expression: x x
       In an equation for ‘&’: (&) x y = x x
     • Relevant bindings include
-        x :: t1 -> t2 (bound at T7734.hs:5:5)
-        (&) :: (t1 -> t2) -> t -> t2 (bound at T7734.hs:5:1)
+        x :: t2 -> t1 (bound at T7734.hs:5:5)
+        (&) :: (t2 -> t1) -> t -> t1 (bound at T7734.hs:5:1)
diff --git a/testsuite/tests/typecheck/should_fail/T8142.stderr b/testsuite/tests/typecheck/should_fail/T8142.stderr
index 3faa530996..53e6798a5e 100644
--- a/testsuite/tests/typecheck/should_fail/T8142.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8142.stderr
@@ -8,7 +8,7 @@ T8142.hs:6:18: error:
     • In the ambiguity check for the inferred type for ‘h’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       When checking the inferred type
-        h :: forall t (g :: * -> *). Nu ((,) t) -> Nu g
+        h :: forall (g :: * -> *) t. Nu ((,) t) -> Nu g
       In an equation for ‘tracer’:
           tracer
             = h
diff --git a/testsuite/tests/typecheck/should_fail/T9109.stderr b/testsuite/tests/typecheck/should_fail/T9109.stderr
index 6a08318ac0..71d88efdc8 100644
--- a/testsuite/tests/typecheck/should_fail/T9109.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9109.stderr
@@ -1,15 +1,15 @@
 
 T9109.hs:8:13: error:
-    • Couldn't match expected type ‘t1’ with actual type ‘Bool’
-        ‘t1’ is untouchable
-          inside the constraints: t ~ Bool
+    • Couldn't match expected type ‘t’ with actual type ‘Bool’
+        ‘t’ is untouchable
+          inside the constraints: t1 ~ Bool
           bound by a pattern with constructor: GBool :: G Bool,
                    in an equation for ‘foo’
           at T9109.hs:8:5-9
-      ‘t1’ is a rigid type variable bound by
-        the inferred type of foo :: G t -> t1 at T9109.hs:8:1
+      ‘t’ is a rigid type variable bound by
+        the inferred type of foo :: G t1 -> t at T9109.hs:8:1
       Possible fix: add a type signature for ‘foo’
     • In the expression: True
       In an equation for ‘foo’: foo GBool = True
     • Relevant bindings include
-        foo :: G t -> t1 (bound at T9109.hs:8:1)
+        foo :: G t1 -> t (bound at T9109.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail004.stderr b/testsuite/tests/typecheck/should_fail/tcfail004.stderr
index c575129cf5..41a55c1ea9 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail004.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail004.stderr
@@ -1,9 +1,9 @@
 
 tcfail004.hs:3:9: error:
-    • Couldn't match expected type ‘(t, t1)’
+    • Couldn't match expected type ‘(t1, t)’
                   with actual type ‘(Integer, Integer, Integer)’
     • In the expression: (1, 2, 3)
       In a pattern binding: (f, g) = (1, 2, 3)
     • Relevant bindings include
-        f :: t (bound at tcfail004.hs:3:2)
-        g :: t1 (bound at tcfail004.hs:3:4)
+        f :: t1 (bound at tcfail004.hs:3:2)
+        g :: t (bound at tcfail004.hs:3:4)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail033.stderr b/testsuite/tests/typecheck/should_fail/tcfail033.stderr
index 94e998f05f..e349ab1116 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail033.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail033.stderr
@@ -1,10 +1,10 @@
 
 tcfail033.hs:4:12: error:
-    • Occurs check: cannot construct the infinite type: t ~ (t, t1)
+    • Occurs check: cannot construct the infinite type: t1 ~ (t1, t)
     • In the expression: x
       In the expression: [x | (x, y) <- buglet]
       In an equation for ‘buglet’: buglet = [x | (x, y) <- buglet]
     • Relevant bindings include
-        y :: t1 (bound at tcfail033.hs:4:19)
-        x :: t (bound at tcfail033.hs:4:17)
-        buglet :: [(t, t1)] (bound at tcfail033.hs:4:1)
+        y :: t (bound at tcfail033.hs:4:19)
+        x :: t1 (bound at tcfail033.hs:4:17)
+        buglet :: [(t1, t)] (bound at tcfail033.hs:4:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail049.stderr b/testsuite/tests/typecheck/should_fail/tcfail049.stderr
index 1b74ce0070..ec83902d6f 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail049.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail049.stderr
@@ -1,2 +1,2 @@
 
-tcfail049.hs:3:7: error: Variable not in scope: g :: t -> t1
+tcfail049.hs:3:7: error: Variable not in scope: g :: t1 -> t
diff --git a/testsuite/tests/typecheck/should_fail/tcfail050.stderr b/testsuite/tests/typecheck/should_fail/tcfail050.stderr
index 2ca5065938..9d6a0c06b2 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail050.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail050.stderr
@@ -1,3 +1,3 @@
 
 tcfail050.hs:3:7: error:
-    Data constructor not in scope: B :: t -> t1
+    Data constructor not in scope: B :: t1 -> t
diff --git a/testsuite/tests/typecheck/should_fail/tcfail140.stderr b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
index 4c3fecec43..f75f77c38a 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail140.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
@@ -9,14 +9,14 @@ tcfail140.hs:10:7: error:
     • Relevant bindings include bar :: t (bound at tcfail140.hs:10:1)
 
 tcfail140.hs:12:10: error:
-    • Couldn't match expected type ‘Integer -> t1’
+    • Couldn't match expected type ‘Integer -> t’
                   with actual type ‘Int’
     • The operator ‘f’ takes two arguments,
       but its type ‘Int -> Int’ has only one
       In the expression: 3 `f` 4
       In an equation for ‘rot’: rot xs = 3 `f` 4
     • Relevant bindings include
-        rot :: t -> t1 (bound at tcfail140.hs:12:1)
+        rot :: t1 -> t (bound at tcfail140.hs:12:1)
 
 tcfail140.hs:14:15: error:
     • Couldn't match expected type ‘t -> b’ with actual type ‘Int’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail198.stderr b/testsuite/tests/typecheck/should_fail/tcfail198.stderr
index 88469939f3..51aaf1d58e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail198.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail198.stderr
@@ -1,6 +1,6 @@
 
 tcfail198.hs:6:36: error:
-    • Couldn't match expected type ‘a2’ with actual type ‘a1’
+    • Couldn't match expected type ‘a2’ with actual type ‘a’
         because type variable ‘a2’ would escape its scope
       This (rigid, skolem) type variable is bound by
         an expression type signature:
@@ -10,6 +10,6 @@ tcfail198.hs:6:36: error:
       In the second argument of ‘(++)’, namely ‘[x :: a]’
       In the expression: xs ++ [x :: a]
     • Relevant bindings include
-        xs :: [a1] (bound at tcfail198.hs:6:21)
-        x :: a1 (bound at tcfail198.hs:6:19)
-        f3 :: [a1] -> [a1] (bound at tcfail198.hs:6:6)
+        xs :: [a] (bound at tcfail198.hs:6:21)
+        x :: a (bound at tcfail198.hs:6:19)
+        f3 :: [a] -> [a] (bound at tcfail198.hs:6:6)