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

1 files changed, 77 insertions, 9 deletions

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