diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index b1b0c077d3e520abdf29bff3cb61f3aaf04c26aa..f7ed16c8a443efafd15b6a51c6581ac348f6bf27 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
@@ -42,7 +41,7 @@ module TcHsType (
reportFloatingKvs,
-- Sort-checking kinds
- tcLHsKindSig,
+ tcLHsKindSig, badKindSig,
-- Pattern type signatures
tcHsPatSigType, tcPatSig, funAppCtxt
@@ -64,6 +63,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 )
@@ -91,7 +91,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
{-
@@ -1955,59 +1955,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
@@ -2016,7 +2011,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 1dc2b5d9d77b4728d6dfcfcb5d13cedb26374780..99a6ff364cee40373f28f40aba011a0bc1996594 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 d9180ad25cd763f2b6f205bdff4efaa5d329b142..926190558556f7694df43acd952b736c526927fe 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -877,10 +877,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
@@ -1024,10 +1032,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
@@ -1049,7 +1057,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 5d756d3adc508aa4f9e39dd61d80255161aa1cf2..817627076a243686bfdef98c1d7491a830e1830c 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
@@ -1516,15 +1513,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 7607413d112737f67e75e2556214651313554dd9..083f3a8b1fe70a9579d6c7da89f55f1a4511cd55 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 0000000000000000000000000000000000000000..15bdbfe31d1d71e20911450167d2ee18b1fa829e
--- /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 4500f12133870f9238e215b89a5ea11fbd13f8ab..d41462ec31411e91b626b6cdeab68e1fd9be7c56 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -179,4 +179,5 @@ test('T14555', normal, compile_fail, [''])
test('T14563', normal, compile_fail, [''])
test('T14723', normal, compile, [''])
test('T14846', normal, compile_fail, [''])
+test('T14515', normal, compile, [''])