Rename kind vars in left-to-right order in bindHsQTyVars

Summary:
When renaming kind variables in an `LHsQTyVars`, we were
erroneously putting all of the kind variables in the binders
//after// the kind variables in the body, resulting in #15568. The
fix is simple: just swap the order of these two around.

Test Plan: make test TEST=T15568

Reviewers: simonpj, bgamari, goldfire

Reviewed By: goldfire

Subscribers: goldfire, rwbarton, carter

GHC Trac Issues: #15568

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

8 files changed, 18 insertions, 4 deletions

diff --git a/testsuite/tests/ghci/scripts/T15568.hs b/testsuite/tests/ghci/scripts/T15568.hs
new file mode 100644
index 0000000000..2172fe2694
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15568.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module T15568 where
+
+import Data.Proxy
+
+type family F (a :: j) :: k
diff --git a/testsuite/tests/ghci/scripts/T15568.script b/testsuite/tests/ghci/scripts/T15568.script
new file mode 100644
index 0000000000..8218ccc7fd
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15568.script
@@ -0,0 +1,4 @@
+:load T15568
+:set -fprint-explicit-foralls
+putStrLn "-- This should print 'forall j k.', not 'forall k j.'"
+:kind F
diff --git a/testsuite/tests/ghci/scripts/T15568.stdout b/testsuite/tests/ghci/scripts/T15568.stdout
new file mode 100644
index 0000000000..e97cc6b040
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15568.stdout
@@ -0,0 +1,2 @@
+-- This should print 'forall j k.', not 'forall k j.'
+F :: forall j k. j -> k
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index d6ba833e35..9765244f1e 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -46,7 +46,7 @@
 
 <interactive>:60:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k2’ cannot be inferred from the right-hand side.
+    Kind variable ‘k1’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       PolyKindVars '[] = '[] -- Defined at <interactive>:60:15
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index b054be9c40..c02fb87e01 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -282,3 +282,4 @@ test('T14796', normal, ghci_script, ['T14796.script'])
 test('T14969', normal, ghci_script, ['T14969.script'])
 test('T15259', normal, ghci_script, ['T15259.script'])
 test('T15341', normal, ghci_script, ['T15341.script'])
+test('T15568', normal, ghci_script, ['T15568.script'])
diff --git a/testsuite/tests/polykinds/T11821a.stderr b/testsuite/tests/polykinds/T11821a.stderr
index 09077f83d3..2e443e637b 100644
--- a/testsuite/tests/polykinds/T11821a.stderr
+++ b/testsuite/tests/polykinds/T11821a.stderr
@@ -1,4 +1,4 @@
 
-T11821a.hs:4:77: error:
+T11821a.hs:4:31: error:
     • Couldn't match ‘k1’ with ‘k2’
     • In the type declaration for ‘SameKind’
diff --git a/testsuite/tests/polykinds/T14520.stderr b/testsuite/tests/polykinds/T14520.stderr
index 07042fde92..9c290ff4a5 100644
--- a/testsuite/tests/polykinds/T14520.stderr
+++ b/testsuite/tests/polykinds/T14520.stderr
@@ -1,6 +1,6 @@
 
 T14520.hs:15:24: error:
     • Expected kind ‘bat w w’,
-        but ‘Id’ has kind ‘XXX * a0 (XXX (a0 ~>> *) a0 kat0 b0) b0’
+        but ‘Id’ has kind ‘XXX a0 * (XXX a0 (a0 ~>> *) kat0 b0) b0’
     • In the first argument of ‘Sing’, namely ‘(Id :: bat w w)’
       In the type signature: sId :: Sing w -> Sing (Id :: bat w w)
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index 829e14ad70..f2fdf82b25 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -66,7 +66,7 @@ T6018fail.hs:59:10: error:
 
 T6018fail.hs:62:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k2’ cannot be inferred from the right-hand side.
+    Kind variable ‘k1’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       PolyKindVars '[] = '[] -- Defined at T6018fail.hs:62:15