Fix tcTyClTyVars to handle SigTvs

Previously, tcTyClTyVars required that the names of the LHsQTyVars
matched up exactly with the names of the kind of the given TyCon.
It now does a bit of matching up when necessary to relax this
restriction.

This commit enables a few tests that had previously been disabled.

The shortcoming this addresses is discussed in #11203, but that
ticket is not directly addressed here.

Test case: polykinds/SigTvKinds, perf/compiler/T9872d

3 files changed, 130 insertions, 63 deletions

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 28d1d3fda1..c7b208e80c 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -82,6 +82,7 @@ import Pair
 import qualified GHC.LanguageExtensions as LangExt
 
 import Data.Maybe
+import Data.List ( partition )
 import Control.Monad
 
 {-
@@ -1580,6 +1581,7 @@ Note [Free-floating kind vars]
 Consider
 
   data T = MkT (forall (a :: k). Proxy a)
+  -- from test ghci/scripts/T7873
 
 This is not an existential datatype, but a higher-rank one. Note that
 the forall to the right of MkT. Also consider
@@ -1603,7 +1605,17 @@ Here's the approach: in the first pass ("kind-checking") we just bring
 k into scope. In the second pass, we certainly hope that k has been
 integrated into the type's (generalized) kind, and so it should be found
 by splitTelescopeTvs. If it's not, then we must have a definition like
-T, and we reject.
+T, and we reject. (But see Note [Tiresome kind checking] about some extra
+processing necessary in the second pass.)
+
+Note [Tiresome kind matching]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Because of the use of SigTvs in kind inference (see #11203, for example)
+sometimes kind variables come into tcTClTyVars (the second, desugaring
+pass in TcTyClDecls) with the wrong names. The best way to fix this up
+is just to unify the kinds, again. So we return HsKind/Kind pairs from
+splitTelescopeTvs that can get unified in tcTyClTyVars, but only if there
+are kind vars the didn't link up in splitTelescopeTvs.
 
 -}
 
@@ -1628,14 +1640,15 @@ splitTelescopeTvs :: Kind         -- of the head of the telescope
                      , NameSet    -- ungeneralized implicit variables (case 2a)
                      , [TyVar]    -- implicit type variables (cases 1 & 2)
                      , [TyVar]    -- explicit type variables (cases 3 & 4)
+                     , [(LHsKind Name, Kind)] -- see Note [Tiresome kind matching]
                      , Kind )     -- result kind
 splitTelescopeTvs kind tvbs@(HsQTvs { hsq_implicit = hs_kvs
                                     , hsq_explicit = hs_tvs })
   = let (bndrs, inner_ki) = splitPiTys kind
-        (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, mk_kind)
+        (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, kind_matches, mk_kind)
           = mk_tvs [] [] bndrs (mkNameSet hs_kvs) hs_tvs
     in
-    (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, mk_kind inner_ki)
+    (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, kind_matches, mk_kind inner_ki)
   where
     mk_tvs :: [TyVar]    -- scoped tv accum (reversed)
            -> [TyVar]    -- implicit tv accum (reversed)
@@ -1646,6 +1659,7 @@ splitTelescopeTvs kind tvbs@(HsQTvs { hsq_implicit = hs_kvs
               , NameSet           -- Case 2a names
               , [TyVar]           -- implicit tyvars
               , [TyVar]           -- explicit tyvars
+              , [(LHsKind Name, Kind)]  -- tiresome kind matches
               , Type -> Type )    -- a function to create the result k
     mk_tvs scoped_tv_acc imp_tv_acc (bndr : bndrs) all_hs_kvs all_hs_tvs
       | Just tv <- binderVar_maybe bndr
@@ -1664,63 +1678,106 @@ splitTelescopeTvs kind tvbs@(HsQTvs { hsq_implicit = hs_kvs
      -- a non-CUSK. The kinds *aren't* generalized, so we won't see them
      -- here.
     mk_tvs scoped_tv_acc imp_tv_acc all_bndrs all_hs_kvs all_hs_tvs
-      = let (scoped, exp_tvs, mk_kind)
-              = mk_tvs2 scoped_tv_acc [] all_bndrs all_hs_tvs in
-        (scoped, all_hs_kvs, reverse imp_tv_acc, exp_tvs, mk_kind)
+      = let (scoped, exp_tvs, kind_matches, mk_kind)
+              = mk_tvs2 scoped_tv_acc [] [] all_bndrs all_hs_tvs in
+        (scoped, all_hs_kvs, reverse imp_tv_acc, exp_tvs, kind_matches, mk_kind)
            -- no more Case (1) or (2)
 
     -- This can't handle Case (1) or Case (2) from [Typechecking telescopes]
     mk_tvs2 :: [TyVar]
             -> [TyVar]   -- new parameter: explicit tv accum (reversed)
+            -> [(LHsKind Name, Kind)]  -- tiresome kind matches accum
             -> [TyBinder]
             -> [LHsTyVarBndr Name]
             -> ( [TyVar]
                , [TyVar]   -- explicit tvs only
+               , [(LHsKind Name, Kind)]  -- tiresome kind matches
                , Type -> Type )
-    mk_tvs2 scoped_tv_acc exp_tv_acc (bndr : bndrs) (hs_tv : hs_tvs)
+    mk_tvs2 scoped_tv_acc exp_tv_acc kind_match_acc (bndr : bndrs) (hs_tv : hs_tvs)
       | Just tv <- binderVar_maybe bndr
       = ASSERT2( isVisibleBinder bndr, err_doc )
         ASSERT( getName tv == hsLTyVarName hs_tv )
-        mk_tvs2 (tv : scoped_tv_acc) (tv : exp_tv_acc) bndrs hs_tvs   -- Case (3)
+        mk_tvs2 (tv : scoped_tv_acc) (tv : exp_tv_acc) kind_match_acc' bndrs hs_tvs
+            -- Case (3)
 
       | otherwise
       = ASSERT( isVisibleBinder bndr )
         let tv = mkTyVar (hsLTyVarName hs_tv) (binderType bndr) in
-        mk_tvs2 (tv : scoped_tv_acc) (tv : exp_tv_acc) bndrs hs_tvs   -- Case (4)
+        mk_tvs2 (tv : scoped_tv_acc) (tv : exp_tv_acc) kind_match_acc' bndrs hs_tvs
+               -- Case (4)
       where
         err_doc = vcat [ ppr (bndr : bndrs)
                        , ppr (hs_tv : hs_tvs)
                        , ppr kind
                        , ppr tvbs ]
 
-    mk_tvs2 scoped_tv_acc exp_tv_acc all_bndrs [] -- All done!
+        kind_match_acc' = case hs_tv of
+          L _ (UserTyVar {})          -> kind_match_acc
+          L _ (KindedTyVar _ hs_kind) -> (hs_kind, kind) : kind_match_acc
+            where kind = binderType bndr
+
+    mk_tvs2 scoped_tv_acc exp_tv_acc kind_match_acc all_bndrs [] -- All done!
       = ( reverse scoped_tv_acc
         , reverse exp_tv_acc
+        , kind_match_acc   -- no need to reverse; it's not ordered
         , mkForAllTys all_bndrs )
 
-    mk_tvs2 _ _ all_bndrs all_hs_tvs
+    mk_tvs2 _ _ _ all_bndrs all_hs_tvs
       = pprPanic "splitTelescopeTvs 2" (vcat [ ppr all_bndrs
                                              , ppr all_hs_tvs ])
 
 
 -----------------------
--- used on first pass only ("kind checking")
-kcTyClTyVars :: Name -> LHsQTyVars Name
+-- | "Kind check" the tyvars to a tycon. This is used during the "kind-checking"
+-- pass in TcTyClsDecls. (Never in getInitialKind, never in the
+-- "type-checking"/desugaring pass.) It works only for LHsQTyVars associated
+-- with a tycon, whose kind is known (partially) via getInitialKinds.
+-- Never emits constraints, though the thing_inside might.
+kcTyClTyVars :: Name   -- ^ of the tycon
+             -> LHsQTyVars Name
              -> TcM a -> TcM a
 kcTyClTyVars tycon hs_tvs thing_inside
-  = tc_tycl_tyvars False tycon hs_tvs $ \_ _ _ _ -> thing_inside
+  = do { kind <- kcLookupKind tycon
+       ; let (scoped_tvs, non_cusk_kv_name_set, all_kvs, all_tvs, _, res_k)
+               = splitTelescopeTvs kind hs_tvs
+       ; traceTc "kcTyClTyVars splitTelescopeTvs:"
+           (vcat [ text "Tycon:" <+> ppr tycon
+                 , text "Kind:" <+> ppr kind
+                 , text "hs_tvs:" <+> ppr hs_tvs
+                 , text "scoped tvs:" <+> pprWithCommas pprTvBndr scoped_tvs
+                 , text "implicit tvs:" <+> pprWithCommas pprTvBndr all_kvs
+                 , text "explicit tvs:" <+> pprWithCommas pprTvBndr all_tvs
+                 , text "non-CUSK kvs:" <+> ppr non_cusk_kv_name_set
+                 , text "res_k:" <+> ppr res_k] )
+
+            -- need to look up the non-cusk kvs in order to get their
+            -- kinds right, in case the kinds were informed by
+            -- the getInitialKinds pass
+       ; let non_cusk_kv_names = nameSetElems non_cusk_kv_name_set
+             free_kvs          = tyCoVarsOfTypes $
+                                 map tyVarKind (all_kvs ++ all_tvs)
+             mk_kv kv_name     = case lookupVarSetByName free_kvs kv_name of
+                                   Just kv -> return kv
+                                   Nothing ->
+                                     -- this kv isn't mentioned in the
+                                     -- LHsQTyVars at all. But maybe
+                                     -- it's mentioned in the body
+                                     -- In any case, just gin up a
+                                     -- meta-kind for it
+                                     do { kv_kind <- newMetaKindVar
+                                        ; return (new_skolem_tv kv_name kv_kind) }
+       ; non_cusk_kvs <- mapM mk_kv non_cusk_kv_names
+
+             -- The non_cusk_kvs are still scoped; they are mentioned by
+             -- name by the user
+       ; tcExtendTyVarEnv (non_cusk_kvs ++ scoped_tvs) $
+         thing_inside }
 
--- used on second pass only ("type checking", really desugaring)
 tcTyClTyVars :: Name -> LHsQTyVars Name      -- LHS of the type or class decl
              -> ([TyVar] -> [TyVar] -> Kind -> Kind -> TcM a) -> TcM a
-tcTyClTyVars = tc_tycl_tyvars True
-
-tc_tycl_tyvars :: Bool  -- are we doing the second pass?
-               -> Name -> LHsQTyVars Name      -- LHS of the type or class decl
-               -> ([TyVar] -> [TyVar] -> Kind -> Kind -> TcM a) -> TcM a
--- Used for the type variables of a type or class decl
--- on both the first and second full passes in TcTyClDecls.
--- *Not* used in the initial-kind run.
+-- ^ Used for the type variables of a type or class decl
+-- on the second full pass (type-checking/desugaring) in TcTyClDecls.
+-- This is *not* used in the initial-kind run, nor in the "kind-checking" pass.
 --
 -- (tcTyClTyVars T [a,b] thing_inside)
 --   where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
@@ -1729,17 +1786,15 @@ tc_tycl_tyvars :: Bool  -- are we doing the second pass?
 --   having also extended the type environment with bindings
 --   for k1,k2,a,b
 --
--- No need to freshen the k's because they are just skolem
--- constants here, and we are at top level anyway.
---
 -- Never emits constraints.
 --
--- The LHsTyVarBndrs is always user-written, and the kind of the tycon
--- is available in the local env.
-tc_tycl_tyvars second_pass tycon hs_tvs thing_inside
+-- The LHsTyVarBndrs is always user-written, and the full, generalised
+-- kind of the tycon is available in the local env.
+tcTyClTyVars tycon hs_tvs thing_inside
   = do { kind <- kcLookupKind tycon
-       ; let (scoped_tvs, non_cusk_kv_name_set, all_kvs, all_tvs, res_k)
-               = splitTelescopeTvs kind hs_tvs
+       ; let ( scoped_tvs, float_kv_name_set, all_kvs
+               , all_tvs, kind_matches, res_k )
+                 = splitTelescopeTvs kind hs_tvs
        ; traceTc "tcTyClTyVars splitTelescopeTvs:"
            (vcat [ text "Tycon:" <+> ppr tycon
                  , text "Kind:" <+> ppr kind
@@ -1747,34 +1802,48 @@ tc_tycl_tyvars second_pass tycon hs_tvs thing_inside
                  , text "scoped tvs:" <+> pprWithCommas pprTvBndr scoped_tvs
                  , text "implicit tvs:" <+> pprWithCommas pprTvBndr all_kvs
                  , text "explicit tvs:" <+> pprWithCommas pprTvBndr all_tvs
-                 , text "non-CUSK kvs:" <+> ppr non_cusk_kv_name_set
+                 , text "floating kvs:" <+> ppr float_kv_name_set
+                 , text "Tiresome kind matches:" <+> ppr kind_matches
                  , text "res_k:" <+> ppr res_k] )
 
-            -- need to look up the non-cusk kvs in order to get their
-            -- kinds right, in case the kinds were informed by
-            -- the getInitialKinds pass
-       ; let non_cusk_kv_names = nameSetElems non_cusk_kv_name_set
-             free_kvs          = tyCoVarsOfTypes $
-                                 map tyVarKind (all_kvs ++ all_tvs)
-             lookup nm         = case lookupVarSetByName free_kvs nm of
-                                   Just tv -> Left tv
-                                   Nothing -> Right nm
-             (non_cusk_kvs, weirds) = partitionWith lookup non_cusk_kv_names
-
-         -- See Note [Free-floating kind vars]  TODO (RAE): Write note.
-       ; weird_kvs <- if second_pass
-                      then do { checkNoErrs $
-                                mapM_ (report_floating_kv all_tvs) weirds
-                              ; return [] }
-                      else do { ks <- mapM (const newMetaKindVar) weirds
-                              ; return (zipWith new_skolem_tv weirds ks) }
-
-       ; tcExtendTyVarEnv (non_cusk_kvs ++ weird_kvs ++ scoped_tvs) $
-         thing_inside (non_cusk_kvs ++ weird_kvs ++ all_kvs) all_tvs kind res_k }
+       ; float_kvs <- deal_with_float_kvs float_kv_name_set kind_matches
+                                          scoped_tvs all_tvs
+
+       ; tcExtendTyVarEnv (float_kvs ++ scoped_tvs) $
+           -- the float_kvs are already in the all_kvs
+         thing_inside all_kvs all_tvs kind res_k }
   where
-    report_floating_kv all_tvs kv_name
+         -- See Note [Free-floating kind vars]
+    deal_with_float_kvs float_kv_name_set kind_matches scoped_tvs all_tvs
+      | isEmptyNameSet float_kv_name_set
+      = return []
+
+      | otherwise
+      = do { -- the floating kvs might just be renamed
+             -- see Note [Tiresome kind matching]
+           ; let float_kv_names = nameSetElems float_kv_name_set
+           ; float_kv_kinds <- mapM (const newMetaKindVar) float_kv_names
+           ; float_kvs <- zipWithM newSigTyVar float_kv_names float_kv_kinds
+           ; discardResult $
+             tcExtendTyVarEnv (float_kvs ++ scoped_tvs) $
+             solveEqualities $
+             forM kind_matches $ \ (hs_kind, kind) ->
+             do { tc_kind <- tcLHsKind hs_kind
+                ; unifyKind noThing tc_kind kind }
+
+           ; zonked_kvs <- mapM ((return . tcGetTyVar "tcTyClTyVars") <=< zonkTcTyVar)
+                                float_kvs
+           ; let (still_sigs, matched_up) = partition isSigTyVar zonked_kvs
+               -- the still_sigs didn't match with anything. They must be
+               -- "free-floating", as in Note [Free-floating kind vars]
+           ; checkNoErrs $ mapM_ (report_floating_kv all_tvs) still_sigs
+
+               -- the matched up kvs are proper scoped kvs.
+           ; return matched_up }
+
+    report_floating_kv all_tvs kv
       = addErr $
-        vcat [ text "Kind variable" <+> quotes (ppr kv_name) <+>
+        vcat [ text "Kind variable" <+> quotes (ppr kv) <+>
                text "is implicitly bound in datatype"
              , quotes (ppr tycon) <> comma <+>
                text "but does not appear as the kind of any"
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index 184628ab16..42f2bc9c16 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -694,19 +694,17 @@ test('T9872c',
      [''])
 test('T9872d',
      [ only_ways(['normal']),
-       expect_broken(11203),
-      # compiler_stats_num_field('bytes allocated',
-      #    [(wordsize(64), 59651432, 5),
+       compiler_stats_num_field('bytes allocated',
+          [(wordsize(64), 566134504, 5),
           # 2014-12-18    796071864   Initally created
           # 2014-12-18    739189056   Reduce type families even more eagerly
           # 2015-01-07    687562440   TrieMap leaf compression
           # 2015-03-17    726679784   tweak to solver; probably flattens more
-      #     (wordsize(32), 59651432, 5)
+           (wordsize(32), 59651432, 5)
           # some date     328810212
           # 2015-07-11    350369584
-	  # 2015-12-11    59651432    Massive improvement from TypeInType
-	  #                           but see also #11196
-      #    ]),
+	  # 2015-12-11    566134504   TypeInType; see #11196
+          ]),
       ],
      compile,
      [''])
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 0005abc87d..d0aa124b90 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -124,6 +124,6 @@ test('T10134', normal, multimod_compile, ['T10134.hs','-v0'])
 test('T10742', normal, compile, [''])
 test('T10934', normal, compile, [''])
 test('T11142', normal, compile_fail, [''])
-test('SigTvKinds', expect_broken(11203), compile, [''])
+test('SigTvKinds', normal, compile, [''])
 test('SigTvKinds2', expect_broken(11203), compile_fail, [''])
 test('T9017', normal, compile_fail, [''])