Fix tcDataKindSig

This patch fixes an outright bug in tcDataKindSig, shown up in Trac
of a data type declaration.  See Note [TyConBinders for the result kind
signature of a data type]

I also took the opportunity to elminate the DataKindCheck argument
and data type from tcDataKindSig, instead moving the check to the
call site, which is easier to understand.

7 files changed, 116 insertions, 84 deletions

diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index a9e8afd1a5..4e60b954d1 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -23,7 +23,6 @@ module TcHsType (
                 -- Type checking type and class decls
         kcLookupTcTyCon, kcTyClTyVars, tcTyClTyVars,
         tcDataKindSig,
-        DataKindCheck(..),
 
         -- Kind-checking types
         -- No kind generalisation, no checkValidType
@@ -41,7 +40,7 @@ module TcHsType (
         reportFloatingKvs,
 
         -- Sort-checking kinds
-        tcLHsKindSig,
+        tcLHsKindSig, badKindSig,
 
         -- Pattern type signatures
         tcHsPatSigType, tcPatSig, funAppCtxt
@@ -63,6 +62,7 @@ import TcSimplify ( solveEqualities )
 import TcType
 import TcHsSyn( zonkSigType )
 import Inst   ( tcInstBinders, tcInstBinder )
+import TyCoRep( TyBinder(..) )  -- Used in tcDataKindSig
 import Type
 import Kind
 import RdrName( lookupLocalRdrOcc )
@@ -90,7 +90,7 @@ import PrelNames hiding ( wildCardName )
 import qualified GHC.LanguageExtensions as LangExt
 
 import Maybes
-import Data.List ( partition, zipWith4, mapAccumR )
+import Data.List ( partition, mapAccumR )
 import Control.Monad
 
 {-
@@ -1983,59 +1983,54 @@ tcTyClTyVars tycon_name thing_inside
             tv      = binderVar binder
             new_fvs = fvs `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv)
 
-
-
 -----------------------------------
-data DataKindCheck
-    -- Plain old data type; better be lifted
-    = LiftedDataKind
-    -- Data families might have a variable return kind.
-    -- See See Note [Arity of data families] in FamInstEnv for more info.
-    | LiftedOrVarDataKind
-    -- Abstract data in hsig files can have any kind at all;
-    -- even unlifted. This is because they might not actually
-    -- be implemented with a data declaration at the end of the day.
-    | AnyDataKind
-
-tcDataKindSig :: DataKindCheck  -- ^ Do we require the result to be *?
-              -> Kind -> TcM ([TyConBinder], Kind)
+tcDataKindSig :: [TyConBinder]
+              -> Kind
+              -> TcM ([TyConBinder], Kind)
 -- GADT decls can have a (perhaps partial) kind signature
---      e.g.  data T :: * -> * -> * where ...
--- This function makes up suitable (kinded) type variables for
--- the argument kinds, and checks that the result kind is indeed * if requested.
--- (Otherwise, checks to make sure that the result kind is either * or a type variable.)
--- See Note [Arity of data families] in FamInstEnv for more info.
--- We use it also to make up argument type variables for for data instances.
+--      e.g.  data T a :: * -> * -> * where ...
+-- This function makes up suitable (kinded) TyConBinders for the
+-- argument kinds.  E.g. in this case it might return
+--   ([b::*, c::*], *)
 -- Never emits constraints.
--- Returns the new TyVars, the extracted TyBinders, and the new, reduced
--- result kind (which should always be Type or a synonym thereof)
-tcDataKindSig kind_check kind
-  = do  { case kind_check of
-            LiftedDataKind ->
-                checkTc (isLiftedTypeKind res_kind)
-                        (badKindSig True kind)
-            LiftedOrVarDataKind ->
-                checkTc (isLiftedTypeKind res_kind || isJust (tcGetCastedTyVar_maybe res_kind))
-                        (badKindSig False kind)
-            AnyDataKind -> return ()
-        ; span <- getSrcSpanM
-        ; us   <- newUniqueSupply
+-- It's a little trickier than you might think: see
+-- Note [TyConBinders for the result kind signature of a data type]
+tcDataKindSig tc_bndrs kind
+  = do  { loc     <- getSrcSpanM
+        ; uniqs   <- newUniqueSupply
         ; rdr_env <- getLocalRdrEnv
-        ; let uniqs = uniqsFromSupply us
-              occs  = [ occ | str <- allNameStrings
-                            , let occ = mkOccName tvName str
-                            , isNothing (lookupLocalRdrOcc rdr_env occ) ]
-                 -- Note [Avoid name clashes for associated data types]
-
-    -- NB: Use the tv from a binder if there is one. Otherwise,
-    -- we end up inventing a new Unique for it, and any other tv
-    -- that mentions the first ends up with the wrong kind.
-              extra_bndrs = zipWith4 mkTyBinderTyConBinder
-                              tv_bndrs (repeat span) uniqs occs
-
-        ; return (extra_bndrs, res_kind) }
+        ; let new_occs = [ occ
+                         | str <- allNameStrings
+                         , let occ = mkOccName tvName str
+                         , isNothing (lookupLocalRdrOcc rdr_env occ)
+                         -- Note [Avoid name clashes for associated data types]
+                         , not (occ `elem` lhs_occs) ]
+              new_uniqs = uniqsFromSupply uniqs
+              subst = mkEmptyTCvSubst (mkInScopeSet (mkVarSet lhs_tvs))
+        ; return (go loc new_occs new_uniqs subst [] kind) }
   where
-    (tv_bndrs, res_kind) = splitPiTys kind
+    lhs_tvs  = map binderVar tc_bndrs
+    lhs_occs = map getOccName lhs_tvs
+
+    go loc occs uniqs subst acc kind
+      = case splitPiTy_maybe kind of
+          Nothing -> (reverse acc, substTy subst kind)
+
+          Just (Anon arg, kind')
+            -> go loc occs' uniqs' subst' (tcb : acc) kind'
+            where
+              arg'   = substTy subst arg
+              tv     = mkTyVar (mkInternalName uniq occ loc) arg'
+              subst' = extendTCvInScope subst tv
+              tcb    = TvBndr tv AnonTCB
+              (uniq:uniqs') = uniqs
+              (occ:occs')   = occs
+
+          Just (Named (TvBndr tv vis), kind')
+            -> go loc occs uniqs subst' (tcb : acc) kind'
+            where
+              (subst', tv') = substTyVarBndr subst tv
+              tcb = TvBndr tv' (NamedTCB vis)
 
 badKindSig :: Bool -> Kind -> SDoc
 badKindSig check_for_type kind
@@ -2044,7 +2039,34 @@ badKindSig check_for_type kind
                text "return kind" ])
         2 (ppr kind)
 
-{-
+{- Note [TyConBinders for the result kind signature of a data type]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Given
+  data T (a::*) :: * -> forall k. k -> *
+we want to generate the extra TyConBinders for T, so we finally get
+  (a::*) (b::*) (k::*) (c::k)
+The function tcDataKindSig generates these extra TyConBinders from
+the result kind signature.
+
+We need to take care to give the TyConBinders
+  (a) OccNames that are fresh (because the TyConBinders of a TyCon
+      must have distinct OccNames
+
+  (b) Uniques that are fresh (obviously)
+
+For (a) we need to avoid clashes with the tyvars declared by
+the user before the "::"; in the above example that is 'a'.
+And also see Note [Avoid name clashes for associated data types].
+
+For (b) suppose we have
+   data T :: forall k. k -> forall k. k -> *
+where the two k's are identical even up to their uniques.  Surprisingly,
+this can happen: see Trac #14515.
+
+It's reasonably easy to solve all this; just run down the list with a
+substitution; hence the recursive 'go' function.  But it has to be
+done.
+
 Note [Avoid name clashes for associated data types]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider    class C a b where
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 89a0ec6272..77522c55ab 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -667,27 +667,27 @@ tcDataFamInstDecl mb_clsinfo
        ; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
        ; axiom_name  <- newFamInstAxiomName fam_tc_name [pats']
 
-         -- Deal with any kind signature.
-         -- See also Note [Arity of data families] in FamInstEnv
-       ; (extra_tcbs, final_res_kind) <- tcDataKindSig LiftedDataKind res_kind'
-
        ; let (eta_pats, etad_tvs) = eta_reduce pats'
              eta_tvs              = filterOut (`elem` etad_tvs) tvs'
                  -- NB: the "extra" tvs from tcDataKindSig would always be eta-reduced
 
-             full_tvs             = eta_tvs ++ etad_tvs
+             full_tcbs = mkTyConBindersPreferAnon (eta_tvs ++ etad_tvs) res_kind'
                  -- Put the eta-removed tyvars at the end
                  -- Remember, tvs' is in arbitrary order (except kind vars are
                  -- first, so there is no reason to suppose that the etad_tvs
                  -- (obtained from the pats) are at the end (Trac #11148)
 
-             extra_pats           = map (mkTyVarTy . binderVar) extra_tcbs
-             all_pats             = pats' `chkAppend` extra_pats
-             orig_res_ty          = mkTyConApp fam_tc all_pats
+         -- Deal with any kind signature.
+         -- See also Note [Arity of data families] in FamInstEnv
+       ; (extra_tcbs, final_res_kind) <- tcDataKindSig full_tcbs res_kind'
+       ; checkTc (isLiftedTypeKind final_res_kind) (badKindSig True res_kind')
+
+       ; let extra_pats  = map (mkTyVarTy . binderVar) extra_tcbs
+             all_pats    = pats' `chkAppend` extra_pats
+             orig_res_ty = mkTyConApp fam_tc all_pats
 
        ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
-           do { let ty_binders = mkTyConBindersPreferAnon full_tvs res_kind'
-                                 `chkAppend` extra_tcbs
+           do { let ty_binders = full_tcbs `chkAppend` extra_tcbs
               ; data_cons <- tcConDecls rec_rep_tc
                                         (ty_binders, orig_res_ty) cons
               ; tc_rhs <- case new_or_data of
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 00f23f930d..24faaa0bc1 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -881,10 +881,18 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
   = tcTyClTyVars tc_name $ \ binders res_kind -> do
   { traceTc "data family:" (ppr tc_name)
   ; checkFamFlag tc_name
-  ; (extra_binders, real_res_kind) <- tcDataKindSig LiftedOrVarDataKind res_kind
+
+  -- Check the kind signature, if any.
+  -- Data families might have a variable return kind.
+  -- See See Note [Arity of data families] in FamInstEnv.
+  ; (extra_binders, final_res_kind) <- tcDataKindSig binders res_kind
+  ; checkTc (isLiftedTypeKind final_res_kind
+             || isJust (tcGetCastedTyVar_maybe final_res_kind))
+            (badKindSig False res_kind)
+
   ; tc_rep_name <- newTyConRepName tc_name
   ; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
-                              real_res_kind
+                              final_res_kind
                               (resultVariableName sig)
                               (DataFamilyTyCon tc_rep_name)
                               parent NotInjective
@@ -1028,10 +1036,10 @@ tcDataDefn roles_info
                      , dd_cons = cons })
  =  do { tcg_env         <- getGblEnv
        ; let hsc_src = tcg_src tcg_env
-             check_kind = if mk_permissive_kind hsc_src cons
-                            then AnyDataKind
-                            else LiftedDataKind
-       ; (extra_bndrs, real_res_kind) <- tcDataKindSig check_kind res_kind
+       ; (extra_bndrs, final_res_kind) <- tcDataKindSig tycon_binders res_kind
+       ; unless (mk_permissive_kind hsc_src cons) $
+         checkTc (isLiftedTypeKind final_res_kind) (badKindSig True res_kind)
+
        ; let final_bndrs  = tycon_binders `chkAppend` extra_bndrs
              roles        = roles_info tc_name
 
@@ -1053,7 +1061,7 @@ tcDataDefn roles_info
              ; tc_rep_nm <- newTyConRepName tc_name
              ; return (mkAlgTyCon tc_name
                                   final_bndrs
-                                  real_res_kind
+                                  final_res_kind
                                   roles
                                   (fmap unLoc cType)
                                   stupid_theta tc_rhs
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 6eaacdfc68..3b4983477c 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -96,7 +96,6 @@ module Type (
         binderRelevantType_maybe, caseBinder,
         isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder, isInvisibleBinder,
         tyConBindersTyBinders,
-        mkTyBinderTyConBinder,
 
         -- ** Common type constructors
         funTyCon,
@@ -238,9 +237,6 @@ import Pair
 import ListSetOps
 import Digraph
 import Unique ( nonDetCmpUnique )
-import SrcLoc  ( SrcSpan )
-import OccName ( OccName )
-import Name    ( mkInternalName )
 
 import Maybes           ( orElse )
 import Data.Maybe       ( isJust, mapMaybe )
@@ -340,7 +336,8 @@ coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc t
                -- Its important to use mkAppTys, rather than (foldl AppTy),
                -- because the function part might well return a
                -- partially-applied type constructor; indeed, usually will!
-coreView (TyConApp tc [])
+
+coreView (TyConApp tc [])       -- At the Core level, Constraint = Type
   | isStarKindSynonymTyCon tc
   = Just liftedTypeKind
 
@@ -1517,15 +1514,6 @@ caseBinder :: TyBinder           -- ^ binder to scrutinize
 caseBinder (Named v) f _ = f v
 caseBinder (Anon t)  _ d = d t
 
--- | Manufacture a new 'TyConBinder' from a 'TyBinder'. Anonymous
--- 'TyBinder's are still assigned names as 'TyConBinder's, so we need
--- the extra gunk with which to construct a 'Name'. Used when producing
--- tyConTyVars from a datatype kind signature. Defined here to avoid module
--- loops.
-mkTyBinderTyConBinder :: TyBinder -> SrcSpan -> Unique -> OccName -> TyConBinder
-mkTyBinderTyConBinder (Named (TvBndr tv argf)) _ _ _ = TvBndr tv (NamedTCB argf)
-mkTyBinderTyConBinder (Anon kind) loc uniq occ
-  = TvBndr (mkTyVar (mkInternalName uniq occ loc) kind) AnonTCB
 
 {-
 %************************************************************************
diff --git a/testsuite/tests/ghci/scripts/T13407.stdout b/testsuite/tests/ghci/scripts/T13407.stdout
index 7607413d11..083f3a8b1f 100644
--- a/testsuite/tests/ghci/scripts/T13407.stdout
+++ b/testsuite/tests/ghci/scripts/T13407.stdout
@@ -1,3 +1,3 @@
 type role Foo phantom phantom
-data Foo (a :: * -> *) (c :: k)
+data Foo (a :: * -> *) (b :: k)
   	-- Defined at <interactive>:3:1
diff --git a/testsuite/tests/polykinds/T14515.hs b/testsuite/tests/polykinds/T14515.hs
new file mode 100644
index 0000000000..15bdbfe31d
--- /dev/null
+++ b/testsuite/tests/polykinds/T14515.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+
+type HRank1 ty = forall k1. k1 -> ty
+type HRank2 ty = forall k2. k2 -> ty
+
+data HREFL11 :: HRank1 (HRank1 Type) -- FAILS
+data HREFL12 :: HRank1 (HRank2 Type)
+data HREFL21 :: HRank2 (HRank1 Type)
+data HREFL22 :: HRank2 (HRank2 Type) -- FAILS
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 89ebc2ab33..ba8b256217 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -182,4 +182,5 @@ test('T14555', normal, compile_fail, [''])
 test('T14563', normal, compile_fail, [''])
 test('T14561', normal, compile_fail, [''])
 test('T14580', normal, compile_fail, [''])
+test('T14515', normal, compile, [''])