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

13 files changed, 123 insertions, 17 deletions

diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs
index e578411360..04260bc0e1 100644
--- a/compiler/hsSyn/HsTypes.hs
+++ b/compiler/hsSyn/HsTypes.hs
@@ -245,10 +245,22 @@ the a in the code. Thus, GHC does a *stable topological sort* on the variables.
 By "stable", we mean that any two variables who do not depend on each other
 preserve their existing left-to-right ordering.
 
-Implicitly bound variables are collected by extractHsTysRdrTyVars and friends
-in RnTypes. These functions thus promise to keep left-to-right ordering.
+Implicitly bound variables are collected by the extract- family of functions
+(extractHsTysRdrTyVars, extractHsTyVarBndrsKVs, etc.) in RnTypes.
+These functions thus promise to keep left-to-right ordering.
 Look for pointers to this note to see the places where the action happens.
 
+Note that we also maintain this ordering in kind signatures. Even though
+there's no visible kind application (yet), having implicit variables be
+quantified in left-to-right order in kind signatures is nice since:
+
+* It's consistent with the treatment for type signatures.
+* It can affect how types are displayed with -fprint-explicit-kinds (see
+  #15568 for an example), which is a situation where knowing the order in
+  which implicit variables are quantified can be useful.
+* In the event that visible kind application is implemented, the order in
+  which we would expect implicit variables to be ordered in kinds will have
+  already been established.
 -}
 
 -- | Located Haskell Context
@@ -337,6 +349,7 @@ data HsImplicitBndrs pass thing   -- See Note [HsType binders]
                                          -- Implicitly-bound kind & type vars
                                          -- Order is important; see
                                          -- Note [Ordering of implicit variables]
+                                         -- in RnTypes
 
          , hsib_body :: thing            -- Main payload (type or list of types)
     }
diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index e5f51660da..a78caaf6ba 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -344,7 +344,7 @@ rnImplicitBndrs bind_free_tvs
 
        ; loc <- getSrcSpanM
           -- NB: kinds before tvs, as mandated by
-          -- Note [Ordering of implicit variables] in HsTypes
+          -- Note [Ordering of implicit variables]
        ; vars <- mapM (newLocalBndrRn . L loc . unLoc) (kvs ++ real_tvs)
 
        ; traceRn "checkMixedVars2" $
@@ -837,7 +837,10 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs hsq_bndrs thing_inside
              -- all these various things are doing
              bndrs, kv_occs, implicit_kvs :: [Located RdrName]
              bndrs        = map hsLTyVarLocName hs_tv_bndrs
-             kv_occs      = nubL (body_kv_occs ++ bndr_kv_occs)
+             kv_occs      = nubL (bndr_kv_occs ++ body_kv_occs)
+                                 -- Make sure to list the binder kvs before the
+                                 -- body kvs, as mandated by
+                                 -- Note [Ordering of implicit variables]
              implicit_kvs = filter_occs rdr_env bndrs kv_occs
                                  -- Deleting bndrs: See Note [Kind-variable ordering]
              -- dep_bndrs is the subset of bndrs that are dependent
@@ -1519,7 +1522,10 @@ In general we want to walk over a type, and find
   * The free kind variables of any kind signatures in the type
 
 Hence we return a pair (kind-vars, type vars)
-See also Note [HsBSig binder lists] in HsTypes
+(See Note [HsBSig binder lists] in HsTypes.)
+Moreover, we preserve the left-to-right order of the first occurrence of each
+variable, while preserving dependency order.
+(See Note [Ordering of implicit variables].)
 
 Most clients of this code just want to know the kind/type vars, without
 duplicates. The function rmDupsInRdrTyVars removes duplicates. That function
@@ -1548,12 +1554,57 @@ var, then this would prevent it from being implicitly quantified (see
 rnImplicitBndrs). In the `foo` example above, that would have the consequence
 of the k in Proxy k being reported as out of scope.
 
+Note [Ordering of implicit variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Since the advent of -XTypeApplications, GHC makes promises about the ordering
+of implicit variable quantification. Specifically, we offer that implicitly
+quantified variables (such as those in const :: a -> b -> a, without a `forall`)
+will occur in left-to-right order of first occurrence. Here are a few examples:
+
+  const :: a -> b -> a       -- forall a b. ...
+  f :: Eq a => b -> a -> a   -- forall a b. ...  contexts are included
+
+  type a <-< b = b -> a
+  g :: a <-< b               -- forall a b. ...  type synonyms matter
+
+  class Functor f where
+    fmap :: (a -> b) -> f a -> f b   -- forall f a b. ...
+    -- The f is quantified by the class, so only a and b are considered in fmap
+
+This simple story is complicated by the possibility of dependency: all variables
+must come after any variables mentioned in their kinds.
+
+  typeRep :: Typeable a => TypeRep (a :: k)   -- forall k a. ...
+
+The k comes first because a depends on k, even though the k appears later than
+the a in the code. Thus, GHC does a *stable topological sort* on the variables.
+By "stable", we mean that any two variables who do not depend on each other
+preserve their existing left-to-right ordering.
+
+Implicitly bound variables are collected by any function which returns a
+FreeKiTyVars, FreeKiTyVarsWithDups, or FreeKiTyVarsNoDups, which notably
+includes the `extract-` family of functions (extractHsTysRdrTyVars,
+extractHsTyVarBndrsKVs, etc.).
+These functions thus promise to keep left-to-right ordering.
+Look for pointers to this note to see the places where the action happens.
+
+Note that we also maintain this ordering in kind signatures. Even though
+there's no visible kind application (yet), having implicit variables be
+quantified in left-to-right order in kind signatures is nice since:
+
+* It's consistent with the treatment for type signatures.
+* It can affect how types are displayed with -fprint-explicit-kinds (see
+  #15568 for an example), which is a situation where knowing the order in
+  which implicit variables are quantified can be useful.
+* In the event that visible kind application is implemented, the order in
+  which we would expect implicit variables to be ordered in kinds will have
+  already been established.
 -}
 
 -- See Note [Kind and type-variable binders]
 -- These lists are guaranteed to preserve left-to-right ordering of
 -- the types the variables were extracted from. See also
--- Note [Ordering of implicit variables] in HsTypes.
+-- Note [Ordering of implicit variables].
 data FreeKiTyVars = FKTV { fktv_kis    :: [Located RdrName]
                          , fktv_tys    :: [Located RdrName] }
 
@@ -1614,8 +1665,10 @@ extractHsTyRdrTyVarsDups ty
 -- | Extracts the free kind variables (but not the type variables) of an
 -- 'HsType'. Does not return any wildcards.
 -- When the same name occurs multiple times in the type, only the first
--- occurrence is returned.
--- See Note [Kind and type-variable binders]
+-- occurrence is returned, and the left-to-right order of variables is
+-- preserved.
+-- See Note [Kind and type-variable binders] and
+-- Note [Ordering of implicit variables].
 extractHsTyRdrTyVarsKindVars :: LHsType GhcPs -> RnM [Located RdrName]
 extractHsTyRdrTyVarsKindVars ty
   = freeKiTyVarsKindVars <$> extractHsTyRdrTyVars ty
@@ -1636,7 +1689,9 @@ extractHsTysRdrTyVarsDups tys
   = extract_ltys TypeLevel tys emptyFKTV
 
 extractHsTyVarBndrsKVs :: [LHsTyVarBndr GhcPs] -> RnM [Located RdrName]
--- Returns the free kind variables of any explictly-kinded binders
+-- Returns the free kind variables of any explictly-kinded binders, returning
+-- variable occurrences in left-to-right order.
+-- See Note [Ordering of implicit variables].
 -- NB: Does /not/ delete the binders themselves.
 --     However duplicates are removed
 --     E.g. given  [k1, a:k1, b:k2]
@@ -1657,6 +1712,9 @@ rmDupsInRdrTyVars (FKTV kis tys)
     tys' = nubL (filterOut (`elemRdr` kis') tys)
 
 extractRdrKindSigVars :: LFamilyResultSig GhcPs -> RnM [Located RdrName]
+-- Returns the free kind variables in a type family result signature, returning
+-- variable occurrences in left-to-right order.
+-- See Note [Ordering of implicit variables].
 extractRdrKindSigVars (L _ resultSig)
     | KindSig _ k                          <- resultSig = kindRdrNameFromSig k
     | TyVarSig _ (L _ (KindedTyVar _ _ k)) <- resultSig = kindRdrNameFromSig k
@@ -1677,6 +1735,8 @@ extractDataDefnKindVars :: HsDataDefn GhcPs -> RnM [Located RdrName]
 --         data D = D
 --         instance forall k (a::k). C @k @* a D where ...
 --
+-- This returns variable occurrences in left-to-right order.
+-- See Note [Ordering of implicit variables].
 extractDataDefnKindVars (HsDataDefn { dd_ctxt = ctxt, dd_kindSig = ksig
                                     , dd_cons = cons })
   = (nubL . freeKiTyVarsKindVars) <$>
@@ -1800,7 +1860,9 @@ extract_hs_tv_bndrs tv_bndrs
               (filterOut (`elemRdr` tv_bndr_rdrs) body_tvs ++ acc_tvs) }
 
 extract_hs_tv_bndrs_kvs :: [LHsTyVarBndr GhcPs] -> RnM [Located RdrName]
--- Returns the free kind variables of any explictly-kinded binders
+-- Returns the free kind variables of any explictly-kinded binders, returning
+-- variable occurrences in left-to-right order.
+-- See Note [Ordering of implicit variables].
 -- NB: Does /not/ delete the binders themselves.
 --     Duplicates are /not/ removed
 --     E.g. given  [k1, a:k1, b:k2]
@@ -1818,7 +1880,13 @@ extract_tv t_or_k ltv@(L _ tv) acc@(FKTV kvs tvs)
   | isTypeLevel t_or_k  = return (FKTV kvs (ltv : tvs))
   | otherwise           = return (FKTV (ltv : kvs) tvs)
 
--- just used in this module; seemed convenient here
+-- Deletes duplicates in a list of Located things.
+--
+-- Importantly, this function is stable with respect to the original ordering
+-- of things in the list. This is important, as it is a property that GHC
+-- relies on to maintain the left-to-right ordering of implicitly quantified
+-- type variables.
+-- See Note [Ordering of implicit variables].
 nubL :: Eq a => [Located a] -> [Located a]
 nubL = nubBy eqLocated
 
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index ed488320b0..a70db2ebda 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1744,7 +1744,7 @@ tcImplicitTKBndrsX new_tv skol_info tv_names thing_inside
           -- use zonkTcTyCoVarBndr because a skol_tv might be a TyVarTv
 
           -- do a stable topological sort, following
-          -- Note [Ordering of implicit variables] in HsTypes
+          -- Note [Ordering of implicit variables] in RnTypes
        ; let final_tvs = toposortTyVars skol_tvs
        ; traceTc "tcImplicitTKBndrs" (ppr tv_names $$ ppr final_tvs)
        ; return (final_tvs, result) }
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 9b4aec670d..33cdae3e63 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1912,7 +1912,7 @@ predTypeEqRel ty
 -- It is also meant to be stable: that is, variables should not
 -- be reordered unnecessarily. The implementation of this
 -- has been observed to be stable, though it is not proven to
--- be so. See also Note [Ordering of implicit variables] in HsTypes
+-- be so. See also Note [Ordering of implicit variables] in RnTypes
 toposortTyVars :: [TyCoVar] -> [TyCoVar]
 toposortTyVars tvs = reverse $
                      [ node_payload node | node <- topologicalSortG $
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index ca782a9399..abd679af3b 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -10688,6 +10688,17 @@ Here are the details:
   if you want the most accurate information with respect to visible type
   application properties.
 
+- Although GHC supports visible *type* applications, it does not yet support
+  visible *kind* applications. However, GHC does follow similar rules for
+  quantifying variables in kind signatures as it does for quantifying type
+  signatures. For instance: ::
+
+    type family F (a :: j) (b :: k) :: l
+      -- F :: forall j k l. j -> k -> l
+
+  In the kind of ``F``, the left-to-right ordering of ``j``, ``k``, and ``l``
+  is preserved.
+
 .. _implicit-parameters:
 
 Implicit parameters
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