X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=e8bcca7260335cf426f87122eec23594224df963;hp=ebcf5b331caa1808df97039df6fd0a83eea57aa3;hb=f5d4c3239e57b0396672ffc302961f84398d730e;hpb=081b6b6e90b26a213e8e3065584c552fd2b64d57 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index ebcf5b3..e8bcca7 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -26,7 +26,8 @@ module TcMType ( newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] newKindVar, newKindVars, lookupTcTyVar, LookupTyVarResult(..), - newMetaTyVar, readMetaTyVar, writeMetaTyVar, + + newMetaTyVar, readMetaTyVar, writeMetaTyVar, isFilledMetaTyVar, -------------------------------- -- Boxy type variables @@ -39,13 +40,13 @@ module TcMType ( -------------------------------- -- Instantiation tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, - tcInstSigTyVars, zonkSigTyVar, + tcInstSigTyVars, tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, tcSkolSigType, tcSkolSigTyVars, occurCheckErr, -------------------------------- -- Checking type validity - Rank, UserTypeCtxt(..), checkValidType, + Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType, SourceTyCtxt(..), checkValidTheta, checkFreeness, checkValidInstHead, checkValidInstance, checkInstTermination, checkValidTypeInst, checkTyFamFreeness, @@ -55,7 +56,7 @@ module TcMType ( -------------------------------- -- Zonking zonkType, zonkTcPredType, - zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar, zonkQuantifiedTyVar, zonkQuantifiedTyVars, zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType, zonkTcKindToKind, zonkTcKind, zonkTopTyVar, @@ -87,6 +88,7 @@ import ListSetOps import UniqSupply import SrcLoc import Outputable +import FastString import Control.Monad ( when, unless ) import Data.List ( (\\) ) @@ -103,6 +105,7 @@ import Data.List ( (\\) ) tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables -> TcType -- Type to instantiate -> TcM ([TcTyVar], TcThetaType, TcType) -- Result + -- (type vars (excl coercion vars), preds (incl equalities), rho) tcInstType inst_tyvars ty = case tcSplitForAllTys ty of ([], rho) -> let -- There may be overloading despite no type variables; @@ -161,7 +164,7 @@ checkKinds swapped tv1 ty2 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2. -- ty2 has been zonked at this stage, which ensures that -- its kind has as much boxity information visible as possible. - | tk2 `isSubKind` tk1 = returnM () + | tk2 `isSubKind` tk1 = return () | otherwise -- Either the kinds aren't compatible @@ -218,9 +221,8 @@ checkTauTvUpdate orig_tv orig_ty -- closed type synonym that expands to a tau type. go (TyConApp tc tys) | isSynTyCon tc = go_syn tc tys - | otherwise = do { tys' <- mappM go tys + | otherwise = do { tys' <- mapM go tys ; return $ occurs (TyConApp tc) tys' } - go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations go (PredTy p) = do { p' <- go_pred p ; return $ occurs1 PredTy p' } go (FunTy arg res) = do { arg' <- go arg @@ -342,23 +344,22 @@ Rather, we should bind t to () (= non_var_ty2). Error mesages in case of kind mismatch. \begin{code} -unifyKindMisMatch ty1 ty2 - = zonkTcKind ty1 `thenM` \ ty1' -> - zonkTcKind ty2 `thenM` \ ty2' -> +unifyKindMisMatch ty1 ty2 = do + ty1' <- zonkTcKind ty1 + ty2' <- zonkTcKind ty2 let - msg = hang (ptext SLIT("Couldn't match kind")) + msg = hang (ptext (sLit "Couldn't match kind")) 2 (sep [quotes (ppr ty1'), - ptext SLIT("against"), + ptext (sLit "against"), quotes (ppr ty2')]) - in failWithTc msg unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred -- tv1 and ty2 are zonked already - = returnM msg + = return msg where - msg = (env2, ptext SLIT("When matching the kinds of") <+> - sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual]) + msg = (env2, ptext (sLit "When matching the kinds of") <+> + sep [quotes pp_expected <+> ptext (sLit "and"), quotes pp_actual]) (pp_expected, pp_actual) | swapped = (pp2, pp1) | otherwise = (pp1, pp2) @@ -381,7 +382,7 @@ occurCheckErr ty containingTy extra = sep [ppr tidy_ty1, char '=', ppr tidy_ty2] ; failWithTcM (env2, hang msg 2 extra) } where - msg = ptext SLIT("Occurs check: cannot construct the infinite type:") + msg = ptext (sLit "Occurs check: cannot construct the infinite type:") \end{code} %************************************************************************ @@ -394,7 +395,7 @@ occurCheckErr ty containingTy newCoVars :: [(TcType,TcType)] -> TcM [CoVar] newCoVars spec = do { us <- newUniqueSupply - ; return [ mkCoVar (mkSysTvName uniq FSLIT("co")) + ; return [ mkCoVar (mkSysTvName uniq (fsLit "co")) (mkCoKind ty1 ty2) | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] } @@ -407,7 +408,7 @@ newKindVar = do { uniq <- newUnique ; return (mkTyVarTy (mkKindVar uniq ref)) } newKindVars :: Int -> TcM [TcKind] -newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ()) +newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ()) \end{code} @@ -473,9 +474,9 @@ newMetaTyVar box_info kind ; ref <- newMutVar Flexi ; let name = mkSysTvName uniq fs fs = case box_info of - BoxTv -> FSLIT("t") - TauTv -> FSLIT("t") - SigTv _ -> FSLIT("a") + BoxTv -> fsLit "t" + TauTv -> fsLit "t" + SigTv _ -> fsLit "a" -- We give BoxTv and TauTv the same string, because -- otherwise we get user-visible differences in error -- messages, which are confusing. If you want to see @@ -496,15 +497,22 @@ readMetaTyVar :: TyVar -> TcM MetaDetails readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) readMutVar (metaTvRef tyvar) +isFilledMetaTyVar :: TyVar -> TcM Bool +-- True of a filled-in (Indirect) meta type variable +isFilledMetaTyVar tv + | not (isTcTyVar tv) = return False + | MetaTv _ ref <- tcTyVarDetails tv + = do { details <- readMutVar ref + ; return (isIndirect details) } + | otherwise = return False + writeMetaTyVar :: TcTyVar -> TcType -> TcM () -#ifndef DEBUG -writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty) -#else +writeMetaTyVar tyvar ty + | not debugIsOn = writeMutVar (metaTvRef tyvar) (Indirect ty) writeMetaTyVar tyvar ty | not (isMetaTyVar tyvar) = pprTrace "writeMetaTyVar" (ppr tyvar) $ - returnM () - + return () | otherwise = ASSERT( isMetaTyVar tyvar ) -- TOM: It should also work for coercions @@ -514,7 +522,6 @@ writeMetaTyVar tyvar ty where k1 = tyVarKind tyvar k2 = typeKind ty -#endif \end{code} @@ -529,12 +536,12 @@ newFlexiTyVar :: Kind -> TcM TcTyVar newFlexiTyVar kind = newMetaTyVar TauTv kind newFlexiTyVarTy :: Kind -> TcM TcType -newFlexiTyVarTy kind - = newFlexiTyVar kind `thenM` \ tc_tyvar -> - returnM (TyVarTy tc_tyvar) +newFlexiTyVarTy kind = do + tc_tyvar <- newFlexiTyVar kind + return (TyVarTy tc_tyvar) newFlexiTyVarTys :: Int -> Kind -> TcM [TcType] -newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind) +newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind) tcInstTyVar :: TyVar -> TcM TcTyVar -- Instantiate with a META type variable @@ -545,7 +552,7 @@ tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst) tcInstTyVars tyvars = do { tc_tvs <- mapM tcInstTyVar tyvars ; let tys = mkTyVarTys tc_tvs - ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) } + ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) } -- Since the tyvars are freshly made, -- they cannot possibly be captured by -- any existing for-alls. Hence zipTopTvSubst @@ -646,33 +653,33 @@ lookupTcTyVar tyvar getTcTyVar tyvar | not (isTcTyVar tyvar) = pprTrace "getTcTyVar" (ppr tyvar) $ - returnM (Just (mkTyVarTy tyvar)) + return (Just (mkTyVarTy tyvar)) | otherwise - = ASSERT2( isTcTyVar tyvar, ppr tyvar ) - readMetaTyVar tyvar `thenM` \ maybe_ty -> + = ASSERT2( isTcTyVar tyvar, ppr tyvar ) do + maybe_ty <- readMetaTyVar tyvar case maybe_ty of - Just ty -> short_out ty `thenM` \ ty' -> - writeMetaTyVar tyvar (Just ty') `thenM_` - returnM (Just ty') + Just ty -> do ty' <- short_out ty + writeMetaTyVar tyvar (Just ty') + return (Just ty') - Nothing -> returnM Nothing + Nothing -> return Nothing short_out :: TcType -> TcM TcType short_out ty@(TyVarTy tyvar) | not (isTcTyVar tyvar) - = returnM ty + = return ty - | otherwise - = readMetaTyVar tyvar `thenM` \ maybe_ty -> + | otherwise = do + maybe_ty <- readMetaTyVar tyvar case maybe_ty of - Just ty' -> short_out ty' `thenM` \ ty' -> - writeMetaTyVar tyvar (Just ty') `thenM_` - returnM ty' + Just ty' -> do ty' <- short_out ty' + writeMetaTyVar tyvar (Just ty') + return ty' - other -> returnM ty + other -> return ty -short_out other_ty = returnM other_ty +short_out other_ty = return other_ty -} \end{code} @@ -687,45 +694,37 @@ short_out other_ty = returnM other_ty \begin{code} zonkTcTyVars :: [TcTyVar] -> TcM [TcType] -zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars +zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet -zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys -> - returnM (tyVarsOfTypes tys) +zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar tyvars zonkTcTyVar :: TcTyVar -> TcM TcType zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar) - zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar + zonk_tc_tyvar (\ tv -> return (TyVarTy tv)) tyvar \end{code} ----------------- Types \begin{code} zonkTcType :: TcType -> TcM TcType -zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty +zonkTcType ty = zonkType (\ tv -> return (TyVarTy tv)) ty zonkTcTypes :: [TcType] -> TcM [TcType] -zonkTcTypes tys = mappM zonkTcType tys +zonkTcTypes tys = mapM zonkTcType tys -zonkTcClassConstraints cts = mappM zonk cts - where zonk (clas, tys) - = zonkTcTypes tys `thenM` \ new_tys -> - returnM (clas, new_tys) +zonkTcClassConstraints cts = mapM zonk cts + where zonk (clas, tys) = do + new_tys <- zonkTcTypes tys + return (clas, new_tys) zonkTcThetaType :: TcThetaType -> TcM TcThetaType -zonkTcThetaType theta = mappM zonkTcPredType theta +zonkTcThetaType theta = mapM zonkTcPredType theta zonkTcPredType :: TcPredType -> TcM TcPredType -zonkTcPredType (ClassP c ts) - = zonkTcTypes ts `thenM` \ new_ts -> - returnM (ClassP c new_ts) -zonkTcPredType (IParam n t) - = zonkTcType t `thenM` \ new_t -> - returnM (IParam n new_t) -zonkTcPredType (EqPred t1 t2) - = zonkTcType t1 `thenM` \ new_t1 -> - zonkTcType t2 `thenM` \ new_t2 -> - returnM (EqPred new_t1 new_t2) +zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts +zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t +zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2 \end{code} ------------------- These ...ToType, ...ToKind versions @@ -756,17 +755,17 @@ zonkTopTyVar tv k = tyVarKind tv default_k = defaultKind k -zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar] -zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar +zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar] +zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar -zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar +zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it. -- -- The quantified type variables often include meta type variables -- we want to freeze them into ordinary type variables, and -- default their kind (e.g. from OpenTypeKind to TypeKind) -- -- see notes with Kind.defaultKind --- The meta tyvar is updated to point to the new regular TyVar. Now any +-- The meta tyvar is updated to point to the new skolem TyVar. Now any -- bound occurences of the original type variable will get zonked to -- the immutable version. -- @@ -780,9 +779,11 @@ zonkQuantifiedTyVar tv | otherwise -- It's a meta-type-variable = do { details <- readMetaTyVar tv - -- Create the new, frozen, regular type variable + -- Create the new, frozen, skolem type variable + -- We zonk to a skolem, not to a regular TcVar + -- See Note [Zonking to Skolem] ; let final_kind = defaultKind (tyVarKind tv) - final_tv = mkTyVar (tyVarName tv) final_kind + final_tv = mkSkolTyVar (tyVarName tv) final_kind UnkSkol -- Bind the meta tyvar to the new tyvar ; case details of @@ -797,8 +798,8 @@ zonkQuantifiedTyVar tv ; return final_tv } \end{code} -[Silly Type Synonyms] - +Note [Silly Type Synonyms] +~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: type C u a = u -- Note 'a' unused @@ -832,6 +833,37 @@ Consider this: All very silly. I think its harmless to ignore the problem. We'll end up with a /\a in the final result but all the occurrences of a will be zonked to () +Note [Zonking to Skolem] +~~~~~~~~~~~~~~~~~~~~~~~~ +We used to zonk quantified type variables to regular TyVars. However, this +leads to problems. Consider this program from the regression test suite: + + eval :: Int -> String -> String -> String + eval 0 root actual = evalRHS 0 root actual + + evalRHS :: Int -> a + evalRHS 0 root actual = eval 0 root actual + +It leads to the deferral of an equality + + (String -> String -> String) ~ a + +which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck). +In the meantime `a' is zonked and quantified to form `evalRHS's signature. +This has the *side effect* of also zonking the `a' in the deferred equality +(which at this point is being handed around wrapped in an implication +constraint). + +Finally, the equality (with the zonked `a') will be handed back to the +simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop. +If we zonk `a' with a regular type variable, we will have this regular type +variable now floating around in the simplifier, which in many places assumes to +only see proper TcTyVars. + +We can avoid this problem by zonking with a skolem. The skolem is rigid +(which we requirefor a quantified variable), but is still a TcTyVar that the +simplifier knows how to deal with. + %************************************************************************ %* * @@ -853,21 +885,19 @@ zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type varia zonkType unbound_var_fn ty = go ty where - go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations - - go (TyConApp tc tys) = mappM go tys `thenM` \ tys' -> - returnM (TyConApp tc tys') - - go (PredTy p) = go_pred p `thenM` \ p' -> - returnM (PredTy p') - - go (FunTy arg res) = go arg `thenM` \ arg' -> - go res `thenM` \ res' -> - returnM (FunTy arg' res') - - go (AppTy fun arg) = go fun `thenM` \ fun' -> - go arg `thenM` \ arg' -> - returnM (mkAppTy fun' arg') + go (TyConApp tc tys) = do tys' <- mapM go tys + return (TyConApp tc tys') + + go (PredTy p) = do p' <- go_pred p + return (PredTy p') + + go (FunTy arg res) = do arg' <- go arg + res' <- go res + return (FunTy arg' res') + + go (AppTy fun arg) = do fun' <- go fun + arg' <- go arg + return (mkAppTy fun' arg') -- NB the mkAppTy; we might have instantiated a -- type variable to a type constructor, so we need -- to pull the TyConApp to the top. @@ -877,23 +907,23 @@ zonkType unbound_var_fn ty | otherwise = return (TyVarTy tyvar) -- Ordinary (non Tc) tyvars occur inside quantified types - go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) - go ty `thenM` \ ty' -> - returnM (ForAllTy tyvar ty') + go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do + ty' <- go ty + return (ForAllTy tyvar ty') - go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' -> - returnM (ClassP c tys') - go_pred (IParam n ty) = go ty `thenM` \ ty' -> - returnM (IParam n ty') - go_pred (EqPred ty1 ty2) = go ty1 `thenM` \ ty1' -> - go ty2 `thenM` \ ty2' -> - returnM (EqPred ty1' ty2') + go_pred (ClassP c tys) = do tys' <- mapM go tys + return (ClassP c tys') + go_pred (IParam n ty) = do ty' <- go ty + return (IParam n ty') + go_pred (EqPred ty1 ty2) = do ty1' <- go ty1 + ty2' <- go ty2 + return (EqPred ty1' ty2') zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable -> TcTyVar -> TcM TcType zonk_tc_tyvar unbound_var_fn tyvar | not (isMetaTyVar tyvar) -- Skolems - = returnM (TyVarTy tyvar) + = return (TyVarTy tyvar) | otherwise -- Mutables = do { cts <- readMetaTyVar tyvar @@ -964,12 +994,12 @@ This might not necessarily show up in kind checking. \begin{code} 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_PolymorphicComponents `thenM` \ polycomp -> +checkValidType ctxt ty = do + traceTc (text "checkValidType" <+> ppr ty) + unboxed <- doptM Opt_UnboxedTuples + rank2 <- doptM Opt_Rank2Types + rankn <- doptM Opt_RankNTypes + polycomp <- doptM Opt_PolymorphicComponents let rank | rankn = Arbitrary | rank2 = Rank 2 @@ -1005,14 +1035,17 @@ checkValidType ctxt ty TySynCtxt _ | unboxed -> UT_Ok ExprSigCtxt | unboxed -> UT_Ok _ -> UT_NotOk - in + -- Check that the thing has kind Type, and is lifted if necessary - checkTc kind_ok (kindErr actual_kind) `thenM_` + checkTc kind_ok (kindErr actual_kind) -- Check the internal validity of the type itself - check_poly_type rank ubx_tup ty `thenM_` + check_type rank ubx_tup ty traceTc (text "checkValidType done" <+> ppr ty) + +checkValidMonoType :: Type -> TcM () +checkValidMonoType ty = check_mono_type ty \end{code} @@ -1023,78 +1056,58 @@ 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_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 (PredTy sty) + = do { dflags <- getDOpts + ; check_pred_ty dflags TypeCtxt sty } -check_tau_type rank ubx_tup (AppTy ty1 ty2) - = check_arg_type ty1 `thenM_` check_arg_type ty2 +check_type rank ubx_tup (TyVarTy _) = return () +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 (NoteTy other_note ty) - = check_tau_type rank ubx_tup ty +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 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 @@ -1108,23 +1121,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 + mapM_ 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 + ; mapM_ (check_type rank' UT_Ok) tys } | otherwise - = mappM_ check_arg_type tys + = mapM_ (check_arg_type rank) tys where ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False } @@ -1136,10 +1153,36 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) ubx_tup_msg = ubxArgTyErr ty ---------------------------------------- -forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty -unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> 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 +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 = sep [ptext (sLit "Illegal polymorphic or qualified type:"), ppr ty] +unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty] +ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty] +kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind] \end{code} Note [Liberal type synonyms] @@ -1196,11 +1239,11 @@ data SourceTyCtxt | InstThetaCtxt -- Context of an instance decl -- instance => C [a] where ... -pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c) -pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type") -pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc) -pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration") -pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type") +pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c) +pprSourceTyCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type") +pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc) +pprSourceTyCtxt InstThetaCtxt = ptext (sLit "the context of an instance declaration") +pprSourceTyCtxt TypeCtxt = ptext (sLit "the context of a type") \end{code} \begin{code} @@ -1210,11 +1253,11 @@ checkValidTheta ctxt theta ------------------------- check_valid_theta ctxt [] - = returnM () -check_valid_theta ctxt theta - = getDOpts `thenM` \ dflags -> - warnTc (notNull dups) (dupPredWarn dups) `thenM_` - mappM_ (check_pred_ty dflags ctxt) theta + = return () +check_valid_theta ctxt theta = do + dflags <- getDOpts + warnTc (notNull dups) (dupPredWarn dups) + mapM_ (check_pred_ty dflags ctxt) theta where (_,dups) = removeDups tcCmpPred theta @@ -1225,7 +1268,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 + ; mapM_ check_mono_type tys ; checkTc (check_class_pred_tys dflags ctxt tys) (predTyVarErr pred $$ how_to_allow) } @@ -1234,7 +1277,7 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys) arity = classArity cls n_tys = length tys arity_err = arityErr "Class" class_name arity n_tys - how_to_allow = parens (ptext SLIT("Use -XFlexibleContexts to permit this")) + how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this")) check_pred_ty dflags ctxt pred@(EqPred ty1 ty2) = do { -- Equational constraints are valid in all contexts if type @@ -1242,13 +1285,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 @@ -1318,7 +1359,7 @@ don't need to check for ambiguity either, because the test can't fail \begin{code} checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM () checkAmbiguity forall_tyvars theta tau_tyvars - = mappM_ complain (filter is_ambig theta) + = mapM_ complain (filter is_ambig theta) where complain pred = addErrTc (ambigErr pred) extended_tau_vars = grow theta tau_tyvars @@ -1331,9 +1372,9 @@ checkAmbiguity forall_tyvars theta tau_tyvars not (ct_var `elemVarSet` extended_tau_vars) ambigErr pred - = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred), - nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$ - ptext SLIT("must be reachable from the type after the '=>'"))] + = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred), + nest 4 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$ + ptext (sLit "must be reachable from the type after the '=>'"))] \end{code} In addition, GHC insists that at least one type variable @@ -1344,7 +1385,7 @@ even in a scope where b is in scope. \begin{code} checkFreeness forall_tyvars theta = do { flexible_contexts <- doptM Opt_FlexibleContexts - ; unless flexible_contexts $ mappM_ complain (filter is_free theta) } + ; unless flexible_contexts $ mapM_ complain (filter is_free theta) } where is_free pred = not (isIPPred pred) && not (any bound_var (varSetElems (tyVarsOfPred pred))) @@ -1352,49 +1393,49 @@ checkFreeness forall_tyvars theta complain pred = addErrTc (freeErr pred) freeErr pred - = sep [ ptext SLIT("All of the type variables in the constraint") <+> + = sep [ ptext (sLit "All of the type variables in the constraint") <+> quotes (pprPred pred) - , ptext SLIT("are already in scope") <+> - ptext SLIT("(at least one must be universally quantified here)") + , ptext (sLit "are already in scope") <+> + ptext (sLit "(at least one must be universally quantified here)") , nest 4 $ - ptext SLIT("(Use -XFlexibleContexts to lift this restriction)") + ptext (sLit "(Use -XFlexibleContexts to lift this restriction)") ] \end{code} \begin{code} checkThetaCtxt ctxt theta - = vcat [ptext SLIT("In the context:") <+> pprTheta theta, - ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ] + = vcat [ptext (sLit "In the context:") <+> pprTheta theta, + ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ] -badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty -eqPredTyErr sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty +badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty +eqPredTyErr sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty $$ - parens (ptext SLIT("Use -XTypeFamilies to permit this")) -predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"), - nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)] -dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups) + parens (ptext (sLit "Use -XTypeFamilies to permit this")) +predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"), + nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)] +dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups) arityErr kind name n m - = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"), + = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"), n_arguments <> comma, text "but has been given", int m] where - n_arguments | n == 0 = ptext SLIT("no arguments") - | n == 1 = ptext SLIT("1 argument") - | True = hsep [int n, ptext SLIT("arguments")] + n_arguments | n == 0 = ptext (sLit "no arguments") + | n == 1 = ptext (sLit "1 argument") + | True = hsep [int n, ptext (sLit "arguments")] ----------------- notMonoType ty = do { ty' <- zonkTcType ty ; env0 <- tcInitTidyEnv ; let (env1, tidy_ty) = tidyOpenType env0 ty' - msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty) + msg = ptext (sLit "Cannot match a monotype with") <+> quotes (ppr tidy_ty) ; failWithTcM (env1, msg) } notMonoArgs ty = do { ty' <- zonkTcType ty ; env0 <- tcInitTidyEnv ; let (env1, tidy_ty) = tidyOpenType env0 ty' - msg = ptext SLIT("Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty) + msg = ptext (sLit "Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty) ; failWithTcM (env1, msg) } \end{code} @@ -1424,12 +1465,12 @@ checkValidInstHead ty -- Should be a source type case getClassPredTys_maybe pred of { Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ; - Just (clas,tys) -> + Just (clas,tys) -> do - getDOpts `thenM` \ dflags -> - mappM_ check_arg_type tys `thenM_` - check_inst_head dflags clas tys `thenM_` - returnM (clas, tys) + dflags <- getDOpts + mapM_ check_mono_type tys + check_inst_head dflags clas tys + return (clas, tys) }} check_inst_head dflags clas tys @@ -1443,32 +1484,31 @@ 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)" $$ text "where T is not a synonym." $$ text "Use -XTypeSynonymInstances if you want to disable this.") - head_type_args_tyvars_msg = parens ( - text "All instance types must be of the form (T a1 ... an)" $$ - text "where a1 ... an are distinct type *variables*" $$ - text "Use -XFlexibleInstances if you want to disable this.") + head_type_args_tyvars_msg = parens (vcat [ + text "All instance types must be of the form (T a1 ... an)", + text "where a1 ... an are type *variables*,", + text "and each type variable appears at most once in the instance head.", + text "Use -XFlexibleInstances if you want to disable this."]) head_one_type_msg = parens ( 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, + = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty, nest 4 msg] \end{code} @@ -1499,7 +1539,7 @@ checkValidInstance tyvars theta clas inst_tys (instTypeErr (pprClassPred clas inst_tys) msg) } where - msg = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"), + msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"), undecidableMsg]) \end{code} @@ -1536,11 +1576,11 @@ checkInstTermination tys theta = Nothing predUndecErr pred msg = sep [msg, - nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)] + nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)] -nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head") -smallerMsg = ptext SLIT("Constraint is no smaller than the instance head") -undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this") +nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head") +smallerMsg = ptext (sLit "Constraint is no smaller than the instance head") +undecidableMsg = ptext (sLit "Use -fallow-undecidable-instances to permit this") \end{code} @@ -1623,7 +1663,7 @@ checkValidTypeInst :: [Type] -> Type -> TcM () checkValidTypeInst typats rhs = do { -- left-hand side contains no type family applications -- (vanilla synonyms are fine, though) - ; mappM_ checkTyFamFreeness typats + ; mapM_ checkTyFamFreeness typats -- the right-hand side is a tau type ; checkTc (isTauTy rhs) $ @@ -1675,22 +1715,22 @@ isTyFamFree = null . tyFamInsts -- Error messages tyFamInstInIndexErr ty - = hang (ptext SLIT("Illegal type family application in type instance") <> + = hang (ptext (sLit "Illegal type family application in type instance") <> colon) 4 $ ppr ty polyTyErr ty - = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $ + = hang (ptext (sLit "Illegal polymorphic type in type instance") <> colon) 4 $ ppr ty famInstUndecErr ty msg = sep [msg, - nest 2 (ptext SLIT("in the type family application:") <+> + nest 2 (ptext (sLit "in the type family application:") <+> pprType ty)] -nestedMsg = ptext SLIT("Nested type family application") -nomoreVarMsg = ptext SLIT("Variable occurs more often than in instance head") -smallerAppMsg = ptext SLIT("Application is no smaller than the instance head") +nestedMsg = ptext (sLit "Nested type family application") +nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head") +smallerAppMsg = ptext (sLit "Application is no smaller than the instance head") \end{code} @@ -1706,7 +1746,6 @@ fvType :: Type -> [TyVar] fvType ty | Just exp_ty <- tcView ty = fvType exp_ty fvType (TyVarTy tv) = [tv] fvType (TyConApp _ tys) = fvTypes tys -fvType (NoteTy _ ty) = fvType ty fvType (PredTy pred) = fvPred pred fvType (FunTy arg res) = fvType arg ++ fvType res fvType (AppTy fun arg) = fvType fun ++ fvType arg @@ -1725,7 +1764,6 @@ sizeType :: Type -> Int sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty sizeType (TyVarTy _) = 1 sizeType (TyConApp _ tys) = sizeTypes tys + 1 -sizeType (NoteTy _ ty) = sizeType ty sizeType (PredTy pred) = sizePred pred sizeType (FunTy arg res) = sizeType arg + sizeType res + 1 sizeType (AppTy fun arg) = sizeType fun + sizeType arg