X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=955d45c551c6a07d209d74bbd69161fc2a0e2400;hp=4633f49a9dc01806fa948d4102d5cdc2efc16de6;hb=c1681a73fa4ca4cf8758264ae387ac09a9e900d8;hpb=335bc125303a226a78b20be8a7b8fec5b6c59d2b diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 4633f49..955d45c 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -47,7 +47,8 @@ module TcMType ( -------------------------------- -- Zonking zonkType, zonkTcPredType, - zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar, + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, + zonkQuantifiedTyVar, zonkQuantifiedTyVars, zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType, zonkTcKindToKind, zonkTcKind, zonkTopTyVar, @@ -61,7 +62,6 @@ module TcMType ( import TypeRep import TcType import Type -import Type import Coercion import Class import TyCon @@ -78,9 +78,10 @@ import Util import Maybes import ListSetOps import UniqSupply +import SrcLoc import Outputable -import Control.Monad ( when ) +import Control.Monad ( when, unless ) import Data.List ( (\\) ) \end{code} @@ -160,19 +161,30 @@ tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar] tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info | tv <- tyvars ] -tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) --- Instantiate a type with fresh skolem constants -tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty - -tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar -tcInstSkolTyVar info tyvar +tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar +-- Instantiate the tyvar, using +-- * the occ-name and kind of the supplied tyvar, +-- * the unique from the monad, +-- * the location either from the tyvar (mb_loc = Nothing) +-- or from mb_loc (Just loc) +tcInstSkolTyVar info mb_loc tyvar = do { uniq <- newUnique - ; let name = setNameUnique (tyVarName tyvar) uniq - kind = tyVarKind tyvar - ; return (mkSkolTyVar name kind info) } + ; let old_name = tyVarName tyvar + kind = tyVarKind tyvar + loc = mb_loc `orElse` getSrcSpan old_name + new_name = mkInternalName uniq (nameOccName old_name) loc + ; return (mkSkolTyVar new_name kind info) } tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] -tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars +-- Get the location from the monad +tcInstSkolTyVars info tyvars + = do { span <- getSrcSpanM + ; mapM (tcInstSkolTyVar info (Just span)) tyvars } + +tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) +-- Instantiate a type with fresh skolem constants +-- Binding location comes from the monad +tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty \end{code} @@ -275,9 +287,14 @@ tcInstTyVars tyvars %************************************************************************ \begin{code} -tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] --- Instantiate with meta SigTvs -tcInstSigTyVars skol_info tyvars +tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar] +-- Instantiate with skolems or meta SigTvs; depending on use_skols +-- Always take location info from the supplied tyvars +tcInstSigTyVars use_skols skol_info tyvars + | use_skols + = mapM (tcInstSkolTyVar skol_info Nothing) tyvars + + | otherwise = mapM (instMetaTyVar (SigTv skol_info)) tyvars zonkSigTyVar :: TcTyVar -> TcM TcTyVar @@ -342,7 +359,7 @@ data LookupTyVarResult -- The result of a lookupTcTyVar call lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult lookupTcTyVar tyvar - = ASSERT( isTcTyVar tyvar ) + = ASSERT2( isTcTyVar tyvar, ppr tyvar ) case details of SkolemTv _ -> return (DoneTv details) MetaTv _ ref -> do { meta_details <- readMutVar ref @@ -405,7 +422,7 @@ zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys -> returnM (tyVarsOfTypes tys) zonkTcTyVar :: TcTyVar -> TcM TcType -zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar ) +zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar) zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar \end{code} @@ -467,17 +484,24 @@ zonkTopTyVar tv k = tyVarKind tv default_k = defaultKind k +zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar] +zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar + zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it. --- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar. --- When we do this, we also default the kind -- see notes with Kind.defaultKind +-- +-- 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 -- bound occurences of the original type variable will get zonked to -- the immutable version. -- -- We leave skolem TyVars alone; they are immutable. zonkQuantifiedTyVar tv - | isSkolemTyVar tv = return tv + | ASSERT( isTcTyVar tv ) + isSkolemTyVar tv = return tv -- It might be a skolem type variable, -- for example from a user type signature @@ -670,9 +694,13 @@ 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_GlasgowExts `thenM` \ gla_exts -> + doptM Opt_UnboxedTuples `thenM` \ unboxed -> + doptM Opt_Rank2Types `thenM` \ rank2 -> + doptM Opt_RankNTypes `thenM` \ rankn -> + doptM Opt_PolymorphicComponents `thenM` \ polycomp -> let - rank | gla_exts = Arbitrary + rank | rankn = Arbitrary + | rank2 = Rank 2 | otherwise = case ctxt of -- Haskell 98 GenPatCtxt -> Rank 0 @@ -683,10 +711,12 @@ checkValidType ctxt ty TySynCtxt _ -> Rank 0 ExprSigCtxt -> Rank 1 FunSigCtxt _ -> Rank 1 - ConArgCtxt _ -> Rank 1 -- We are given the type of the entire - -- constructor, hence rank 1 + ConArgCtxt _ -> if polycomp + then Rank 2 + -- We are given the type of the entire + -- constructor, hence rank 1 + else Rank 1 ForSigCtxt _ -> Rank 1 - RuleSigCtxt _ -> Rank 1 SpecInstCtxt -> Rank 1 actual_kind = typeKind ty @@ -699,14 +729,10 @@ checkValidType ctxt ty ForSigCtxt _ -> isLiftedTypeKind actual_kind other -> isSubArgTypeKind actual_kind - ubx_tup | not gla_exts = UT_NotOk - | otherwise = case ctxt of - TySynCtxt _ -> UT_Ok - ExprSigCtxt -> UT_Ok - other -> UT_NotOk - -- Unboxed tuples ok in function results, - -- but for type synonyms we allow them even at - -- top level + ubx_tup = case ctxt of + 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_` @@ -803,12 +829,14 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) -- type Foo a = Tree [a] -- f :: Foo a b -> ... ; case tcView ty of - Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion - Nothing -> failWithTc arity_msg - - ; gla_exts <- doptM Opt_GlasgowExts - ; if gla_exts then - -- If -fglasgow-exts then don't check the type arguments + Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion + Nothing -> unless (isOpenTyCon tc -- No expansion if open + && tyConArity tc <= length tys) $ + failWithTc arity_msg + + ; ok <- doptM Opt_PartiallyAppliedClosedTypeSynonyms + ; if ok && not (isOpenTyCon tc) then + -- Don't check the type arguments of *closed* synonyms. -- This allows us to instantiate a synonym defn with a -- for-all type, or with a partially-applied type synonym. -- e.g. type T a b = a @@ -825,8 +853,8 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) } | isUnboxedTupleTyCon tc - = doptM Opt_GlasgowExts `thenM` \ gla_exts -> - checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_` + = 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 -- more unboxed tuples, so can't use check_arg_ty @@ -835,7 +863,7 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) = mappM_ check_arg_type tys where - ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False } + ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False } n_args = length tys tc_arity = tyConArity tc @@ -901,25 +929,38 @@ check_valid_theta ctxt theta ------------------------- check_pred_ty dflags ctxt pred@(ClassP cls tys) - = -- Class predicates are valid in all contexts - checkTc (arity == n_tys) arity_err `thenM_` - - -- Check the form of the argument types - mappM_ check_arg_type tys `thenM_` - checkTc (check_class_pred_tys dflags ctxt tys) - (predTyVarErr pred $$ how_to_allow) - + = do { -- Class predicates are valid in all contexts + ; checkTc (arity == n_tys) arity_err + + -- Check the form of the argument types + ; mappM_ check_arg_type tys + ; checkTc (check_class_pred_tys dflags ctxt tys) + (predTyVarErr pred $$ how_to_allow) + } where class_name = className cls arity = classArity cls n_tys = length tys arity_err = arityErr "Class" class_name arity n_tys - how_to_allow = parens (ptext SLIT("Use -fglasgow-exts 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 + -- families are permitted + ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred) + + -- Check the form of the argument types + ; check_eq_arg_type ty1 + ; check_eq_arg_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 - -- Implicit parameters only allows in type + -- 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 subtle + -- The reason for not allowing implicit params in instances is a bit + -- subtle. -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ... -- then when we saw (e :: (?x::Int) => t) it would be unclear how to -- discharge all the potential usas of the ?x in e. For example, a @@ -933,12 +974,12 @@ check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty) check_class_pred_tys dflags ctxt tys = case ctxt of TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine - InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys + InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys -- Further checks on head and theta in -- checkInstTermination - other -> gla_exts || all tyvar_head tys + other -> flexible_contexts || all tyvar_head tys where - gla_exts = dopt Opt_GlasgowExts dflags + flexible_contexts = dopt Opt_FlexibleContexts dflags undecidable_ok = dopt Opt_AllowUndecidableInstances dflags ------------------------- @@ -1012,7 +1053,8 @@ even in a scope where b is in scope. \begin{code} checkFreeness forall_tyvars theta - = mappM_ complain (filter is_free theta) + = do { flexible_contexts <- doptM Opt_FlexibleContexts + ; unless flexible_contexts $ mappM_ complain (filter is_free theta) } where is_free pred = not (isIPPred pred) && not (any bound_var (varSetElems (tyVarsOfPred pred))) @@ -1032,6 +1074,9 @@ checkThetaCtxt ctxt theta ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ] badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty +eqPredTyErr sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty + $$ + parens (ptext SLIT("Use -ftype-families 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) @@ -1081,19 +1126,30 @@ checkValidInstHead ty -- Should be a source type check_inst_head dflags clas tys -- If GlasgowExts then check at least one isn't a type variable - | dopt Opt_GlasgowExts dflags - = mapM_ check_one tys - - -- WITH HASKELL 98, MUST HAVE C (T a b c) - | otherwise - = checkTc (isSingleton tys && tcValidInstHeadTy first_ty) - (instTypeErr (pprClassPred clas tys) head_shape_msg) - + = do checkTc (dopt Opt_TypeSynonymInstances dflags || + all tcInstHeadTyNotSynonym tys) + (instTypeErr (pprClassPred clas tys) head_type_synonym_msg) + checkTc (dopt Opt_FlexibleInstances dflags || + all tcInstHeadTyAppAllTyVars tys) + (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg) + checkTc (dopt Opt_MultiParamTypeClasses dflags || + isSingleton tys) + (instTypeErr (pprClassPred clas tys) head_one_type_msg) + mapM_ check_one tys where - (first_ty : _) = tys + 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_shape_msg = parens (text "The instance type must be of form (T a b c)" $$ - text "where T is not a synonym, and a,b,c are distinct type variables") + 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. @@ -1119,16 +1175,16 @@ instTypeErr pp_ty msg \begin{code} checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM () checkValidInstance tyvars theta clas inst_tys - = do { gla_exts <- doptM Opt_GlasgowExts - ; undecidable_ok <- doptM Opt_AllowUndecidableInstances + = do { undecidable_ok <- doptM Opt_AllowUndecidableInstances ; checkValidTheta InstThetaCtxt theta ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys) -- Check that instance inference will terminate (if we care) - -- For Haskell 98, checkValidTheta has already done that - ; when (gla_exts && not undecidable_ok) $ - mapM_ failWithTc (checkInstTermination inst_tys theta) + -- For Haskell 98 this will already have been done by checkValidTheta, + -- but as we may be using other extensions we need to check. + ; unless undecidable_ok $ + mapM_ addErrTc (checkInstTermination inst_tys theta) -- The Coverage Condition ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys) @@ -1139,7 +1195,11 @@ checkValidInstance tyvars theta clas inst_tys undecidableMsg]) \end{code} -Termination test: each assertion in the context satisfies +Termination test: the so-called "Paterson conditions" (see Section 5 of +"Understanding functionsl dependencies via Constraint Handling Rules, +JFP Jan 2007). + +We check that each assertion in the context satisfies: (1) no variable has more occurrences in the assertion than in the head, and (2) the assertion has fewer constructors and variables (taken together and counting repetitions) than the head.