diff options
-rw-r--r-- | compiler/typecheck/TcHsType.hs | 411 | ||||
-rw-r--r-- | compiler/typecheck/TcMType.hs | 10 | ||||
-rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 107 | ||||
-rw-r--r-- | compiler/typecheck/TcValidity.hs | 1 | ||||
-rw-r--r-- | compiler/types/TyCon.hs | 63 | ||||
-rw-r--r-- | testsuite/tests/ghci/scripts/T7873.stderr | 9 | ||||
-rw-r--r-- | testsuite/tests/polykinds/T11821.hs | 31 | ||||
-rw-r--r-- | testsuite/tests/polykinds/all.T | 1 |
8 files changed, 264 insertions, 369 deletions
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index c5333994bb..49cc6a892c 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -20,7 +20,7 @@ module TcHsType ( tcImplicitTKBndrs, tcImplicitTKBndrsType, tcExplicitTKBndrs, -- Type checking type and class decls - kcLookupKind, kcTyClTyVars, tcTyClTyVars, + kcLookupTcTyCon, kcTyClTyVars, tcTyClTyVars, tcHsConArgType, tcDataKindSig, -- Kind-checking types @@ -1200,18 +1200,17 @@ tcWildCardBinders wcs thing_inside -- HsDecls. -- -- This function does not do telescope checking. -kcHsTyVarBndrs :: Bool -- ^ True <=> the decl being checked has a CUSK +kcHsTyVarBndrs :: Name -- ^ of the thing being checked + -> Bool -- ^ True <=> the decl being checked has a CUSK -> Bool -- ^ True <=> the decl is an open type/data family -> Bool -- ^ True <=> all the hsq_implicit are *kind* vars -- (will give these kind * if -XNoTypeInType) -> LHsQTyVars Name -> TcM (Kind, r) -- ^ the result kind, possibly with other info - -> TcM ([TcTyBinder], TcKind, r) - -- ^ The bound variables in the kind, the result kind, - -- with the other info. - -- Always returns Named binders; sort out Named vs. Anon - -- yourself. -kcHsTyVarBndrs cusk open_fam all_kind_vars + -> TcM (Bool -> TcTyCon, r) + -- ^ a way to make a TcTyCon, with the other info. + -- The Bool says whether the tycon can be unsaturated. +kcHsTyVarBndrs name cusk open_fam all_kind_vars (HsQTvs { hsq_implicit = kv_ns, hsq_explicit = hs_tvs , hsq_dependent = dep_names }) thing_inside | cusk @@ -1235,17 +1234,40 @@ kcHsTyVarBndrs cusk open_fam all_kind_vars ; when (not (null meta_tvs)) $ report_non_cusk_tvs (qkvs ++ tvs) - ; return ( mkNamedBinders Specified good_tvs ++ binders - , res_kind, stuff ) }} + -- if any of the scoped_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 tycon_tyvars = good_tvs ++ tvs + all_mentioned_tvs = mapUnionVarSet (tyCoVarsOfType . tyVarKind) + tycon_tyvars + `unionVarSet` tyCoVarsOfType res_kind + unmentioned_kvs = filterOut (`elemVarSet` all_mentioned_tvs) + scoped_kvs + ; reportFloatingKvs name tycon_tyvars unmentioned_kvs + + ; let final_binders = mkNamedBinders Specified good_tvs ++ binders + mk_tctc unsat = mkTcTyCon name tycon_tyvars + final_binders res_kind + unsat (scoped_kvs ++ tvs) + -- the tvs contain the binders already + -- in scope from an enclosing class, but + -- re-adding tvs to the env't doesn't cause + -- harm + ; return ( mk_tctc, stuff ) }} | otherwise = do { kv_kinds <- mk_kv_kinds ; scoped_kvs <- zipWithM newSigTyVar kv_ns kv_kinds -- the names must line up in splitTelescopeTvs - ; (_, binders, res_kind, stuff) + ; (tvs, binders, res_kind, stuff) <- tcExtendTyVarEnv2 (kv_ns `zip` scoped_kvs) $ bind_telescope hs_tvs thing_inside - ; return (binders, res_kind, stuff) } + ; let -- NB: Don't add scoped_kvs to tyConTyVars, because they + -- must remain lined up with the binders + mk_tctc unsat = mkTcTyCon name tvs + binders res_kind unsat + (scoped_kvs ++ tvs) + ; return (mk_tctc, stuff) } where -- if -XNoTypeInType and we know all the implicits are kind vars, -- just give the kind *. This prevents test @@ -1486,71 +1508,6 @@ look through unification variables! Hence using zonked_kinds when forming tvs'. -Note [Typechecking telescopes] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The function tcTyClTyVars has to bind the scoped type and kind -variables in a telescope. For example: - -class Foo k (t :: Proxy k -> k2) where ... - -By the time [kt]cTyClTyVars is called, we know *something* about the kind of Foo, -at least that it has the form - - Foo :: forall (k2 :: mk2). forall (k :: mk1) -> (Proxy mk1 k -> k2) -> Constraint - -if it has a CUSK (Foo does not, in point of fact) or - - Foo :: forall (k :: mk1) -> (Proxy mk1 k -> k2) -> Constraint - -if it does not, where mk1 and mk2 are meta-kind variables (mk1, mk2 :: *). - -When calling tcTyClTyVars, this kind is further generalized w.r.t. any -free variables appearing in mk1 or mk2. So, mk_tvs must handle -that possibility. Perhaps we discover that mk1 := Maybe k3 and mk2 := *, -so we have - -Foo :: forall (k3 :: *). forall (k2 :: *). forall (k :: Maybe k3) -> - (Proxy (Maybe k3) k -> k2) -> Constraint - -We now have several sorts of variables to think about: -1) The variable k3 is not mentioned in the source at all. It is neither - explicitly bound nor ever used. It is *not* a scoped kind variable, - and should not be bound when type-checking the scope of the telescope. - -2) The variable k2 is mentioned in the source, but it is not explicitly - bound. It *is* a scoped kind variable, and will appear in the - hsq_implicit field of a LHsTyVarBndrs. - - 2a) In the non-CUSK case, these variables won't have been generalized - yet and don't appear in the looked-up kind. So we just return these - in a NameSet. - -3) The variable k is mentioned in the source with an explicit binding. - It *is* a scoped type variable, and will appear in the - hsq_explicit field of a LHsTyVarBndrs. - -4) The variable t is bound in the source, but it is never mentioned later - in the kind. It *is* a scoped variable (it can appear in the telescope - scope, even though it is non-dependent), and will appear in the - hsq_explicit field of a LHsTyVarBndrs. - -splitTelescopeTvs walks through the output of a splitPiTys on the -telescope head's kind (Foo, in our example), creating a list of tyvars -to be bound within the telescope scope. It must simultaneously walk -through the hsq_implicit and hsq_explicit fields of a LHsTyVarBndrs. -Comments in the code refer back to the cases in this Note. - -Cases (1) and (2) can be mixed together, but these cases must appear before -cases (3) and (4) (the implicitly bound vars always precede the explicitly -bound ones). So, we handle the lists in two stages (mk_tvs and -mk_tvs2). - -As a further wrinkle, it's possible that the variables in case (2) have -been reordered. This is because hsq_implicit is ordered by the renamer, -but there may be dependency among the variables. Of course, the order in -the kind must take dependency into account. So we use a NameSet to keep -these straightened out. - Note [Free-floating kind vars] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider @@ -1576,174 +1533,43 @@ of a tycon tyvar. But it isn't. Why accept S? Because kind inference tells us that a has kind k, so it's all OK. -Here's the approach: in the first pass ("kind-checking") we just bring -k into scope. In the second pass, we certainly hope that k has been -integrated into the type's (generalized) kind, and so it should be found -by splitTelescopeTvs. If it's not, then we must have a definition like -T, and we reject. (But see Note [Tiresome kind checking] about some extra -processing necessary in the second pass.) - -Note [Tiresome kind matching] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Because of the use of SigTvs in kind inference (see #11203, for example) -sometimes kind variables come into tcTyClTyVars (the second, desugaring -pass in TcTyClDecls) with the wrong names. The best way to fix this up -is just to unify the kinds, again. So we return HsKind/Kind pairs from -splitTelescopeTvs that can get unified in tcTyClTyVars, but only if there -are kind vars the didn't link up in splitTelescopeTvs. +Our approach depends on whether or not the datatype has a CUSK. + +Non-CUSK: In the first pass (kcTyClTyVars) we just bring +k into scope. In the second pass (tcTyClTyVars), +we check to make sure that k has been unified with some other variable +(or generalized over, making k into a skolem). If it hasn't been, then +it must be a free-floating kind var. Error. + +CUSK: When we determine the tycon's final, never-to-be-changed kind +in kcHsTyVarBndrs, we check to make sure all implicitly-bound kind +vars are indeed mentioned in a kind somewhere. If not, error. -} -------------------- -- getInitialKind has made a suitably-shaped kind for the type or class --- Unpack it, and attribute those kinds to the type variables --- Extend the env with bindings for the tyvars, taken from --- the kind of the tycon/class. Give it to the thing inside, and --- check the result kind matches -kcLookupKind :: Name -> TcM ([TyBinder], Kind) -kcLookupKind nm +-- Look it up in the local environment. This is used only for tycons +-- that we're currently type-checking, so we're sure to find a TcTyCon. +kcLookupTcTyCon :: Name -> TcM TcTyCon +kcLookupTcTyCon nm = do { tc_ty_thing <- tcLookup nm - ; case tc_ty_thing of - ATcTyCon tc -> return (tyConBinders tc, tyConResKind tc) - AGlobal (ATyCon tc) -> return (tyConBinders tc, tyConResKind tc) - _ -> pprPanic "kcLookupKind" (ppr tc_ty_thing) } - --- See Note [Typechecking telescopes] -splitTelescopeTvs :: [TyBinder] -- telescope binders - -> LHsQTyVars Name - -> ( [TyVar] -- scoped type variables - , NameSet -- ungeneralized implicit variables (case 2a) - , [TyVar] -- implicit type variables (cases 1 & 2) - , [TyVar] -- explicit type variables (cases 3 & 4) - , [(LHsKind Name, Kind)] ) -- see Note [Tiresome kind matching] -splitTelescopeTvs bndrs tvbs@(HsQTvs { hsq_implicit = hs_kvs - , hsq_explicit = hs_tvs }) - = let (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, kind_matches) - = mk_tvs [] [] bndrs (mkNameSet hs_kvs) hs_tvs - in - (scoped_tvs, non_cusk_imp_names, imp_tvs, exp_tvs, kind_matches) - where - mk_tvs :: [TyVar] -- scoped tv accum (reversed) - -> [TyVar] -- implicit tv accum (reversed) - -> [TyBinder] - -> NameSet -- implicit variables - -> [LHsTyVarBndr Name] -- explicit variables - -> ( [TyVar] -- the tyvars to be lexically bound - , NameSet -- Case 2a names - , [TyVar] -- implicit tyvars - , [TyVar] -- explicit tyvars - , [(LHsKind Name, Kind)] ) -- tiresome kind matches - mk_tvs scoped_tv_acc imp_tv_acc (bndr : bndrs) all_hs_kvs all_hs_tvs - | Just tv <- binderVar_maybe bndr - , isInvisibleBinder bndr - , let tv_name = getName tv - , tv_name `elemNameSet` all_hs_kvs - = mk_tvs (tv : scoped_tv_acc) (tv : imp_tv_acc) - bndrs (all_hs_kvs `delFromNameSet` tv_name) all_hs_tvs -- Case (2) - - | Just tv <- binderVar_maybe bndr - , isInvisibleBinder bndr - = mk_tvs scoped_tv_acc (tv : imp_tv_acc) - bndrs all_hs_kvs all_hs_tvs -- Case (1) - - -- there may actually still be some hs_kvs, if we're kind checking - -- a non-CUSK. The kinds *aren't* generalized, so we won't see them - -- here. - mk_tvs scoped_tv_acc imp_tv_acc all_bndrs all_hs_kvs all_hs_tvs - = let (scoped, exp_tvs, kind_matches) - = mk_tvs2 scoped_tv_acc [] [] all_bndrs all_hs_tvs in - (scoped, all_hs_kvs, reverse imp_tv_acc, exp_tvs, kind_matches) - -- no more Case (1) or (2) - - -- This can't handle Case (1) or Case (2) from [Typechecking telescopes] - mk_tvs2 :: [TyVar] - -> [TyVar] -- new parameter: explicit tv accum (reversed) - -> [(LHsKind Name, Kind)] -- tiresome kind matches accum - -> [TyBinder] - -> [LHsTyVarBndr Name] - -> ( [TyVar] - , [TyVar] -- explicit tvs only - , [(LHsKind Name, Kind)] ) -- tiresome kind matches - mk_tvs2 scoped_tv_acc exp_tv_acc kind_match_acc (bndr : bndrs) (hs_tv : hs_tvs) - | Just tv <- binderVar_maybe bndr - = ASSERT2( isVisibleBinder bndr, err_doc ) - ASSERT( getName tv == hsLTyVarName hs_tv ) - mk_tvs2 (tv : scoped_tv_acc) (tv : exp_tv_acc) kind_match_acc' bndrs hs_tvs - -- Case (3) - - | otherwise - = ASSERT( isVisibleBinder bndr ) - let tv = mkTyVar (hsLTyVarName hs_tv) (binderType bndr) in - mk_tvs2 (tv : scoped_tv_acc) (tv : exp_tv_acc) kind_match_acc' bndrs hs_tvs - -- Case (4) - where - err_doc = vcat [ ppr (bndr : bndrs) - , ppr (hs_tv : hs_tvs) - , ppr tvbs ] - - kind_match_acc' = case hs_tv of - L _ (UserTyVar {}) -> kind_match_acc - L _ (KindedTyVar _ hs_kind) -> (hs_kind, kind) : kind_match_acc - where kind = binderType bndr - - mk_tvs2 scoped_tv_acc exp_tv_acc kind_match_acc [] [] -- All done! - = ( reverse scoped_tv_acc - , reverse exp_tv_acc - , kind_match_acc ) -- no need to reverse; it's not ordered - - mk_tvs2 _ _ _ all_bndrs all_hs_tvs - = pprPanic "splitTelescopeTvs 2" (vcat [ ppr all_bndrs - , ppr all_hs_tvs ]) - + ; return $ case tc_ty_thing of + ATcTyCon tc -> tc + _ -> pprPanic "kcLookupTcTyCon" (ppr tc_ty_thing) } ----------------------- --- | "Kind check" the tyvars to a tycon. This is used during the "kind-checking" +-- | Bring tycon tyvars into scope. This is used during the "kind-checking" -- pass in TcTyClsDecls. (Never in getInitialKind, never in the --- "type-checking"/desugaring pass.) It works only for LHsQTyVars associated --- with a tycon, whose kind is known (partially) via getInitialKinds. +-- "type-checking"/desugaring pass.) -- Never emits constraints, though the thing_inside might. -kcTyClTyVars :: Name -- ^ of the tycon - -> LHsQTyVars Name - -> TcM a -> TcM a -kcTyClTyVars tycon hs_tvs thing_inside - = do { (binders, res_kind) <- kcLookupKind tycon - ; let (scoped_tvs, non_cusk_kv_name_set, all_kvs, all_tvs, _) - = splitTelescopeTvs binders hs_tvs - ; traceTc "kcTyClTyVars splitTelescopeTvs:" - (vcat [ text "Tycon:" <+> ppr tycon - , text "Binders:" <+> ppr binders - , text "res_kind:" <+> ppr res_kind - , text "hs_tvs:" <+> ppr hs_tvs - , text "scoped tvs:" <+> pprWithCommas pprTvBndr scoped_tvs - , text "implicit tvs:" <+> pprWithCommas pprTvBndr all_kvs - , text "explicit tvs:" <+> pprWithCommas pprTvBndr all_tvs - , text "non-CUSK kvs:" <+> ppr non_cusk_kv_name_set ] ) - - -- need to look up the non-cusk kvs in order to get their - -- kinds right, in case the kinds were informed by - -- the getInitialKinds pass - ; let non_cusk_kv_names = nameSetElems non_cusk_kv_name_set - free_kvs = tyCoVarsOfTypes $ - map tyVarKind (all_kvs ++ all_tvs) - mk_kv kv_name = case lookupVarSetByName free_kvs kv_name of - Just kv -> return kv - Nothing -> - -- this kv isn't mentioned in the - -- LHsQTyVars at all. But maybe - -- it's mentioned in the body - -- In any case, just gin up a - -- meta-kind for it - do { kv_kind <- newMetaKindVar - ; return (new_skolem_tv kv_name kv_kind) } - ; non_cusk_kvs <- mapM mk_kv non_cusk_kv_names - - -- The non_cusk_kvs are still scoped; they are mentioned by - -- name by the user - ; tcExtendTyVarEnv (non_cusk_kvs ++ scoped_tvs) $ - thing_inside } - -tcTyClTyVars :: Name -> LHsQTyVars Name -- LHS of the type or class decl - -> ([TyVar] -> [TyVar] -> [TyBinder] -> Kind -> TcM a) -> TcM a +kcTyClTyVars :: Name -> TcM a -> TcM a +kcTyClTyVars tycon_name thing_inside + = do { tycon <- kcLookupTcTyCon tycon_name + ; tcExtendTyVarEnv (tcTyConScopedTyVars tycon) $ thing_inside } + +tcTyClTyVars :: Name + -> ([TyVar] -> [TyBinder] -> Kind -> TcM a) -> TcM a -- ^ Used for the type variables of a type or class decl -- on the second full pass (type-checking/desugaring) in TcTyClDecls. -- This is *not* used in the initial-kind run, nor in the "kind-checking" pass. @@ -1752,7 +1578,7 @@ tcTyClTyVars :: Name -> LHsQTyVars Name -- LHS of the type or class decl -- (tcTyClTyVars T [a,b] thing_inside) -- where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> * -- calls thing_inside with arguments --- [k1,k2] [a,b] [k1:*, k2:*, a:k1 -> *, b:k1] (k2 -> *) +-- [k1,k2,a,b] [k1:*, k2:*, Anon (k1 -> *), Anon k1] (k2 -> *) -- having also extended the type environment with bindings -- for k1,k2,a,b -- @@ -1760,69 +1586,27 @@ tcTyClTyVars :: Name -> LHsQTyVars Name -- LHS of the type or class decl -- -- The LHsTyVarBndrs is always user-written, and the full, generalised -- kind of the tycon is available in the local env. -tcTyClTyVars tycon hs_tvs thing_inside - = do { (binders, res_kind) <- kcLookupKind tycon - ; let ( scoped_tvs, float_kv_name_set, all_kvs - , all_tvs, kind_matches ) - = splitTelescopeTvs binders hs_tvs - ; traceTc "tcTyClTyVars splitTelescopeTvs:" - (vcat [ text "Tycon:" <+> ppr tycon - , text "Binders:" <+> ppr binders - , text "res_kind:" <+> ppr res_kind - , text "hs_tvs.hsq_implicit:" <+> ppr (hsq_implicit hs_tvs) - , text "hs_tvs.hsq_explicit:" <+> ppr (hsq_explicit hs_tvs) - , text "scoped tvs:" <+> pprWithCommas pprTvBndr scoped_tvs - , text "implicit tvs:" <+> pprWithCommas pprTvBndr all_kvs - , text "explicit tvs:" <+> pprWithCommas pprTvBndr all_tvs - , text "floating kvs:" <+> ppr float_kv_name_set - , text "Tiresome kind matches:" <+> ppr kind_matches ] ) - - ; float_kvs <- deal_with_float_kvs float_kv_name_set kind_matches - scoped_tvs all_tvs - - ; tcExtendTyVarEnv (float_kvs ++ scoped_tvs) $ - -- the float_kvs are already in the all_kvs - thing_inside all_kvs all_tvs binders res_kind } +tcTyClTyVars tycon_name thing_inside + = do { tycon <- kcLookupTcTyCon tycon_name + + ; let scoped_tvs = tcTyConScopedTyVars tycon + + -- these are all zonked: + tkvs = tyConTyVars tycon + binders = tyConBinders tycon + res_kind = tyConResKind tycon + + -- See Note [Free-floating kind vars] + ; zonked_scoped_tvs <- mapM zonkTcTyVarToTyVar scoped_tvs + ; let still_sig_tvs = filter isSigTyVar zonked_scoped_tvs + ; checkNoErrs $ reportFloatingKvs tycon_name + zonked_scoped_tvs still_sig_tvs + + -- Add the *unzonked* tyvars to the env't, because those + -- are the ones mentioned in the source. + ; tcExtendTyVarEnv scoped_tvs $ + thing_inside tkvs binders res_kind } where - -- See Note [Free-floating kind vars] - deal_with_float_kvs float_kv_name_set kind_matches scoped_tvs all_tvs - | isEmptyNameSet float_kv_name_set - = return [] - - | otherwise - = do { -- the floating kvs might just be renamed - -- see Note [Tiresome kind matching] - ; let float_kv_names = nameSetElems float_kv_name_set - ; float_kv_kinds <- mapM (const newMetaKindVar) float_kv_names - ; float_kvs <- zipWithM newSigTyVar float_kv_names float_kv_kinds - ; discardResult $ - tcExtendTyVarEnv (float_kvs ++ scoped_tvs) $ - solveEqualities $ - forM kind_matches $ \ (hs_kind, kind) -> - do { tc_kind <- tcLHsKind hs_kind - ; unifyKind noThing tc_kind kind } - - ; zonked_kvs <- mapM ((return . tcGetTyVar "tcTyClTyVars") <=< zonkTcTyVar) - float_kvs - ; let (still_sigs, matched_up) = partition isSigTyVar zonked_kvs - -- the still_sigs didn't match with anything. They must be - -- "free-floating", as in Note [Free-floating kind vars] - ; checkNoErrs $ mapM_ (report_floating_kv all_tvs) still_sigs - - -- the matched up kvs are proper scoped kvs. - ; return matched_up } - - report_floating_kv all_tvs kv - = addErr $ - vcat [ text "Kind variable" <+> quotes (ppr kv) <+> - text "is implicitly bound in datatype" - , quotes (ppr tycon) <> comma <+> - text "but does not appear as the kind of any" - , text "of its type variables. Perhaps you meant" - , text "to bind it (with TypeInType) explicitly somewhere?" - , if null all_tvs then empty else - hang (text "Type variables with inferred kinds:") - 2 (pprTvBndrs all_tvs) ] ----------------------------------- tcDataKindSig :: Kind -> TcM ([TyVar], [TyBinder], Kind) @@ -2151,3 +1935,34 @@ funAppCtxt fun arg arg_no = hang (hsep [ text "In the", speakNth arg_no, ptext (sLit "argument of"), quotes (ppr fun) <> text ", namely"]) 2 (quotes (ppr arg)) + +-- See Note [Free-floating kind vars] +reportFloatingKvs :: Name -- of the tycon + -> [TcTyVar] -- all tyvars, not necessarily zonked + -> [TcTyVar] -- floating tyvars + -> TcM () +reportFloatingKvs tycon_name all_tvs bad_tvs + = unless (null bad_tvs) $ -- don't bother zonking if there's no error + do { all_tvs <- mapM zonkTcTyVarToTyVar all_tvs + ; bad_tvs <- mapM zonkTcTyVarToTyVar bad_tvs + ; let (tidy_env, tidy_all_tvs) = tidyOpenTyCoVars emptyTidyEnv all_tvs + tidy_bad_tvs = map (tidyTyVarOcc tidy_env) bad_tvs + ; typeintype <- xoptM LangExt.TypeInType + ; mapM_ (report typeintype tidy_all_tvs) tidy_bad_tvs } + where + report typeintype tidy_all_tvs tidy_bad_tv + = addErr $ + vcat [ text "Kind variable" <+> quotes (ppr tidy_bad_tv) <+> + text "is implicitly bound in datatype" + , quotes (ppr tycon_name) <> comma <+> + text "but does not appear as the kind of any" + , text "of its type variables. Perhaps you meant" + , text "to bind it" <+> ppWhen (not typeintype) + (text "(with TypeInType)") <+> + text "explicitly somewhere?" + , ppWhen (not (null tidy_all_tvs)) $ + hang (text "Type variables with inferred kinds:") + 2 (ppr_tv_bndrs tidy_all_tvs) ] + + ppr_tv_bndrs tvs = sep (map pp_tv tvs) + pp_tv tv = parens (ppr tv <+> dcolon <+> ppr (tyVarKind tv)) diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index c2b3f0267b..861fa10ce7 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -67,7 +67,8 @@ module TcMType ( mkTypeErrorThing, mkTypeErrorThingArgs, tidyEvVar, tidyCt, tidySkolemInfo, skolemiseUnboundMetaTyVar, - zonkTcTyVar, zonkTcTyVars, zonkTyCoVarsAndFV, zonkTcTypeAndFV, + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTyVar, + zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkTyCoVarsAndFVList, zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars, zonkQuantifiedTyVar, zonkQuantifiedTyVarOrType, @@ -1406,6 +1407,13 @@ zonkTcTyVar tv zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv ; return (mkTyVarTy z_tv) } +-- Variant that assumes that any result of zonking is still a TyVar. +-- Should be used only on skolems and SigTvs +zonkTcTyVarToTyVar :: TcTyVar -> TcM TcTyVar +zonkTcTyVarToTyVar tv + = do { ty <- zonkTcTyVar tv + ; return (tcGetTyVar "zonkTcTyVarToVar" ty) } + {- %************************************************************************ %* * diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 6cd8bbb9b6..c467c32894 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -349,18 +349,22 @@ kcTyClGroup decls _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env) kc_binders = tyConBinders tc kc_res_kind = tyConResKind tc + kc_tyvars = tyConTyVars tc ; kvs <- kindGeneralize (mkForAllTys kc_binders kc_res_kind) ; (kc_binders', kc_res_kind') <- zonkTcKindToKind kc_binders kc_res_kind + ; kc_tyvars <- mapM zonkTcTyVarToTyVar kc_tyvars -- Make sure kc_kind' has the final, zonked kind variables ; traceTc "Generalise kind" $ vcat [ ppr name, ppr kc_binders, ppr kc_res_kind - , ppr kvs, ppr kc_binders', ppr kc_res_kind' ] + , ppr kvs, ppr kc_binders', ppr kc_res_kind' + , ppr kc_tyvars, ppr (tcTyConScopedTyVars tc)] - ; return (mkTcTyCon name + ; return (mkTcTyCon name (kvs ++ kc_tyvars) (mkNamedBinders Invisible kvs ++ kc_binders') kc_res_kind' - (mightBeUnsaturatedTyCon tc)) } + (mightBeUnsaturatedTyCon tc) + (tcTyConScopedTyVars tc)) } generaliseTCD :: TcTypeEnv -> LTyClDecl Name -> TcM [TcTyCon] @@ -434,13 +438,11 @@ getInitialKind :: TyClDecl Name -- No family instances are passed to getInitialKinds getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats }) - = do { (cl_binders, cl_kind, inner_prs) <- - kcHsTyVarBndrs cusk False True ktvs $ + = do { (mk_tctc, inner_prs) <- + kcHsTyVarBndrs name cusk False True ktvs $ do { inner_prs <- getFamDeclInitialKinds (Just cusk) ats ; return (constraintKind, inner_prs) } - ; cl_binders <- mapM zonkTcTyBinder cl_binders - ; cl_kind <- zonkTcType cl_kind - ; let main_pr = mkTcTyConPair (mkTcTyCon name cl_binders cl_kind True) + ; let main_pr = mkTcTyConPair (mk_tctc True) ; return (main_pr : inner_prs) } where cusk = hsDeclHasCusk decl @@ -449,15 +451,13 @@ getInitialKind decl@(DataDecl { tcdLName = L _ name , tcdTyVars = ktvs , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig , dd_cons = cons } }) - = do { (decl_binders, decl_kind, _) <- - kcHsTyVarBndrs (hsDeclHasCusk decl) False True ktvs $ + = do { (mk_tctc, _) <- + kcHsTyVarBndrs name (hsDeclHasCusk decl) False True ktvs $ do { res_k <- case m_sig of Just ksig -> tcLHsKind ksig Nothing -> return liftedTypeKind ; return (res_k, ()) } - ; decl_binders <- mapM zonkTcTyBinder decl_binders - ; decl_kind <- zonkTcType decl_kind - ; let main_pr = mkTcTyConPair (mkTcTyCon name decl_binders decl_kind True) + ; let main_pr = mkTcTyConPair (mk_tctc True) inner_prs = [ (unLoc con, APromotionErr RecDataConPE) | L _ con' <- cons, con <- getConNames con' ] ; return (main_pr : inner_prs) } @@ -483,8 +483,8 @@ getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName = L _ name , fdTyVars = ktvs , fdResultSig = L _ resultSig , fdInfo = info }) - = do { (fam_binders, fam_kind, _) <- - kcHsTyVarBndrs cusk open True ktvs $ + = do { (mk_tctc, _) <- + kcHsTyVarBndrs name cusk open True ktvs $ do { res_k <- case resultSig of KindSig ki -> tcLHsKind ki TyVarSig (L _ (KindedTyVar _ ki)) -> tcLHsKind ki @@ -494,9 +494,7 @@ getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName = L _ name -- by default | otherwise -> newMetaKindVar ; return (res_k, ()) } - ; fam_binders <- mapM zonkTcTyBinder fam_binders - ; fam_kind <- zonkTcType fam_kind - ; return [ mkTcTyConPair (mkTcTyCon name fam_binders fam_kind unsat) ] } + ; return [ mkTcTyConPair (mk_tctc unsat) ] } where cusk = famDeclHasCusk mb_cusk decl (open, unsat) = case info of @@ -526,13 +524,13 @@ kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name , tcdRhs = rhs }) -- Returns a possibly-unzonked kind = tcAddDeclCtxt decl $ - do { (syn_binders, syn_kind, _) <- - kcHsTyVarBndrs (hsDeclHasCusk decl) False True hs_tvs $ + do { (mk_tctc, _) <- + kcHsTyVarBndrs name (hsDeclHasCusk decl) False True hs_tvs $ do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs)) ; (_, rhs_kind) <- tcLHsType rhs ; traceTc "kcd2" (ppr name) ; return (rhs_kind, ()) } - ; return (mkTcTyCon name syn_binders syn_kind False) } + ; return (mk_tctc False) } kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl) ------------------------------------------------------------------------ @@ -547,7 +545,7 @@ kcTyClDecl :: TyClDecl Name -> TcM () -- result kind signature have already been dealt with -- by getInitialKind, so we can ignore them here. -kcTyClDecl (DataDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdDataDefn = defn }) +kcTyClDecl (DataDecl { tcdLName = L _ name, tcdDataDefn = defn }) | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn = mapM_ (wrapLocM kcConDecl) cons -- hs_tvs and dd_kindSig already dealt with in getInitialKind @@ -558,15 +556,15 @@ kcTyClDecl (DataDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdDataDefn = de -- (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn - = kcTyClTyVars name hs_tvs $ + = kcTyClTyVars name $ do { _ <- tcHsContext ctxt ; mapM_ (wrapLocM kcConDecl) cons } kcTyClDecl decl@(SynDecl {}) = pprPanic "kcTyClDecl" (ppr decl) -kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs - , tcdCtxt = ctxt, tcdSigs = sigs }) - = kcTyClTyVars name hs_tvs $ +kcTyClDecl (ClassDecl { tcdLName = L _ name + , tcdCtxt = ctxt, tcdSigs = sigs }) + = kcTyClTyVars name $ do { _ <- tcHsContext ctxt ; mapM_ (wrapLocM kc_sig) sigs } where @@ -574,18 +572,13 @@ kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs kc_sig _ = return () kcTyClDecl (FamDecl (FamilyDecl { fdLName = L _ fam_tc_name - , fdTyVars = hs_tvs , fdInfo = fd_info })) -- closed type families look at their equations, but other families don't -- do anything here = case fd_info of ClosedTypeFamily (Just eqns) -> - do { (tc_binders, tc_res_kind) <- kcLookupKind fam_tc_name - ; let fam_tc_shape = ( fam_tc_name - , length $ hsQTvExplicit hs_tvs - , tc_binders - , tc_res_kind ) - ; mapM_ (kcTyFamInstEqn fam_tc_shape) eqns } + do { fam_tc <- kcLookupTcTyCon fam_tc_name + ; mapM_ (kcTyFamInstEqn (famTyConShape fam_tc)) eqns } _ -> return () ------------------- @@ -596,7 +589,8 @@ kcConDecl (ConDeclH98 { con_name = name, con_qvars = ex_tvs -- the 'False' says that the existentials don't have a CUSK, as the -- concept doesn't really apply here. We just need to bring the variables -- into scope. - do { _ <- kcHsTyVarBndrs False False False ((fromMaybe emptyLHsQTvs ex_tvs)) $ + do { _ <- kcHsTyVarBndrs (unLoc name) False False False + ((fromMaybe emptyLHsQTvs ex_tvs)) $ do { _ <- tcHsContext (fromMaybe (noLoc []) ex_ctxt) ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details) ; return (panic "kcConDecl", ()) } @@ -729,32 +723,32 @@ tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd }) -- "type" synonym declaration tcTyClDecl1 _parent rec_info - (SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs }) + (SynDecl { tcdLName = L _ tc_name, tcdRhs = rhs }) = ASSERT( isNothing _parent ) - tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind -> - tcTySynRhs rec_info tc_name (kvs' ++ tvs') binders res_kind rhs + tcTyClTyVars tc_name $ \ tkvs' binders res_kind -> + tcTySynRhs rec_info tc_name tkvs' binders res_kind rhs -- "data/newtype" declaration tcTyClDecl1 _parent rec_info - (DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn }) + (DataDecl { tcdLName = L _ tc_name, tcdDataDefn = defn }) = ASSERT( isNothing _parent ) - tcTyClTyVars tc_name tvs $ \ kvs' tvs' tycon_binders res_kind -> - tcDataDefn rec_info tc_name (kvs' ++ tvs') tycon_binders res_kind defn + tcTyClTyVars tc_name $ \ tkvs' tycon_binders res_kind -> + tcDataDefn rec_info tc_name tkvs' tycon_binders res_kind defn tcTyClDecl1 _parent rec_info - (ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs + (ClassDecl { tcdLName = L _ class_name , tcdCtxt = ctxt, tcdMeths = meths , tcdFDs = fundeps, tcdSigs = sigs , tcdATs = ats, tcdATDefs = at_defs }) = ASSERT( isNothing _parent ) do { clas <- fixM $ \ clas -> - tcTyClTyVars class_name tvs $ \ kvs' tvs' binders res_kind -> + tcTyClTyVars class_name $ \ tkvs' binders res_kind -> do { MASSERT( isConstraintKind res_kind ) -- This little knot is just so we can get -- hold of the name of the class TyCon, which we -- need to look up its recursiveness - ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr kvs' $$ - ppr tvs' $$ ppr binders) + ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr tkvs' $$ + ppr binders) ; let tycon_name = tyConName (classTyCon clas) tc_isrec = rti_is_rec rec_info tycon_name roles = rti_roles rec_info tycon_name @@ -767,10 +761,10 @@ tcTyClDecl1 _parent rec_info ; at_stuff <- tcClassATs class_name clas ats at_defs ; mindef <- tcClassMinimalDef class_name sigs sig_stuff ; clas <- buildClass - class_name (kvs' ++ tvs') roles ctxt' binders + class_name tkvs' roles ctxt' binders fds' at_stuff sig_stuff mindef tc_isrec - ; traceTc "tcClassDecl" (ppr fundeps $$ ppr (kvs' ++ tvs') $$ + ; traceTc "tcClassDecl" (ppr fundeps $$ ppr tkvs' $$ ppr fds') ; return clas } @@ -785,12 +779,12 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na , fdTyVars = tvs, fdResultSig = L _ sig , fdInjectivityAnn = inj }) | DataFamily <- fam_info - = tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind -> do + = tcTyClTyVars tc_name $ \ tkvs' binders res_kind -> do { traceTc "data family:" (ppr tc_name) ; checkFamFlag tc_name ; (extra_tvs, extra_binders, real_res_kind) <- tcDataKindSig res_kind ; tc_rep_name <- newTyConRepName tc_name - ; let final_tvs = (kvs' ++ tvs') `chkAppend` extra_tvs -- we may not need these + ; let final_tvs = tkvs' `chkAppend` extra_tvs -- we may not need these tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders) real_res_kind final_tvs (resultVariableName sig) @@ -799,12 +793,11 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na ; return tycon } | OpenTypeFamily <- fam_info - = tcTyClTyVars tc_name tvs $ \ kvs' tvs' binders res_kind -> do + = tcTyClTyVars tc_name $ \ tkvs' binders res_kind -> do { traceTc "open type family:" (ppr tc_name) ; checkFamFlag tc_name - ; let all_tvs = kvs' ++ tvs' - ; inj' <- tcInjectivity all_tvs inj - ; let tycon = mkFamilyTyCon tc_name binders res_kind all_tvs + ; inj' <- tcInjectivity tkvs' inj + ; let tycon = mkFamilyTyCon tc_name binders res_kind tkvs' (resultVariableName sig) OpenSynFamilyTyCon parent inj' ; return tycon } @@ -816,11 +809,10 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na -- the variables in the header scope only over the injectivity -- declaration but this is not involved here ; (tvs', inj', binders, res_kind) - <- tcTyClTyVars tc_name tvs - $ \ kvs' tvs' binders res_kind -> - do { let all_tvs = kvs' ++ tvs' - ; inj' <- tcInjectivity all_tvs inj - ; return (all_tvs, inj', binders, res_kind) } + <- tcTyClTyVars tc_name + $ \ tkvs' binders res_kind -> + do { inj' <- tcInjectivity tkvs' inj + ; return (tkvs', inj', binders, res_kind) } ; checkFamFlag tc_name -- make sure we have -XTypeFamilies @@ -904,6 +896,7 @@ tcInjectivity tvs (Just (L loc (InjectivityAnn _ lInjNames))) (text "Illegal injectivity annotation" $$ text "Use TypeFamilyDependencies to allow this") ; inj_tvs <- mapM (tcLookupTyVar . unLoc) lInjNames + ; inj_tvs <- mapM zonkTcTyVarToTyVar inj_tvs -- zonk the kinds ; let inj_ktvs = filterVarSet isTyVar $ -- no injective coercion vars closeOverKinds (mkVarSet inj_tvs) ; let inj_bools = map (`elemVarSet` inj_ktvs) tvs diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 243d5d7bcb..0833243b19 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -1966,4 +1966,3 @@ allDistinctTyVars tkvs (ty : tys) Nothing -> False Just tv | tv `elemVarSet` tkvs -> False | otherwise -> allDistinctTyVars (tkvs `extendVarSet` tv) tys - diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs index 5a54690c9e..0f9f4343e4 100644 --- a/compiler/types/TyCon.hs +++ b/compiler/types/TyCon.hs @@ -85,6 +85,7 @@ module TyCon( algTcFields, tyConRuntimeRepInfo, tyConBinders, tyConResKind, + tcTyConScopedTyVars, -- ** Manipulating TyCons expandSynTyCon_maybe, @@ -599,10 +600,14 @@ data TyCon tyConUnsat :: Bool, -- ^ can this tycon be unsaturated? -- See Note [The binders/kind/arity fields of a TyCon] + tyConTyVars :: [TyVar], -- ^ The TyCon's parameterised tyvars tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind. tyConResKind :: Kind, -- ^ Result kind tyConKind :: Kind, -- ^ Kind of this TyCon - tyConArity :: Arity -- ^ Arity + tyConArity :: Arity, -- ^ Arity + + tcTyConScopedTyVars :: [TyVar] -- ^ Scoped tyvars over the + -- tycon's body. See Note [TcTyCon] } deriving Typeable @@ -953,6 +958,45 @@ so the coercion tycon CoT must have kind: T ~ [] and arity: 0 +Note [TcTyCon] +~~~~~~~~~~~~~~ +When checking a type/class declaration (in module TcTyClsDecls), we come +upon knowledge of the eventual tycon in bits and pieces. First, we use +getInitialKinds to look over the user-provided kind signature of a tycon +(including, for example, the number of parameters written to the tycon) +to get an initial shape of the tycon's kind. 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. +We then generalize to get the tycon's final, fixed kind. Finally, once +this has happened for all tycons in a mutually recursive group, we +can desugar the lot. + +For convenience, we store partially-known tycons in TcTyCons, which +might store meta-variables. These TcTyCons are stored in the local +environment in TcTyClsDecls, until the real full TyCons can be created +during desugaring. A desugared program should never have a TcTyCon. + +A challenging piece in all of this is that we end up taking three separate +passes over every declaration: one in getInitialKind (this pass look only +at the head, not the body), one in kcTyClDecls (to kind-check the body), +and a final one in tcTyClDecls (to desugar). In the latter two passes, +we need to connect the user-written type variables in an LHsQTyVars +with the variables in the tycon's inferred kind. Because the tycon might +not have a CUSK, this matching up is, in general, quite hard to do. +(Look through the git history between Dec 2015 and Apr 2016 for +TcHsType.splitTelescopeTvs!) Instead of trying, we just store the list +of type variables to bring into scope in the later passes when we create +a TcTyCon in getInitialKinds. Much easier this way! These tyvars are +brought into scope in kcTyClTyVars and tcTyClTyVars, both in TcHsType. + +It is important that the scoped type variables not be zonked, as some +scoped type variables come into existence as SigTvs. If we zonk, the +Unique will change and the user-written occurrences won't match up with +what we expect. + +In a TcTyCon, everything is zonked (except the scoped vars) after +the kind-checking pass. + ************************************************************************ * * TyConRepName @@ -1284,17 +1328,21 @@ mkTupleTyCon name binders res_kind arity tyvars con sort parent -- TcErrors sometimes calls typeKind. -- See also Note [Kind checking recursive type and class declarations] -- in TcTyClsDecls. -mkTcTyCon :: Name -> [TyBinder] -> Kind -- ^ /result/ kind only - -> Bool -- ^ Can this be unsaturated? +mkTcTyCon :: Name -> [TyVar] + -> [TyBinder] -> Kind -- ^ /result/ kind only + -> Bool -- ^ Can this be unsaturated? + -> [TyVar] -- ^ Scoped type variables, see Note [TcTyCon] -> TyCon -mkTcTyCon name binders res_kind unsat +mkTcTyCon name tvs binders res_kind unsat scoped_tvs = TcTyCon { tyConUnique = getUnique name , tyConName = name + , tyConTyVars = tvs , tyConBinders = binders , tyConResKind = res_kind , tyConKind = mkForAllTys binders res_kind , tyConUnsat = unsat - , tyConArity = length binders } + , tyConArity = length binders + , tcTyConScopedTyVars = scoped_tvs } -- | Create an unlifted primitive 'TyCon', such as @Int#@ mkPrimTyCon :: Name -> [TyBinder] @@ -1407,8 +1455,9 @@ isAbstractTyCon _ = False -- Used when recovering from errors makeTyConAbstract :: TyCon -> TyCon makeTyConAbstract tc - = mkTcTyCon (tyConName tc) (tyConBinders tc) (tyConResKind tc) - (mightBeUnsaturatedTyCon tc) + = mkTcTyCon (tyConName tc) (tyConTyVars tc) + (tyConBinders tc) (tyConResKind tc) + (mightBeUnsaturatedTyCon tc) [{- no scoped vars -}] -- | Does this 'TyCon' represent something that cannot be defined in Haskell? isPrimTyCon :: TyCon -> Bool diff --git a/testsuite/tests/ghci/scripts/T7873.stderr b/testsuite/tests/ghci/scripts/T7873.stderr index 3b6f4f64c1..ad8a55b70a 100644 --- a/testsuite/tests/ghci/scripts/T7873.stderr +++ b/testsuite/tests/ghci/scripts/T7873.stderr @@ -1,7 +1,6 @@ <interactive>:2:1: error: - • Kind variable ‘k’ is implicitly bound in datatype - ‘D1’, but does not appear as the kind of any - of its type variables. Perhaps you meant - to bind it (with TypeInType) explicitly somewhere? - • In the data declaration for ‘D1’ + Kind variable ‘k’ is implicitly bound in datatype + ‘D1’, but does not appear as the kind of any + of its type variables. Perhaps you meant + to bind it explicitly somewhere? diff --git a/testsuite/tests/polykinds/T11821.hs b/testsuite/tests/polykinds/T11821.hs new file mode 100644 index 0000000000..82efeb5f98 --- /dev/null +++ b/testsuite/tests/polykinds/T11821.hs @@ -0,0 +1,31 @@ +{-# LANGUAGE RankNTypes, DataKinds, PolyKinds, GADTs, TypeFamilies, UndecidableInstances #-} +module NotInScope where + +import Data.Proxy + +type KindOf (a :: k) = ('KProxy :: KProxy k) +data TyFun :: * -> * -> * +type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2 + +data Lgo2 l1 + l2 + l3 + (l4 :: b) + (l5 :: TyFun [a] b) + = forall (arg :: [a]) . KindOf (Apply (Lgo2 l1 l2 l3 l4) arg) ~ KindOf (Lgo l1 l2 l3 l4 arg) => + Lgo2KindInference + +data Lgo1 l1 + l2 + l3 + (l4 :: TyFun b (TyFun [a] b -> *)) + = forall (arg :: b) . KindOf (Apply (Lgo1 l1 l2 l3) arg) ~ KindOf (Lgo2 l1 l2 l3 arg) => + Lgo1KindInference + +type family Lgo f + z0 + xs0 + (a1 :: b) + (a2 :: [a]) :: b where + Lgo f z0 xs0 z '[] = z + Lgo f z0 xs0 z ('(:) x xs) = Apply (Apply (Lgo1 f z0 xs0) (Apply (Apply f z) x)) xs diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index 17d02119b1..f2e274b060 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -146,3 +146,4 @@ test('T11611', normal, compile_fail, ['']) test('T11648', normal, compile, ['']) test('T11648b', normal, compile_fail, ['']) test('KindVType', normal, compile_fail, ['']) +test('T11821', normal, compile, ['']) |