Quantify class variables first in associated families' kinds

Summary:
Previously, `kcLHsQTyVars` would always quantify class-bound
variables invisibly in the kinds of associated types, resulting in
#15591. We counteract this by explicitly passing the class-bound
variables to `kcLHsQTyVars` and quantifying over the ones that are
mentioned in the associated type such that (1) they are specified,
and (2) they come before other kind variables.
See `Note [Kind variable ordering for associated types]`.

Test Plan: make test TEST=T15591

Reviewers: goldfire, simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #15591

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

7 files changed, 138 insertions, 30 deletions

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index a9d6d46344..4b755e4086 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1514,10 +1514,13 @@ tcWildCardBinders wc_names thing_inside
 kcLHsQTyVars :: Name              -- ^ of the thing being checked
              -> TyConFlavour      -- ^ What sort of 'TyCon' is being checked
              -> Bool              -- ^ True <=> the decl being checked has a CUSK
+             -> [(Name, TyVar)]   -- ^ If the thing being checked is associated
+                                  --   with a class, this is the class's scoped
+                                  --   type variables. Empty otherwise.
              -> LHsQTyVars GhcRn
              -> TcM Kind          -- ^ The result kind
              -> TcM TcTyCon       -- ^ A suitably-kinded TcTyCon
-kcLHsQTyVars name flav cusk
+kcLHsQTyVars name flav cusk parent_tv_prs
   user_tyvars@(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns
                                            , hsq_dependent = dep_names }
                       , hsq_explicit = hs_tvs }) thing_inside
@@ -1532,7 +1535,16 @@ kcLHsQTyVars name flav cusk
        ; let tc_binders_unzonked = zipWith mk_tc_binder hs_tvs tc_tvs
        ; dvs  <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys scoped_kvs $
                                             mkTyConKind tc_binders_unzonked res_kind)
-       ; qkvs <- quantifyTyVars emptyVarSet dvs
+       ; let -- Any type variables bound by the parent class that are specified
+             -- in this declaration (associated with the class). We single
+             -- these out because we want to bind these first in this
+             -- declaration's kind.
+             -- See Note [Kind variable ordering for associated types].
+             reused_from_parent_tv_prs =
+               filter (\(_, tv) -> tv `elemDVarSet` dv_kvs dvs
+                                || tv `elemDVarSet` dv_tvs dvs) parent_tv_prs
+             reused_from_parent_tvs = map snd reused_from_parent_tv_prs
+       ; qkvs <- quantifyTyVars (mkVarSet reused_from_parent_tvs) dvs
          -- don't call tcGetGlobalTyCoVars. For associated types, it gets the
          -- tyvars from the enclosing class -- but that's wrong. We *do* want
          -- to quantify over those tyvars.
@@ -1553,21 +1565,37 @@ kcLHsQTyVars name flav cusk
                                            scoped_kvs
        ; reportFloatingKvs name flav all_tc_tvs unmentioned_kvs
 
-       ; let final_binders =  map (mkNamedTyConBinder Inferred) qkvs
-                           ++ map (mkNamedTyConBinder Specified) scoped_kvs
+       ; let all_scoped_kvs = reused_from_parent_tvs ++ scoped_kvs
+             final_binders =  map (mkNamedTyConBinder Inferred) qkvs
+                           ++ map (mkNamedTyConBinder Specified) all_scoped_kvs
                            ++ tc_binders
+             all_tv_prs = reused_from_parent_tv_prs ++
+                          mkTyVarNamePairs (scoped_kvs ++ tc_tvs)
              tycon = mkTcTyCon name (ppr user_tyvars) final_binders res_kind
-                               (mkTyVarNamePairs (scoped_kvs ++ tc_tvs))
-                               flav
+                               all_tv_prs flav
                            -- the tvs contain the binders already
                            -- in scope from an enclosing class, but
                            -- re-adding tvs to the env't doesn't cause
                            -- harm
 
        ; traceTc "kcLHsQTyVars: cusk" $
-         vcat [ ppr name, ppr kv_ns, ppr hs_tvs, ppr dep_names
-              , ppr tc_tvs, ppr (mkTyConKind final_binders res_kind)
-              , ppr qkvs, ppr final_binders ]
+         vcat [ text "name" <+> ppr name
+              , text "kv_ns" <+> ppr kv_ns
+              , text "hs_tvs" <+> ppr hs_tvs
+              , text "dep_names" <+> ppr dep_names
+              , text "scoped_kvs" <+> ppr scoped_kvs
+              , text "reused_from_parent_tv_prs"
+                <+> ppr reused_from_parent_tv_prs
+              , text "tc_tvs" <+> ppr tc_tvs
+              , text "res_kind" <+> ppr res_kind
+              , text "dvs" <+> ppr dvs
+              , text "qkvs" <+> ppr qkvs
+              , text "all_scoped_kvs" <+> ppr all_scoped_kvs
+              , text "tc_binders" <+> ppr tc_binders
+              , text "final_binders" <+> ppr final_binders
+              , text "mkTyConKind final_binders res_kind"
+                <+> ppr (mkTyConKind final_binders res_kind)
+              , text "all_tv_prs" <+> ppr all_tv_prs ]
 
        ; return tycon }
 
@@ -1601,7 +1629,7 @@ kcLHsQTyVars name flav cusk
        | otherwise
        = mkAnonTyConBinder tv
 
-kcLHsQTyVars _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
+kcLHsQTyVars _ _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
 
 kcLHsQTyVarBndrs :: Bool   -- True <=> bump the TcLevel when bringing vars into scope
                  -> Bool   -- True <=> Default un-annotated tyvar
@@ -1685,6 +1713,40 @@ See Note [Associated type tyvar names] in Class and
 We must do the same for family instance decls, where the in-scope
 variables may be bound by the enclosing class instance decl.
 Hence the use of tcImplicitQTKBndrs in tcFamTyPats.
+
+Note [Kind variable ordering for associated types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+What should be the kind of `T` in the following example? (#15591)
+
+  class C (a :: Type) where
+    type T (x :: f a)
+
+As per Note [Ordering of implicit variables] in RnTypes, we want to quantify
+the kind variables in left-to-right order of first occurrence in order to
+support visible kind application. But we cannot perform this analysis on just
+T alone, since its variable `a` actually occurs /before/ `f` if you consider
+the fact that `a` was previously bound by the parent class `C`. That is to say,
+the kind of `T` should end up being:
+
+  T :: forall a f. f a -> Type
+
+(It wouldn't necessarily be /wrong/ if the kind ended up being, say,
+forall f a. f a -> Type, but that would not be as predictable for users of
+visible kind application.)
+
+In contrast, if `T` were redefined to be a top-level type family, like `T2`
+below:
+
+  type family T2 (x :: f (a :: Type))
+
+Then `a` first appears /after/ `f`, so the kind of `T2` should be:
+
+  T2 :: forall f a. f a -> Type
+
+In order to make this distinction, we need to know (in kcLHsQTyVars) which
+type variables have been bound by the parent class (if there is one). With
+the class-bound variables in hand, we can ensure that we always quantify
+these first.
 -}
 
 
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 8419b90465..ae64f084b0 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -73,6 +73,7 @@ import BasicTypes
 import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
+import Control.Monad.Zip
 import Data.List
 import Data.List.NonEmpty ( NonEmpty(..) )
 import qualified Data.Set as Set
@@ -630,11 +631,12 @@ getInitialKind :: TyClDecl GhcRn -> TcM [TcTyCon]
 
 getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
   = do { let cusk = hsDeclHasCusk decl
-       ; tycon <- kcLHsQTyVars name ClassFlavour cusk ktvs $
+       ; tycon <- kcLHsQTyVars name ClassFlavour cusk [] ktvs $
                   return constraintKind
+       ; let parent_tv_prs = tcTyConScopedTyVars tycon
             -- See Note [Don't process associated types in kcLHsQTyVars]
-       ; inner_tcs <- tcExtendNameTyVarEnv (tcTyConScopedTyVars tycon) $
-                      getFamDeclInitialKinds (Just cusk) ats
+       ; inner_tcs <- tcExtendNameTyVarEnv parent_tv_prs $
+                      getFamDeclInitialKinds (Just (cusk, parent_tv_prs)) ats
        ; return (tycon : inner_tcs) }
 
 getInitialKind decl@(DataDecl { tcdLName = L _ name
@@ -642,7 +644,8 @@ getInitialKind decl@(DataDecl { tcdLName = L _ name
                               , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
                                                          , dd_ND = new_or_data } })
   = do  { tycon <-
-           kcLHsQTyVars name (newOrDataToFlavour new_or_data) (hsDeclHasCusk decl) ktvs $
+           kcLHsQTyVars name (newOrDataToFlavour new_or_data)
+                        (hsDeclHasCusk decl) [] ktvs $
            case m_sig of
              Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig
              Nothing   -> return liftedTypeKind
@@ -655,7 +658,8 @@ getInitialKind (FamDecl { tcdFam = decl })
 getInitialKind decl@(SynDecl { tcdLName = L _ name
                              , tcdTyVars = ktvs
                              , tcdRhs = rhs })
-  = do  { tycon <- kcLHsQTyVars name TypeSynonymFlavour (hsDeclHasCusk decl) ktvs $
+  = do  { tycon <- kcLHsQTyVars name TypeSynonymFlavour (hsDeclHasCusk decl)
+                                [] ktvs $
             case kind_annotation rhs of
               Nothing -> newMetaKindVar
               Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig
@@ -671,20 +675,31 @@ getInitialKind (DataDecl _ (L _ _) _ _ (XHsDataDefn _)) = panic "getInitialKind"
 getInitialKind (XTyClDecl _) = panic "getInitialKind"
 
 ---------------------------------
-getFamDeclInitialKinds :: Maybe Bool  -- if assoc., CUSKness of assoc. class
-                       -> [LFamilyDecl GhcRn]
-                       -> TcM [TcTyCon]
-getFamDeclInitialKinds mb_cusk decls
-  = mapM (addLocM (getFamDeclInitialKind mb_cusk)) decls
-
-getFamDeclInitialKind :: Maybe Bool  -- if assoc., CUSKness of assoc. class
-                      -> FamilyDecl GhcRn
-                      -> TcM TcTyCon
-getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
-                                               , fdTyVars    = ktvs
-                                               , fdResultSig = L _ resultSig
-                                               , fdInfo      = info })
-  = do { tycon <- kcLHsQTyVars name flav cusk ktvs $
+getFamDeclInitialKinds
+  :: Maybe (Bool, [(Name, TyVar)])
+     -- ^ If this family declaration is associated with a class, this is
+     --   @'Just' (cusk, cls_tv_prs)@, where @cusk@ indicates the CUSKness of
+     --   the associated class and @cls_tv_prs@ contains the class's scoped
+     --   type variables.
+  -> [LFamilyDecl GhcRn]
+  -> TcM [TcTyCon]
+getFamDeclInitialKinds mb_parent_info decls
+  = mapM (addLocM (getFamDeclInitialKind mb_parent_info)) decls
+
+getFamDeclInitialKind
+  :: Maybe (Bool, [(Name, TyVar)])
+     -- ^ If this family declaration is associated with a class, this is
+     --   @'Just' (cusk, cls_tv_prs)@, where @cusk@ indicates the CUSKness of
+     --   the associated class and @cls_tv_prs@ contains the class's scoped
+     --   type variables.
+  -> FamilyDecl GhcRn
+  -> TcM TcTyCon
+getFamDeclInitialKind mb_parent_info
+    decl@(FamilyDecl { fdLName     = L _ name
+                     , fdTyVars    = ktvs
+                     , fdResultSig = L _ resultSig
+                     , fdInfo      = info })
+  = do { tycon <- kcLHsQTyVars name flav cusk parent_tv_prs ktvs $
            case resultSig of
              KindSig _ ki                          -> tcLHsKindSig ctxt ki
              TyVarSig _ (L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki
@@ -695,7 +710,9 @@ getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName     = L _ name
                | otherwise                -> newMetaKindVar
        ; return tycon }
   where
-    cusk  = famDeclHasCusk mb_cusk decl
+    (mb_cusk, mb_parent_tv_prs) = munzip mb_parent_info
+    cusk          = famDeclHasCusk mb_cusk decl
+    parent_tv_prs = mb_parent_tv_prs `orElse` []
     flav  = case info of
       DataFamily         -> DataFamilyFlavour (isJust mb_cusk)
       OpenTypeFamily     -> OpenTypeFamilyFlavour (isJust mb_cusk)
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 4fd6f1b2af..1664dbc571 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -10711,6 +10711,18 @@ Here are the details:
   In the kind of ``F``, the left-to-right ordering of ``j``, ``k``, and ``l``
   is preserved.
 
+  If a family declaration is associated with a class, then class-bound
+  variables always come first in the kind of the family. For instance: ::
+
+    class C (a :: Type) where
+      type T (x :: f a)
+      -- T :: forall a f. f a -> Type
+
+  Contrast this with the kind of the following top-level family declaration: ::
+
+    type family T2 (x :: f a)
+    -- T2 :: forall f a. f a -> Type
+
 .. _implicit-parameters:
 
 Implicit parameters
diff --git a/testsuite/tests/ghci/scripts/T15591.hs b/testsuite/tests/ghci/scripts/T15591.hs
new file mode 100644
index 0000000000..eccf628eed
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15591.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+module Foo where
+
+import Data.Kind
+
+type family T1 (x :: f (a :: Type))
+
+class C (a :: Type) where
+  type T2 (x :: f a)
diff --git a/testsuite/tests/ghci/scripts/T15591.script b/testsuite/tests/ghci/scripts/T15591.script
new file mode 100644
index 0000000000..0afd32e1e6
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15591.script
@@ -0,0 +1,4 @@
+:load T15591
+:set -fprint-explicit-foralls
+:kind T1
+:kind T2
diff --git a/testsuite/tests/ghci/scripts/T15591.stdout b/testsuite/tests/ghci/scripts/T15591.stdout
new file mode 100644
index 0000000000..28dbd49dc1
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T15591.stdout
@@ -0,0 +1,2 @@
+T1 :: forall (f :: * -> *) a. f a -> *
+T2 :: forall a (f :: * -> *). f a -> *
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index 290c274a94..dcc4855ab4 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -284,3 +284,4 @@ test('T15259', normal, ghci_script, ['T15259.script'])
 test('T15341', normal, ghci_script, ['T15341.script'])
 test('T15568', normal, ghci_script, ['T15568.script'])
 test('T15325', normal, ghci_script, ['T15325.script'])
+test('T15591', normal, ghci_script, ['T15591.script'])