diff options
| -rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 58 | ||||
| -rw-r--r-- | compiler/typecheck/TcValidity.hs | 92 |
2 files changed, 86 insertions, 64 deletions
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 20c79bd46f..49c6082ba4 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -398,8 +398,7 @@ 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 [Bad telescopes] in -TcValidity. +kind generalisation, as described in Note [Generalisation for type constructors] However, we have to check again *after* kind generalisation, to catch something like this: @@ -555,13 +554,16 @@ kcTyClGroup decls ; 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 [Bad telescopes] in TcValidity - ; checkValidTelescope tc_binders user_tyvars empty - ; kvs <- kindGeneralize (mkTyConKind 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 @@ -576,8 +578,7 @@ kcTyClGroup decls ; tc_res_kind' <- zonkTcTypeToTypeX env tc_res_kind -- See Note [Check telescope again during generalisation] - ; let extra = text "NB: Implicitly declared variables come before others." - ; checkValidTelescope all_binders user_tyvars extra + ; checkValidTelescope all_binders user_tyvars -- Make sure tc_kind' has the final, zonked kind variables ; traceTc "Generalise kind" $ @@ -590,6 +591,49 @@ kcTyClGroup decls scoped_tvs' (tyConFlavour tc)) } +{- 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) + + 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. + +See Note [Keeping scoped variables in order: Explicit] for how this +check works for `forall x y z.` written in a type. +-} {- Note [Work out final tyConBinders] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 392c2543a6..936eed842f 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -2062,38 +2062,6 @@ 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. (We could probably figure out to put b between a and c. -But I think this is doing users a disservice, in the long run.) -(Testcase: dependent/should_fail/BadTelescope4) - -To catch these errors, we call checkValidTelescope during kind-checking -datatype declarations. This must be done *before* kind-generalization, -because kind-generalization might observe, say, T1, see that k is free -in a's kind, and generalize over it, producing nonsense. It also must -be done *after* kind-generalization, in order to catch the T2 case, which -becomes apparent only after generalizing. - -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. @@ -2104,35 +2072,45 @@ check works for `forall x y z.` written in a type. -- because k isn't in scope when a is bound. This check has to come before -- general validity checking, because once we kind-generalise, this sort -- of problem is harder to spot (as we'll generalise over the unbound --- k in a's type.) See also Note [Bad telescopes]. +-- k in a's type.) +-- +-- See Note [Generalisation for type constructors] in TcTyClsDecls for +-- data type declarations +-- and Note [Keeping scoped variables in order: Explicit] in TcHsType +-- for foralls checkValidTelescope :: [TyConBinder] -- explicit vars (zonked) -> SDoc -- original, user-written telescope - -> SDoc -- extra text to print -> TcM () -checkValidTelescope tvbs user_tyvars extra - = do { let tvs = binderVars tvbs - - (_, sorted_tidied_tvs) = tidyVarBndrs emptyTidyEnv $ - toposortTyVars tvs - ; unless (go [] emptyVarSet (binderVars tvbs)) $ - addErr $ - vcat [ hang (text "These kind and type variables:" <+> user_tyvars $$ - text "are out of dependency order. Perhaps try this ordering:") - 2 (pprTyVars sorted_tidied_tvs) - , extra ] } - +checkValidTelescope tvbs user_tyvars + = unless (null bad_tvbs) $ addErr $ + vcat [ hang (text "These kind and type variables:" <+> user_tyvars $$ + text "are out of dependency order. Perhaps try this ordering:") + 2 (pprTyVars sorted_tidied_tvs) + , extra ] where - go :: [TyVar] -- misplaced variables - -> TyVarSet -> [TyVar] -> Bool - go errs in_scope [] = null (filter (`elemVarSet` in_scope) errs) - -- report an error only when the variable in the kind is brought - -- into scope later in the telescope. Otherwise, we'll just quantify - -- over it in kindGeneralize, as we should. - - go errs in_scope (tv:tvs) - = let bad_tvs = filterOut (`elemVarSet` in_scope) $ - tyCoVarsOfTypeList (tyVarKind tv) - in go (bad_tvs ++ errs) (in_scope `extendVarSet` tv) tvs + tvs = binderVars tvbs + (_, sorted_tidied_tvs) = tidyVarBndrs emptyTidyEnv (toposortTyVars tvs) + + (_, bad_tvbs) = foldl add_one (mkVarSet tvs, []) tvbs + + add_one :: (TyVarSet, [TyConBinder]) + -> TyConBinder + -> (TyVarSet, [TyConBinder]) + add_one (bad_bndrs, acc) tvb + | fkvs `intersectsVarSet` bad_bndrs + = (bad', tvb : acc) + | otherwise + = (bad', acc) + where + tv = binderVar tvb + 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." + {- ************************************************************************ |