diff options
Diffstat (limited to 'compiler/GHC/Tc/TyCl.hs')
| -rw-r--r-- | compiler/GHC/Tc/TyCl.hs | 203 |
1 files changed, 104 insertions, 99 deletions
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs index 2cefd67c7f..9cd0b2a66c 100644 --- a/compiler/GHC/Tc/TyCl.hs +++ b/compiler/GHC/Tc/TyCl.hs @@ -30,6 +30,8 @@ import GHC.Prelude import GHC.Hs import GHC.Driver.Types import GHC.Tc.TyCl.Build +import GHC.Tc.Solver( pushLevelAndSolveEqualities, pushLevelAndSolveEqualitiesX + , reportUnsolvedEqualities ) import GHC.Tc.Utils.Monad import GHC.Tc.Utils.Env import GHC.Tc.Validity @@ -38,7 +40,6 @@ import GHC.Tc.TyCl.Utils import GHC.Tc.TyCl.Class import {-# SOURCE #-} GHC.Tc.TyCl.Instance( tcInstDecls1 ) import GHC.Tc.Deriv (DerivInfo(..)) -import GHC.Tc.Utils.Unify ( checkTvConstraints ) import GHC.Tc.Gen.HsType import GHC.Tc.Instance.Class( AssocInstInfo(..) ) import GHC.Tc.Utils.TcMType @@ -644,13 +645,18 @@ kcTyClGroup kisig_env decls | otherwise = Left d - ; checked_tcs <- checkInitialKinds kinded_decls + ; checked_tcs <- checkNoErrs $ + checkInitialKinds kinded_decls + -- checkNoErrs because we are about to extend + -- the envt with these tycons, and we get + -- knock-on errors if we have tycons with + -- malformed kinds + ; inferred_tcs - <- tcExtendKindEnvWithTyCons checked_tcs $ - pushTcLevelM_ $ -- We are going to kind-generalise, so - -- unification variables in here must - -- be one level in - solveEqualities $ + <- tcExtendKindEnvWithTyCons checked_tcs $ + pushLevelAndSolveEqualities UnkSkol [] $ + -- We are going to kind-generalise, so unification + -- variables in here must be one level in do { -- Step 1: Bind kind variables for all decls mono_tcs <- inferInitialKinds kindless_decls @@ -2300,10 +2306,8 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs roles = roles_info tycon_name -- for TyCon and Class ; (ctxt, fds, sig_stuff, at_stuff) - <- pushTcLevelM_ $ - solveEqualities $ - checkTvConstraints skol_info (binderVars binders) $ - -- The checkTvConstraints is needed bring into scope the + <- pushLevelAndSolveEqualities skol_info (binderVars binders) $ + -- The (binderVars binders) is needed bring into scope the -- skolems bound by the class decl header (#17841) do { ctxt <- tcHsContext hs_ctxt ; fds <- mapM (addLocM tc_fundep) fundeps @@ -2311,7 +2315,8 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs ; at_stuff <- tcClassATs class_name clas ats at_defs ; return (ctxt, fds, sig_stuff, at_stuff) } - -- The solveEqualities will report errors for any + + -- The pushLevelAndSolveEqualities will report errors for any -- unsolved equalities, so these zonks should not encounter -- any unfilled coercion variables unless there is such an error -- The zonk also squeeze out the TcTyCons, and converts @@ -2703,13 +2708,13 @@ 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 $ + ; rhs_ty <- pushLevelAndSolveEqualities skol_info (binderVars binders) $ tcCheckLHsType hs_ty (TheKind res_kind) ; rhs_ty <- zonkTcTypeToType rhs_ty ; let roles = roles_info tc_name - tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty - ; return tycon } + ; return (buildSynTyCon tc_name binders res_kind roles rhs_ty) } + where + skol_info = TyConSkol TypeSynonymFlavour tc_name tcDataDefn :: SDoc -> RolesInfo -> Name -> HsDataDefn GhcRn -> TcM (TyCon, [DerivInfo]) @@ -2739,7 +2744,9 @@ tcDataDefn err_ctxt roles_info tc_name ; unless (mk_permissive_kind hsc_src cons) $ checkDataKindSig (DataDeclSort new_or_data) final_res_kind - ; stupid_tc_theta <- pushTcLevelM_ $ solveEqualities $ tcHsContext ctxt + ; let skol_tvs = binderVars tycon_binders + ; stupid_tc_theta <- pushLevelAndSolveEqualities skol_info skol_tvs $ + tcHsContext ctxt ; stupid_theta <- zonkTcTypesToTypes stupid_tc_theta ; kind_signatures <- xoptM LangExt.KindSignatures @@ -2775,6 +2782,9 @@ tcDataDefn err_ctxt roles_info tc_name ; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs) ; return (tycon, [deriv_info]) } where + skol_info = TyConSkol flav tc_name + flav = newOrDataToFlavour new_or_data + -- Abstract data types in hsig files can have arbitrary kinds, -- because they may be implemented by type synonyms -- (which themselves can have arbitrary kinds, not just *). See #13955. @@ -2912,40 +2922,38 @@ or (Type -> Type) for the equations above) and the instantiated kind. Note [Generalising in tcTyFamInstEqnGuts] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have something like - type instance forall (a::k) b. F t1 t2 = rhs + type instance forall (a::k) b. F (Proxy t1) _ = rhs Then imp_vars = [k], exp_bndrs = [a::k, b] -We want to quantify over - * k, a, and b (all user-specified) - * and any inferred free kind vars from - - the kinds of k, a, b - - the types t1, t2 +We want to quantify over all the free vars of the LHS including + * any invisible kind variables arising from instantiating tycons, + such as Proxy + * wildcards such as '_' above -However, unlike a type signature like - f :: forall (a::k). blah +So, the simple thing is + - Gather candidates from the LHS + - Include any user-specified forall'd variables, so that we get an + error from Validity.checkFamPatBinders if a forall'd variable is + not bound on the LHS + - Quantify over them +Note that, unlike a type signature like + f :: forall (a::k). blah we do /not/ care about the Inferred/Specified designation or order for the final quantified tyvars. Type-family instances are not invoked directly in Haskell source code, so visible type application etc plays no role. -So, the simple thing is - - gather candidates from [k, a, b] and pats - - quantify over them - -Hence the slightly mysterious call: - candidateQTyVarsOfTypes (pats ++ mkTyVarTys scoped_tvs) +See also Note [Re-quantify type variables in rules] in +GHC.Tc.Gen.Rule, which explains a /very/ similar design when +generalising over the type of a rewrite rule. -Simple, neat, but a little non-obvious! - -See also Note [Re-quantify type variables in rules] in GHC.Tc.Gen.Rule, which explains -a very similar design when generalising over the type of a rewrite rule. -} -------------------------- tcTyFamInstEqnGuts :: TyCon -> AssocInstInfo - -> [Name] -> [LHsTyVarBndr () GhcRn] -- Implicit and explicicit binder + -> [Name] -> [LHsTyVarBndr () GhcRn] -- Implicit and explicit binder -> HsTyPats GhcRn -- Patterns -> LHsType GhcRn -- RHS -> TcM ([TyVar], [TcType], TcType) -- (tyvars, pats, rhs) @@ -2958,11 +2966,10 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty -- This code is closely related to the code -- in GHC.Tc.Gen.HsType.kcCheckDeclHeader_cusk - ; (imp_tvs, (exp_tvs, (lhs_ty, rhs_ty))) - <- pushTcLevelM_ $ - solveEqualities $ - bindImplicitTKBndrs_Q_Skol imp_vars $ - bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $ + ; (tclvl, wanted, (imp_tvs, (exp_tvs, (lhs_ty, rhs_ty)))) + <- pushLevelAndSolveEqualitiesX "tcTyFamInstEqnGuts" $ + bindImplicitTKBndrs_Q_Skol imp_vars $ + bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $ do { (lhs_ty, rhs_kind) <- tcFamTyPats fam_tc hs_pats -- Ensure that the instance is consistent with its -- parent class (#16008) @@ -2970,21 +2977,20 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty ; rhs_ty <- tcCheckLHsType hs_rhs_ty (TheKind rhs_kind) ; return (lhs_ty, rhs_ty) } - -- See Note [Generalising in tcTyFamInstEqnGuts] -- This code (and the stuff immediately above) is very similar -- to that in tcDataFamInstHeader. Maybe we should abstract the -- common code; but for the moment I concluded that it's -- clearer to duplicate it. Still, if you fix a bug here, -- check there too! - ; let scoped_tvs = imp_tvs ++ exp_tvs - ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs) + + -- See Note [Generalising in tcTyFamInstEqnGuts] + ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys (imp_tvs ++ exp_tvs)) ; qtvs <- quantifyTyVars dvs + ; reportUnsolvedEqualities FamInstSkol qtvs tclvl wanted ; 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 @@ -3167,11 +3173,11 @@ tcConDecl :: KnotTied TyCon -- Representation tycon. Knot-tied! -> TcM [DataCon] tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data - (ConDeclH98 { con_name = name + (ConDeclH98 { con_name = lname@(L _ name) , con_ex_tvs = explicit_tkv_nms , con_mb_cxt = hs_ctxt , con_args = hs_args }) - = addErrCtxt (dataConCtxtName [name]) $ + = addErrCtxt (dataConCtxtName [lname]) $ do { -- NB: the tyvars from the declaration header are in scope -- Get hold of the existential type variables @@ -3182,62 +3188,63 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data ; traceTc "tcConDecl 1" (vcat [ ppr name, ppr explicit_tkv_nms ]) - ; (exp_tvbndrs, (ctxt, arg_tys, field_lbls, stricts)) - <- pushTcLevelM_ $ - solveEqualities $ - bindExplicitTKBndrs_Skol explicit_tkv_nms $ + ; (tclvl, wanted, (exp_tvbndrs, (ctxt, arg_tys, field_lbls, stricts))) + <- pushLevelAndSolveEqualitiesX "tcConDecl:H98" $ + bindExplicitTKBndrs_Skol explicit_tkv_nms $ do { ctxt <- tcHsMbContext hs_ctxt ; let exp_kind = getArgExpKind new_or_data res_kind ; btys <- tcConArgs exp_kind hs_args - ; field_lbls <- lookupConstructorFields (unLoc name) + ; field_lbls <- lookupConstructorFields name ; let (arg_tys, stricts) = unzip btys ; return (ctxt, arg_tys, field_lbls, stricts) } + ; let tmpl_tvs = binderVars tmpl_bndrs + ; let fake_ty = mkSpecForAllTys tmpl_tvs $ + mkInvisForAllTys exp_tvbndrs $ + mkPhiTy ctxt $ + mkVisFunTys arg_tys $ + unitTy + -- That type is a lie, of course. (It shouldn't end in ()!) + -- And we could construct a proper result type from the info + -- at hand. But the result would mention only the tmpl_tvs, + -- and so it just creates more work to do it right. Really, + -- we're only doing this to find the right kind variables to + -- quantify over, and this type is fine for that purpose. -- exp_tvs have explicit, user-written binding sites -- the kvs below are those kind variables entirely unmentioned by the user -- and discovered only by generalization - ; kvs <- kindGeneralizeAll (mkSpecForAllTys tmpl_tvs $ - mkInvisForAllTys exp_tvbndrs $ - mkPhiTy ctxt $ - mkVisFunTys arg_tys $ - unitTy) - -- That type is a lie, of course. (It shouldn't end in ()!) - -- And we could construct a proper result type from the info - -- at hand. But the result would mention only the tmpl_tvs, - -- and so it just creates more work to do it right. Really, - -- we're only doing this to find the right kind variables to - -- quantify over, and this type is fine for that purpose. + ; kvs <- kindGeneralizeAll fake_ty + + ; let skol_tvs = kvs ++ tmpl_tvs ++ binderVars exp_tvbndrs + ; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted -- Zonk to Types ; (ze, qkvs) <- zonkTyBndrs kvs ; (ze, user_qtvbndrs) <- zonkTyVarBindersX ze exp_tvbndrs - ; let user_qtvs = binderVars user_qtvbndrs ; arg_tys <- zonkScaledTcTypesToTypesX ze arg_tys ; ctxt <- zonkTcTypesToTypesX ze ctxt - ; fam_envs <- tcGetFamInstEnvs - -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here ; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls) ; let univ_tvbs = tyConInvisTVBinders tmpl_bndrs univ_tvs = binderVars univ_tvbs - ex_tvbs = mkTyVarBinders InferredSpec qkvs ++ - user_qtvbndrs - ex_tvs = qkvs ++ user_qtvs + ex_tvbs = mkTyVarBinders InferredSpec qkvs ++ user_qtvbndrs + ex_tvs = binderVars ex_tvbs -- For H98 datatypes, the user-written tyvar binders are precisely -- the universals followed by the existentials. -- See Note [DataCon user type variable binders] in GHC.Core.DataCon. user_tvbs = univ_tvbs ++ ex_tvbs - buildOneDataCon (L _ name) = do - { is_infix <- tcConIsInfixH98 name hs_args - ; rep_nm <- newTyConRepName name - ; buildDataCon fam_envs name is_infix rep_nm + ; traceTc "tcConDecl 2" (ppr name) + ; is_infix <- tcConIsInfixH98 name hs_args + ; rep_nm <- newTyConRepName name + ; fam_envs <- tcGetFamInstEnvs + ; dc <- buildDataCon fam_envs name is_infix rep_nm stricts Nothing field_lbls univ_tvs ex_tvs user_tvbs [{- no eq_preds -}] ctxt arg_tys @@ -3245,10 +3252,10 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data -- NB: we put data_tc, the type constructor gotten from the -- constructor type signature into the data constructor; -- that way checkValidDataCon can complain if it's wrong. - } - ; traceTc "tcConDecl 2" (ppr name) - ; mapM buildOneDataCon [name] - } + + ; return [dc] } + where + skol_info = DataConSkol name tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data -- NB: don't use res_kind here, as it's ill-scoped. Instead, @@ -3262,12 +3269,10 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data do { traceTc "tcConDecl 1 gadt" (ppr names) ; let (L _ name : _) = names - ; (imp_tvs, (exp_tvbndrs, (ctxt, arg_tys, res_ty, field_lbls, stricts))) - <- pushTcLevelM_ $ -- We are going to generalise - solveEqualities $ -- We won't get another crack, and we don't - -- want an error cascade - bindImplicitTKBndrs_Skol implicit_tkv_nms $ - bindExplicitTKBndrs_Skol explicit_tkv_nms $ + ; (tclvl, wanted, (imp_tvs, (exp_tvbndrs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))) + <- pushLevelAndSolveEqualitiesX "tcConDecl:GADT" $ + bindImplicitTKBndrs_Skol implicit_tkv_nms $ + bindExplicitTKBndrs_Skol explicit_tkv_nms $ do { ctxt <- tcHsMbContext cxt ; (res_ty, res_kind) <- tcInferLHsTypeKind hs_res_ty -- See Note [GADT return kinds] @@ -3281,17 +3286,19 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data ; return (ctxt, arg_tys, res_ty, field_lbls, stricts) } ; imp_tvs <- zonkAndScopedSort imp_tvs - - ; tkvs <- kindGeneralizeAll (mkSpecForAllTys imp_tvs $ - mkInvisForAllTys exp_tvbndrs $ - mkPhiTy ctxt $ - mkVisFunTys arg_tys $ - res_ty) - - ; let tvbndrs = (mkTyVarBinders InferredSpec tkvs) - ++ (mkTyVarBinders SpecifiedSpec imp_tvs) + ; let con_ty = mkSpecForAllTys imp_tvs $ + mkInvisForAllTys exp_tvbndrs $ + mkPhiTy ctxt $ + mkVisFunTys arg_tys $ + res_ty + ; kvs <- kindGeneralizeAll con_ty + + ; let tvbndrs = mkTyVarBinders InferredSpec kvs + ++ mkTyVarBinders SpecifiedSpec imp_tvs ++ exp_tvbndrs + ; reportUnsolvedEqualities skol_info (binderVars tvbndrs) tclvl wanted + -- Zonk to Types ; (ze, tvbndrs) <- zonkTyVarBinders tvbndrs ; arg_tys <- zonkScaledTcTypesToTypesX ze arg_tys @@ -3306,11 +3313,9 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data arg_tys' = substScaledTys arg_subst arg_tys res_ty' = substTy arg_subst res_ty - - ; fam_envs <- tcGetFamInstEnvs - -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here ; traceTc "tcConDecl 2" (ppr names $$ ppr field_lbls) + ; fam_envs <- tcGetFamInstEnvs ; let buildOneDataCon (L _ name) = do { is_infix <- tcConIsInfixGADT name hs_args @@ -3325,9 +3330,9 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data -- constructor type signature into the data constructor; -- that way checkValidDataCon can complain if it's wrong. } - ; traceTc "tcConDecl 2" (ppr names) - ; mapM buildOneDataCon names - } + ; mapM buildOneDataCon names } + where + skol_info = DataConSkol (unLoc (head names)) {- Note [GADT return kinds] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ |