diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2020-01-23 09:40:33 +0000 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-02-01 02:28:45 -0500 |
commit | 913287a0fa5370a2488ce560f2dfba61db51055d (patch) | |
tree | 6506f059b45bd05b29b45095c3a3cbdb49f2f609 | |
parent | cd11042337a829da1dfbd19ca1a46feabdd23147 (diff) | |
download | haskell-913287a0fa5370a2488ce560f2dfba61db51055d.tar.gz |
Fix scoping of TyCon binders in TcTyClsDecls
This patch fixes #17566 by refactoring the way we decide the final
identity of the tyvars in the TyCons of a possibly-recursive nest
of type and class decls, possibly with associated types.
It's all laid out in
Note [Swizzling the tyvars before generaliseTcTyCon]
Main changes:
* We have to generalise each decl (with its associated types)
all at once: TcTyClsDecls.generaliseTyClDecl
* The main new work is done in TcTyClsDecls.swizzleTcTyConBndrs
* The mysterious TcHsSyn.zonkRecTyVarBndrs dies altogether
Other smaller things:
* A little refactoring, moving bindTyClTyVars from tcTyClDecl1
to tcDataDefn, tcSynRhs, etc. Clearer, reduces the number of
parameters
* Reduce the amount of swizzling required.
Specifically, bindExplicitTKBndrs_Q_Tv doesn't need
to clone a new Name for the TyVarTv, and not
cloning means that in the vasly common case,
swizzleTyConBndrs is a no-op
In detail:
Rename newTyVarTyVar --> cloneTyVarTyVar
Add newTyVarTyTyVar that doesn't clone
Use the non-cloning newTyVarTyVar in
bindExplicitTKBndrs_Q_Tv
Rename newFlexiKindedTyVarTyVar
--> cloneFlexiKindedTyVarTyVar
* Define new utility function and use it
HsDecls.familyDeclName ::
FamilyDecl (GhcPass p) -> IdP (GhcPass p)
Updates haddock submodule.
-rw-r--r-- | compiler/GHC/Hs/Decls.hs | 25 | ||||
-rw-r--r-- | compiler/deSugar/ExtractDocs.hs | 4 | ||||
-rw-r--r-- | compiler/typecheck/TcHsSyn.hs | 50 | ||||
-rw-r--r-- | compiler/typecheck/TcHsType.hs | 269 | ||||
-rw-r--r-- | compiler/typecheck/TcMType.hs | 50 | ||||
-rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 446 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T11203.stderr | 4 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T11821a.stderr | 4 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/Makefile | 5 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T17566.hs | 20 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/T17566a.hs | 15 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 1 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T17566b.hs | 7 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T17566b.stderr | 4 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T17566c.hs | 11 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T17566c.stderr | 6 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/all.T | 2 | ||||
m--------- | utils/haddock | 0 |
18 files changed, 625 insertions, 298 deletions
diff --git a/compiler/GHC/Hs/Decls.hs b/compiler/GHC/Hs/Decls.hs index 827f26bedc..aeec0820ed 100644 --- a/compiler/GHC/Hs/Decls.hs +++ b/compiler/GHC/Hs/Decls.hs @@ -83,7 +83,7 @@ module GHC.Hs.Decls ( RoleAnnotDecl(..), LRoleAnnotDecl, roleAnnotDeclName, -- ** Injective type families FamilyResultSig(..), LFamilyResultSig, InjectivityAnn(..), LInjectivityAnn, - resultVariableName, + resultVariableName, familyDeclLName, familyDeclName, -- * Grouping HsGroup(..), emptyRdrGroup, emptyRnGroup, appendGroups, hsGroupInstDecls, @@ -710,11 +710,14 @@ tyFamInstDeclLName (TyFamInstDecl (HsIB _ (XFamEqn nec))) tyFamInstDeclLName (TyFamInstDecl (XHsImplicitBndrs nec)) = noExtCon nec -tyClDeclLName :: TyClDecl pass -> Located (IdP pass) -tyClDeclLName (FamDecl { tcdFam = FamilyDecl { fdLName = ln } }) = ln -tyClDeclLName decl = tcdLName decl +tyClDeclLName :: TyClDecl (GhcPass p) -> Located (IdP (GhcPass p)) +tyClDeclLName (FamDecl { tcdFam = fd }) = familyDeclLName fd +tyClDeclLName (SynDecl { tcdLName = ln }) = ln +tyClDeclLName (DataDecl { tcdLName = ln }) = ln +tyClDeclLName (ClassDecl { tcdLName = ln }) = ln +tyClDeclLName (XTyClDecl nec) = noExtCon nec -tcdName :: TyClDecl pass -> IdP pass +tcdName :: TyClDecl (GhcPass p) -> IdP (GhcPass p) tcdName = unLoc . tyClDeclLName tyClDeclTyVars :: TyClDecl pass -> LHsQTyVars pass @@ -1140,6 +1143,16 @@ data FamilyInfo pass -- said "type family Foo x where .." | ClosedTypeFamily (Maybe [LTyFamInstEqn pass]) + +------------- Functions over FamilyDecls ----------- + +familyDeclLName :: FamilyDecl (GhcPass p) -> Located (IdP (GhcPass p)) +familyDeclLName (FamilyDecl { fdLName = n }) = n +familyDeclLName (XFamilyDecl nec) = noExtCon nec + +familyDeclName :: FamilyDecl (GhcPass p) -> IdP (GhcPass p) +familyDeclName = unLoc . familyDeclLName + famResultKindSignature :: FamilyResultSig (GhcPass p) -> Maybe (LHsKind (GhcPass p)) famResultKindSignature (NoSig _) = Nothing famResultKindSignature (KindSig _ ki) = Just ki @@ -1155,6 +1168,8 @@ resultVariableName :: FamilyResultSig (GhcPass a) -> Maybe (IdP (GhcPass a)) resultVariableName (TyVarSig _ sig) = Just $ hsLTyVarName sig resultVariableName _ = Nothing +------------- Pretty printing FamilyDecls ----------- + instance OutputableBndrId p => Outputable (FamilyDecl (GhcPass p)) where ppr = pprFamilyDecl TopLevel diff --git a/compiler/deSugar/ExtractDocs.hs b/compiler/deSugar/ExtractDocs.hs index 8612a05cb9..632207c41f 100644 --- a/compiler/deSugar/ExtractDocs.hs +++ b/compiler/deSugar/ExtractDocs.hs @@ -14,7 +14,6 @@ import GHC.Hs.Binds import GHC.Hs.Doc import GHC.Hs.Decls import GHC.Hs.Extension -import GHC.Hs.Pat import GHC.Hs.Types import GHC.Hs.Utils import Name @@ -117,8 +116,7 @@ user-written. This lets us relate Names (from ClsInsts) to comments (associated with InstDecls and DerivDecls). -} -getMainDeclBinder :: XRec pass Pat ~ Located (Pat pass) => - HsDecl pass -> [IdP pass] +getMainDeclBinder :: HsDecl (GhcPass p) -> [IdP (GhcPass p)] getMainDeclBinder (TyClD _ d) = [tcdName d] getMainDeclBinder (ValD _ d) = case collectHsBindBinders d of diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs index 3d060191eb..9db8880fc9 100644 --- a/compiler/typecheck/TcHsSyn.hs +++ b/compiler/typecheck/TcHsSyn.hs @@ -36,7 +36,7 @@ module TcHsSyn ( zonkTopBndrs, ZonkEnv, ZonkFlexi(..), emptyZonkEnv, mkEmptyZonkEnv, initZonkEnv, zonkTyVarBinders, zonkTyVarBindersX, zonkTyVarBinderX, - zonkTyBndrs, zonkTyBndrsX, zonkRecTyVarBndrs, + zonkTyBndrs, zonkTyBndrsX, zonkTcTypeToType, zonkTcTypeToTypeX, zonkTcTypesToTypes, zonkTcTypesToTypesX, zonkTyVarOcc, @@ -327,20 +327,14 @@ extendZonkEnv ze@(ZonkEnv { ze_tv_env = tyco_env, ze_id_env = id_env }) vars where (tycovars, ids) = partition isTyCoVar vars -extendIdZonkEnv1 :: ZonkEnv -> Var -> ZonkEnv -extendIdZonkEnv1 ze@(ZonkEnv { ze_id_env = id_env }) id +extendIdZonkEnv :: ZonkEnv -> Var -> ZonkEnv +extendIdZonkEnv ze@(ZonkEnv { ze_id_env = id_env }) id = ze { ze_id_env = extendVarEnv id_env id id } -extendTyZonkEnv1 :: ZonkEnv -> TyVar -> ZonkEnv -extendTyZonkEnv1 ze@(ZonkEnv { ze_tv_env = ty_env }) tv +extendTyZonkEnv :: ZonkEnv -> TyVar -> ZonkEnv +extendTyZonkEnv ze@(ZonkEnv { ze_tv_env = ty_env }) tv = ze { ze_tv_env = extendVarEnv ty_env tv tv } -extendTyZonkEnvN :: ZonkEnv -> [(Name,TyVar)] -> ZonkEnv -extendTyZonkEnvN ze@(ZonkEnv { ze_tv_env = ty_env }) pairs - = ze { ze_tv_env = foldl add ty_env pairs } - where - add env (name, tv) = extendVarEnv_Directly env (getUnique name) tv - setZonkType :: ZonkEnv -> ZonkFlexi -> ZonkEnv setZonkType ze flexi = ze { ze_flexi = flexi } @@ -429,7 +423,7 @@ zonkEvVarOcc env v zonkCoreBndrX :: ZonkEnv -> Var -> TcM (ZonkEnv, Var) zonkCoreBndrX env v | isId v = do { v' <- zonkIdBndr env v - ; return (extendIdZonkEnv1 env v', v') } + ; return (extendIdZonkEnv env v', v') } | otherwise = zonkTyBndrX env v zonkCoreBndrsX :: ZonkEnv -> [Var] -> TcM (ZonkEnv, [Var]) @@ -444,12 +438,16 @@ zonkTyBndrsX = mapAccumLM zonkTyBndrX zonkTyBndrX :: ZonkEnv -> TcTyVar -> TcM (ZonkEnv, TyVar) -- This guarantees to return a TyVar (not a TcTyVar) -- then we add it to the envt, so all occurrences are replaced +-- +-- It does not clone: the new TyVar has the sane Name +-- as the old one. This important when zonking the +-- TyVarBndrs of a TyCon, whose Names may scope. zonkTyBndrX env tv = ASSERT2( isImmutableTyVar tv, ppr tv <+> dcolon <+> ppr (tyVarKind tv) ) do { ki <- zonkTcTypeToTypeX env (tyVarKind tv) -- Internal names tidy up better, for iface files. ; let tv' = mkTyVar (tyVarName tv) ki - ; return (extendTyZonkEnv1 env tv', tv') } + ; return (extendTyZonkEnv env tv', tv') } zonkTyVarBinders :: [VarBndr TcTyVar vis] -> TcM (ZonkEnv, [VarBndr TyVar vis]) @@ -466,22 +464,6 @@ zonkTyVarBinderX env (Bndr tv vis) = do { (env', tv') <- zonkTyBndrX env tv ; return (env', Bndr tv' vis) } -zonkRecTyVarBndrs :: [Name] -> [TcTyVar] -> TcM (ZonkEnv, [TyVar]) --- This rather specialised function is used in exactly one place. --- See Note [Tricky scoping in generaliseTcTyCon] in TcTyClsDecls. -zonkRecTyVarBndrs names tc_tvs - = initZonkEnv $ \ ze -> - fixM $ \ ~(_, rec_new_tvs) -> - do { let ze' = extendTyZonkEnvN ze $ - zipWithLazy (\ tc_tv new_tv -> (getName tc_tv, new_tv)) - tc_tvs rec_new_tvs - ; new_tvs <- zipWithM (zonk_one ze') names tc_tvs - ; return (ze', new_tvs) } - where - zonk_one ze name tc_tv - = do { ki <- zonkTcTypeToTypeX ze (tyVarKind tc_tv) - ; return (mkTyVar name ki) } - zonkTopExpr :: HsExpr GhcTcId -> TcM (HsExpr GhcTc) zonkTopExpr e = initZonkEnv $ \ ze -> zonkExpr ze e @@ -1357,7 +1339,7 @@ zonk_pat env (WildPat ty) zonk_pat env (VarPat x (L l v)) = do { v' <- zonkIdBndr env v - ; return (extendIdZonkEnv1 env v', VarPat x (L l v')) } + ; return (extendIdZonkEnv env v', VarPat x (L l v')) } zonk_pat env (LazyPat x pat) = do { (env', pat') <- zonkPat env pat @@ -1369,7 +1351,7 @@ zonk_pat env (BangPat x pat) zonk_pat env (AsPat x (L loc v) pat) = do { v' <- zonkIdBndr env v - ; (env', pat') <- zonkPat (extendIdZonkEnv1 env v') pat + ; (env', pat') <- zonkPat (extendIdZonkEnv env v') pat ; return (env', AsPat x (L loc v') pat') } zonk_pat env (ViewPat ty expr pat) @@ -1459,7 +1441,7 @@ zonk_pat env (NPlusKPat ty (L loc n) (L l lit1) lit2 e1 e2) ; lit1' <- zonkOverLit env2 lit1 ; lit2' <- zonkOverLit env2 lit2 ; ty' <- zonkTcTypeToTypeX env2 ty - ; return (extendIdZonkEnv1 env2 n', + ; return (extendIdZonkEnv env2 n', NPlusKPat ty' (L loc n') (L l lit1') lit2' e1' e2') } zonk_pat env (CoPat x co_fn pat ty) @@ -1607,7 +1589,7 @@ zonkCoreExpr env (Case scrut b ty alts) = do scrut' <- zonkCoreExpr env scrut ty' <- zonkTcTypeToTypeX env ty b' <- zonkIdBndr env b - let env1 = extendIdZonkEnv1 env b' + let env1 = extendIdZonkEnv env b' alts' <- mapM (zonkCoreAlt env1) alts return $ Case scrut' b' ty' alts' @@ -1621,7 +1603,7 @@ zonkCoreBind :: ZonkEnv -> CoreBind -> TcM (ZonkEnv, CoreBind) zonkCoreBind env (NonRec v e) = do v' <- zonkIdBndr env v e' <- zonkCoreExpr env e - let env1 = extendIdZonkEnv1 env v' + let env1 = extendIdZonkEnv env v' return (env1, NonRec v' e') zonkCoreBind env (Rec pairs) = do (env1, pairs') <- fixM go diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 32fbae7a14..5726fc019d 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -2009,11 +2009,10 @@ kcInferDeclHeader name flav -- -- mkAnonTyConBinder: see Note [No polymorphic recursion] - all_tv_prs = (kv_ns `zip` scoped_kvs) ++ - (hsLTyVarNames hs_tvs `zip` tc_tvs) - -- NB: bindIplicitTKBndrs_Q_Tv makes /freshly-named/ unification - -- variables, hence the need to zip here. Ditto bindExplicit.. - -- See TcMType Note [Unification variables need fresh Names] + all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs) + -- NB: bindExplicitTKBndrs_Q_Tv does not clone; + -- ditto Implicit + -- See Note [Non-cloning for tyvar binders] tycon = mkTcTyCon name tc_binders res_kind all_tv_prs False -- not yet generalised @@ -2039,98 +2038,102 @@ kcCheckDeclHeader_sig -> LHsQTyVars GhcRn -- ^ Binders in the header -> TcM ContextKind -- ^ The result kind. AnyKind == no result signature -> TcM TcTyCon -- ^ A suitably-kinded TcTyCon -kcCheckDeclHeader_sig kisig name flav ktvs kc_res_ki = - addTyConFlavCtxt name flav $ - pushTcLevelM_ $ - solveEqualities $ -- #16687 - bind_implicit (hsq_ext ktvs) $ \implicit_tcv_prs -> do - - -- Step 1: zip user-written binders with quantifiers from the kind signature. - -- For example: - -- - -- type F :: forall k -> k -> forall j. j -> Type - -- data F i a b = ... - -- - -- Results in the following 'zipped_binders': - -- - -- TyBinder LHsTyVarBndr - -- --------------------------------------- - -- ZippedBinder forall k -> i - -- ZippedBinder k -> a - -- ZippedBinder forall j. - -- ZippedBinder j -> b - -- - let (zipped_binders, excess_bndrs, kisig') = zipBinders kisig (hsq_explicit ktvs) - - -- Report binders that don't have a corresponding quantifier. - -- For example: - -- - -- type T :: Type -> Type - -- data T b1 b2 b3 = ... - -- - -- Here, b1 is zipped with Type->, while b2 and b3 are excess binders. - -- - unless (null excess_bndrs) $ failWithTc (tooManyBindersErr kisig' excess_bndrs) - - -- Convert each ZippedBinder to TyConBinder for tyConBinders - -- and to [(Name, TcTyVar)] for tcTyConScopedTyVars - (vis_tcbs, concat -> explicit_tv_prs) <- mapAndUnzipM zipped_to_tcb zipped_binders - - tcExtendNameTyVarEnv explicit_tv_prs $ do - - -- Check that inline kind annotations on binders are valid. - -- For example: - -- - -- type T :: Maybe k -> Type - -- data T (a :: Maybe j) = ... - -- - -- Here we unify Maybe k ~ Maybe j - mapM_ check_zipped_binder zipped_binders - - -- Kind-check the result kind annotation, if present: - -- - -- data T a b :: res_ki where - -- ^^^^^^^^^ - -- We do it here because at this point the environment has been - -- extended with both 'implicit_tcv_prs' and 'explicit_tv_prs'. - m_res_ki <- kc_res_ki >>= \ctx_k -> - case ctx_k of - AnyKind -> return Nothing - _ -> Just <$> newExpectedKind ctx_k - - -- Step 2: split off invisible binders. - -- For example: - -- - -- type F :: forall k1 k2. (k1, k2) -> Type - -- type family F - -- - -- Does 'forall k1 k2' become a part of 'tyConBinders' or 'tyConResKind'? - -- See Note [Arity inference in kcCheckDeclHeader_sig] - let (invis_binders, r_ki) = split_invis kisig' m_res_ki - - -- Convert each invisible TyCoBinder to TyConBinder for tyConBinders. - invis_tcbs <- mapM invis_to_tcb invis_binders - - -- Check that the inline result kind annotation is valid. - -- For example: - -- - -- type T :: Type -> Maybe k - -- type family T a :: Maybe j where - -- - -- Here we unify Maybe k ~ Maybe j - whenIsJust m_res_ki $ \res_ki -> - discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig] - unifyKind Nothing r_ki res_ki +kcCheckDeclHeader_sig kisig name flav + (HsQTvs { hsq_ext = implicit_nms + , hsq_explicit = explicit_nms }) kc_res_ki + = addTyConFlavCtxt name flav $ + do { -- Step 1: zip user-written binders with quantifiers from the kind signature. + -- For example: + -- + -- type F :: forall k -> k -> forall j. j -> Type + -- data F i a b = ... + -- + -- Results in the following 'zipped_binders': + -- + -- TyBinder LHsTyVarBndr + -- --------------------------------------- + -- ZippedBinder forall k -> i + -- ZippedBinder k -> a + -- ZippedBinder forall j. + -- ZippedBinder j -> b + -- + let (zipped_binders, excess_bndrs, kisig') = zipBinders kisig explicit_nms + + -- Report binders that don't have a corresponding quantifier. + -- For example: + -- + -- type T :: Type -> Type + -- data T b1 b2 b3 = ... + -- + -- Here, b1 is zipped with Type->, while b2 and b3 are excess binders. + -- + ; unless (null excess_bndrs) $ failWithTc (tooManyBindersErr kisig' excess_bndrs) + + -- Convert each ZippedBinder to TyConBinder for tyConBinders + -- and to [(Name, TcTyVar)] for tcTyConScopedTyVars + ; (vis_tcbs, concat -> explicit_tv_prs) <- mapAndUnzipM zipped_to_tcb zipped_binders + + ; (implicit_tvs, (invis_binders, r_ki)) + <- pushTcLevelM_ $ + solveEqualities $ -- #16687 + bindImplicitTKBndrs_Tv implicit_nms $ + tcExtendNameTyVarEnv explicit_tv_prs $ + do { -- Check that inline kind annotations on binders are valid. + -- For example: + -- + -- type T :: Maybe k -> Type + -- data T (a :: Maybe j) = ... + -- + -- Here we unify Maybe k ~ Maybe j + mapM_ check_zipped_binder zipped_binders + + -- Kind-check the result kind annotation, if present: + -- + -- data T a b :: res_ki where + -- ^^^^^^^^^ + -- We do it here because at this point the environment has been + -- extended with both 'implicit_tcv_prs' and 'explicit_tv_prs'. + ; ctx_k <- kc_res_ki + ; m_res_ki <- case ctx_k of + AnyKind -> return Nothing + _ -> Just <$> newExpectedKind ctx_k + + -- Step 2: split off invisible binders. + -- For example: + -- + -- type F :: forall k1 k2. (k1, k2) -> Type + -- type family F + -- + -- Does 'forall k1 k2' become a part of 'tyConBinders' or 'tyConResKind'? + -- See Note [Arity inference in kcCheckDeclHeader_sig] + ; let (invis_binders, r_ki) = split_invis kisig' m_res_ki + + -- Check that the inline result kind annotation is valid. + -- For example: + -- + -- type T :: Type -> Maybe k + -- type family T a :: Maybe j where + -- + -- Here we unify Maybe k ~ Maybe j + ; whenIsJust m_res_ki $ \res_ki -> + discardResult $ -- See Note [discardResult in kcCheckDeclHeader_sig] + unifyKind Nothing r_ki res_ki + + ; return (invis_binders, r_ki) } -- Zonk the implicitly quantified variables. - implicit_tv_prs <- mapSndM zonkTcTyVarToTyVar implicit_tcv_prs + ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs + + -- Convert each invisible TyCoBinder to TyConBinder for tyConBinders. + ; invis_tcbs <- mapM invis_to_tcb invis_binders -- Build the final, generalized TcTyCon - let tcbs = vis_tcbs ++ invis_tcbs - all_tv_prs = implicit_tv_prs ++ explicit_tv_prs - tc = mkTcTyCon name tcbs r_ki all_tv_prs True flav + ; let tcbs = vis_tcbs ++ invis_tcbs + implicit_tv_prs = implicit_nms `zip` implicit_tvs + all_tv_prs = implicit_tv_prs ++ explicit_tv_prs + tc = mkTcTyCon name tcbs r_ki all_tv_prs True flav - traceTc "kcCheckDeclHeader_sig done:" $ vcat + ; traceTc "kcCheckDeclHeader_sig done:" $ vcat [ text "tyConName = " <+> ppr (tyConName tc) , text "kisig =" <+> debugPprType kisig , text "tyConKind =" <+> debugPprType (tyConKind tc) @@ -2138,7 +2141,7 @@ kcCheckDeclHeader_sig kisig name flav ktvs kc_res_ki = , text "tcTyConScopedTyVars" <+> ppr (tcTyConScopedTyVars tc) , text "tyConResKind" <+> debugPprType (tyConResKind tc) ] - return tc + ; return tc } where -- Consider this declaration: -- @@ -2208,14 +2211,6 @@ kcCheckDeclHeader_sig kisig name flav ktvs kc_res_ki = MASSERT(null stv) return tcb - -- similar to: bindImplicitTKBndrs_Tv - bind_implicit :: [Name] -> ([(Name,TcTyVar)] -> TcM a) -> TcM a - bind_implicit tv_names thing_inside = - do { let new_tv name = do { tcv <- newFlexiKindedTyVarTyVar name - ; return (name, tcv) } - ; tcvs <- mapM new_tv tv_names - ; tcExtendNameTyVarEnv tcvs (thing_inside tcvs) } - -- Check that the inline kind annotation on a binder is valid -- by unifying it with the kind of the quantifier. check_zipped_binder :: ZippedBinder -> TcM () @@ -2245,6 +2240,8 @@ kcCheckDeclHeader_sig kisig name flav ktvs kc_res_ki = n_inst = n_sig_invis_bndrs - n_res_invis_bndrs in splitPiTysInvisibleN n_inst sig_ki +kcCheckDeclHeader_sig _ _ _ (XLHsQTyVars nec) _ = noExtCon nec + -- A quantifier from a kind signature zipped with a user-written binder for it. data ZippedBinder = ZippedBinder TyBinder (Maybe (LHsTyVarBndr GhcRn)) @@ -2578,6 +2575,56 @@ expectedKindInCtxt _ = OpenKind * * ********************************************************************* -} +{- Note [Non-cloning for tyvar binders] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +bindExplictTKBndrs_Q_Skol, bindExplictTKBndrs_Skol, do not clone; +and nor do the Implicit versions. There is no need. + +bindExplictTKBndrs_Q_Tv does not clone; and similarly Implicit. +We take advantage of this in kcInferDeclHeader: + all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs) +If we cloned, we'd need to take a bit more care here; not hard. + +The main payoff is that avoidng gratuitious cloning means that we can +almost always take the fast path in swizzleTcTyConBndrs. "Almost +always" means not the case of mutual recursion with polymorphic kinds. + + +Note [Cloning for tyvar binders] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +bindExplicitTKBndrs_Tv does cloning, making up a Name with a fresh Unique, +unlike bindExplicitTKBndrs_Q_Tv. (Nor do the Skol variants clone.) +And similarly for bindImplicit... + +This for a narrow and tricky reason which, alas, I couldn't find a +simpler way round. #16221 is the poster child: + + data SameKind :: k -> k -> * + data T a = forall k2 (b :: k2). MkT (SameKind a b) !Int + +When kind-checking T, we give (a :: kappa1). Then: + +- In kcConDecl we make a TyVarTv unification variable kappa2 for k2 + (as described in Note [Kind-checking for GADTs], even though this + example is an existential) +- So we get (b :: kappa2) via bindExplicitTKBndrs_Tv +- We end up unifying kappa1 := kappa2, because of the (SameKind a b) + +Now we generalise over kappa2. But if kappa2's Name is precisely k2 +(i.e. we did not clone) we'll end up giving T the utterlly final kind + T :: forall k2. k2 -> * +Nothing directly wrong with that but when we typecheck the data constructor +we have k2 in scope; but then it's brought into scope /again/ when we find +the forall k2. This is chaotic, and we end up giving it the type + MkT :: forall k2 (a :: k2) k2 (b :: k2). + SameKind @k2 a b -> Int -> T @{k2} a +which is bogus -- because of the shadowing of k2, we can't +apply T to the kind or a! + +And there no reason /not/ to clone the Name when making a unification +variable. So that's what we do. +-} + -------------------------------------- -- Implicit binders -------------------------------------- @@ -2585,10 +2632,12 @@ expectedKindInCtxt _ = OpenKind bindImplicitTKBndrs_Skol, bindImplicitTKBndrs_Tv, bindImplicitTKBndrs_Q_Skol, bindImplicitTKBndrs_Q_Tv :: [Name] -> TcM a -> TcM ([TcTyVar], a) -bindImplicitTKBndrs_Skol = bindImplicitTKBndrsX newFlexiKindedSkolemTyVar -bindImplicitTKBndrs_Tv = bindImplicitTKBndrsX newFlexiKindedTyVarTyVar bindImplicitTKBndrs_Q_Skol = bindImplicitTKBndrsX (newImplicitTyVarQ newFlexiKindedSkolemTyVar) bindImplicitTKBndrs_Q_Tv = bindImplicitTKBndrsX (newImplicitTyVarQ newFlexiKindedTyVarTyVar) +bindImplicitTKBndrs_Skol = bindImplicitTKBndrsX newFlexiKindedSkolemTyVar +bindImplicitTKBndrs_Tv = bindImplicitTKBndrsX cloneFlexiKindedTyVarTyVar + -- newFlexiKinded... see Note [Non-cloning for tyvar binders] + -- cloneFlexiKindedTyVarTyVar: see Note [Cloning for tyvar binders] bindImplicitTKBndrsX :: (Name -> TcM TcTyVar) -- new_tv function @@ -2621,7 +2670,10 @@ newFlexiKindedSkolemTyVar = newFlexiKindedTyVar newSkolemTyVar newFlexiKindedTyVarTyVar :: Name -> TcM TyVar newFlexiKindedTyVarTyVar = newFlexiKindedTyVar newTyVarTyVar - -- See Note [Unification variables need fresh Names] in TcMType + +cloneFlexiKindedTyVarTyVar :: Name -> TcM TyVar +cloneFlexiKindedTyVarTyVar = newFlexiKindedTyVar cloneTyVarTyVar + -- See Note [Cloning for tyvar binders] -------------------------------------- -- Explicit binders @@ -2633,7 +2685,9 @@ bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv -> TcM ([TcTyVar], a) bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (tcHsTyVarBndr newSkolemTyVar) -bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr newTyVarTyVar) +bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr cloneTyVarTyVar) + -- newSkolemTyVar: see Note [Non-cloning for tyvar binders] + -- cloneTyVarTyVar: see Note [Cloning for tyvar binders] bindExplicitTKBndrs_Q_Skol, bindExplicitTKBndrs_Q_Tv :: ContextKind @@ -2643,6 +2697,8 @@ bindExplicitTKBndrs_Q_Skol, bindExplicitTKBndrs_Q_Tv bindExplicitTKBndrs_Q_Skol ctxt_kind = bindExplicitTKBndrsX (tcHsQTyVarBndr ctxt_kind newSkolemTyVar) bindExplicitTKBndrs_Q_Tv ctxt_kind = bindExplicitTKBndrsX (tcHsQTyVarBndr ctxt_kind newTyVarTyVar) + -- See Note [Non-cloning for tyvar binders] + bindExplicitTKBndrsX :: (HsTyVarBndr GhcRn -> TcM TcTyVar) @@ -2662,7 +2718,7 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside -- is mentioned in the kind of a later binder -- e.g. forall k (a::k). blah -- NB: tv's Name may differ from hs_tv's - -- See TcMType Note [Unification variables need fresh Names] + -- See TcMType Note [Cloning for tyvar binders] ; (tvs,res) <- tcExtendNameTyVarEnv [(hsTyVarName hs_tv, tv)] $ go hs_tvs ; return (tv:tvs, res) } @@ -2670,7 +2726,6 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside ----------------- tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar) -> HsTyVarBndr GhcRn -> TcM TcTyVar --- Returned TcTyVar has the same name; no cloning tcHsTyVarBndr new_tv (UserTyVar _ (L _ tv_nm)) = do { kind <- newMetaKindVar ; new_tv tv_nm kind } diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index 8a50e6690d..52599c925c 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -57,7 +57,8 @@ module TcMType ( -- Instantiation newMetaTyVars, newMetaTyVarX, newMetaTyVarsX, newMetaTyVarTyVars, newMetaTyVarTyVarX, - newTyVarTyVar, newPatSigTyVar, newSkolemTyVar, newWildCardX, + newTyVarTyVar, cloneTyVarTyVar, + newPatSigTyVar, newSkolemTyVar, newWildCardX, tcInstType, tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt, tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX, @@ -707,30 +708,6 @@ cloneMetaTyVarName name ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ At the moment we give a unification variable a System Name, which influences the way it is tidied; see TypeRep.tidyTyVarBndr. - -Note [Unification variables need fresh Names] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Whenever we allocate a unification variable (MetaTyVar) we give -it a fresh name. #16221 is a very tricky case that illustrates -why this is important: - - data SameKind :: k -> k -> * - data T0 a = forall k2 (b :: k2). MkT0 (SameKind a b) !Int - -When kind-checking T0, we give (a :: kappa1). Then, in kcConDecl -we allocate a unification variable kappa2 for k2, and then we -end up unifying kappa1 := kappa2 (because of the (SameKind a b). - -Now we generalise over kappa2; but if kappa2's Name is k2, -we'll end up giving T0 the kind forall k2. k2 -> *. Nothing -directly wrong with that but when we typecheck the data constrautor -we end up giving it the type - MkT0 :: forall k1 (a :: k1) k2 (b :: k2). - SameKind @k2 a b -> Int -> T0 @{k2} a -which is bogus. The result type should be T0 @{k1} a. - -And there no reason /not/ to clone the Name when making a -unification variable. So that's what we do. -} metaInfoToTyVarName :: MetaInfo -> FastString @@ -762,9 +739,18 @@ newSkolemTyVar name kind newTyVarTyVar :: Name -> Kind -> TcM TcTyVar -- See Note [TyVarTv] --- See Note [Unification variables need fresh Names] +-- Does not clone a fresh unique newTyVarTyVar name kind = do { details <- newMetaDetails TyVarTv + ; let tyvar = mkTcTyVar name kind details + ; traceTc "newTyVarTyVar" (ppr tyvar) + ; return tyvar } + +cloneTyVarTyVar :: Name -> Kind -> TcM TcTyVar +-- See Note [TyVarTv] +-- Clones a fresh unique +cloneTyVarTyVar name kind + = do { details <- newMetaDetails TyVarTv ; uniq <- newUnique ; let name' = name `setNameUnique` uniq tyvar = mkTcTyVar name' kind details @@ -772,7 +758,7 @@ newTyVarTyVar name kind -- We want to keep the original more user-friendly Name -- In practical terms that means that in error messages, -- when the Name is tidied we get 'a' rather than 'a0' - ; traceTc "newTyVarTyVar" (ppr tyvar) + ; traceTc "cloneTyVarTyVar" (ppr tyvar) ; return tyvar } newPatSigTyVar :: Name -> Kind -> TcM TcTyVar @@ -1315,11 +1301,11 @@ collect_cand_qtvs orig_ty is_dep bound dvs ty go dv (CoercionTy co) = collect_cand_qtvs_co orig_ty bound dv co go dv (TyVarTy tv) - | is_bound tv = return dv - | otherwise = do { m_contents <- isFilledMetaTyVar_maybe tv - ; case m_contents of - Just ind_ty -> go dv ind_ty - Nothing -> go_tv dv tv } + | is_bound tv = return dv + | otherwise = do { m_contents <- isFilledMetaTyVar_maybe tv + ; case m_contents of + Just ind_ty -> go dv ind_ty + Nothing -> go_tv dv tv } go dv (ForAllTy (Bndr tv _) ty) = do { dv1 <- collect_cand_qtvs orig_ty True bound dv (tyVarKind tv) diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index bceb901c8a..3048d6178d 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -6,7 +6,7 @@ TcTyClsDecls: Typecheck type and class declarations -} -{-# LANGUAGE CPP, TupleSections, MultiWayIf #-} +{-# LANGUAGE CPP, TupleSections, ScopedTypeVariables, MultiWayIf #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE ViewPatterns #-} @@ -80,11 +80,12 @@ import qualified GHC.LanguageExtensions as LangExt import Control.Monad import Data.Foldable import Data.Function ( on ) +import Data.Functor.Identity import Data.List import qualified Data.List.NonEmpty as NE import Data.List.NonEmpty ( NonEmpty(..) ) import qualified Data.Set as Set - +import Data.Tuple( swap ) {- ************************************************************************ @@ -433,6 +434,108 @@ TcTyCons are used for two distinct purposes See also Note [Type checking recursive type and class declarations]. +Note [Swizzling the tyvars before generaliseTcTyCon] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +This Note only applies when /inferring/ the kind of a TyCon. +If there is a separate kind signature, or a CUSK, we take an entirely +different code path. + +For inference, consider + class C (f :: k) x where + type T f + op :: D f => blah + class D (g :: j) y where + op :: C g => y -> blah + +Here C and D are considered mutually recursive. Neither has a CUSK. +Just before generalisation we have the (un-quantified) kinds + C :: k1 -> k2 -> Constraint + T :: k1 -> Type + D :: k1 -> Type -> Constraint +Notice that f's kind and g's kind have been unified to 'k1'. We say +that k1 is the "representative" of k in C's decl, and of j in D's decl. + +Now when quantifying, we'd like to end up with + C :: forall {k2}. forall k. k -> k2 -> Constraint + T :: forall k. k -> Type + D :: forall j. j -> Type -> Constraint + +That is, we want to swizzle the representative to have the Name given +by the user. Partly this is to improve error messages and the output of +:info in GHCi. But it is /also/ important because the code for a +default method may mention the class variable(s), but at that point +(tcClassDecl2), we only have the final class tyvars available. +(Alternatively, we could record the scoped type variables in the +TyCon, but it's a nuisance to do so.) + +Notes: + +* On the input to generaliseTyClDecl, the mapping between the + user-specified Name and the representative TyVar is recorded in the + tyConScopedTyVars of the TcTyCon. NB: you first need to zonk to see + this representative TyVar. + +* The swizzling is actually performed by swizzleTcTyConBndrs + +* We must do the swizzling across the whole class decl. Consider + class C f where + type S (f :: k) + type T f + Here f's kind k is a parameter of C, and its identity is shared + with S and T. So if we swizzle the representative k at all, we + must do so consistently for the entire declaration. + + Hence the call to check_duplicate_tc_binders is in generaliseTyClDecl, + rather than in generaliseTcTyCon. + +There are errors to catch here. Suppose we had + class E (f :: j) (g :: k) where + op :: SameKind f g -> blah + +Then, just before generalisation we will have the (unquantified) + E :: k1 -> k1 -> Constraint + +That's bad! Two distinctly-named tyvars (j and k) have ended up with +the same representative k1. So when swizzling, we check (in +check_duplicate_tc_binders) that two distinct source names map +to the same representative. + +Here's an interesting case: + class C1 f where + type S (f :: k1) + type T (f :: k2) +Here k1 and k2 are different Names, but they end up mapped to the +same representative TyVar. To make the swizzling consistent (remember +we must have a single k across C1, S and T) we reject the program. + +Another interesting case + class C2 f where + type S (f :: k) (p::Type) + type T (f :: k) (p::Type->Type) + +Here the two k's (and the two p's) get distinct Uniques, because they +are seen by the renamer as locally bound in S and T resp. But again +the two (distinct) k's end up bound to the same representative TyVar. +You might argue that this should be accepted, but it's definitely +rejected (via an entirely different code path) if you add a kind sig: + type C2' :: j -> Constraint + class C2' f where + type S (f :: k) (p::Type) +We get + • Expected kind ‘j’, but ‘f’ has kind ‘k’ + • In the associated type family declaration for ‘S’ + +So we reject C2 too, even without the kind signature. We have +to do a bit of work to get a good error message, since both k's +look the same to the user. + +Another case + class C3 (f :: k1) where + type S (f :: k2) + +This will be rejected too. + + Note [Type environment evolution] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ As we typecheck a group of declarations the type environment evolves. @@ -571,107 +674,227 @@ kcTyClGroup kisig_env decls -- Finally, go through each tycon and give it its final kind, -- with all the required, specified, and inferred variables -- in order. - ; generalized_tcs <- mapAndReportM generaliseTcTyCon inferred_tcs + ; let inferred_tc_env = mkNameEnv $ + map (\tc -> (tyConName tc, tc)) inferred_tcs + ; generalized_tcs <- concatMapM (generaliseTyClDecl inferred_tc_env) + kindless_decls ; let poly_tcs = checked_tcs ++ generalized_tcs ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs) ; return poly_tcs } - where ppr_tc_kinds tcs = vcat (map pp_tc tcs) pp_tc tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc) -generaliseTcTyCon :: TcTyCon -> TcM TcTyCon -generaliseTcTyCon tc +type ScopedPairs = [(Name, TcTyVar)] + -- The ScopedPairs for a TcTyCon are precisely + -- specified-tvs ++ required-tvs + -- You can distinguish them because there are tyConArity required-tvs + +generaliseTyClDecl :: NameEnv TcTyCon -> LTyClDecl GhcRn -> TcM [TcTyCon] +-- See Note [Swizzling the tyvars before generaliseTcTyCon] +generaliseTyClDecl inferred_tc_env (L _ decl) + = do { let names_in_this_decl :: [Name] + names_in_this_decl = tycld_names decl + + -- Extract the specified/required binders and skolemise them + ; tc_with_tvs <- mapM skolemise_tc_tycon names_in_this_decl + + -- Zonk, to manifest the side-effects of skolemisation to the swizzler + -- NB: it's important to skolemise them all before this step. E.g. + -- class C f where { type T (f :: k) } + -- We only skolemise k when looking at T's binders, + -- but k appears in f's kind in C's binders. + ; tc_infos <- mapM zonk_tc_tycon tc_with_tvs + + -- Swizzle + ; swizzled_infos <- tcAddDeclCtxt decl (swizzleTcTyConBndrs tc_infos) + + -- And finally generalise + ; mapAndReportM generaliseTcTyCon swizzled_infos } + where + tycld_names :: TyClDecl GhcRn -> [Name] + tycld_names decl = tcdName decl : at_names decl + + at_names :: TyClDecl GhcRn -> [Name] + at_names (ClassDecl { tcdATs = ats }) = map (familyDeclName . unLoc) ats + at_names _ = [] -- Only class decls have associated types + + skolemise_tc_tycon :: Name -> TcM (TcTyCon, ScopedPairs) + -- Zonk and skolemise the Specified and Required binders + skolemise_tc_tycon tc_name + = do { let tc = lookupNameEnv_NF inferred_tc_env tc_name + -- This lookup should not fail + ; scoped_prs <- mapSndM zonkAndSkolemise (tcTyConScopedTyVars tc) + ; return (tc, scoped_prs) } + + zonk_tc_tycon :: (TcTyCon, ScopedPairs) -> TcM (TcTyCon, ScopedPairs, TcKind) + zonk_tc_tycon (tc, scoped_prs) + = do { scoped_prs <- mapSndM zonkTcTyVarToTyVar scoped_prs + -- We really have to do this again, even though + -- we have just done zonkAndSkolemise + ; res_kind <- zonkTcType (tyConResKind tc) + ; return (tc, scoped_prs, res_kind) } + +swizzleTcTyConBndrs :: [(TcTyCon, ScopedPairs, TcKind)] + -> TcM [(TcTyCon, ScopedPairs, TcKind)] +swizzleTcTyConBndrs tc_infos + | all no_swizzle swizzle_prs + -- This fast path happens almost all the time + -- See Note [Non-cloning for tyvar binders] in TcHsType + = do { traceTc "Skipping swizzleTcTyConBndrs for" (ppr (map fstOf3 tc_infos)) + ; return tc_infos } + + | otherwise + = do { check_duplicate_tc_binders + + ; traceTc "swizzleTcTyConBndrs" $ + vcat [ text "before" <+> ppr_infos tc_infos + , text "swizzle_prs" <+> ppr swizzle_prs + , text "after" <+> ppr_infos swizzled_infos ] + + ; return swizzled_infos } + + where + swizzled_infos = [ (tc, mapSnd swizzle_var scoped_prs, swizzle_ty kind) + | (tc, scoped_prs, kind) <- tc_infos ] + + swizzle_prs :: [(Name,TyVar)] + -- Pairs the user-specifed Name with its representative TyVar + -- See Note [Swizzling the tyvars before generaliseTcTyCon] + swizzle_prs = [ pr | (_, prs, _) <- tc_infos, pr <- prs ] + + no_swizzle :: (Name,TyVar) -> Bool + no_swizzle (nm, tv) = nm == tyVarName tv + + ppr_infos infos = vcat [ ppr tc <+> pprTyVars (map snd prs) + | (tc, prs, _) <- infos ] + + -- Check for duplicates + -- E.g. data SameKind (a::k) (b::k) + -- data T (a::k1) (b::k2) = MkT (SameKind a b) + -- Here k1 and k2 start as TyVarTvs, and get unified with each other + -- If this happens, things get very confused later, so fail fast + check_duplicate_tc_binders :: TcM () + check_duplicate_tc_binders = unless (null err_prs) $ + do { mapM_ report_dup err_prs; failM } + + -------------- Error reporting ------------ + err_prs :: [(Name,Name)] + err_prs = [ (n1,n2) + | pr :| prs <- findDupsEq ((==) `on` snd) swizzle_prs + , (n1,_):(n2,_):_ <- [nubBy ((==) `on` fst) (pr:prs)] ] + -- This nubBy avoids bogus error reports when we have + -- [("f", f), ..., ("f",f)....] in swizzle_prs + -- which happens with class C f where { type T f } + + report_dup :: (Name,Name) -> TcM () + report_dup (n1,n2) + = setSrcSpan (getSrcSpan n2) $ addErrTc $ + hang (text "Different names for the same type variable:") 2 info + where + info | nameOccName n1 /= nameOccName n2 + = quotes (ppr n1) <+> text "and" <+> quotes (ppr n2) + | otherwise -- Same OccNames! See C2 in + -- Note [Swizzling the tyvars before generaliseTcTyCon] + = vcat [ quotes (ppr n1) <+> text "bound at" <+> ppr (getSrcLoc n1) + , quotes (ppr n2) <+> text "bound at" <+> ppr (getSrcLoc n2) ] + + -------------- The swizzler ------------ + -- This does a deep traverse, simply doing a + -- Name-to-Name change, governed by swizzle_env + -- The 'swap' is what gets from the representative TyVar + -- back to the original user-specified Name + swizzle_env = mkVarEnv (map swap swizzle_prs) + + swizzleMapper :: TyCoMapper () Identity + swizzleMapper = TyCoMapper { tcm_tyvar = swizzle_tv + , tcm_covar = swizzle_cv + , tcm_hole = swizzle_hole + , tcm_tycobinder = swizzle_bndr + , tcm_tycon = swizzle_tycon } + swizzle_hole _ hole = pprPanic "swizzle_hole" (ppr hole) + -- These types are pre-zonked + swizzle_tycon tc = pprPanic "swizzle_tc" (ppr tc) + -- TcTyCons can't appear in kinds (yet) + swizzle_tv _ tv = return (mkTyVarTy (swizzle_var tv)) + swizzle_cv _ cv = return (mkCoVarCo (swizzle_var cv)) + + swizzle_bndr _ tcv _ + = return ((), swizzle_var tcv) + + swizzle_var :: Var -> Var + swizzle_var v + | Just nm <- lookupVarEnv swizzle_env v + = updateVarType swizzle_ty (v `setVarName` nm) + | otherwise + = updateVarType swizzle_ty v + + swizzle_ty ty = runIdentity (mapType swizzleMapper () ty) + + +generaliseTcTyCon :: (TcTyCon, ScopedPairs, TcKind) -> TcM TcTyCon +generaliseTcTyCon (tc, scoped_prs, tc_res_kind) -- See Note [Required, Specified, and Inferred for types] = setSrcSpan (getSrcSpan tc) $ addTyConCtxt tc $ - do { let tc_name = tyConName tc - tc_res_kind = tyConResKind tc - spec_req_prs = tcTyConScopedTyVars tc - - (spec_req_names, spec_req_tvs) = unzip spec_req_prs - -- NB: spec_req_tvs includes both Specified and Required - -- Running example in Note [Inferring kinds for type declarations] - -- spec_req_prs = [ ("k1",kk1), ("a", (aa::kk1)) - -- , ("k2",kk2), ("x", (xx::kk2))] - -- where "k1" denotes the Name k1, and kk1, aa, etc are MetaTyVars, - -- specifically TyVarTvs - - -- Step 0: zonk and skolemise the Specified and Required binders - -- It's essential that they are skolems, not MetaTyVars, - -- for Step 3 to work right - ; spec_req_tvs <- mapM zonkAndSkolemise spec_req_tvs - -- Running example, where kk1 := kk2, so we get - -- [kk2,kk2] - - -- Step 1: Check for duplicates - -- E.g. data SameKind (a::k) (b::k) - -- data T (a::k1) (b::k2) = MkT (SameKind a b) - -- Here k1 and k2 start as TyVarTvs, and get unified with each other - -- If this happens, things get very confused later, so fail fast - ; checkDuplicateTyConBinders spec_req_names spec_req_tvs + do { -- Step 1: Separate Specified from Required variables + -- NB: spec_req_tvs = spec_tvs ++ req_tvs + -- And req_tvs is 1-1 with tyConTyVars + -- See Note [Scoped tyvars in a TcTyCon] in TyCon + ; let spec_req_tvs = map snd scoped_prs + n_spec = length spec_req_tvs - tyConArity tc + (spec_tvs, req_tvs) = splitAt n_spec spec_req_tvs + sorted_spec_tvs = scopedSort spec_tvs + -- NB: We can't do the sort until we've zonked + -- Maintain the L-R order of scoped_tvs -- Step 2a: find all the Inferred variables we want to quantify over - -- NB: candidateQTyVarsOfKinds zonks as it goes ; dvs1 <- candidateQTyVarsOfKinds $ - (tc_res_kind : map tyVarKind spec_req_tvs) + (tc_res_kind : map tyVarKind spec_req_tvs) ; let dvs2 = dvs1 `delCandidates` spec_req_tvs -- Step 2b: quantify, mainly meaning skolemise the free variables -- Returned 'inferred' are scope-sorted and skolemised ; inferred <- quantifyTyVars dvs2 - -- Step 3a: rename all the Specified and Required tyvars back to - -- TyVars with their oroginal user-specified name. Example - -- class C a_r23 where .... - -- By this point we have scoped_prs = [(a_r23, a_r89[TyVarTv])] - -- We return with the TyVar a_r23[TyVar], - -- and ze mapping a_r89 :-> a_r23[TyVar] - ; traceTc "generaliseTcTyCon: before zonkRec" - (vcat [ text "spec_req_tvs =" <+> pprTyVars spec_req_tvs + ; traceTc "generaliseTcTyCon: pre zonk" + (vcat [ text "tycon =" <+> ppr tc + , text "spec_req_tvs =" <+> pprTyVars spec_req_tvs + , text "tc_res_kind =" <+> ppr tc_res_kind + , text "dvs1 =" <+> ppr dvs1 , text "inferred =" <+> pprTyVars inferred ]) - ; (ze, final_spec_req_tvs) <- zonkRecTyVarBndrs spec_req_names spec_req_tvs - -- So ze maps from the tyvars that have ended up - -- Step 3b: Apply that mapping to the other variables - -- (remember they all started as TyVarTvs). - -- They have been skolemised by quantifyTyVars. - ; (ze, inferred) <- zonkTyBndrsX ze inferred - ; tc_res_kind <- zonkTcTypeToTypeX ze tc_res_kind + -- Step 3: Final zonk (following kind generalisation) + -- See Note [Swizzling the tyvars before generaliseTcTyCon] + ; ze <- emptyZonkEnv + ; (ze, inferred) <- zonkTyBndrsX ze inferred + ; (ze, sorted_spec_tvs) <- zonkTyBndrsX ze sorted_spec_tvs + ; (ze, req_tvs) <- zonkTyBndrsX ze req_tvs + ; tc_res_kind <- zonkTcTypeToTypeX ze tc_res_kind ; traceTc "generaliseTcTyCon: post zonk" $ vcat [ text "tycon =" <+> ppr tc , text "inferred =" <+> pprTyVars inferred - , text "ze =" <+> ppr ze - , text "spec_req_prs =" <+> ppr spec_req_prs , text "spec_req_tvs =" <+> pprTyVars spec_req_tvs - , text "final_spec_req_tvs =" <+> pprTyVars final_spec_req_tvs ] - - -- Step 4: Find the Specified and Inferred variables - -- NB: spec_req_tvs = spec_tvs ++ req_tvs - -- And req_tvs is 1-1 with tyConTyVars - -- See Note [Scoped tyvars in a TcTyCon] in TyCon - ; let n_spec = length final_spec_req_tvs - tyConArity tc - (spec_tvs, req_tvs) = splitAt n_spec final_spec_req_tvs - specified = scopedSort spec_tvs - -- NB: maintain the L-R order of scoped_tvs - - -- Step 5: Make the TyConBinders. - to_user tv = lookupTyVarOcc ze tv `orElse` tv - dep_fv_set = mapVarSet to_user (candidateKindVars dvs1) + , text "sorted_spec_tvs =" <+> pprTyVars sorted_spec_tvs + , text "req_tvs =" <+> ppr req_tvs + , text "zonk-env =" <+> ppr ze ] + + -- Step 4: Make the TyConBinders. + ; let dep_fv_set = candidateKindVars dvs1 inferred_tcbs = mkNamedTyConBinders Inferred inferred - specified_tcbs = mkNamedTyConBinders Specified specified + specified_tcbs = mkNamedTyConBinders Specified sorted_spec_tvs required_tcbs = map (mkRequiredTyConBinder dep_fv_set) req_tvs - -- Step 6: Assemble the final list. + -- Step 5: Assemble the final list. final_tcbs = concat [ inferred_tcbs , specified_tcbs , required_tcbs ] - -- Step 7: Make the result TcTyCon - tycon = mkTcTyCon tc_name final_tcbs tc_res_kind - (mkTyVarNamePairs final_spec_req_tvs) + -- Step 6: Make the result TcTyCon + tycon = mkTcTyCon (tyConName tc) final_tcbs tc_res_kind + (mkTyVarNamePairs (sorted_spec_tvs ++ req_tvs)) True {- it's generalised now -} (tyConFlavour tc) @@ -679,32 +902,18 @@ generaliseTcTyCon tc vcat [ text "tycon =" <+> ppr tc , text "tc_res_kind =" <+> ppr tc_res_kind , text "dep_fv_set =" <+> ppr dep_fv_set - , text "final_spec_req_tvs =" <+> pprTyVars final_spec_req_tvs - , text "inferred =" <+> pprTyVars inferred - , text "specified =" <+> pprTyVars specified + , text "inferred_tcbs =" <+> ppr inferred_tcbs + , text "specified_tcbs =" <+> ppr specified_tcbs , text "required_tcbs =" <+> ppr required_tcbs , text "final_tcbs =" <+> ppr final_tcbs ] - -- Step 8: Check for validity. + -- Step 7: Check for validity. -- We do this here because we're about to put the tycon into the -- the environment, and we don't want anything malformed there ; checkTyConTelescope tycon ; return tycon } -checkDuplicateTyConBinders :: [Name] -> [TcTyVar] -> TcM () -checkDuplicateTyConBinders spec_req_names spec_req_tvs - | null dups = return () - | otherwise = mapM_ report_dup dups >> failM - where - dups :: [(Name,Name)] - dups = findDupTyVarTvs $ spec_req_names `zip` spec_req_tvs - - report_dup (n1, n2) - = setSrcSpan (getSrcSpan n2) $ - addErrTc (text "Couldn't match" <+> quotes (ppr n1) - <+> text "with" <+> quotes (ppr n2)) - {- Note [Required, Specified, and Inferred for types] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Each forall'd type variable in a type or kind is one of @@ -1029,8 +1238,8 @@ mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats }) = unitNameEnv nm (APromotionErr ClassPE) `plusNameEnv` - mkNameEnv [ (name, APromotionErr TyConPE) - | (L _ (FamilyDecl { fdLName = L _ name })) <- ats ] + mkNameEnv [ (familyDeclName at, APromotionErr TyConPE) + | L _ at <- ats ] mk_prom_err_env (DataDecl { tcdLName = L _ name , tcdDataDefn = HsDataDefn { dd_cons = cons } }) @@ -1770,17 +1979,14 @@ tcTyClDecl1 _parent roles_info , tcdRhs = rhs }) = ASSERT( isNothing _parent ) fmap noDerivInfos $ - bindTyClTyVars tc_name $ \ binders res_kind -> - tcTySynRhs roles_info tc_name binders res_kind rhs + tcTySynRhs roles_info tc_name rhs -- "data/newtype" declaration tcTyClDecl1 _parent roles_info decl@(DataDecl { tcdLName = L _ tc_name , tcdDataDefn = defn }) = ASSERT( isNothing _parent ) - bindTyClTyVars tc_name $ \ tycon_binders res_kind -> - tcDataDefn (tcMkDeclCtxt decl) roles_info tc_name - tycon_binders res_kind defn + tcDataDefn (tcMkDeclCtxt decl) roles_info tc_name defn tcTyClDecl1 _parent roles_info (ClassDecl { tcdLName = L _ class_name @@ -1884,10 +2090,10 @@ tcClassATs class_name cls ats at_defs ; mapM tc_at ats } where at_def_tycon :: LTyFamDefltDecl GhcRn -> Name - at_def_tycon (L _ eqn) = tyFamInstDeclName eqn + at_def_tycon = tyFamInstDeclName . unLoc at_fam_name :: LFamilyDecl GhcRn -> Name - at_fam_name (L _ decl) = unLoc (fdLName decl) + at_fam_name = familyDeclName . unLoc at_names = mkNameSet (map at_fam_name ats) @@ -2226,12 +2432,11 @@ tcInjectivity tcbs (Just (L loc (InjectivityAnn _ lInjNames))) , ppr inj_ktvs, ppr inj_bools ]) ; return $ Injective inj_bools } -tcTySynRhs :: RolesInfo - -> Name - -> [TyConBinder] -> Kind +tcTySynRhs :: RolesInfo -> Name -> LHsType GhcRn -> TcM TyCon -tcTySynRhs roles_info tc_name binders res_kind hs_ty - = do { env <- getLclEnv +tcTySynRhs roles_info tc_name hs_ty + = bindTyClTyVars tc_name $ \ binders res_kind -> + do { env <- getLclEnv ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env)) ; rhs_ty <- pushTcLevelM_ $ solveEqualities $ @@ -2241,27 +2446,29 @@ tcTySynRhs roles_info tc_name binders res_kind hs_ty tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty ; return tycon } -tcDataDefn :: SDoc - -> RolesInfo -> Name - -> [TyConBinder] -> Kind +tcDataDefn :: SDoc -> RolesInfo -> Name -> HsDataDefn GhcRn -> TcM (TyCon, [DerivInfo]) -- NB: not used for newtype/data instances (whether associated or not) -tcDataDefn err_ctxt - roles_info - tc_name tycon_binders res_kind +tcDataDefn err_ctxt roles_info tc_name (HsDataDefn { dd_ND = new_or_data, dd_cType = cType , dd_ctxt = ctxt , dd_kindSig = mb_ksig -- Already in tc's kind -- via inferInitialKinds , dd_cons = cons , dd_derivs = derivs }) - = do { gadt_syntax <- dataDeclChecks tc_name new_or_data ctxt cons + = bindTyClTyVars tc_name $ \ tycon_binders res_kind -> + -- The TyCon tyvars must scope over + -- - the stupid theta (dd_ctxt) + -- - for H98 constructors only, the ConDecl + -- But it does no harm to bring them into scope + -- over GADT ConDecls as well; and it's awkward not to + do { gadt_syntax <- dataDeclChecks tc_name new_or_data ctxt cons + ; (extra_bndrs, final_res_kind) <- etaExpandAlgTyCon tycon_binders res_kind ; tcg_env <- getGblEnv - ; (extra_bndrs, final_res_kind) <- etaExpandAlgTyCon tycon_binders res_kind ; let hsc_src = tcg_src tcg_env ; unless (mk_permissive_kind hsc_src cons) $ - checkDataKindSig (DataDeclSort new_or_data) final_res_kind + checkDataKindSig (DataDeclSort new_or_data) final_res_kind ; stupid_tc_theta <- pushTcLevelM_ $ solveEqualities $ tcHsContext ctxt ; stupid_theta <- zonkTcTypesToTypes stupid_tc_theta @@ -2326,7 +2533,7 @@ tcDataDefn err_ctxt DataType -> return (mkDataTyConRhs data_cons) NewType -> ASSERT( not (null data_cons) ) mkNewTyConRhs tc_name tycon (head data_cons) -tcDataDefn _ _ _ _ _ (XHsDataDefn nec) = noExtCon nec +tcDataDefn _ _ _ (XHsDataDefn nec) = noExtCon nec ------------------------- @@ -2382,7 +2589,13 @@ tcTyFamInstEqn fam_tc mb_clsinfo , feqn_rhs = hs_rhs_ty }})) = ASSERT( getName fam_tc == eqn_tc_name ) setSrcSpan loc $ - do { + do { traceTc "tcTyFamInstEqn" $ + vcat [ ppr fam_tc <+> ppr hs_pats + , text "fam tc bndrs" <+> pprTyVars (tyConTyVars fam_tc) + , case mb_clsinfo of + NotAssociated -> empty + InClsInst { ai_class = cls } -> text "class" <+> ppr cls <+> pprTyVars (classTyVars cls) ] + -- First, check the arity of visible arguments -- If we wait until validity checking, we'll get kind errors -- below when an arity error will be much easier to understand. @@ -2466,7 +2679,7 @@ tcTyFamInstEqnGuts :: TyCon -> AssocInstInfo -> TcM ([TyVar], [TcType], TcType) -- (tyvars, pats, rhs) -- Used only for type families, not data families tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty - = do { traceTc "tcTyFamInstEqnGuts {" (vcat [ ppr fam_tc <+> ppr hs_pats ]) + = do { traceTc "tcTyFamInstEqnGuts {" (ppr fam_tc) -- By now, for type families (but not data families) we should -- have checked that the number of patterns matches tyConArity @@ -2495,6 +2708,13 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs) ; qtvs <- quantifyTyVars dvs + ; traceTc "tcTyFamInstEqnGuts 2" $ + vcat [ ppr fam_tc + , text "scoped_tvs" <+> pprTyVars scoped_tvs + , text "lhs_ty" <+> ppr lhs_ty + , text "dvs" <+> ppr dvs + , text "qtvs" <+> pprTyVars qtvs ] + ; (ze, qtvs) <- zonkTyBndrs qtvs ; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty ; rhs_ty <- zonkTcTypeToTypeX ze rhs_ty @@ -2817,7 +3037,7 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data ; return (ctxt, final_arg_tys, res_ty, field_lbls, stricts) } ; imp_tvs <- zonkAndScopedSort imp_tvs - ; let user_tvs = imp_tvs ++ exp_tvs + ; let user_tvs = imp_tvs ++ exp_tvs ; tkvs <- kindGeneralizeAll (mkSpecForAllTys user_tvs $ mkPhiTy ctxt $ diff --git a/testsuite/tests/polykinds/T11203.stderr b/testsuite/tests/polykinds/T11203.stderr index f5c72133ae..e6f30c0335 100644 --- a/testsuite/tests/polykinds/T11203.stderr +++ b/testsuite/tests/polykinds/T11203.stderr @@ -1,4 +1,4 @@ T11203.hs:7:24: error: - • Couldn't match ‘k1’ with ‘k2’ - • In the data type declaration for ‘Q’ + • Different names for the same type variable: ‘k1’ and ‘k2’ + • In the data declaration for ‘Q’ diff --git a/testsuite/tests/polykinds/T11821a.stderr b/testsuite/tests/polykinds/T11821a.stderr index f55c703524..50d58df8f5 100644 --- a/testsuite/tests/polykinds/T11821a.stderr +++ b/testsuite/tests/polykinds/T11821a.stderr @@ -1,4 +1,4 @@ T11821a.hs:4:31: error: - • Couldn't match ‘k1’ with ‘k2’ - • In the type synonym declaration for ‘SameKind’ + • Different names for the same type variable: ‘k1’ and ‘k2’ + • In the type declaration for ‘SameKind’ diff --git a/testsuite/tests/typecheck/should_compile/Makefile b/testsuite/tests/typecheck/should_compile/Makefile index 5255485601..5c0c84f8ec 100644 --- a/testsuite/tests/typecheck/should_compile/Makefile +++ b/testsuite/tests/typecheck/should_compile/Makefile @@ -75,3 +75,8 @@ T14934: $(RM) -f T14934a.o T14934a.hi T14934.o T14934.hi '$(TEST_HC)' $(TEST_HC_OPTS) -c T14934a.hs -O '$(TEST_HC)' $(TEST_HC_OPTS) -c T14934.hs -O + +T17566: + $(RM) -f T17566a.o T17566a.hi T17566.o T17566.hi + '$(TEST_HC)' $(TEST_HC_OPTS) -c T17566a.hs + '$(TEST_HC)' $(TEST_HC_OPTS) -c T17566.hs diff --git a/testsuite/tests/typecheck/should_compile/T17566.hs b/testsuite/tests/typecheck/should_compile/T17566.hs new file mode 100644 index 0000000000..5996bd7d47 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T17566.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +module T17566 where + +import Data.Kind +import Data.Proxy +import T17566a + +type family F1 (x :: Proxy a) :: Proxy a +instance C1 Proxy z where + type T1 x = F1 x + data D1 x + +type family F2 (x :: Proxy a) :: Proxy a +instance C2 Proxy z where + type T2 x = F2 x + data D2 x diff --git a/testsuite/tests/typecheck/should_compile/T17566a.hs b/testsuite/tests/typecheck/should_compile/T17566a.hs new file mode 100644 index 0000000000..6255a7a7ba --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T17566a.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +module T17566a where + +import Data.Kind + +class C1 (f :: k -> Type) z where + type T1 (x :: f a) :: f a + data D1 (x :: f a) + +class C2 f z where + type T2 (x :: f a) :: f a + data D2 (x :: f a) diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 80b11ca851..0f61b57faf 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -692,3 +692,4 @@ test('T17202', expect_broken(17202), compile, ['']) test('T15839a', normal, compile, ['']) test('T15839b', normal, compile, ['']) test('T17343', exit_code(1), compile_and_run, ['']) +test('T17566', [extra_files(['T17566a.hs'])], makefile_test, []) diff --git a/testsuite/tests/typecheck/should_fail/T17566b.hs b/testsuite/tests/typecheck/should_fail/T17566b.hs new file mode 100644 index 0000000000..7b1711ada6 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T17566b.hs @@ -0,0 +1,7 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +module T17566b where + +class C f where + type T1 (f :: k1) + type T2 (f :: k2) diff --git a/testsuite/tests/typecheck/should_fail/T17566b.stderr b/testsuite/tests/typecheck/should_fail/T17566b.stderr new file mode 100644 index 0000000000..be3c0e19bd --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T17566b.stderr @@ -0,0 +1,4 @@ + +T17566b.hs:7:17: error: + • Different names for the same type variable: ‘k1’ and ‘k2’ + • In the class declaration for ‘C’ diff --git a/testsuite/tests/typecheck/should_fail/T17566c.hs b/testsuite/tests/typecheck/should_fail/T17566c.hs new file mode 100644 index 0000000000..d7d68a050c --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T17566c.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +module T17566c where + +import Data.Kind + +class C2 f z where + type T2 (f :: k -> Type) + data D2 (x :: (f :: k -> Type) a) diff --git a/testsuite/tests/typecheck/should_fail/T17566c.stderr b/testsuite/tests/typecheck/should_fail/T17566c.stderr new file mode 100644 index 0000000000..df5e5c0739 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T17566c.stderr @@ -0,0 +1,6 @@ + +T17566c.hs:11:23: error: + • Different names for the same type variable: + ‘k’ bound at T17566c.hs:10:17 + ‘k’ bound at T17566c.hs:11:23 + • In the class declaration for ‘C2’ diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index e11c239742..f0f290c405 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -550,3 +550,5 @@ test('T17355', normal, compile_fail, ['']) test('T17360', normal, compile_fail, ['']) test('T17563', normal, compile_fail, ['']) test('T16946', normal, compile_fail, ['']) +test('T17566b', normal, compile_fail, ['']) +test('T17566c', normal, compile_fail, ['']) diff --git a/utils/haddock b/utils/haddock -Subproject 4808003d2238f76aee96d22cc022cee3e049f6a +Subproject f3e3c4a766805a1bbea75bf23b84fdaaf053c22 |