From 5e04ae341a945ef430e9d941b34722b8de1f6aae Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Mon, 7 Jan 2008 11:54:51 +0000 Subject: [PATCH] Add -XImpredicativeTypes, and tighten up type-validity checking (cf Trac 2019) Somehow we didn't have a separate flag for impredicativity; now we do. Furthermore, Trac #2019 showed up a missing test for monotypes in data constructor return types. And I realised that we were even allowing things like Num (forall a. a) => ... which we definitely should not. This patch insists on monotypes in several places where we were (wrongly) too liberal before. Could be merged to 6.8 but no big deal. --- compiler/main/DynFlags.hs | 15 +-- compiler/typecheck/TcMType.lhs | 178 +++++++++++++++++++---------------- compiler/typecheck/TcTyClsDecls.lhs | 3 + docs/users_guide/flags.xml | 6 ++ docs/users_guide/glasgow_exts.xml | 4 +- 5 files changed, 116 insertions(+), 90 deletions(-) diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index 07ed33f..91c7f43 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -232,6 +232,7 @@ data DynFlag | Opt_LiberalTypeSynonyms | Opt_Rank2Types | Opt_RankNTypes + | Opt_ImpredicativeTypes | Opt_TypeOperators | Opt_PrintExplicitForalls @@ -1288,9 +1289,10 @@ xFlags = [ ( "TransformListComp", Opt_TransformListComp ), ( "ForeignFunctionInterface", Opt_ForeignFunctionInterface ), ( "UnliftedFFITypes", Opt_UnliftedFFITypes ), - ( "LiberalTypeSynonyms", Opt_LiberalTypeSynonyms ), + ( "LiberalTypeSynonyms", Opt_LiberalTypeSynonyms ), ( "Rank2Types", Opt_Rank2Types ), ( "RankNTypes", Opt_RankNTypes ), + ( "ImpredicativeTypes", Opt_ImpredicativeTypes ), ( "TypeOperators", Opt_TypeOperators ), ( "RecursiveDo", Opt_RecursiveDo ), ( "Arrows", Opt_Arrows ), @@ -1339,9 +1341,9 @@ glasgowExtsFlags = [ Opt_PrintExplicitForalls , Opt_ForeignFunctionInterface , Opt_UnliftedFFITypes - , Opt_GADTs - , Opt_ImplicitParams - , Opt_ScopedTypeVariables + , Opt_GADTs + , Opt_ImplicitParams + , Opt_ScopedTypeVariables , Opt_UnboxedTuples , Opt_TypeSynonymInstances , Opt_StandaloneDeriving @@ -1351,13 +1353,14 @@ glasgowExtsFlags = [ , Opt_ConstrainedClassMethods , Opt_MultiParamTypeClasses , Opt_FunctionalDependencies - , Opt_MagicHash + , Opt_MagicHash , Opt_PolymorphicComponents , Opt_ExistentialQuantification , Opt_UnicodeSyntax , Opt_PatternGuards , Opt_LiberalTypeSynonyms , Opt_RankNTypes + , Opt_ImpredicativeTypes , Opt_TypeOperators , Opt_RecursiveDo , Opt_ParallelListComp @@ -1365,7 +1368,7 @@ glasgowExtsFlags = [ , Opt_KindSignatures , Opt_PatternSignatures , Opt_GeneralizedNewtypeDeriving - , Opt_TypeFamilies ] + , Opt_TypeFamilies ] ------------------ isFlag :: [(String,a)] -> String -> Bool diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 3357004..f1f9082 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -46,7 +46,7 @@ module TcMType ( -------------------------------- -- Checking type validity - Rank, UserTypeCtxt(..), checkValidType, + Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType, SourceTyCtxt(..), checkValidTheta, checkFreeness, checkValidInstHead, checkValidInstance, checkInstTermination, checkValidTypeInst, checkTyFamFreeness, @@ -1009,9 +1009,9 @@ checkValidType :: UserTypeCtxt -> Type -> TcM () -- Checks that the type is valid for the given context checkValidType ctxt ty = traceTc (text "checkValidType" <+> ppr ty) `thenM_` - doptM Opt_UnboxedTuples `thenM` \ unboxed -> - doptM Opt_Rank2Types `thenM` \ rank2 -> - doptM Opt_RankNTypes `thenM` \ rankn -> + doptM Opt_UnboxedTuples `thenM` \ unboxed -> + doptM Opt_Rank2Types `thenM` \ rank2 -> + doptM Opt_RankNTypes `thenM` \ rankn -> doptM Opt_PolymorphicComponents `thenM` \ polycomp -> let rank | rankn = Arbitrary @@ -1053,9 +1053,12 @@ checkValidType ctxt ty checkTc kind_ok (kindErr actual_kind) `thenM_` -- Check the internal validity of the type itself - check_poly_type rank ubx_tup ty `thenM_` + check_type rank ubx_tup ty `thenM_` traceTc (text "checkValidType done" <+> ppr ty) + +checkValidMonoType :: Type -> TcM () +checkValidMonoType ty = check_mono_type ty \end{code} @@ -1066,78 +1069,61 @@ decRank :: Rank -> Rank decRank Arbitrary = Arbitrary decRank (Rank n) = Rank (n-1) +nonZeroRank :: Rank -> Bool +nonZeroRank (Rank 0) = False +nonZeroRank _ = True + ---------------------------------------- data UbxTupFlag = UT_Ok | UT_NotOk -- The "Ok" version means "ok if -fglasgow-exts is on" ---------------------------------------- -check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM () -check_poly_type (Rank 0) ubx_tup ty - = check_tau_type (Rank 0) ubx_tup ty - -check_poly_type rank ubx_tup ty - | null tvs && null theta - = check_tau_type rank ubx_tup ty - | otherwise - = do { check_valid_theta SigmaCtxt theta - ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow +check_mono_type :: Type -> TcM () -- No foralls anywhere + -- No unlifted types of any kind +check_mono_type ty + = do { check_type (Rank 0) UT_NotOk ty + ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } + +check_type :: Rank -> UbxTupFlag -> Type -> TcM () +-- The args say what the *type* context requires, independent +-- of *flag* settings. You test the flag settings at usage sites. +-- +-- Rank is allowed rank for function args +-- Rank 0 means no for-alls anywhere + +check_type rank ubx_tup ty + | not (null tvs && null theta) + = do { checkTc (nonZeroRank rank) (forAllTyErr ty) + -- Reject e.g. (Maybe (?x::Int => Int)), + -- with a decent error message + ; check_valid_theta SigmaCtxt theta + ; check_type rank ubx_tup tau -- Allow foralls to right of arrow ; checkFreeness tvs theta ; checkAmbiguity tvs theta (tyVarsOfType tau) } where (tvs, theta, tau) = tcSplitSigmaTy ty ----------------------------------------- -check_arg_type :: Type -> TcM () --- The sort of type that can instantiate a type variable, --- or be the argument of a type constructor. --- Not an unboxed tuple, but now *can* be a forall (since impredicativity) --- Other unboxed types are very occasionally allowed as type --- arguments depending on the kind of the type constructor --- --- For example, we want to reject things like: --- --- instance Ord a => Ord (forall s. T s a) --- and --- g :: T s (forall b.b) --- --- NB: unboxed tuples can have polymorphic or unboxed args. --- This happens in the workers for functions returning --- product types with polymorphic components. --- But not in user code. --- Anyway, they are dealt with by a special case in check_tau_type - -check_arg_type ty - = check_poly_type Arbitrary UT_NotOk ty `thenM_` - checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) - ----------------------------------------- -check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM () --- Rank is allowed rank for function args --- No foralls otherwise - -check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty) -check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty) - -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message - -- Naked PredTys don't usually show up, but they can as a result of -- {-# SPECIALISE instance Ord Char #-} -- The Right Thing would be to fix the way that SPECIALISE instance pragmas -- are handled, but the quick thing is just to permit PredTys here. -check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags -> - check_pred_ty dflags TypeCtxt sty +check_type rank ubx_tup (PredTy sty) + = do { dflags <- getDOpts + ; check_pred_ty dflags TypeCtxt sty } -check_tau_type rank ubx_tup (TyVarTy _) = returnM () -check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty) - = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_` - check_poly_type rank UT_Ok res_ty +check_type rank ubx_tup (TyVarTy _) = returnM () +check_type rank ubx_tup ty@(FunTy arg_ty res_ty) + = do { check_type (decRank rank) UT_NotOk arg_ty + ; check_type rank UT_Ok res_ty } -check_tau_type rank ubx_tup (AppTy ty1 ty2) - = check_arg_type ty1 `thenM_` check_arg_type ty2 +check_type rank ubx_tup (AppTy ty1 ty2) + = do { check_arg_type rank ty1 + ; check_arg_type rank ty2 } -check_tau_type rank ubx_tup (NoteTy other_note ty) - = check_tau_type rank ubx_tup ty +check_type rank ubx_tup (NoteTy other_note ty) + = check_type rank ubx_tup ty -check_tau_type rank ubx_tup ty@(TyConApp tc tys) +check_type rank ubx_tup ty@(TyConApp tc tys) | isSynTyCon tc = do { -- Check that the synonym has enough args -- This applies equally to open and closed synonyms @@ -1151,23 +1137,27 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) ; liberal <- doptM Opt_LiberalTypeSynonyms ; if not liberal || isOpenSynTyCon tc then -- For H98 and synonym families, do check the type args - mappM_ check_arg_type tys + mappM_ check_mono_type tys else -- In the liberal case (only for closed syns), expand then check case tcView ty of - Just ty' -> check_tau_type rank ubx_tup ty' + Just ty' -> check_type rank ubx_tup ty' Nothing -> pprPanic "check_tau_type" (ppr ty) } | isUnboxedTupleTyCon tc - = doptM Opt_UnboxedTuples `thenM` \ ub_tuples_allowed -> - checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg `thenM_` - mappM_ (check_tau_type (Rank 0) UT_Ok) tys - -- Args are allowed to be unlifted, or + = do { ub_tuples_allowed <- doptM Opt_UnboxedTuples + ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg + + ; impred <- doptM Opt_ImpredicativeTypes + ; let rank' = if impred then rank else Rank 0 + -- c.f. check_arg_type + -- However, args are allowed to be unlifted, or -- more unboxed tuples, so can't use check_arg_ty + ; mappM_ (check_type rank' UT_Ok) tys } | otherwise - = mappM_ check_arg_type tys + = mappM_ (check_arg_type rank) tys where ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False } @@ -1179,8 +1169,34 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) ubx_tup_msg = ubxArgTyErr ty ---------------------------------------- +check_arg_type :: Rank -> Type -> TcM () +-- The sort of type that can instantiate a type variable, +-- or be the argument of a type constructor. +-- Not an unboxed tuple, but now *can* be a forall (since impredicativity) +-- Other unboxed types are very occasionally allowed as type +-- arguments depending on the kind of the type constructor +-- +-- For example, we want to reject things like: +-- +-- instance Ord a => Ord (forall s. T s a) +-- and +-- g :: T s (forall b.b) +-- +-- NB: unboxed tuples can have polymorphic or unboxed args. +-- This happens in the workers for functions returning +-- product types with polymorphic components. +-- But not in user code. +-- Anyway, they are dealt with by a special case in check_tau_type + +check_arg_type rank ty + = do { impred <- doptM Opt_ImpredicativeTypes + ; let rank' = if impred then rank else Rank 0 -- Monotype unless impredicative + ; check_type rank' UT_NotOk ty + ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } + +---------------------------------------- forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty -unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty +unliftedArgErr ty = ptext SLIT("Illegal unlifted type:") <+> ppr ty ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind \end{code} @@ -1268,7 +1284,7 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys) ; checkTc (arity == n_tys) arity_err -- Check the form of the argument types - ; mappM_ check_arg_type tys + ; mappM_ check_mono_type tys ; checkTc (check_class_pred_tys dflags ctxt tys) (predTyVarErr pred $$ how_to_allow) } @@ -1285,13 +1301,11 @@ check_pred_ty dflags ctxt pred@(EqPred ty1 ty2) ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred) -- Check the form of the argument types - ; check_eq_arg_type ty1 - ; check_eq_arg_type ty2 + ; check_mono_type ty1 + ; check_mono_type ty2 } - where - check_eq_arg_type = check_poly_type (Rank 0) UT_NotOk -check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty +check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_mono_type ty -- Implicit parameters only allowed in type -- signatures; not in instance decls, superclasses etc -- The reason for not allowing implicit params in instances is a bit @@ -1470,7 +1484,7 @@ checkValidInstHead ty -- Should be a source type Just (clas,tys) -> getDOpts `thenM` \ dflags -> - mappM_ check_arg_type tys `thenM_` + mappM_ check_mono_type tys `thenM_` check_inst_head dflags clas tys `thenM_` returnM (clas, tys) }} @@ -1486,7 +1500,13 @@ check_inst_head dflags clas tys checkTc (dopt Opt_MultiParamTypeClasses dflags || isSingleton tys) (instTypeErr (pprClassPred clas tys) head_one_type_msg) - mapM_ check_one tys + mapM_ check_mono_type tys + -- For now, I only allow tau-types (not polytypes) in + -- the head of an instance decl. + -- E.g. instance C (forall a. a->a) is rejected + -- One could imagine generalising that, but I'm not sure + -- what all the consequences might be + where head_type_synonym_msg = parens ( text "All instance types must be of the form (T t1 ... tn)" $$ @@ -1502,14 +1522,6 @@ check_inst_head dflags clas tys text "Only one type can be given in an instance head." $$ text "Use -XMultiParamTypeClasses if you want to allow more.") - -- For now, I only allow tau-types (not polytypes) in - -- the head of an instance decl. - -- E.g. instance C (forall a. a->a) is rejected - -- One could imagine generalising that, but I'm not sure - -- what all the consequences might be - check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty - ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } - instTypeErr pp_ty msg = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, nest 4 msg] diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs index 83b2114..89afedf 100644 --- a/compiler/typecheck/TcTyClsDecls.lhs +++ b/compiler/typecheck/TcTyClsDecls.lhs @@ -1054,6 +1054,9 @@ checkValidDataCon tc con addErrCtxt (dataConCtxt con) $ do { checkTc (dataConTyCon con == tc) (badDataConTyCon con) ; checkValidType ctxt (dataConUserType con) + ; checkValidMonoType (dataConOrigResTy con) + -- Disallow MkT :: T (forall a. a->a) + -- Reason: it's really the argument of an equality constraint ; ifM (isNewTyCon tc) (checkNewDataCon con) } where diff --git a/docs/users_guide/flags.xml b/docs/users_guide/flags.xml index cb993af..6694adf 100644 --- a/docs/users_guide/flags.xml +++ b/docs/users_guide/flags.xml @@ -797,6 +797,12 @@ + + Enable impredicative types. + dynamic + + + Enable existential quantification. dynamic diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index 26fff9a..3b83551 100644 --- a/docs/users_guide/glasgow_exts.xml +++ b/docs/users_guide/glasgow_exts.xml @@ -4501,7 +4501,9 @@ for rank-2 types. Impredicative polymorphism -GHC supports impredicative polymorphism. This means +GHC supports impredicative polymorphism, +enabled with . +This means that you can call a polymorphic function at a polymorphic type, and parameterise data structures over polymorphic types. For example: -- 1.7.10.4