diff options
Diffstat (limited to 'compiler/typecheck')
| -rw-r--r-- | compiler/typecheck/FamInst.hs | 10 | ||||
| -rw-r--r-- | compiler/typecheck/TcClassDcl.hs | 4 | ||||
| -rw-r--r-- | compiler/typecheck/TcDeriv.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcErrors.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcGenDeriv.hs | 4 | ||||
| -rw-r--r-- | compiler/typecheck/TcGenGenerics.hs | 4 | ||||
| -rw-r--r-- | compiler/typecheck/TcHsSyn.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcHsType.hs | 235 | ||||
| -rw-r--r-- | compiler/typecheck/TcInstDcls.hs | 2 | ||||
| -rw-r--r-- | compiler/typecheck/TcMType.hs | 411 | ||||
| -rw-r--r-- | compiler/typecheck/TcPatSyn.hs | 52 | ||||
| -rw-r--r-- | compiler/typecheck/TcRules.hs | 26 | ||||
| -rw-r--r-- | compiler/typecheck/TcSMonad.hs | 15 | ||||
| -rw-r--r-- | compiler/typecheck/TcSigs.hs | 6 | ||||
| -rw-r--r-- | compiler/typecheck/TcSimplify.hs | 21 | ||||
| -rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 573 | ||||
| -rw-r--r-- | compiler/typecheck/TcType.hs | 149 | ||||
| -rw-r--r-- | compiler/typecheck/TcValidity.hs | 48 |
18 files changed, 892 insertions, 674 deletions
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs index 8f1f7ba5f6..5825232574 100644 --- a/compiler/typecheck/FamInst.hs +++ b/compiler/typecheck/FamInst.hs @@ -168,7 +168,13 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc }) -- Note [Linting type synonym applications]. case lintTypes dflags tcvs' (rhs':lhs') of Nothing -> pure () - Just fail_msg -> pprPanic "Core Lint error" fail_msg + Just fail_msg -> pprPanic "Core Lint error" (vcat [ fail_msg + , ppr fam_tc + , ppr subst + , ppr tvs' + , ppr cvs' + , ppr lhs' + , ppr rhs' ]) ; return (FamInst { fi_fam = tyConName fam_tc , fi_flavor = flavor , fi_tcs = roughMatchTcs lhs @@ -893,7 +899,7 @@ unusedInjectiveVarsErr (Pair invis_vars vis_vars) errorBuilder tyfamEqn has_kinds = not $ isEmptyVarSet invis_vars doc = sep [ what <+> text "variable" <> - pluralVarSet tvs <+> pprVarSet tvs (pprQuotedList . toposortTyVars) + pluralVarSet tvs <+> pprVarSet tvs (pprQuotedList . scopedSort) , text "cannot be inferred from the right-hand side." ] what = case (has_types, has_kinds) of (True, True) -> text "Type and kind" diff --git a/compiler/typecheck/TcClassDcl.hs b/compiler/typecheck/TcClassDcl.hs index 118a219af6..fe29c3d1d0 100644 --- a/compiler/typecheck/TcClassDcl.hs +++ b/compiler/typecheck/TcClassDcl.hs @@ -514,8 +514,8 @@ tcATDefault loc inst_subst defined_ats (ATI fam_tc defs) rhs' = substTyUnchecked subst' rhs_ty tcv' = tyCoVarsOfTypesList pat_tys' (tv', cv') = partition isTyVar tcv' - tvs' = toposortTyVars tv' - cvs' = toposortTyVars cv' + tvs' = scopedSort tv' + cvs' = scopedSort cv' ; rep_tc_name <- newFamInstTyConName (L loc (tyConName fam_tc)) pat_tys' ; let axiom = mkSingleCoAxiom Nominal rep_tc_name tvs' cvs' fam_tc pat_tys' rhs' diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs index 6f749fc60f..bb9c76ba61 100644 --- a/compiler/typecheck/TcDeriv.hs +++ b/compiler/typecheck/TcDeriv.hs @@ -815,7 +815,7 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred final_tkvs = tyCoVarsOfTypesWellScoped $ final_cls_tys ++ final_tc_args - ; let tkvs = toposortTyVars $ fvVarList $ + ; let tkvs = scopedSort $ fvVarList $ unionFV (tyCoFVsOfTypes tc_args_to_keep) (FV.mkFVs deriv_tvs) Just kind_subst = mb_match diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 951107bbcf..1fd98f1aa5 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -485,7 +485,7 @@ reportBadTelescope ctxt env (Just telescope) skols text "are out of dependency order. Perhaps try this ordering:") 2 (pprTyVars sorted_tvs) - sorted_tvs = toposortTyVars skols + sorted_tvs = scopedSort skols reportBadTelescope _ _ Nothing skols = pprPanic "reportBadTelescope" (ppr skols) diff --git a/compiler/typecheck/TcGenDeriv.hs b/compiler/typecheck/TcGenDeriv.hs index b3a4d536d1..84147c6b64 100644 --- a/compiler/typecheck/TcGenDeriv.hs +++ b/compiler/typecheck/TcGenDeriv.hs @@ -1840,8 +1840,8 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty rep_rhs_ty = mkTyConApp fam_tc rep_rhs_tys rep_tcvs = tyCoVarsOfTypesList rep_lhs_tys (rep_tvs, rep_cvs) = partition isTyVar rep_tcvs - rep_tvs' = toposortTyVars rep_tvs - rep_cvs' = toposortTyVars rep_cvs + rep_tvs' = scopedSort rep_tvs + rep_cvs' = scopedSort rep_cvs pp_lhs = ppr (mkTyConApp fam_tc rep_lhs_tys) -- Same as inst_tys, but with the last argument type replaced by the diff --git a/compiler/typecheck/TcGenGenerics.hs b/compiler/typecheck/TcGenGenerics.hs index 9da94280ce..6372c66912 100644 --- a/compiler/typecheck/TcGenGenerics.hs +++ b/compiler/typecheck/TcGenGenerics.hs @@ -434,8 +434,8 @@ tc_mkRepFamInsts gk tycon inst_tys = repTy' = substTy subst repTy tcv' = tyCoVarsOfTypeList inst_ty (tv', cv') = partition isTyVar tcv' - tvs' = toposortTyVars tv' - cvs' = toposortTyVars cv' + tvs' = scopedSort tv' + cvs' = scopedSort cv' axiom = mkSingleCoAxiom Nominal rep_name tvs' cvs' fam_tc inst_tys repTy' diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs index a2016888c2..f5fedc9d51 100644 --- a/compiler/typecheck/TcHsSyn.hs +++ b/compiler/typecheck/TcHsSyn.hs @@ -423,7 +423,7 @@ 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 zonkTyBndrX env tv - = ASSERT( isImmutableTyVar 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 diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 2194fa08fa..3706c236c6 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -53,7 +53,10 @@ module TcHsType ( zonkPromoteType, -- Pattern type signatures - tcHsPatSigType, tcPatSig, funAppCtxt + tcHsPatSigType, tcPatSig, + + -- Error messages + funAppCtxt, addTyConFlavCtxt ) where #include "HsVersions.h" @@ -1368,7 +1371,7 @@ as a degenerate case of some (pi (x :: t) -> s) and then this will all get more permissive. Note [Kind generalisation and TyVarTvs] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider data T (a :: k1) x = MkT (S a ()) data S (b :: k2) y = MkS (T b ()) @@ -1383,7 +1386,7 @@ in TcBinds. There are some wrinkles * We always want to kind-generalise over TyVarTvs, and /not/ default - them to Type. Another way to say this is: a SigTV should /never/ + them to Type. Another way to say this is: a TyVarTv should /never/ stand for a type, even via defaulting. Hence the check in TcSimplify.defaultTyVarTcS, and TcMType.defaultTyVar. Here's another example (Trac #14555): @@ -1396,12 +1399,22 @@ There are some wrinkles data SameKind :: k -> k -> * data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b) Here we will unify k1 with k2, but this time doing so is an error, - because k1 and k2 are bound in the same delcaration. + because k1 and k2 are bound in the same declaration. - We sort this out using findDupTyVarTvs, in TcTyClTyVars; very much + We sort this out using findDupTyVarTvs, in TcHsType.tcTyClTyVars; very much as we do with partial type signatures in mk_psig_qtvs in TcBinds.chooseInferredQuantifiers +* Even the Required arguments should be made into TyVarTvs, not skolems. + Consider + + data T k (a :: k) + + Here, k is a Required, dependent variable. For uniformity, it is helpful + to have k be a TyVarTv, in parallel with other dependent variables. + (This is key in the call to quantifyTyVars in kcTyClGroup, where quantifyTyVars + expects not to see unknown skolems.) + Note [Keeping scoped variables in order: Explicit] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When the user writes `forall a b c. blah`, we bring a, b, and c into @@ -1432,7 +1445,7 @@ signature), we need to come up with some ordering on these variables. This is done by bumping the TcLevel, bringing the tyvars into scope, and then type-checking the thing_inside. The constraints are all wrapped in an implication, which is then solved. Finally, we can -zonk all the binders and then order them with toposortTyVars. +zonk all the binders and then order them with scopedSort. It's critical to solve before zonking and ordering in order to uncover any unifications. You might worry that this eager solving could cause @@ -1468,8 +1481,9 @@ raise the TcLevel. To avoid these variables from ever being visible in the surrounding context, we must obey the following dictum: Every metavariable in a type must either be - (A) promoted, or - (B) generalized. + (A) promoted + (B) generalized, or + (C) zapped to Any If a variable is generalized, then it becomes a skolem and no longer has a proper TcLevel. (I'm ignoring the TcLevel on a skolem here, as @@ -1479,6 +1493,8 @@ sig -- or because the metavars are constrained -- see kindGeneralizeLocal) we need to promote to maintain (MetaTvInv) of Note [TcLevel and untouchable type variables] in TcType. +For more about (C), see Note [Naughty quantification candidates] in TcMType. + After promoting/generalizing, we need to zonk *again* because both promoting and generalizing fill in metavariables. @@ -1514,69 +1530,93 @@ tcWildCardBinders wc_names thing_inside kcLHsQTyVars :: Name -- ^ of the thing being checked -> TyConFlavour -- ^ What sort of 'TyCon' is being checked -> Bool -- ^ True <=> the decl being checked has a CUSK - -> [(Name, TyVar)] -- ^ If the thing being checked is associated - -- with a class, this is the class's scoped - -- type variables. Empty otherwise. -> LHsQTyVars GhcRn -> TcM Kind -- ^ The result kind -> TcM TcTyCon -- ^ A suitably-kinded TcTyCon -kcLHsQTyVars name flav cusk parent_tv_prs +kcLHsQTyVars name flav cusk user_tyvars@(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns , hsq_dependent = dep_names } , hsq_explicit = hs_tvs }) thing_inside | cusk - = do { (scoped_kvs, (tc_tvs, res_kind)) + -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls + = addTyConFlavCtxt name flav $ + do { (scoped_kvs, (tc_tvs, res_kind)) <- solveEqualities $ tcImplicitQTKBndrs skol_info kv_ns $ kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside - -- Now, because we're in a CUSK, quantify over the mentioned - -- kind vars, in dependency order. - ; let tc_binders_unzonked = zipWith mk_tc_binder hs_tvs tc_tvs - ; dvs <- zonkTcTypeAndSplitDepVars (mkSpecForAllTys scoped_kvs $ - mkTyConKind tc_binders_unzonked res_kind) - ; let -- Any type variables bound by the parent class that are specified - -- in this declaration (associated with the class). We single - -- these out because we want to bind these first in this - -- declaration's kind. - -- See Note [Kind variable ordering for associated types]. - reused_from_parent_tv_prs = - filter (\(_, tv) -> tv `elemDVarSet` dv_kvs dvs - || tv `elemDVarSet` dv_tvs dvs) parent_tv_prs - reused_from_parent_tvs = map snd reused_from_parent_tv_prs - ; qkvs <- quantifyTyVars (mkVarSet reused_from_parent_tvs) dvs - -- don't call tcGetGlobalTyCoVars. For associated types, it gets the - -- tyvars from the enclosing class -- but that's wrong. We *do* want - -- to quantify over those tyvars. - - ; scoped_kvs <- mapM zonkTcTyVarToTyVar scoped_kvs - ; tc_tvs <- mapM zonkTcTyVarToTyVar tc_tvs - ; res_kind <- zonkTcType res_kind - ; let tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs - - -- If any of the scoped_kvs aren't actually mentioned in a binder's + ; let class_tc_binders + | Just class_tc <- tyConFlavourAssoc_maybe flav + = tyConBinders class_tc -- class has a CUSK, so these are zonked + -- and fully settled + | otherwise + = [] + + class_tv_set = mkVarSet (binderVars class_tc_binders) + local_specified = filterOut (`elemVarSet` class_tv_set) scoped_kvs + -- NB: local_specified are guaranteed to be in a well-scoped + -- order because of tcImplicitQTKBndrs + + -- NB: candidateQTyVarsOfType is OK with unzonked input + ; candidates <- candidateQTyVarsOfType class_tv_set $ + mkSpecForAllTys local_specified $ + mkSpecForAllTys tc_tvs $ + res_kind + -- The type above is a bit wrong, in that we're using foralls for all + -- the tc_tvs, even those that aren't dependent. This is OK, though, + -- because we're building the type only to extract the variables to + -- quantify. We use mk_tc_binder below to get this right. + + ; local_inferred <- quantifyTyVars class_tv_set candidates + + ; local_specified <- mapM zonkTyCoVarKind local_specified + ; tc_tvs <- mapM zonkTyCoVarKind tc_tvs + ; res_kind <- zonkTcType res_kind + + ; let dep_tv_set = tyCoVarsOfTypes (res_kind : map tyVarKind tc_tvs) + local_tcbs = concat [ mkNamedTyConBinders Inferred local_inferred + , mkNamedTyConBinders Specified local_specified + , map (mkRequiredTyConBinder dep_tv_set) tc_tvs ] + + free_class_tv_set = tyCoVarsOfTypes (res_kind : map binderType local_tcbs) + `delVarSetList` map binderVar local_tcbs + + used_class_tcbs = filter ((`elemVarSet` free_class_tv_set) . binderVar) + class_tc_binders + + -- Suppose we have class C k where type F (x :: k). We can't have + -- k *required* in F, so it becomes Specified + to_invis_tcb tcb + | Required <- tyConBinderArgFlag tcb + = mkNamedTyConBinder Specified (binderVar tcb) + | otherwise + = tcb + + used_class_tcbs_invis = map to_invis_tcb used_class_tcbs + + all_tcbs = used_class_tcbs_invis ++ local_tcbs + + -- If the ordering from + -- Note [Required, Specified, and Inferred for types] in TcTyClsDecls + -- doesn't work, we catch it here, before an error cascade + ; checkValidTelescope all_tcbs (ppr user_tyvars) + + -- If any of the all_kvs aren't actually mentioned in a binder's -- kind (or the return kind), then we're in the CUSK case from -- Note [Free-floating kind vars] - ; let all_tc_tvs = scoped_kvs ++ tc_tvs - all_mentioned_tvs = mapUnionVarSet (tyCoVarsOfType . tyVarKind) - all_tc_tvs - `unionVarSet` tyCoVarsOfType res_kind - unmentioned_kvs = filterOut (`elemVarSet` all_mentioned_tvs) - scoped_kvs - ; reportFloatingKvs name flav all_tc_tvs unmentioned_kvs - - ; let all_scoped_kvs = reused_from_parent_tvs ++ scoped_kvs - final_binders = map (mkNamedTyConBinder Inferred) qkvs - ++ map (mkNamedTyConBinder Specified) all_scoped_kvs - ++ tc_binders - all_tv_prs = reused_from_parent_tv_prs ++ - mkTyVarNamePairs (scoped_kvs ++ tc_tvs) - tycon = mkTcTyCon name (ppr user_tyvars) final_binders res_kind - all_tv_prs flav - -- the tvs contain the binders already - -- in scope from an enclosing class, but - -- re-adding tvs to the env't doesn't cause - -- harm + ; let all_kvs = concat [ map binderVar used_class_tcbs_invis + , local_inferred + , local_specified ] + + all_mentioned_tvs = dep_tv_set `unionVarSet` + tyCoVarsOfTypes (map tyVarKind all_kvs) + + unmentioned_kvs = filterOut (`elemVarSet` all_mentioned_tvs) all_kvs + ; reportFloatingKvs name flav (map binderVar all_tcbs) unmentioned_kvs + + ; let all_tv_prs = mkTyVarNamePairs (scoped_kvs ++ tc_tvs) + tycon = mkTcTyCon name (ppr user_tyvars) all_tcbs res_kind + all_tv_prs True {- it is generalised -} flav ; traceTc "kcLHsQTyVars: cusk" $ vcat [ text "name" <+> ppr name @@ -1584,17 +1624,11 @@ kcLHsQTyVars name flav cusk parent_tv_prs , text "hs_tvs" <+> ppr hs_tvs , text "dep_names" <+> ppr dep_names , text "scoped_kvs" <+> ppr scoped_kvs - , text "reused_from_parent_tv_prs" - <+> ppr reused_from_parent_tv_prs , text "tc_tvs" <+> ppr tc_tvs , text "res_kind" <+> ppr res_kind - , text "dvs" <+> ppr dvs - , text "qkvs" <+> ppr qkvs - , text "all_scoped_kvs" <+> ppr all_scoped_kvs - , text "tc_binders" <+> ppr tc_binders - , text "final_binders" <+> ppr final_binders - , text "mkTyConKind final_binders res_kind" - <+> ppr (mkTyConKind final_binders res_kind) + , text "all_tcbs" <+> ppr all_tcbs + , text "mkTyConKind all_tcbs res_kind" + <+> ppr (mkTyConKind all_tcbs res_kind) , text "all_tv_prs" <+> ppr all_tv_prs ] ; return tycon } @@ -1607,10 +1641,15 @@ kcLHsQTyVars name flav cusk parent_tv_prs kcLHsQTyVarBndrs cusk open_fam skol_info hs_tvs thing_inside ; let -- NB: Don't add scoped_kvs to tyConTyVars, because they - -- must remain lined up with the binders + -- might unify with kind vars in other types in a mutually + -- recursive group. See Note [Kind generalisation and TyVarTvs] tc_binders = zipWith mk_tc_binder hs_tvs tc_tvs + -- Also, note that tc_binders has the tyvars from only the + -- user-written tyvarbinders. See S1 in Note [How TcTyCons work] + -- in TcTyClsDecls tycon = mkTcTyCon name (ppr user_tyvars) tc_binders res_kind (mkTyVarNamePairs (scoped_kvs ++ tc_tvs)) + False -- not yet generalised flav ; traceTc "kcLHsQTyVars: not-cusk" $ @@ -1629,7 +1668,7 @@ kcLHsQTyVars name flav cusk parent_tv_prs | otherwise = mkAnonTyConBinder tv -kcLHsQTyVars _ _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars" +kcLHsQTyVars _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars" kcLHsQTyVarBndrs :: Bool -- True <=> bump the TcLevel when bringing vars into scope -> Bool -- True <=> Default un-annotated tyvar @@ -1679,7 +1718,7 @@ kcLHsQTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing -- Open type/data families default their variables -- variables to kind *. But don't default in-scope -- class tyvars, of course - ; tv <- newSkolemTyVar name kind + ; tv <- new_tv name kind ; return (tv, False) } } kc_hs_tv (KindedTyVar _ lname@(L _ name) lhs_kind) @@ -1691,11 +1730,18 @@ kcLHsQTyVarBndrs cusk open_fam skol_info (L _ hs_tv : hs_tvs) thing unifyKind (Just (HsTyVar noExt NotPromoted lname)) kind (tyVarKind tv) ; return (tv, True) } - _ -> do { tv <- newSkolemTyVar name kind + _ -> do { tv <- new_tv name kind ; return (tv, False) } } kc_hs_tv (XTyVarBndr{}) = panic "kc_hs_tv" + + new_tv :: Name -> Kind -> TcM TcTyVar + new_tv + | cusk = newSkolemTyVar + | otherwise = newTyVarTyVar + -- Third wrinkle in Note [Kind generalisation and TyVarTvs] + {- Note [Kind-checking tyvar binders for associated types] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When kind-checking the type-variable binders for associated @@ -1762,10 +1808,13 @@ kcImplicitTKBndrs :: [Name] -- of the vars -> TcM ([TcTyVar], a) -- returns the tyvars created -- these are *not* dependency ordered kcImplicitTKBndrs var_ns thing_inside - = do { tkvs <- mapM newFlexiKindedTyVarTyVar var_ns - ; result <- tcExtendTyVarEnv tkvs thing_inside - ; return (tkvs, result) } - + -- NB: Just use tyvars that are in scope, if any. Otherwise, we + -- get #15711, where GHC forgets that a variable used in an associated + -- type is the same as the one used in the enclosing class + = do { tkvs_pairs <- mapM (newFlexiKindedQTyVar newTyVarTyVar) var_ns + ; let tkvs_to_scope = [ tkv | (tkv, True) <- tkvs_pairs ] + ; result <- tcExtendTyVarEnv tkvs_to_scope thing_inside + ; return (map fst tkvs_pairs, result) } tcImplicitTKBndrs, tcImplicitTKBndrsSig, tcImplicitQTKBndrs :: SkolemInfo @@ -1774,7 +1823,8 @@ tcImplicitTKBndrs, tcImplicitTKBndrsSig, tcImplicitQTKBndrs -> TcM ([TcTyVar], a) tcImplicitTKBndrs = tcImplicitTKBndrsX newFlexiKindedSkolemTyVar tcImplicitTKBndrsSig = tcImplicitTKBndrsX newFlexiKindedTyVarTyVar -tcImplicitQTKBndrs = tcImplicitTKBndrsX newFlexiKindedQTyVar +tcImplicitQTKBndrs = tcImplicitTKBndrsX + (\nm -> fst <$> newFlexiKindedQTyVar newSkolemTyVar nm) tcImplicitTKBndrsX :: (Name -> TcM TcTyVar) -- new_tv function -> SkolemInfo @@ -1809,19 +1859,20 @@ tcImplicitTKBndrsX new_tv skol_info tv_names thing_inside -- do a stable topological sort, following -- Note [Ordering of implicit variables] in RnTypes - ; let final_tvs = toposortTyVars skol_tvs + ; let final_tvs = scopedSort skol_tvs ; traceTc "tcImplicitTKBndrs" (ppr tv_names $$ ppr final_tvs) ; return (final_tvs, result) } -newFlexiKindedQTyVar :: Name -> TcM TcTyVar --- Make a new skolem for an implicit binder in a type/class/type +newFlexiKindedQTyVar :: (Name -> Kind -> TcM TyVar) -> Name -> TcM (TcTyVar, Bool) +-- Make a new tyvar for an implicit binder in a type/class/type -- instance declaration, with a flexi-kind -- But check for in-scope-ness, and if so return that instead -newFlexiKindedQTyVar name +-- Returns True as second return value iff this created a real new tyvar +newFlexiKindedQTyVar mk_tv name = do { mb_tv <- tcLookupLcl_maybe name ; case mb_tv of - Just (ATyVar _ tv) -> return tv - _ -> newFlexiKindedSkolemTyVar name } + Just (ATyVar _ tv) -> return (tv, False) + _ -> (, True) <$> newFlexiKindedTyVar mk_tv name } newFlexiKindedTyVar :: (Name -> Kind -> TcM TyVar) -> Name -> TcM TyVar newFlexiKindedTyVar new_tv name @@ -1981,17 +2032,21 @@ kindGeneralizeLocal wanted kind_or_type ; constrained <- zonkTyCoVarsAndFV (tyCoVarsOfWC wanted) ; (_, constrained) <- promoteTyVarSet constrained - -- NB: zonk here, after promotion - ; kvs <- zonkTcTypeAndFV kind_or_type - ; let dvs = DV { dv_kvs = kvs, dv_tvs = emptyDVarSet } - ; gbl_tvs <- tcGetGlobalTyCoVars -- Already zonked + ; let mono_tvs = gbl_tvs `unionVarSet` constrained + + -- use the "Kind" variant here, as any types we see + -- here will already have all type variables quantified; + -- thus, every free variable is really a kv, never a tv. + ; dvs <- candidateQTyVarsOfKind mono_tvs kind_or_type + ; traceTc "kindGeneralizeLocal" (vcat [ ppr wanted , ppr kind_or_type , ppr constrained + , ppr mono_tvs , ppr dvs ]) - ; quantifyTyVars (gbl_tvs `unionVarSet` constrained) dvs } + ; quantifyTyVars mono_tvs dvs } {- Note [Kind generalisation] @@ -2819,3 +2874,9 @@ failIfEmitsConstraints thing_inside ; reportAllUnsolved lie ; return res } + +-- | Add a "In the data declaration for T" or some such. +addTyConFlavCtxt :: Name -> TyConFlavour -> TcM a -> TcM a +addTyConFlavCtxt name flav + = addErrCtxt $ hsep [ text "In the", ppr flav + , text "declaration for", quotes (ppr name) ] diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs index c9d9dd0ab6..ba2fd7588e 100644 --- a/compiler/typecheck/TcInstDcls.hs +++ b/compiler/typecheck/TcInstDcls.hs @@ -648,7 +648,7 @@ tcDataFamInstDecl mb_clsinfo ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) -> do { let ty_binders = full_tcbs `chkAppend` extra_tcbs ; data_cons <- tcConDecls rec_rep_tc - (ty_binders, orig_res_ty) cons + ty_binders orig_res_ty cons ; tc_rhs <- case new_or_data of DataType -> return (mkDataTyConRhs data_cons) NewType -> ASSERT( not (null data_cons) ) diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index fb5f1b515a..c3786e20bf 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -25,7 +25,7 @@ module TcMType ( newFmvTyVar, newFskTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, - newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar, + newMetaDetails, isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar, -------------------------------- -- Expected types @@ -67,10 +67,11 @@ module TcMType ( zonkTcTyVarToTyVar, zonkTyVarTyVarPairs, zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkTyCoVarsAndFVList, - zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars, + candidateQTyVarsOfType, candidateQTyVarsOfKind, + candidateQTyVarsOfTypes, CandidatesQTvs(..), zonkQuantifiedTyVar, defaultTyVar, quantifyTyVars, - zonkTcTyCoVarBndr, zonkTcTyVarBinder, + zonkTcTyCoVarBndr, zonkTyConBinders, zonkTcType, zonkTcTypes, zonkCo, zonkTyCoVarKind, @@ -93,6 +94,7 @@ import GhcPrelude import TyCoRep import TcType import Type +import TyCon import Coercion import Class import Var @@ -119,8 +121,9 @@ import qualified GHC.LanguageExtensions as LangExt import Control.Monad import Maybes -import Data.List ( mapAccumL ) +import Data.List ( mapAccumL, partition ) import Control.Arrow ( second ) +import qualified Data.Semigroup as Semi {- ************************************************************************ @@ -703,16 +706,23 @@ readMetaTyVar :: TyVar -> TcM MetaDetails readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) readMutVar (metaTyVarRef tyvar) +isFilledMetaTyVar_maybe :: TcTyVar -> TcM (Maybe Type) +isFilledMetaTyVar_maybe tv + | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv + = do { cts <- readTcRef ref + ; case cts of + Indirect ty -> return (Just ty) + Flexi -> return Nothing } + | otherwise + = return Nothing + isFilledMetaTyVar :: TyVar -> TcM Bool -- True of a filled-in (Indirect) meta type variable -isFilledMetaTyVar tv - | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv - = do { details <- readMutVar ref - ; return (isIndirect details) } - | otherwise = return False +isFilledMetaTyVar tv = isJust <$> isFilledMetaTyVar_maybe tv isUnfilledMetaTyVar :: TyVar -> TcM Bool -- True of a un-filled-in (Flexi) meta type variable +-- NB: Not the opposite of isFilledMetaTyVar isUnfilledMetaTyVar tv | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv = do { details <- readMutVar ref @@ -794,7 +804,6 @@ writeMetaTyVarRef tyvar ref ty double_upd_msg details = hang (text "Double update of meta tyvar") 2 (ppr tyvar $$ ppr details) - {- Note [Level check when unifying] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When unifying @@ -961,6 +970,291 @@ newMetaTyVarTyAtLevel tc_lvl kind {- ********************************************************************* * * + Finding variables to quantify over +* * +********************************************************************* -} + +data CandidatesQTvs -- See Note [Dependent type variables] + -- See Note [CandidatesQTvs determinism and order] + -- NB: All variables stored here are MetaTvs. No exceptions. + = DV { dv_kvs :: DTyVarSet -- "kind" metavariables (dependent) + , dv_tvs :: DTyVarSet -- "type" metavariables (non-dependent) + -- A variable may appear in both sets + -- E.g. T k (x::k) The first occurrence of k makes it + -- show up in dv_tvs, the second in dv_kvs + -- See Note [Dependent type variables] + , dv_cvs :: CoVarSet + -- These are covars. We will *not* quantify over these, but + -- we must make sure also not to quantify over any cv's kinds, + -- so we include them here as further direction for quantifyTyVars + } + +instance Semi.Semigroup CandidatesQTvs where + (DV { dv_kvs = kv1, dv_tvs = tv1, dv_cvs = cv1 }) + <> (DV { dv_kvs = kv2, dv_tvs = tv2, dv_cvs = cv2 }) + = DV { dv_kvs = kv1 `unionDVarSet` kv2 + , dv_tvs = tv1 `unionDVarSet` tv2 + , dv_cvs = cv1 `unionVarSet` cv2 } + +instance Monoid CandidatesQTvs where + mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet, dv_cvs = emptyVarSet } + mappend = (Semi.<>) + +instance Outputable CandidatesQTvs where + ppr (DV {dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) + = text "DV" <+> braces (pprWithCommas id [ text "dv_kvs =" <+> ppr kvs + , text "dv_tvs =" <+> ppr tvs + , text "dv_cvs =" <+> ppr cvs ]) + +closeOverKindsCQTvs :: TyCoVarSet -- globals + -> CandidatesQTvs -> TcM CandidatesQTvs +-- Don't close the covars; this is done in quantifyTyVars. Note that +-- closing over the CoVars would introduce tyvars into the CoVarSet. +closeOverKindsCQTvs gbl_tvs dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) + = do { let all_kinds = map tyVarKind (dVarSetElems (kvs `unionDVarSet` tvs)) + ; foldlM (collect_cand_qtvs True gbl_tvs) dv all_kinds } + +{- Note [Dependent type variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In Haskell type inference we quantify over type variables; but we only +quantify over /kind/ variables when -XPolyKinds is on. Without -XPolyKinds +we default the kind variables to *. + +So, to support this defaulting, and only for that reason, when +collecting the free vars of a type, prior to quantifying, we must keep +the type and kind variables separate. + +But what does that mean in a system where kind variables /are/ type +variables? It's a fairly arbitrary distinction based on how the +variables appear: + + - "Kind variables" appear in the kind of some other free variable + + These are the ones we default to * if -XPolyKinds is off + + - "Type variables" are all free vars that are not kind variables + +E.g. In the type T k (a::k) + 'k' is a kind variable, because it occurs in the kind of 'a', + even though it also appears at "top level" of the type + 'a' is a type variable, because it doesn't + +We gather these variables using a CandidatesQTvs record: + DV { dv_kvs: Variables free in the kind of a free type variable + or of a forall-bound type variable + , dv_tvs: Variables sytactically free in the type } + +So: dv_kvs are the kind variables of the type + (dv_tvs - dv_kvs) are the type variable of the type + +Note that + +* A variable can occur in both. + T k (x::k) The first occurrence of k makes it + show up in dv_tvs, the second in dv_kvs + +* We include any coercion variables in the "dependent", + "kind-variable" set because we never quantify over them. + +* The "kind variables" might depend on each other; e.g + (k1 :: k2), (k2 :: *) + The "type variables" do not depend on each other; if + one did, it'd be classified as a kind variable! + +Note [CandidatesQTvs determinism and order] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +* Determinism: when we quantify over type variables we decide the + order in which they appear in the final type. Because the order of + type variables in the type can end up in the interface file and + affects some optimizations like worker-wrapper, we want this order to + be deterministic. + + To achieve that we use deterministic sets of variables that can be + converted to lists in a deterministic order. For more information + about deterministic sets see Note [Deterministic UniqFM] in UniqDFM. + +* Order: as well as being deterministic, we use an + accumulating-parameter style for candidateQTyVarsOfType so that we + add variables one at a time, left to right. That means we tend to + produce the variables in left-to-right order. This is just to make + it bit more predicatable for the programmer. + +Note [Naughty quantification candidates] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider (#14880, dependent/should_compile/T14880-2) + + forall arg. ... (alpha[tau]:arg) ... + +We have a metavariable alpha whose kind is a locally bound (skolem) variable. +This can arise while type-checking a user-written type signature +(see the test case for the full code). According to +Note [Recipe for checking a signature] in TcHsType, we try to solve +all constraints that arise during checking before looking to kind-generalize. +However, in the case above, this solving pass does not unify alpha, because +it is utterly unconstrained. The question is: what to do with alpha? + +We can't generalize it, because it would have to be generalized *after* +arg, and implicit generalization always goes before explicit generalization. +We can't simply leave it be, because this type is about to go into the +typing environment (as the type of some let-bound variable, say), and then +chaos erupts when we try to instantiate. In any case, we'll never learn +anything more about alpha anyway. + +So, we zap it, eagerly, to Any. We don't have to do this eager zapping +in terms (say, in `length []`) because terms are never re-examined before +the final zonk (which zaps any lingering metavariables to Any). + +The right time to do this eager zapping is during generalization, when +every metavariable is either (A) promoted, (B) generalized, or (C) zapped +(according again to Note [Recipe for checking a signature] in TcHsType). + +Accordingly, when quantifyTyVars is skolemizing the variables to quantify, +these naughty ones are zapped to Any. We identify the naughty ones by +looking for out-of-scope tyvars in the candidate tyvars' kinds, where +we assume that all in-scope tyvars are in the gbl_tvs passed to quantifyTyVars. +In the example above, we would have `alpha` in the CandidatesQTvs, but +`arg` wouldn't be in the gbl_tvs. Hence, alpha is naughty, and zapped to +Any. Naughty variables are discovered by is_naughty_tv in quantifyTyVars. + +-} + +-- | Gathers free variables to use as quantification candidates (in +-- 'quantifyTyVars'). This might output the same var +-- in both sets, if it's used in both a type and a kind. +-- See Note [CandidatesQTvs determinism and order] +-- See Note [Dependent type variables] +candidateQTyVarsOfType :: TcTyVarSet -- zonked set of global/mono tyvars + -> TcType -- not necessarily zonked + -> TcM CandidatesQTvs +candidateQTyVarsOfType gbl_tvs ty = closeOverKindsCQTvs gbl_tvs =<< + collect_cand_qtvs False gbl_tvs mempty ty + +-- | Like 'candidateQTyVarsOfType', but consider every free variable +-- to be dependent. This is appropriate when generalizing a *kind*, +-- instead of a type. (That way, -XNoPolyKinds will default the variables +-- to Type.) +candidateQTyVarsOfKind :: TcTyVarSet -- zonked set of global/mono tyvars + -> TcKind -- not necessarily zonked + -> TcM CandidatesQTvs +candidateQTyVarsOfKind gbl_tvs ty = closeOverKindsCQTvs gbl_tvs =<< + collect_cand_qtvs True gbl_tvs mempty ty + +collect_cand_qtvs :: Bool -- True <=> consider every fv in Type to be dependent + -> VarSet -- bound variables (both locally bound and globally bound) + -> CandidatesQTvs -> Type -> TcM CandidatesQTvs +collect_cand_qtvs is_dep bound dvs ty + = go dvs ty + where + go dv (AppTy t1 t2) = foldlM go dv [t1, t2] + go dv (TyConApp _ tys) = foldlM go dv tys + go dv (FunTy arg res) = foldlM go dv [arg, res] + go dv (LitTy {}) = return dv + go dv (CastTy ty co) = do dv1 <- go dv ty + collect_cand_qtvs_co bound dv1 co + go dv (CoercionTy co) = collect_cand_qtvs_co bound dv co + + go dv (TyVarTy tv) + | is_bound tv + = return dv + + | isImmutableTyVar tv + = WARN(True, (sep [ text "Note [Naughty quantification candidates] skolem:" + , ppr tv <+> dcolon <+> ppr (tyVarKind tv) ])) + return dv -- This happens when processing kinds of variables affected by + -- Note [Naughty quantification candidates] + -- NB: CandidatesQTvs stores only MetaTvs, so don't store an + -- immutable tyvar here. + + | otherwise + = ASSERT2( isMetaTyVar tv, ppr tv <+> dcolon <+> ppr (tyVarKind tv) $$ ppr ty $$ ppr bound ) + do { m_contents <- isFilledMetaTyVar_maybe tv + ; case m_contents of + Just ind_ty -> go dv ind_ty + + Nothing -> return $ insert_tv dv tv } + + go dv (ForAllTy (Bndr tv _) ty) + = do { dv1 <- collect_cand_qtvs True bound dv (tyVarKind tv) + ; collect_cand_qtvs is_dep (bound `extendVarSet` tv) dv1 ty } + + is_bound tv = tv `elemVarSet` bound + + insert_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv + | is_dep = dv { dv_kvs = kvs `extendDVarSet` tv } + | otherwise = dv { dv_tvs = tvs `extendDVarSet` tv } + -- You might be tempted (like I was) to use unitDVarSet and mappend here. + -- However, the union algorithm for deterministic sets depends on (roughly) + -- the size of the sets. The elements from the smaller set end up to the + -- right of the elements from the larger one. When sets are equal, the + -- left-hand argument to `mappend` goes to the right of the right-hand + -- argument. In our case, if we use unitDVarSet and mappend, we learn that + -- the free variables of (a -> b -> c -> d) are [b, a, c, d], and we then + -- quantify over them in that order. (The a comes after the b because we + -- union the singleton sets as ({a} `mappend` {b}), producing {b, a}. Thereafter, + -- the size criterion works to our advantage.) This is just annoying to + -- users, so I use `extendDVarSet`, which unambiguously puts the new element + -- to the right. Note that the unitDVarSet/mappend implementation would not + -- be wrong against any specification -- just suboptimal and confounding to users. + +collect_cand_qtvs_co :: VarSet -- bound variables + -> CandidatesQTvs -> Coercion -> TcM CandidatesQTvs +collect_cand_qtvs_co bound = go_co + where + go_co dv (Refl ty) = collect_cand_qtvs True bound dv ty + go_co dv (GRefl _ ty mco) = do dv1 <- collect_cand_qtvs True bound dv ty + go_mco dv1 mco + go_co dv (TyConAppCo _ _ cos) = foldlM go_co dv cos + go_co dv (AppCo co1 co2) = foldlM go_co dv [co1, co2] + go_co dv (FunCo _ co1 co2) = foldlM go_co dv [co1, co2] + go_co dv (AxiomInstCo _ _ cos) = foldlM go_co dv cos + go_co dv (AxiomRuleCo _ cos) = foldlM go_co dv cos + go_co dv (UnivCo prov _ t1 t2) = do dv1 <- go_prov dv prov + dv2 <- collect_cand_qtvs True bound dv1 t1 + collect_cand_qtvs True bound dv2 t2 + go_co dv (SymCo co) = go_co dv co + go_co dv (TransCo co1 co2) = foldlM go_co dv [co1, co2] + go_co dv (NthCo _ _ co) = go_co dv co + go_co dv (LRCo _ co) = go_co dv co + go_co dv (InstCo co1 co2) = foldlM go_co dv [co1, co2] + go_co dv (KindCo co) = go_co dv co + go_co dv (SubCo co) = go_co dv co + + go_co dv (HoleCo hole) = do m_co <- unpackCoercionHole_maybe hole + case m_co of + Just co -> go_co dv co + Nothing -> return $ insert_cv dv (coHoleCoVar hole) + + go_co dv (CoVarCo cv) + | is_bound cv + = return dv + | otherwise + = return $ insert_cv dv cv + + go_co dv (ForAllCo tcv kind_co co) + = do { dv1 <- go_co dv kind_co + ; collect_cand_qtvs_co (bound `extendVarSet` tcv) dv1 co } + + go_mco dv MRefl = return dv + go_mco dv (MCo co) = go_co dv co + + go_prov dv UnsafeCoerceProv = return dv + go_prov dv (PhantomProv co) = go_co dv co + go_prov dv (ProofIrrelProv co) = go_co dv co + go_prov dv (PluginProv _) = return dv + + insert_cv dv@(DV { dv_cvs = cvs }) cv + = dv { dv_cvs = cvs `extendVarSet` cv } + + is_bound tv = tv `elemVarSet` bound + +-- | Like 'splitDepVarsOfType', but over a list of types +candidateQTyVarsOfTypes :: TyCoVarSet -- zonked global ty/covars + -> [Type] -> TcM CandidatesQTvs +candidateQTyVarsOfTypes gbl_tvs tys = closeOverKindsCQTvs gbl_tvs =<< + foldlM (collect_cand_qtvs False gbl_tvs) mempty tys + +{- ********************************************************************* +* * Quantification * * ************************************************************************ @@ -988,7 +1282,7 @@ has free vars {f,a}, but we must add 'k' as well! Hence step (2). With -XPolyKinds, it treats both classes of variables identically. * quantifyTyVars never quantifies over - - a coercion variable + - a coercion variable (or any tv mentioned in the kind of a covar) - a runtime-rep variable Note [quantifyTyVars determinism] @@ -1007,52 +1301,61 @@ Note [Deterministic UniqFM] in UniqDFM. quantifyTyVars :: TcTyCoVarSet -- Global tvs; already zonked - -> CandidatesQTvs -- See Note [Dependent type variables] in TcType + -> CandidatesQTvs -- See Note [Dependent type variables] -- Already zonked -> TcM [TcTyVar] -- See Note [quantifyTyVars] -- Can be given a mixture of TcTyVars and TyVars, in the case of -- associated type declarations. Also accepts covars, but *never* returns any. - -quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) - = do { traceTc "quantifyTyVars" (vcat [ppr dvs, ppr gbl_tvs]) - ; let dep_kvs = dVarSetElemsWellScoped $ - dep_tkvs `dVarSetMinusVarSet` gbl_tvs +quantifyTyVars gbl_tvs + dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs, dv_cvs = covars }) + = do { traceTc "quantifyTyVars 1" (vcat [ppr dvs, ppr gbl_tvs]) + ; let mono_tvs = gbl_tvs `unionVarSet` closeOverKinds covars + -- NB: All variables in the kind of a covar must not be + -- quantified over, as we don't quantify over the covar. + + dep_kvs = dVarSetElemsWellScoped $ + dep_tkvs `dVarSetMinusVarSet` mono_tvs -- dVarSetElemsWellScoped: put the kind variables into -- well-scoped order. -- E.g. [k, (a::k)] not the other way roud nondep_tvs = dVarSetElems $ (nondep_tkvs `minusDVarSet` dep_tkvs) - `dVarSetMinusVarSet` gbl_tvs - -- See Note [Dependent type variables] in TcType + `dVarSetMinusVarSet` mono_tvs + -- See Note [Dependent type variables] -- The `minus` dep_tkvs removes any kind-level vars -- e.g. T k (a::k) Since k appear in a kind it'll -- be in dv_kvs, and is dependent. So remove it from -- dv_tvs which will also contain k -- No worry about dependent covars here; -- they are all in dep_tkvs - -- No worry about scoping, because these are all - -- type variables -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV + -- See Note [Naughty quantification candidates] + (naughty_deps, final_dep_kvs) = partition (is_naughty_tv mono_tvs) dep_kvs + (naughty_nondeps, final_nondep_tvs) = partition (is_naughty_tv mono_tvs) nondep_tvs + + ; mapM_ zap_naughty_tv (naughty_deps ++ naughty_nondeps) + -- In the non-PolyKinds case, default the kind variables -- to *, and zonk the tyvars as usual. Notice that this -- may make quantifyTyVars return a shorter list -- than it was passed, but that's ok ; poly_kinds <- xoptM LangExt.PolyKinds - ; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs - ; nondep_tvs' <- mapMaybeM (zonk_quant False) nondep_tvs + ; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) final_dep_kvs + ; nondep_tvs' <- mapMaybeM (zonk_quant False) final_nondep_tvs ; let final_qtvs = dep_kvs' ++ nondep_tvs' -- Because of the order, any kind variables -- mentioned in the kinds of the nondep_tvs' -- now refer to the dep_kvs' - ; traceTc "quantifyTyVars" - (vcat [ text "globals:" <+> ppr gbl_tvs - , text "nondep:" <+> pprTyVars nondep_tvs - , text "dep:" <+> pprTyVars dep_kvs - , text "dep_kvs'" <+> pprTyVars dep_kvs' + ; traceTc "quantifyTyVars 2" + (vcat [ text "globals:" <+> ppr gbl_tvs + , text "mono_tvs:" <+> ppr mono_tvs + , text "nondep:" <+> pprTyVars nondep_tvs + , text "dep:" <+> pprTyVars dep_kvs + , text "dep_kvs'" <+> pprTyVars dep_kvs' , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ]) -- We should never quantify over coercion variables; check this @@ -1061,6 +1364,11 @@ quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) ; return final_qtvs } where + -- See Note [Naughty quantification candidates] + is_naughty_tv mono_tvs tv + = anyVarSet (isSkolemTyVar <&&> (not . (`elemVarSet` mono_tvs))) $ + tyCoVarsOfType (tyVarKind tv) + -- zonk_quant returns a tyvar if it should be quantified over; -- otherwise, it returns Nothing. The latter case happens for -- * Kind variables, with -XNoPolyKinds: don't quantify over these @@ -1080,6 +1388,10 @@ quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) False -> do { tv <- zonkQuantifiedTyVar tkv ; return (Just tv) } } + zap_naughty_tv tv + = WARN(True, text "naughty quantification candidate: " <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)) + writeMetaTyVar tv (anyTypeOfKind (tyVarKind tv)) + zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- The quantified type variables often include meta type variables -- we want to freeze them into ordinary type variables @@ -1162,7 +1474,7 @@ skolemiseUnboundMetaTyVar tv ; kind <- zonkTcType (tyVarKind tv) ; let uniq = getUnique tv -- NB: Use same Unique as original tyvar. This is - -- important for TcHsType.splitTelescopeTvs to work properly + -- convenient in reading dumps, but is otherwise inessential. tv_name = getOccName tv final_name = mkInternalName uniq tv_name span @@ -1352,15 +1664,6 @@ zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet zonkTcTypeAndFV ty = tyCoVarsOfTypeDSet <$> zonkTcType ty --- | Zonk a type and call 'candidateQTyVarsOfType' on it. -zonkTcTypeAndSplitDepVars :: TcType -> TcM CandidatesQTvs -zonkTcTypeAndSplitDepVars ty - = candidateQTyVarsOfType <$> zonkTcType ty - -zonkTcTypesAndSplitDepVars :: [TcType] -> TcM CandidatesQTvs -zonkTcTypesAndSplitDepVars tys - = candidateQTyVarsOfTypes <$> mapM zonkTcType tys - zonkTyCoVar :: TyCoVar -> TcM TcType -- Works on TyVars and TcTyVars zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv @@ -1409,8 +1712,8 @@ zonkImplication implic@(Implic { ic_skols = skols , ic_given = given , ic_wanted = wanted , ic_info = info }) - = do { skols' <- mapM zonkTcTyCoVarBndr skols -- Need to zonk their kinds! - -- as Trac #7230 showed + = do { skols' <- mapM zonkTyCoVarKind skols -- Need to zonk their kinds! + -- as Trac #7230 showed ; given' <- mapM zonkEvVar given ; info' <- zonkSkolemInfo info ; wanted' <- zonkWCRec wanted @@ -1552,7 +1855,7 @@ zonkTcTypeMapper = TyCoMapper , tcm_tyvar = const zonkTcTyVar , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv) , tcm_hole = hole - , tcm_tycobinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv + , tcm_tycobinder = \_env tv _vis -> ((), ) <$> zonkTyCoVarKind tv , tcm_tycon = return } where hole :: () -> CoercionHole -> TcM Coercion @@ -1583,17 +1886,25 @@ zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar -- unification variables. zonkTcTyCoVarBndr tyvar | isTyVarTyVar tyvar - = tcGetTyVar "zonkTcTyCoVarBndr TyVarTv" <$> zonkTcTyVar tyvar + -- We want to preserve the binding location of the original TyVarTv. + -- This is important for error messages. If we don't do this, then + -- we get bad locations in, e.g., typecheck/should_fail/T2688 + = do { zonked_ty <- zonkTcTyVar tyvar + ; let zonked_tyvar = tcGetTyVar "zonkTcTyCoVarBndr TyVarTv" zonked_ty + zonked_name = getName zonked_tyvar + reloc'd_name = setNameLoc zonked_name (getSrcSpan tyvar) + ; return (setTyVarName zonked_tyvar reloc'd_name) } | otherwise - -- can't use isCoVar, because it looks at a TyCon. Argh. - = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), pprTyVar tyvar ) - updateTyVarKindM zonkTcType tyvar - -zonkTcTyVarBinder :: VarBndr TcTyVar vis -> TcM (VarBndr TcTyVar vis) -zonkTcTyVarBinder (Bndr tv vis) - = do { tv' <- zonkTcTyCoVarBndr tv - ; return (Bndr tv' vis) } + = ASSERT2( isImmutableTyVar tyvar || isCoVar tyvar, pprTyVar tyvar ) + zonkTyCoVarKind tyvar + +zonkTyConBinders :: [TyConBinder] -> TcM [TyConBinder] +zonkTyConBinders = mapM zonk1 + where + zonk1 (Bndr tv vis) + = do { tv' <- zonkTcTyCoVarBndr tv + ; return (Bndr tv' vis) } zonkTcTyVar :: TcTyVar -> TcM TcType -- Simply look through all Flexis diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index e86ff3c34b..4a770b563d 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -164,13 +164,6 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details (prov_theta, prov_evs) = unzip (mapMaybe mkProvEvidence filtered_prov_dicts) - -- Report bad universal type variables - -- See Note [Type variables whose kind is captured] - ; let bad_tvs = [ tv | tv <- univ_tvs - , tyCoVarsOfType (tyVarKind tv) - `intersectsVarSet` ex_tv_set ] - ; mapM_ (badUnivTvErr ex_tvs) bad_tvs - -- Report coercions that esacpe -- See Note [Coercions that escape] ; args <- mapM zonkId args @@ -217,20 +210,6 @@ mkProvEvidence ev_id pred = evVarPred ev_id eq_con_args = [evId ev_id] -badUnivTvErr :: [TyVar] -> TyVar -> TcM () --- See Note [Type variables whose kind is captured] -badUnivTvErr ex_tvs bad_tv - = addErrTc $ - vcat [ text "Universal type variable" <+> quotes (ppr bad_tv) - <+> text "has existentially bound kind:" - , nest 2 (ppr_with_kind bad_tv) - , hang (text "Existentially-bound variables:") - 2 (vcat (map ppr_with_kind ex_tvs)) - , text "Probable fix: give the pattern synonym a type signature" - ] - where - ppr_with_kind tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv) - dependentArgErr :: (Id, DTyCoVarSet) -> TcM () -- See Note [Coercions that escape] dependentArgErr (arg, bad_cos) @@ -293,37 +272,6 @@ marginally less efficient, if the builder/martcher are not inlined. See also Note [Lift equality constaints when quantifying] in TcType -Note [Type variables whose kind is captured] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - data AST a = Sym [a] - class Prj s where { prj :: [a] -> Maybe (s a) - pattern P x <= Sym (prj -> Just x) - -Here we get a matcher with this type - $mP :: forall s a. Prj s => AST a -> (s a -> r) -> r -> r - -No problem. But note that 's' is not fixed by the type of the -pattern (AST a), nor is it existentially bound. It's really only -fixed by the type of the continuation. - -Trac #14552 showed that this can go wrong if the kind of 's' mentions -existentially bound variables. We obviously can't make a type like - $mP :: forall (s::k->*) a. Prj s => AST a -> (forall k. s a -> r) - -> r -> r -But neither is 's' itself existentially bound, so the forall (s::k->*) -can't go in the inner forall either. (What would the matcher apply -the continuation to?) - -So we just fail in this case, with a pretty terrible error message. -Maybe we could do better, but I can't see how. (It'd be possible to -default 's' to (Any k), but that probably isn't what the user wanted, -and it not straightforward to implement, because by the time we see -the problem, simplifyInfer has already skolemised 's'.) - -This stuff can only happen in the presence of view patterns, with -PolyKinds, so it's a bit of a corner case. - Note [Coercions that escape] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Trac #14507 showed an example where the inferred type of the matcher diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs index 56f3f07a44..4bcd203a2b 100644 --- a/compiler/typecheck/TcRules.hs +++ b/compiler/typecheck/TcRules.hs @@ -86,8 +86,8 @@ tcRule (HsRule { rd_ext = ext ; (stuff,_) <- pushTcLevelM $ generateRuleConstraints ty_bndrs tm_bndrs lhs rhs - ; let (id_bndrs, lhs', lhs_wanted - , rhs', rhs_wanted, rule_ty, tc_lvl) = stuff + ; let (tv_bndrs, id_bndrs, lhs', lhs_wanted + , rhs', rhs_wanted, rule_ty, tc_lvl) = stuff ; traceTc "tcRule 1" (vcat [ pprFullRuleName rname , ppr lhs_wanted @@ -110,14 +110,16 @@ tcRule (HsRule { rd_ext = ext -- during zonking (see TcHsSyn.zonkRule) ; let tpl_ids = lhs_evs ++ id_bndrs - ; forall_tkvs <- zonkTcTypesAndSplitDepVars $ - rule_ty : map idType tpl_ids ; gbls <- tcGetGlobalTyCoVars -- Even though top level, there might be top-level -- monomorphic bindings from the MR; test tc111 + ; forall_tkvs <- candidateQTyVarsOfTypes gbls $ + map (mkSpecForAllTys tv_bndrs) $ -- don't quantify over lexical tyvars + rule_ty : map idType tpl_ids ; qtkvs <- quantifyTyVars gbls forall_tkvs ; traceTc "tcRule" (vcat [ pprFullRuleName rname , ppr forall_tkvs , ppr qtkvs + , ppr tv_bndrs , ppr rule_ty , vcat [ ppr id <+> dcolon <+> ppr (idType id) | id <- tpl_ids ] ]) @@ -127,10 +129,11 @@ tcRule (HsRule { rd_ext = ext -- For the LHS constraints we must solve the remaining constraints -- (a) so that we report insoluble ones -- (b) so that we bind any soluble ones - ; let skol_info = RuleSkol name - ; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs + ; let all_qtkvs = qtkvs ++ tv_bndrs + skol_info = RuleSkol name + ; (lhs_implic, lhs_binds) <- buildImplicationFor tc_lvl skol_info all_qtkvs lhs_evs residual_lhs_wanted - ; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl skol_info qtkvs + ; (rhs_implic, rhs_binds) <- buildImplicationFor tc_lvl skol_info all_qtkvs lhs_evs rhs_wanted ; emitImplications (lhs_implic `unionBags` rhs_implic) @@ -138,14 +141,15 @@ tcRule (HsRule { rd_ext = ext , rd_name = rname , rd_act = act , rd_tyvs = ty_bndrs -- preserved for ppr-ing - , rd_tmvs = map (noLoc . RuleBndr noExt . noLoc) (qtkvs ++ tpl_ids) + , rd_tmvs = map (noLoc . RuleBndr noExt . noLoc) (all_qtkvs ++ tpl_ids) , rd_lhs = mkHsDictLet lhs_binds lhs' , rd_rhs = mkHsDictLet rhs_binds rhs' } } tcRule (XRuleDecl _) = panic "tcRule" generateRuleConstraints :: Maybe [LHsTyVarBndr GhcRn] -> [LRuleBndr GhcRn] -> LHsExpr GhcRn -> LHsExpr GhcRn - -> TcM ( [TcId] + -> TcM ( [TyVar] + , [TcId] , LHsExpr GhcTc, WantedConstraints , LHsExpr GhcTc, WantedConstraints , TcType @@ -166,9 +170,7 @@ generateRuleConstraints ty_bndrs tm_bndrs lhs rhs ; (rhs', rhs_wanted) <- captureConstraints $ tcMonoExpr rhs (mkCheckExpType rule_ty) ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted - ; return (id_bndrs, lhs', all_lhs_wanted - , rhs', rhs_wanted, rule_ty, lvl) } } - -- Slightly curious that tv_bndrs is not returned + ; return (tv_bndrs, id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty, lvl) } } -- See Note [TcLevel in type checking rules] tcRuleBndrs :: Maybe [LHsTyVarBndr GhcRn] -> [LRuleBndr GhcRn] diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 43e8512d82..68a514fbd9 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -105,7 +105,7 @@ module TcSMonad ( zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo, zonkTyCoVarsAndFVList, zonkSimples, zonkWC, - zonkTcTyCoVarBndr, + zonkTyCoVarKind, -- References newTcRef, readTcRef, writeTcRef, updTcRef, @@ -3095,14 +3095,7 @@ pprEq :: TcType -> TcType -> SDoc pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2 isFilledMetaTyVar_maybe :: TcTyVar -> TcS (Maybe Type) -isFilledMetaTyVar_maybe tv - = case tcTyVarDetails tv of - MetaTv { mtv_ref = ref } - -> do { cts <- readTcRef ref - ; case cts of - Indirect ty -> return (Just ty) - Flexi -> return Nothing } - _ -> return Nothing +isFilledMetaTyVar_maybe tv = wrapTcS (TcM.isFilledMetaTyVar_maybe tv) isFilledMetaTyVar :: TcTyVar -> TcS Bool isFilledMetaTyVar tv = wrapTcS (TcM.isFilledMetaTyVar tv) @@ -3131,8 +3124,8 @@ zonkSimples cts = wrapTcS (TcM.zonkSimples cts) zonkWC :: WantedConstraints -> TcS WantedConstraints zonkWC wc = wrapTcS (TcM.zonkWC wc) -zonkTcTyCoVarBndr :: TcTyCoVar -> TcS TcTyCoVar -zonkTcTyCoVarBndr tv = wrapTcS (TcM.zonkTcTyCoVarBndr tv) +zonkTyCoVarKind :: TcTyCoVar -> TcS TcTyCoVar +zonkTyCoVarKind tv = wrapTcS (TcM.zonkTyCoVarKind tv) {- ********************************************************************* * * diff --git a/compiler/typecheck/TcSigs.hs b/compiler/typecheck/TcSigs.hs index ada91786c0..f7a41e58bf 100644 --- a/compiler/typecheck/TcSigs.hs +++ b/compiler/typecheck/TcSigs.hs @@ -349,9 +349,9 @@ tcPatSynSig name sig_ty -- These are /signatures/ so we zonk to squeeze out any kind -- unification variables. Do this after kindGeneralize which may -- default kind variables to *. - ; implicit_tvs <- mapM zonkTcTyCoVarBndr implicit_tvs - ; univ_tvs <- mapM zonkTcTyCoVarBndr univ_tvs - ; ex_tvs <- mapM zonkTcTyCoVarBndr ex_tvs + ; implicit_tvs <- mapM zonkTyCoVarKind implicit_tvs + ; univ_tvs <- mapM zonkTyCoVarKind univ_tvs + ; ex_tvs <- mapM zonkTyCoVarKind ex_tvs ; req <- zonkTcTypes req ; prov <- zonkTcTypes prov ; body_ty <- zonkTcType body_ty diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index 562340f0da..6ef62c80a8 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -674,7 +674,7 @@ simplifyInfer :: TcLevel -- Used when generating the constraints simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds | isEmptyWC wanteds = do { gbl_tvs <- tcGetGlobalTyCoVars - ; dep_vars <- zonkTcTypesAndSplitDepVars (map snd name_taus) + ; dep_vars <- candidateQTyVarsOfTypes gbl_tvs (map snd name_taus) ; qtkvs <- quantifyTyVars gbl_tvs dep_vars ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs) ; return (qtkvs, [], emptyTcEvBinds, emptyWC, False) } @@ -1083,8 +1083,12 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates ; (prom, _) <- promoteTyVarSet mono_tvs -- Default any kind/levity vars - ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} - = candidateQTyVarsOfTypes candidates + ; DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} + <- candidateQTyVarsOfTypes mono_tvs candidates + -- any covars should already be handled by + -- the logic in decideMonoTyVars, which looks at + -- the constraints generated + ; poly_kinds <- xoptM LangExt.PolyKinds ; default_kvs <- mapM (default_one poly_kinds True) (dVarSetElems cand_kvs) @@ -1150,11 +1154,10 @@ decideQuantifiedTyVars mono_tvs name_taus psigs candidates -- Keep the psig_tys first, so that candidateQTyVarsOfTypes produces -- them in that order, so that the final qtvs quantifies in the same -- order as the partial signatures do (Trac #13524) - ; let DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} - = candidateQTyVarsOfTypes $ - psig_tys ++ candidates ++ tau_tys - pick = (`dVarSetIntersectVarSet` grown_tcvs) - dvs_plus = DV { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs } + ; dv@DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} <- candidateQTyVarsOfTypes mono_tvs $ + psig_tys ++ candidates ++ tau_tys + ; let pick = (`dVarSetIntersectVarSet` grown_tcvs) + dvs_plus = dv { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs } ; traceTc "decideQuantifiedTyVars" (vcat [ text "seed_tys =" <+> ppr seed_tys @@ -1696,7 +1699,7 @@ checkBadTelescope :: Implication -> TcS Bool checkBadTelescope (Implic { ic_telescope = m_telescope , ic_skols = skols }) | isJust m_telescope - = do{ skols <- mapM TcS.zonkTcTyCoVarBndr skols + = do{ skols <- mapM TcS.zonkTyCoVarKind skols ; return (go emptyVarSet (reverse skols))} | otherwise diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index ea1299825f..5725cfd703 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -73,7 +73,6 @@ import BasicTypes import qualified GHC.LanguageExtensions as LangExt import Control.Monad -import Control.Monad.Zip import Data.List import Data.List.NonEmpty ( NonEmpty(..) ) import qualified Data.Set as Set @@ -346,11 +345,15 @@ TcTyCons are used for two distinct purposes of parameters written to the tycon) to get an initial shape of the tycon's kind. We record that shape in a TcTyCon. + For CUSK tycons, the TcTyCon has the final, generalised kind. + For non-CUSK tycons, the TcTyCon has as its tyConBinders only + the explicit arguments given -- no kind variables, etc. + S2) Then, using these initial kinds, we kind-check the body of the tycon (class methods, data constructors, etc.), filling in the metavariables in the tycon's initial kind. - S3) We then generalize to get the tycon's final, fixed + S3) We then generalize to get the (non-CUSK) tycon's final, fixed kind. Finally, once this has happened for all tycons in a mutually recursive group, we can desugar the lot. @@ -390,35 +393,6 @@ TcTyCons are used for two distinct purposes See also Note [Type checking recursive type and class declarations]. -Note [Check telescope again during generalisation] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The telescope check before kind generalisation is useful to catch something -like this: - - data T a k = MkT (Proxy (a :: k)) - -Clearly, the k has to come first. Checking for this problem must come before -kind generalisation, as described in Note [Generalisation for type constructors] - -However, we have to check again *after* kind generalisation, to catch something -like this: - - data SameKind :: k -> k -> Type -- to force unification - data S a (b :: a) (d :: SameKind c b) - -Note that c has no explicit binding site. As such, it's quantified by kind -generalisation. (Note that kcHsTyVarBndrs does not return such variables -as binders in its returned TcTyCon.) The user-written part of this telescope -is well-ordered; no earlier variables depend on later ones. However, after -kind generalisation, we put c up front, like so: - - data S {c :: a} a (b :: a) (d :: SameKind c b) - -We now have a problem. We could detect this problem just by looking at the -free vars of the kinds of the generalised variables (the kvs), but we get -such a nice error message out of checkValidTelescope that it seems like the -right thing to do. - Note [Type environment evolution] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ As we typecheck a group of declarations the type environment evolves. @@ -532,9 +506,17 @@ kcTyClGroup decls tcExtendKindEnvWithTyCons initial_tcs $ mapM_ kcLTyClDecl decls - -- Step 3: generalisation + -- Step 3: skolemisation -- Kind checking done for this group - -- Now we have to kind generalize the flexis + -- Now we have to kind skolemise the flexis + ; candidates <- gather_quant_candidates initial_tcs + ; _ <- quantifyTyVars emptyVarSet candidates + -- We'll get the actual vars to quantify over later. + + -- Step 4: generalisation + -- Finally, go through each tycon and give it its final kind, + -- with all the required, specified, and inferred variables + -- in order. ; poly_tcs <- mapAndReportM generalise initial_tcs ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs) @@ -544,123 +526,219 @@ kcTyClGroup decls ppr_tc_kinds tcs = vcat (map pp_tc tcs) pp_tc tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc) - generalise :: TcTyCon -> TcM TcTyCon - -- For polymorphic things this is a no-op - generalise tc - = setSrcSpan (getSrcSpan tc) $ - addTyConCtxt tc $ - do { let name = tyConName tc - ; tc_binders <- mapM zonkTcTyVarBinder (tyConBinders tc) - ; tc_res_kind <- zonkTcType (tyConResKind tc) - ; let scoped_tvs = tcTyConScopedTyVars tc - user_tyvars = tcTyConUserTyVars tc - tc_tyvars = binderVars tc_binders - - -- See Note [checkValidDependency] - ; checkValidDependency tc_binders tc_res_kind - - -- See Note [Generalisation for type constructors] - ; let kvs_to_gen = tyCoVarsOfTypesDSet (tc_res_kind : map tyVarKind tc_tyvars) - `delDVarSetList` tc_tyvars - dvs = DV { dv_kvs = kvs_to_gen, dv_tvs = emptyDVarSet } - ; kvs <- quantifyTyVars emptyVarSet dvs - - -- See Note [Work out final tyConBinders] - ; scoped_tvs' <- zonkTyVarTyVarPairs scoped_tvs - ; let (specified_kvs, inferred_kvs) = partition is_specified kvs - user_specified_tkvs = mkVarSet (map snd scoped_tvs') - is_specified kv = kv `elemVarSet` user_specified_tkvs - all_binders = mkNamedTyConBinders Inferred inferred_kvs ++ - mkNamedTyConBinders Specified specified_kvs ++ - tc_binders - - ; (env, all_binders') <- zonkTyVarBinders all_binders - ; tc_res_kind' <- zonkTcTypeToTypeX env tc_res_kind - - -- See Note [Check telescope again during generalisation] - ; checkValidTelescope all_binders user_tyvars - - -- Make sure tc_kind' has the final, zonked kind variables - ; traceTc "Generalise kind" $ - vcat [ ppr name, ppr tc_binders, ppr (mkTyConKind tc_binders tc_res_kind) - , ppr kvs, ppr all_binders, ppr tc_res_kind - , ppr all_binders', ppr tc_res_kind' - , ppr scoped_tvs ] - - ; return (mkTcTyCon name user_tyvars all_binders' tc_res_kind' - scoped_tvs' - (tyConFlavour tc)) } + gather_quant_candidates :: [TcTyCon] -> TcM CandidatesQTvs + gather_quant_candidates tcs = mconcat <$> mapM gather1 tcs -{- Note [Generalisation for type constructors] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider test T14066g: - data SameKind :: k -> k -> Type - -We find that the Specified variable has kind (c :: a). We always -put Specified variables before Required ones, so we should reject. - - -Now that we can mix type and kind variables, there are an awful lot of -ways to shoot yourself in the foot. Here are some. - -data SameKind :: k -> k -> * -- just to force unification - -1. data T1 a k (b :: k) (x :: SameKind a b) + gather1 :: TcTyCon -> TcM CandidatesQTvs + gather1 tc + | tcTyConIsPoly tc -- these don't need generalisation + = return mempty - The problem here is that we discover that a and b should have the same - kind. But this kind mentions k, which is bound *after* a. - (Testcase: dependent/should_fail/BadTelescope) - -2. data Q a (b :: a) (d :: SameKind c b) - - Note that c is not bound; it is Specified, not Required. Yet its - kind mentions a. Because we have a nice rule that all Specified - variables come before Required ones this is bogus. (We could - probably figure out to put c between a and b. But I think this is - doing users a disservice, in the long run.) (Testcase: - dependent/should_fail/BadTelescope4) - - So, when finding the free vars to generalise, we should look at the - kinds of all Q's binders, plus its result kind, and delete Q's - binders, leaving just {c}. We should NOT try to short-cut by taking - the free vars of the half-baked kind - (forall a. a -> SameKind c b -> *) - because since 'c' is free we also think 'a' (another 'a'!) is - free in that kind. - -To catch these dependency errors, we call checkValidTelescope during -kind-checking datatype declarations. + | otherwise + = do { tc_binders <- zonkTyConBinders (tyConBinders tc) + ; tc_res_kind <- zonkTcType (tyConResKind tc) -See Note [Keeping scoped variables in order: Explicit] for how this -check works for `forall x y z.` written in a type. --} + ; let tvs = mkDVarSet $ map binderVar tc_binders + kvs = tyCoVarsOfTypesDSet (tc_res_kind : map binderType tc_binders) + `minusDVarSet` tvs -{- Note [Work out final tyConBinders] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - data T f (a::k1) b = MkT (f a b) (T f a b) + ; return (mempty { dv_kvs = kvs, dv_tvs = tvs }) } -We should get - T :: forall {k2} k1. (k1 -> k2 -> *) -> k1 -> k2 -> * + generalise :: TcTyCon -> TcM TcTyCon + generalise tc + | tcTyConIsPoly tc + = return tc -- nothing to do here; we already have the final kind + -- This is just an optimization; generalising is a no-op -Note that: - * k1 is Specified, because it appears in a user-written kind - * k2 is Inferred, because it doesn't appear at all in the - original declaration + | otherwise + -- See Note [Required, Specified, and Inferred for types] + = do { -- Step 0: get the tyvars from the enclosing class (if any) + (all_class_tctvs, class_scoped_tvs) <- get_class_tvs tc + + -- Step 1: gather all the free variables + ; tc_tvs <- mapM zonkTcTyCoVarBndr (map binderVar (tyConBinders tc)) + ; tc_res_kind <- zonkTcType (tyConResKind tc) + ; scoped_tv_pairs <- zonkTyVarTyVarPairs (tcTyConScopedTyVars tc) + + ; let all_fvs = tyCoVarsOfTypesDSet (tc_res_kind : map tyVarKind tc_tvs) + scoped_tvs = map snd scoped_tv_pairs + + ; MASSERT( all ((== Required) . tyConBinderArgFlag) (tyConBinders tc) ) + + -- Step 2: Select out the Required arguments; that is, the tc_binders + ; let no_req_fvs = all_fvs `delDVarSetList` tc_tvs + + -- Step 3: partition remaining variables into class variables and + -- local variables (matters only for associated types) + (class_fvs, local_fvs) + = partitionDVarSet (`elemDVarSet` all_class_tctvs) no_req_fvs + + -- Step 4: For each set so far, use the set to select the scoped_tvs. + -- We take from the scoped_tvs to preserve order. These tvs will become + -- the Specified ones. + class_specified = filter (`elemDVarSet` class_fvs) class_scoped_tvs + local_specified = filter (`elemDVarSet` local_fvs) scoped_tvs + + -- Step 5: Order the specified variables by ScopedSort + -- See Note [ScopedSort] in Type + class_specified_sorted = scopedSort class_specified + local_specified_sorted = scopedSort local_specified + + -- Step 6: Remove the Specified ones from the fv sets. These are the + -- Inferred ones. + class_inferred_set = class_fvs `delDVarSetList` class_specified_sorted + local_inferred_set = local_fvs `delDVarSetList` local_specified_sorted + + class_inferred = dVarSetElemsWellScoped class_inferred_set + local_inferred = dVarSetElemsWellScoped local_inferred_set + + -- Step 7: Make the TyConBinders. + class_inferred_tcbs = mkNamedTyConBinders Inferred class_inferred + class_specified_tcbs = mkNamedTyConBinders Specified class_specified_sorted + local_inferred_tcbs = mkNamedTyConBinders Inferred local_inferred + local_specified_tcbs = mkNamedTyConBinders Specified local_specified_sorted + + mk_req_tcb tv + | tv `elemDVarSet` all_fvs = mkNamedTyConBinder Required tv + | otherwise = mkAnonTyConBinder tv + + required_tcbs = map mk_req_tcb tc_tvs + + -- Step 8: Assemble the final list. + final_tcbs = concat [ class_inferred_tcbs + , class_specified_tcbs + , local_inferred_tcbs + , local_specified_tcbs + , required_tcbs ] + + -- Step 9: Check for validity. We do this here because we're about to + -- put the tycon into the environment, and we don't want anything malformed + -- in the environment. + ; let user_tyvars = tcTyConUserTyVars tc + ; setSrcSpan (getSrcSpan tc) $ + addTyConCtxt tc $ + checkValidTelescope final_tcbs user_tyvars + + -- Step 10: Make the result TcTyCon + ; let name = tyConName tc + ; traceTc "Generalise kind" $ + vcat [ text "name =" <+> ppr name + , text "all_class_tctvs =" <+> ppr all_class_tctvs + , text "class_scoped_tvs =" <+> ppr class_scoped_tvs + , text "tc_tvs =" <+> ppr tc_tvs + , text "tc_res_kind =" <+> ppr tc_res_kind + , text "scoped_tvs =" <+> ppr scoped_tvs + , text "class_inferred_tcbs =" <+> ppr class_inferred_tcbs + , text "class_specified_tcbs =" <+> ppr class_specified_tcbs + , text "local_inferred_tcbs =" <+> ppr local_inferred_tcbs + , text "local_specified_tcbs =" <+> ppr local_specified_tcbs + , text "required_tcbs =" <+> ppr required_tcbs ] + ; return $ mkTcTyCon name user_tyvars final_tcbs tc_res_kind scoped_tv_pairs + True {- it's generalised now -} (tyConFlavour tc) } + + get_class_tvs :: TcTyCon -> TcM (DTyCoVarSet, [TcTyVar]) + -- returns all tyConTyVars of the enclosing class, as well as its + -- scoped type variables. Both are zonked. + get_class_tvs at_tc + | Just class_tc <- tyConAssoc_maybe at_tc + = do { -- We can't just call tyConTyVars, because the enclosing class + -- hasn't been generalised yet + tc_binders <- zonkTyConBinders (tyConBinders class_tc) + ; tc_res_kind <- zonkTcType (tyConResKind class_tc) + ; scoped_tvs <- mapM zonkTcTyVarToTyVar (map snd (tcTyConScopedTyVars class_tc)) + + ; return ( tyCoVarsOfTypesDSet (tc_res_kind : map binderType tc_binders) + `extendDVarSetList` tyConTyVars class_tc + , scoped_tvs ) } -However, at this point in kcTyClGroup, the tc_binders are -simply [f, a, b], the user-written argumennts to the TyCon. -(Why? Because that's what we need for the recursive uses in -T's RHS.) + | otherwise + = return (emptyDVarSet, []) -So kindGeneralize will generalise over /both/ k1 /and/ k2. -Yet we must distinguish them, and we must put the Inferred -ones first. How can we tell the difference? Well, the -Specified variables will be among the tyConScopedTyVars of -the TcTyCon. +{- Note [Required, Specified, and Inferred for types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We have some design choices in how we classify the tyvars bound +in a type declaration. (Here, I use "type" to refer to any TyClDecl.) +Much of the debate is memorialized in #15743. This Note documents +the final conclusion. + +First, a reminder: + * a Required argument is one that must be provided at every call site + * a Specified argument is one that can be inferred at call sites, but + may be instantiated with visible type application + * an Inferred argument is one that must be inferred at call sites; it + is unavailable for use with visible type application. + +Why have Inferred at all? Because we just can't make user-facing promises +about the ordering of some variables. These might swizzle around even between +minor released. By forbidding visible type application, we ensure users +aren't caught unawares. See also +Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep. + +When inferring the ordering of variables (that is, for those +variables that he user has not specified the order with an explicit `forall`) +we use the following order: + + 1. Inferred variables from an enclosing class (associated types only) + 2. Specified variables from an enclosing class (associated types only) + 3. Inferred variables not from an enclosing class + 4. Specified variables not from an enclosing class + 5. Required variables before a top-level :: + 6. All variables after a top-level :: + +If this ordering does not make a valid telescope, we reject the definition. + +This idea is implemented in the generalise function within kcTyClGroup (for +declarations without CUSKs), and in kcLHsQTyVars (for declarations with +CUSKs). Note that neither definition worries about point (6) above, as this +is nicely handled by not mangling the res_kind. (Mangling res_kinds is done +*after* all this stuff, in tcDataDefn's call to tcDataKindSig.) We can +easily tell Inferred apart from Specified by looking at the scoped tyvars; +Specified are always included there. + +One other small open question here: how to classify variables from an +enclosing class? Here is an example: + + class C (a :: k) where + type F a + +In the kind of F, should k be Inferred or Specified? Currently, we mark +it as Specified, as we can commit to an ordering, based on the ordering +of class variables in the enclosing class declaration. If k were not mentioned +in the class head, then it would be Inferred. The alternative to this +approach is to make the Inferred/Specified distinction locally, by just +looking at the declaration for F. This lowers the availability of type +application, but makes the reasoning more local. However, this alternative +also disagrees with the treatment for methods, where all class variables +are Specified, regardless of whether or not the variable is mentioned in the +method type. + +A few points of motivation for the ordering above: + +* We put the class variables before the local variables in a nod to the + treatment for class methods, where class variables (and the class constraint) + come first. While this is an unforced design decision, it never rejects + more declarations, as class variables can never depend on local variables. + +* We rigidly require the ordering above, even though we could be much more + permissive. Relevant musings are at + https://ghc.haskell.org/trac/ghc/ticket/15743#comment:7 + The bottom line conclusion is that, if the user wants a different ordering, + then can specify it themselves, and it is better to be predictable and dumb + than clever and capricious. + + I (Richard) conjecture we could be fully permissive, allowing all classes + of variables to intermix. We would have to augment ScopedSort to refuse to + reorder Required variables (or check that it wouldn't have). But this would + allow more programs. See #15743 for examples. Interestingly, Idris seems + to allow this intermixing. The intermixing would be fully specified, in that + we can be sure that inference wouldn't change between versions. However, + would users be able to predict it? That I cannot answer. + +Test cases (and tickets) relevant to these design decisions: + T15591* + T15592* + T15743* -Hence partitioning by is_specified. See Trac #15592 for -some discussion. -} -------------- @@ -721,12 +799,12 @@ getInitialKind :: TyClDecl GhcRn -> TcM [TcTyCon] getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats }) = do { let cusk = hsDeclHasCusk decl - ; tycon <- kcLHsQTyVars name ClassFlavour cusk [] ktvs $ + ; tycon <- kcLHsQTyVars name ClassFlavour cusk ktvs $ return constraintKind ; let parent_tv_prs = tcTyConScopedTyVars tycon -- See Note [Don't process associated types in kcLHsQTyVars] ; inner_tcs <- tcExtendNameTyVarEnv parent_tv_prs $ - getFamDeclInitialKinds (Just (cusk, parent_tv_prs)) ats + getFamDeclInitialKinds (Just tycon) ats ; return (tycon : inner_tcs) } getInitialKind decl@(DataDecl { tcdLName = L _ name @@ -735,7 +813,7 @@ getInitialKind decl@(DataDecl { tcdLName = L _ name , dd_ND = new_or_data } }) = do { tycon <- kcLHsQTyVars name (newOrDataToFlavour new_or_data) - (hsDeclHasCusk decl) [] ktvs $ + (hsDeclHasCusk decl) ktvs $ case m_sig of Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig Nothing -> return liftedTypeKind @@ -749,7 +827,7 @@ getInitialKind decl@(SynDecl { tcdLName = L _ name , tcdTyVars = ktvs , tcdRhs = rhs }) = do { tycon <- kcLHsQTyVars name TypeSynonymFlavour (hsDeclHasCusk decl) - [] ktvs $ + ktvs $ case kind_annotation rhs of Nothing -> newMetaKindVar Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig @@ -766,47 +844,38 @@ getInitialKind (XTyClDecl _) = panic "getInitialKind" --------------------------------- getFamDeclInitialKinds - :: Maybe (Bool, [(Name, TyVar)]) - -- ^ If this family declaration is associated with a class, this is - -- @'Just' (cusk, cls_tv_prs)@, where @cusk@ indicates the CUSKness of - -- the associated class and @cls_tv_prs@ contains the class's scoped - -- type variables. + :: Maybe TcTyCon -- ^ Enclosing class TcTyCon, if any -> [LFamilyDecl GhcRn] -> TcM [TcTyCon] -getFamDeclInitialKinds mb_parent_info decls - = mapM (addLocM (getFamDeclInitialKind mb_parent_info)) decls +getFamDeclInitialKinds mb_parent_tycon decls + = mapM (addLocM (getFamDeclInitialKind mb_parent_tycon)) decls getFamDeclInitialKind - :: Maybe (Bool, [(Name, TyVar)]) - -- ^ If this family declaration is associated with a class, this is - -- @'Just' (cusk, cls_tv_prs)@, where @cusk@ indicates the CUSKness of - -- the associated class and @cls_tv_prs@ contains the class's scoped - -- type variables. + :: Maybe TcTyCon -- ^ Enclosing class TcTyCon, if any -> FamilyDecl GhcRn -> TcM TcTyCon -getFamDeclInitialKind mb_parent_info +getFamDeclInitialKind mb_parent_tycon decl@(FamilyDecl { fdLName = L _ name , fdTyVars = ktvs , fdResultSig = L _ resultSig , fdInfo = info }) - = do { tycon <- kcLHsQTyVars name flav cusk parent_tv_prs ktvs $ - case resultSig of - KindSig _ ki -> tcLHsKindSig ctxt ki - TyVarSig _ (L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki - _ -- open type families have * return kind by default - | tcFlavourIsOpen flav -> return liftedTypeKind + = kcLHsQTyVars name flav cusk ktvs $ + case resultSig of + KindSig _ ki -> tcLHsKindSig ctxt ki + TyVarSig _ (L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki + _ -- open type families have * return kind by default + | tcFlavourIsOpen flav -> return liftedTypeKind -- closed type families have their return kind inferred -- by default - | otherwise -> newMetaKindVar - ; return tycon } + | otherwise -> newMetaKindVar where - (mb_cusk, mb_parent_tv_prs) = munzip mb_parent_info - cusk = famDeclHasCusk mb_cusk decl - parent_tv_prs = mb_parent_tv_prs `orElse` [] + mb_cusk = tcTyConIsPoly <$> mb_parent_tycon + cusk = famDeclHasCusk mb_cusk decl flav = case info of - DataFamily -> DataFamilyFlavour (isJust mb_cusk) - OpenTypeFamily -> OpenTypeFamilyFlavour (isJust mb_cusk) - ClosedTypeFamily _ -> ClosedTypeFamilyFlavour + DataFamily -> DataFamilyFlavour mb_parent_tycon + OpenTypeFamily -> OpenTypeFamilyFlavour mb_parent_tycon + ClosedTypeFamily _ -> ASSERT( isNothing mb_parent_tycon ) + ClosedTypeFamilyFlavour ctxt = TyFamResKindCtxt name getFamDeclInitialKind _ (XFamilyDecl _) = panic "getFamDeclInitialKind" @@ -815,7 +884,7 @@ kcLTyClDecl :: LTyClDecl GhcRn -> TcM () -- See Note [Kind checking for type and class decls] kcLTyClDecl (L loc decl) | hsDeclHasCusk decl -- See Note [Skip decls with CUSKs in kcLTyClDecl] - = traceTc "kcTyClDecl skipped due to cusk" (ppr tc_name) + = traceTc "kcTyClDecl skipped due to cusk:" (ppr tc_name) | otherwise = setSrcSpan loc $ @@ -1373,7 +1442,8 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na -- Process the equations, creating CoAxBranches ; let tc_fam_tc = mkTcTyCon tc_name (ppr user_tyvars) binders res_kind - [] ClosedTypeFamilyFlavour + [] False {- this doesn't matter here -} + ClosedTypeFamilyFlavour ; branches <- mapAndReportM (tcTyFamInstEqn tc_fam_tc Nothing) eqns -- Do not attempt to drop equations dominated by earlier @@ -1488,7 +1558,7 @@ tcDataDefn roles_info ; tycon <- fixM $ \ tycon -> do { let res_ty = mkTyConApp tycon (mkTyVarTys (binderVars final_bndrs)) - ; data_cons <- tcConDecls tycon (final_bndrs, res_ty) cons + ; data_cons <- tcConDecls tycon final_bndrs res_ty cons ; tc_rhs <- mk_tc_rhs hsc_src tycon data_cons ; tc_rep_nm <- newTyConRepName tc_name ; return (mkAlgTyCon tc_name @@ -1558,7 +1628,8 @@ kcTyFamInstEqn _ (L _ (HsIB _ (XFamEqn _))) = panic "kcTyFamInstEqn" kcTyFamEqnRhs :: Maybe ClsInstInfo -> LHsType GhcRn -- ^ Eqn RHS -> TcKind -- ^ Inferred kind of left-hand side - -> TcM ([TcType], TcKind) -- ^ New pats, inst'ed kind of left-hand side + -> TcM ([TcTyVar], [TcType], TcKind) + -- ^ New pattern skolems, New pats, inst'ed kind of left-hand side kcTyFamEqnRhs mb_clsinfo rhs_hs_ty lhs_ki = do { -- It's still possible the lhs_ki has some foralls. Instantiate these away. (new_pats, insted_lhs_ki) @@ -1573,7 +1644,8 @@ kcTyFamEqnRhs mb_clsinfo rhs_hs_ty lhs_ki ; _ <- tcCheckLHsType rhs_hs_ty insted_lhs_ki - ; return (new_pats, insted_lhs_ki) } + ; return ([], new_pats, insted_lhs_ki) } + -- we never introduce new skolems here where mb_kind_env = thdOf3 <$> mb_clsinfo @@ -1600,7 +1672,7 @@ tcTyFamInstEqn fam_tc mb_clsinfo ; pats' <- zonkTcTypesToTypesX ze pats ; traceTc "tcTyFamInstEqn 3" (ppr eqn_tc_name <+> ppr pats $$ ppr rhs_ty) ; rhs_ty' <- zonkTcTypeToTypeX ze rhs_ty - ; traceTc "tcTyFamInstEqn 4" (ppr fam_tc <+> pprTyVars tvs') + ; traceTc "tcTyFamInstEqn 4 }" (ppr fam_tc <+> pprTyVars tvs') ; return (mkCoAxBranch tvs' [] pats' rhs_ty' (map (const Nominal) tvs') loc) } @@ -1611,12 +1683,12 @@ kcDataDefn :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars -- (associated types only) -> DataFamInstDecl GhcRn -> TcKind -- ^ the kind of the tycon applied to pats - -> TcM ([TcType], TcKind) + -> TcM ([TcTyVar], [TcType], TcKind) -- ^ the kind signature might force instantiation - -- of the tycon; this returns any extra args and the inst'ed kind + -- of the tycon; this returns any extra skolems, args and the inst'ed kind -- See Note [Instantiating a family tycon] -- Used for 'data instance' only --- Ordinary 'data' is handled by kcTyClDec +-- Ordinary 'data' is handled by kcTyClDecl kcDataDefn mb_kind_env (DataFamInstDecl { dfid_eqn = HsIB { hsib_body = FamEqn { feqn_tycon = fam_name @@ -1643,8 +1715,6 @@ kcDataDefn mb_kind_env ; let (tvs_to_skolemise, inner_res_kind) = tcSplitForAllTys exp_res_kind ; (skol_subst, tvs') <- tcInstSkolTyVars tvs_to_skolemise - -- we don't need to do anything substantive with the tvs' because the - -- quantifyTyVars in tcFamTyPats will catch them. ; let inner_res_kind' = substTyAddInScope skol_subst inner_res_kind tv_prs = zip (map tyVarName tvs_to_skolemise) tvs' @@ -1665,7 +1735,7 @@ kcDataDefn mb_kind_env ; rhs_ki <- zonkTcType rhs_ki ; MASSERT( lhs_ki `tcEqType` rhs_ki ) } - ; return (new_args, lhs_ki) } + ; return (tvs', new_args, lhs_ki) } where bogus_ty = pprPanic "kcDataDefn" (ppr fam_name <+> ppr pats) pp_fam_app = pprFamInstLHS fam_name mb_bndrs pats fixity (unLoc ctxt) mb_kind @@ -1699,12 +1769,8 @@ to instantiate the k. With data family instances, this problem can be even more intricate, due to Note [Arity of data families] in FamInstEnv. See indexed-types/should_compile/T12369 for an example. -So, the kind-checker must return both the new args (that is, Type -(Type -> Type) for the equations above) and the instantiated kind. - -Because we don't need this information in the kind-checking phase of -checking closed type families, we don't require these extra pieces of -information in tc_fam_ty_pats. +So, the kind-checker must return the new skolems and args (that is, Type +or (Type -> Type) for the equations above) and the instantiated kind. Note [Failing early in kcDataDefn] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1747,7 +1813,7 @@ tcFamTyPats :: TyCon -> [Name] -- Implicitly bound kind/type variable names -> Maybe [LHsTyVarBndr GhcRn] -> HsTyPats GhcRn -- Type patterns - -> (TcKind -> TcM ([TcType], TcKind)) + -> (TcKind -> TcM ([TcTyVar], [TcType], TcKind)) -- kind-checker for RHS -- See Note [Instantiating a family tycon] -> ( [TcTyVar] -- Kind and type variables @@ -1781,7 +1847,7 @@ tcFamTyPats fam_tc mb_clsinfo wrongNumberOfParmsErr vis_arity -- report only explicit arguments - ; (imp_tvs, (exp_tvs, (typats, (more_typats, res_kind)))) + ; (imp_tvs, (exp_tvs, (typats, (more_tyvars, more_typats, res_kind)))) <- solveEqualities $ -- See Note [Constraints in patterns] tcImplicitQTKBndrs FamInstSkol imp_vars $ tcExplicitTKBndrs FamInstSkol (fromMaybe [] mb_expl_bndrs) $ @@ -1822,9 +1888,26 @@ tcFamTyPats fam_tc mb_clsinfo -- them into skolems, so that we don't subsequently -- replace a meta kind var with (Any *) -- Very like kindGeneralize - ; let all_pats = typats `chkAppend` more_typats - ; vars <- zonkTcTypesAndSplitDepVars all_pats + ; let all_pats = typats `chkAppend` more_typats + fam_app = mkTyConApp fam_tc all_pats + + user_tvs = exp_tvs ++ imp_tvs `chkAppend` more_tyvars + + -- the user_tvs might have quantified kind variables from + -- an enclosing class/instance; make sure to bring these into scope + extra_tvs = case mb_clsinfo of + Nothing -> [] + Just (_, inst_tvs, _) -> + filter (`elemVarSet` tyCoVarsOfType (mkSpecForAllTys user_tvs fam_app)) + inst_tvs + + all_tvs = extra_tvs ++ user_tvs + + -- the user_tvs are already bound in the pats; don't quantify over these again. + ; vars <- candidateQTyVarsOfType emptyVarSet $ + mkSpecForAllTys all_tvs fam_app ; qtkvs <- quantifyTyVars emptyVarSet vars + ; let all_qtkvs = qtkvs ++ all_tvs ; when debugIsOn $ do { all_pats <- mapM zonkTcType all_pats @@ -1838,26 +1921,27 @@ tcFamTyPats fam_tc mb_clsinfo $$ ppr all_pats $$ ppr qtkvs) -- See Note [Free-floating kind vars] in TcHsType - ; let all_mentioned_tvs = mkVarSet qtkvs - -- qtkvs has all the tyvars bound by LHS - -- type patterns - unmentioned_imp_tvs = filterOut (`elemVarSet` all_mentioned_tvs) imp_tvs + ; lhs_tvs <- zonkTcTypeAndFV fam_app + ; let unmentioned_tvs = filterOut (`elemDVarSet` lhs_tvs) imp_tvs -- If there are tyvars left over, we can -- assume they're free-floating, since they -- aren't bound by a type pattern + -- Recall that user are those lexically + -- used in the equation. As skolems, they + -- don't need zonking. ; checkNoErrs $ reportFloatingKvs fam_name flav - qtkvs unmentioned_imp_tvs + (dVarSetElemsWellScoped lhs_tvs) unmentioned_tvs -- Error if exp_tvs contains anything that is still unused. -- See Note [Unused explicitly bound variables in a family pattern] - ; let unmentioned_exp_tvs = filterOut (`elemVarSet` all_mentioned_tvs) exp_tvs + ; let unmentioned_exp_tvs = filterOut (`elemDVarSet` lhs_tvs) exp_tvs ; checkNoErrs $ mapM_ (unusedExplicitForAllErr . Var.varName) unmentioned_exp_tvs - ; scopeTyVars FamInstSkol qtkvs $ + ; scopeTyVars FamInstSkol all_qtkvs $ -- Extend envt with TcTyVars not TyVars, because the -- kind checking etc done by thing_inside does not expect -- to encounter TyVars; it expects TcTyVars - thing_inside qtkvs all_pats res_kind } + thing_inside all_qtkvs all_pats res_kind } where fam_name = tyConName fam_tc flav = tyConFlavour fam_tc @@ -2019,11 +2103,11 @@ consUseGadtSyntax _ = False -- All constructors have same shape ----------------------------------- -tcConDecls :: KnotTied TyCon -> ([KnotTied TyConBinder], KnotTied Type) +tcConDecls :: KnotTied TyCon -> [KnotTied TyConBinder] -> KnotTied Type -> [LConDecl GhcRn] -> TcM [DataCon] -- Why both the tycon tyvars and binders? Because the tyvars -- have all the names and the binders have the visibilities. -tcConDecls rep_tycon (tmpl_bndrs, res_tmpl) +tcConDecls rep_tycon tmpl_bndrs res_tmpl = concatMapM $ addLocM $ tcConDecl rep_tycon (mkTyConTagMap rep_tycon) tmpl_bndrs res_tmpl -- It's important that we pay for tag allocation here, once per TyCon, @@ -2203,7 +2287,7 @@ quantifyConDecl :: TcTyCoVarSet -- outer tvs, not to be quantified over; zonked -> TcType -> TcM [TcTyVar] quantifyConDecl gbl_tvs ty = do { ty <- zonkTcType ty - ; let fvs = candidateQTyVarsOfType ty + ; fvs <- candidateQTyVarsOfType gbl_tvs ty ; quantifyTyVars gbl_tvs fvs } tcConIsInfixH98 :: Name @@ -2311,8 +2395,7 @@ rejigConRes :: [KnotTied TyConBinder] -> KnotTied Type -- Template for result -- data instance T [a] b c ... -- gives template ([a,b,c], T [a] b c) -- Type must be of kind *! - -> [TyVar] -- The constructor's user-written, inferred - -- type variables + -> [TyVar] -- The constructor's inferred type variables -> [TyVar] -- The constructor's user-written, specified -- type variables -> KnotTied Type -- res_ty type must be of kind * @@ -3363,75 +3446,6 @@ For example: data T a = A { m1 :: a, _m2 :: a } | B { m1 :: a } -Note [checkValidDependency] -~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - - data Proxy k (a :: k) - data Proxy2 k a = P (Proxy k a) - -(This is test dependent/should_fail/InferDependency.) While it seems GHC can -figure out the dependency between the arguments to Proxy2, this case errors. -The problem is that when we build the initial kind (getInitialKind) for -a tycon, we need to decide whether an argument is dependent or not. At first, -I thought we could just assume that *all* arguments are dependent, and then -patch it up later. However, this causes problems in error messages (where -tycon's have mysterious kinds "forall (a :: k) -> blah") and in unification -(where we try to unify kappa ~ forall (a :: k) -> blah, failing because the -RHS is not a tau-type). Perhaps a cleverer algorithm could sort this out -(say, by storing the dependency flag in a mutable cell and by avoiding -these fancy kinds in error messages depending on the extension in effect) -but it doesn't seem worth it. - -So: we choose the dependency for each argument variable once and for all -in getInitialKind. This means that any dependency must be lexically manifest. - -checkValidDependency checks to make sure that no lexically non-dependent -argument actually appears in a kind. Note the example above, where the k -in Proxy2 is a dependent argument, but this fact is not lexically -manifest. checkValidDependency will reject. This function must be called -*before* kind generalization, because kind generalization works with -the result of mkTyConKind, which will think that Proxy2's kind is -Type -> k -> Type, where k is unbound. (It won't use a forall for a -"non-dependent" argument k.) --} - --- | See Note [checkValidDependency] -checkValidDependency :: [TyConBinder] -- zonked - -> TcKind -- zonked (result kind) - -> TcM () -checkValidDependency binders res_kind - = go (tyCoVarsOfType res_kind) (reverse binders) - where - go :: TyCoVarSet -- fvs from scope - -> [TyConBinder] -- binders, in reverse order - -> TcM () - go _ [] = return () -- all set - go fvs (tcb : tcbs) - | not (isNamedTyConBinder tcb) && tcb_var `elemVarSet` fvs - = do { setSrcSpan (getSrcSpan tcb_var) $ - addErrTc (vcat [ text "Type constructor argument" <+> quotes (ppr tcb_var) <+> - text "is used dependently." - , text "Any dependent arguments must be obviously so, not inferred" - , text "by the type-checker." - , hang (text "Inferred argument kinds:") - 2 (vcat (map pp_binder binders)) - , text "Suggestion: use" <+> quotes (ppr tcb_var) <+> - text "in a kind to make the dependency clearer." ]) - ; go new_fvs tcbs } - - | otherwise - = go new_fvs tcbs - where - new_fvs = fvs `delVarSet` tcb_var - `unionVarSet` tyCoVarsOfType tcb_kind - - tcb_var = binderVar tcb - tcb_kind = tyVarKind tcb_var - - pp_binder binder = ppr (binderVar binder) <+> dcolon <+> ppr (binderType binder) - -{- ************************************************************************ * * Checking role validity @@ -3813,13 +3827,10 @@ incoherentRoles = (text "Roles other than" <+> quotes (text "nominal") <+> (text "Use IncoherentInstances to allow this; bad role found") addTyConCtxt :: TyCon -> TcM a -> TcM a -addTyConCtxt tc - = addErrCtxt ctxt +addTyConCtxt tc = addTyConFlavCtxt name flav where name = getName tc - flav = ppr (tyConFlavour tc) - ctxt = hsep [ text "In the", flav - , text "declaration for", quotes (ppr name) ] + flav = tyConFlavour tc addRoleAnnotCtxt :: Name -> TcM a -> TcM a addRoleAnnotCtxt name diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 8fcdde1dad..2ddb4c4604 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -104,7 +104,6 @@ module TcType ( -- * Finding "exact" (non-dead) type variables exactTyCoVarsOfType, exactTyCoVarsOfTypes, - candidateQTyVarsOfType, candidateQTyVarsOfTypes, CandidatesQTvs(..), anyRewritableTyVar, --------------------------------- @@ -181,7 +180,7 @@ module TcType ( pprTheta, pprParendTheta, pprThetaArrowTy, pprClassPred, pprTCvBndr, pprTCvBndrs, - TypeSize, sizeType, sizeTypes, toposortTyVars, + TypeSize, sizeType, sizeTypes, scopedSort, --------------------------------- -- argument visibility @@ -225,11 +224,10 @@ import FastString import ErrUtils( Validity(..), MsgDoc, isValid ) import qualified GHC.LanguageExtensions as LangExt -import Data.List ( mapAccumL ) +import Data.List ( mapAccumL, foldl' ) import Data.Functor.Identity( Identity(..) ) import Data.IORef import Data.List.NonEmpty( NonEmpty(..) ) -import qualified Data.Semigroup as Semi {- ************************************************************************ @@ -1007,149 +1005,6 @@ would re-occur and we end up with an infinite loop in which each kicks out the other (Trac #14363). -} -{- ********************************************************************* -* * - Type and kind variables in a type -* * -********************************************************************* -} - -data CandidatesQTvs -- See Note [Dependent type variables] - -- See Note [CandidatesQTvs determinism and order] - = DV { dv_kvs :: DTyCoVarSet -- "kind" variables (dependent) - , dv_tvs :: DTyVarSet -- "type" variables (non-dependent) - -- A variable may appear in both sets - -- E.g. T k (x::k) The first occurrence of k makes it - -- show up in dv_tvs, the second in dv_kvs - -- See Note [Dependent type variables] - } - -instance Semi.Semigroup CandidatesQTvs where - (DV { dv_kvs = kv1, dv_tvs = tv1 }) <> (DV { dv_kvs = kv2, dv_tvs = tv2 }) - = DV { dv_kvs = kv1 `unionDVarSet` kv2 - , dv_tvs = tv1 `unionDVarSet` tv2} - -instance Monoid CandidatesQTvs where - mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet } - mappend = (Semi.<>) - -instance Outputable CandidatesQTvs where - ppr (DV {dv_kvs = kvs, dv_tvs = tvs }) - = text "DV" <+> braces (sep [ text "dv_kvs =" <+> ppr kvs - , text "dv_tvs =" <+> ppr tvs ]) - -{- Note [Dependent type variables] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In Haskell type inference we quantify over type variables; but we only -quantify over /kind/ variables when -XPolyKinds is on. Without -XPolyKinds -we default the kind variables to *. - -So, to support this defaulting, and only for that reason, when -collecting the free vars of a type, prior to quantifying, we must keep -the type and kind variables separate. - -But what does that mean in a system where kind variables /are/ type -variables? It's a fairly arbitrary distinction based on how the -variables appear: - - - "Kind variables" appear in the kind of some other free variable - PLUS any free coercion variables - - These are the ones we default to * if -XPolyKinds is off - - - "Type variables" are all free vars that are not kind variables - -E.g. In the type T k (a::k) - 'k' is a kind variable, because it occurs in the kind of 'a', - even though it also appears at "top level" of the type - 'a' is a type variable, because it doesn't - -We gather these variables using a CandidatesQTvs record: - DV { dv_kvs: Variables free in the kind of a free type variable - or of a forall-bound type variable - , dv_tvs: Variables sytactically free in the type } - -So: dv_kvs are the kind variables of the type - (dv_tvs - dv_kvs) are the type variable of the type - -Note that - -* A variable can occur in both. - T k (x::k) The first occurrence of k makes it - show up in dv_tvs, the second in dv_kvs - -* We include any coercion variables in the "dependent", - "kind-variable" set because we never quantify over them. - -* Both sets are un-ordered, of course. - -* The "kind variables" might depend on each other; e.g - (k1 :: k2), (k2 :: *) - The "type variables" do not depend on each other; if - one did, it'd be classified as a kind variable! - -Note [CandidatesQTvs determinism and order] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -* Determinism: when we quantify over type variables we decide the - order in which they appear in the final type. Because the order of - type variables in the type can end up in the interface file and - affects some optimizations like worker-wrapper, we want this order to - be deterministic. - - To achieve that we use deterministic sets of variables that can be - converted to lists in a deterministic order. For more information - about deterministic sets see Note [Deterministic UniqFM] in UniqDFM. - -* Order: as well as being deterministic, we use an - accumulating-parameter style for candidateQTyVarsOfType so that we - add variables one at a time, left to right. That means we tend to - produce the variables in left-to-right order. This is just to make - it bit more predicatable for the programmer. --} - --- | Worker for 'splitDepVarsOfType'. This might output the same var --- in both sets, if it's used in both a type and a kind. --- See Note [CandidatesQTvs determinism and order] --- See Note [Dependent type variables] -candidateQTyVarsOfType :: Type -> CandidatesQTvs -candidateQTyVarsOfType = split_dvs emptyVarSet mempty - -split_dvs :: VarSet -> CandidatesQTvs -> Type -> CandidatesQTvs -split_dvs bound dvs ty - = go dvs ty - where - go dv (AppTy t1 t2) = go (go dv t1) t2 - go dv (TyConApp _ tys) = foldl' go dv tys - go dv (FunTy arg res) = go (go dv arg) res - go dv (LitTy {}) = dv - go dv (CastTy ty co) = go dv ty `mappend` go_co co - go dv (CoercionTy co) = dv `mappend` go_co co - - go dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) (TyVarTy tv) - | tv `elemVarSet` bound - = dv - | otherwise - = DV { dv_kvs = kvs `unionDVarSet` - kill_bound (tyCoVarsOfTypeDSet (tyVarKind tv)) - , dv_tvs = tvs `extendDVarSet` tv } - - go dv (ForAllTy (Bndr tv _) ty) - = DV { dv_kvs = kvs `unionDVarSet` - kill_bound (tyCoVarsOfTypeDSet (tyVarKind tv)) - , dv_tvs = tvs } - where - DV { dv_kvs = kvs, dv_tvs = tvs } = split_dvs (bound `extendVarSet` tv) dv ty - - go_co co = DV { dv_kvs = kill_bound (tyCoVarsOfCoDSet co) - , dv_tvs = emptyDVarSet } - - kill_bound free - | isEmptyVarSet bound = free - | otherwise = free `dVarSetMinusVarSet` bound - --- | Like 'splitDepVarsOfType', but over a list of types -candidateQTyVarsOfTypes :: [Type] -> CandidatesQTvs -candidateQTyVarsOfTypes = foldl' (split_dvs emptyVarSet) mempty - {- ************************************************************************ * * diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 936eed842f..f9aad513b7 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -1779,7 +1779,8 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pat = do { -- Check that the associated type indeed comes from this class -- See [Mismatched class methods and associated type families] -- in TcInstDecls. - checkTc (Just clas == tyConAssoc_maybe fam_tc) + + checkTc (Just (classTyCon clas) == tyConAssoc_maybe fam_tc) (badATErr (className clas) (tyConName fam_tc)) -- Check type args first (more comprehensible) @@ -1789,9 +1790,9 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pat ; checkTcM (all check_arg kind_shapes) (tidy_env2, pp_wrong_at_arg $$ ppSuggestExplicitKinds) - ; traceTc "cfi" (vcat [ ppr inst_tvs - , ppr arg_shapes - , ppr mini_env ]) } + ; traceTc "checkConsistentFamInst" (vcat [ ppr inst_tvs + , ppr arg_shapes + , ppr mini_env ]) } where arg_shapes :: [AssocInstArgShape] arg_shapes = [ (lookupVarEnv mini_env fam_tc_tv, at_ty) @@ -2062,6 +2063,33 @@ famPatErr fam_tc tvs pats Telescope checking * * ************************************************************************ + +Note [Bad telescopes] +~~~~~~~~~~~~~~~~~~~~~ +Now that we can mix type and kind variables, there are an awful lot of +ways to shoot yourself in the foot. Here are some. + + data SameKind :: k -> k -> * -- just to force unification + +1. data T1 a k (b :: k) (x :: SameKind a b) + +The problem here is that we discover that a and b should have the same +kind. But this kind mentions k, which is bound *after* a. +(Testcase: dependent/should_fail/BadTelescope) + +2. data T2 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d) + +Note that b is not bound. Yet its kind mentions a. Because we have +a nice rule that all implicitly bound variables come before others, +this is bogus. + +To catch these errors, we call checkValidTelescope during kind-checking +datatype declarations. See also +Note [Required, Specified, and Inferred for types] in TcTyClsDecls. + +Note [Keeping scoped variables in order: Explicit] discusses how this +check works for `forall x y z.` written in a type. + -} -- | Check a list of binders to see if they make a valid telescope. @@ -2089,7 +2117,7 @@ checkValidTelescope tvbs user_tyvars , extra ] where tvs = binderVars tvbs - (_, sorted_tidied_tvs) = tidyVarBndrs emptyTidyEnv (toposortTyVars tvs) + (_, sorted_tidied_tvs) = tidyVarBndrs emptyTidyEnv (scopedSort tvs) (_, bad_tvbs) = foldl add_one (mkVarSet tvs, []) tvbs @@ -2106,11 +2134,11 @@ checkValidTelescope tvbs user_tyvars fkvs = tyCoVarsOfType (tyVarKind tv) bad' = bad_bndrs `delVarSet` tv - extra | all (isVisibleArgFlag . tyConBinderArgFlag) bad_tvbs - = empty - | otherwise - = text "NB: Implicitly declared variables come before others." - + extra + | any isInvisibleTyConBinder tvbs + = text "NB: Implicitly declared variables come before others." + | otherwise + = empty {- ************************************************************************ |