X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=55b16d95bea7b44b1155fe4d8d28d83ec8cfb88b;hb=72e37dedee9e8a109ebda4b13e49b7133b530591;hp=0845853f1375288ae3b070306bcf76bc4a873c20;hpb=2423c249f5ca7785d0ec89eb33e72662da7561c1;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 0845853..55b16d9 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -62,7 +62,6 @@ module TcMType ( import TypeRep import TcType import Type -import Type import Coercion import Class import TyCon @@ -82,7 +81,7 @@ import UniqSupply import SrcLoc import Outputable -import Control.Monad ( when ) +import Control.Monad ( when, unless ) import Data.List ( (\\) ) \end{code} @@ -360,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 @@ -423,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} @@ -827,12 +826,15 @@ 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 + 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 ; gla_exts <- doptM Opt_GlasgowExts - ; if gla_exts then - -- If -fglasgow-exts then don't check the type arguments + ; if gla_exts && not (isOpenTyCon tc) then + -- If -fglasgow-exts 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 @@ -925,14 +927,14 @@ 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 @@ -940,10 +942,23 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys) arity_err = arityErr "Class" class_name arity n_tys how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this")) +check_pred_ty dflags ctxt pred@(EqPred ty1 ty2) + = do { -- Equational constraints are valid in all contexts if indexed + -- types are permitted + ; checkTc (dopt Opt_IndexedTypes 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 @@ -1058,6 +1073,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 -findexed-types 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) @@ -1118,8 +1136,8 @@ check_inst_head dflags clas tys where (first_ty : _) = tys - 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_shape_msg = parens (text "The instance type must be of form (T a1 ... an)" $$ + text "where T is not a synonym, and a1 ... an are distinct type *variables*") -- For now, I only allow tau-types (not polytypes) in -- the head of an instance decl. @@ -1154,7 +1172,7 @@ checkValidInstance tyvars theta clas 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) + mapM_ addErrTc (checkInstTermination inst_tys theta) -- The Coverage Condition ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys) @@ -1165,7 +1183,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.