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

@@ -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

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 }
@@ -1178,9 +1168,35 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys)
     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
     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]

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

docs/users_guide/flags.xml

@@ -796,6 +796,12 @@
 	      <entry>dynamic</entry>
 	      <entry><option>-XNoRankNTypes</option></entry>
 	    </row>
+	    <row>
+	      <entry><option>-XImpredicativeTypes</option></entry>
+	      <entry>Enable <link linkend="impredicative-polymorphism">impredicative types</link>.</entry>
+	      <entry>dynamic</entry>
+	      <entry><option>-XNoImpredicativeTypes</option></entry>
+	    </row>
 	    <row>
 	      <entry><option>-XExistentialQuantification</option></entry>
 	      <entry>Enable <link linkend="existential-quantification">existential quantification</link>.</entry>

docs/users_guide/glasgow_exts.xml

@@ -4501,7 +4501,9 @@ for rank-2 types.
 <sect2 id="impredicative-polymorphism">
 <title>Impredicative polymorphism
 </title>
-<para>GHC supports <emphasis>impredicative polymorphism</emphasis>.  This means
+<para>GHC supports <emphasis>impredicative polymorphism</emphasis>, 
+enabled with <option>-XImpredicativeTypes</option>.  
+This means
 that you can call a polymorphic function at a polymorphic type, and
 parameterise data structures over polymorphic types.  For example:
 <programlisting>