X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=e2381b6f72c51e91e9e121c36e814036819332f7;hp=23c3381581a2dd4a62b1b1e9597bf8e335e7f161;hb=84923cc7de2a93c22a2f72daf9ac863959efae13;hpb=44ba24dc84d271ca9bd5ab5060cb63ed87f585e3 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 23c3381..e2381b6 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -1,9 +1,12 @@ % +% (c) The University of Glasgow 2006 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 % -\section{Monadic type operations} -This module contains monadic operations over types that contain mutable type variables +Monadic type operations + +This module contains monadic operations over types that contain +mutable type variables \begin{code} module TcMType ( @@ -44,9 +47,10 @@ module TcMType ( -------------------------------- -- Zonking zonkType, zonkTcPredType, - zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar, + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, + zonkQuantifiedTyVar, zonkQuantifiedTyVars, zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType, - zonkTcKindToKind, zonkTcKind, + zonkTcKindToKind, zonkTcKind, zonkTopTyVar, readKindVar, writeKindVar @@ -54,60 +58,31 @@ module TcMType ( #include "HsVersions.h" - -- friends: -import TypeRep ( Type(..), PredType(..), -- Friend; can see representation - ThetaType - ) -import TcType ( TcType, TcThetaType, TcTauType, TcPredType, - TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), - MetaDetails(..), SkolemInfo(..), BoxInfo(..), - BoxyTyVar, BoxyType, UserTypeCtxt(..), kindVarRef, - mkKindVar, isMetaTyVar, isSigTyVar, metaTvRef, - tcCmpPred, isClassPred, tcGetTyVar, - tcSplitPhiTy, tcSplitPredTy_maybe, - tcSplitAppTy_maybe, - tcValidInstHeadTy, tcSplitForAllTys, - tcIsTyVarTy, tcSplitSigmaTy, - isUnLiftedType, isIPPred, - typeKind, isSkolemTyVar, - mkAppTy, mkTyVarTy, mkTyVarTys, - tyVarsOfPred, getClassPredTys_maybe, - tyVarsOfType, tyVarsOfTypes, tcView, - pprPred, pprTheta, pprClassPred ) -import Type ( Kind, KindVar, - isLiftedTypeKind, isSubArgTypeKind, isSubOpenTypeKind, - liftedTypeKind, defaultKind - ) -import Type ( TvSubst, zipTopTvSubst, substTy ) -import Coercion ( mkCoKind ) -import Class ( Class, classArity, className ) -import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon, - tyConArity, tyConName ) -import Var ( TyVar, tyVarKind, tyVarName, isTcTyVar, - mkTyVar, mkTcTyVar, tcTyVarDetails, - CoVar, mkCoVar ) - - -- Assertions -#ifdef DEBUG -import TcType ( isFlexi, isBoxyTyVar, isImmutableTyVar ) -import Type ( isSubKind ) -#endif +import TypeRep +import TcType +import Type +import Coercion +import Class +import TyCon +import Var -- others: import TcRnMonad -- TcType, amongst others -import FunDeps ( grow, checkInstCoverage ) -import Name ( Name, setNameUnique, mkSysTvName ) +import FunDeps +import Name import VarSet -import DynFlags ( dopt, DynFlag(..) ) -import Util ( nOfThem, isSingleton, notNull ) -import ListSetOps ( removeDups ) -import UniqSupply ( uniqsFromSupply ) +import ErrUtils +import DynFlags +import Util +import Maybes +import ListSetOps +import UniqSupply +import SrcLoc import Outputable import Control.Monad ( when ) import Data.List ( (\\) ) - \end{code} @@ -186,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 SrcLoc -> 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` getSrcLoc 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 (srcSpanStart 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} @@ -301,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 @@ -368,7 +359,8 @@ data LookupTyVarResult -- The result of a lookupTcTyVar call lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult lookupTcTyVar tyvar - = case details of + = ASSERT2( isTcTyVar tyvar, ppr tyvar ) + case details of SkolemTv _ -> return (DoneTv details) MetaTv _ ref -> do { meta_details <- readMutVar ref ; case meta_details of @@ -468,17 +460,48 @@ zonkTcPredType (EqPred t1 t2) are used at the end of type checking \begin{code} +zonkTopTyVar :: TcTyVar -> TcM TcTyVar +-- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables +-- to default the kind of ? and ?? etc to *. This is important to ensure that +-- instance declarations match. For example consider +-- instance Show (a->b) +-- foo x = show (\_ -> True) +-- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??), +-- and that won't match the typeKind (*) in the instance decl. +-- +-- Because we are at top level, no further constraints are going to affect these +-- type variables, so it's time to do it by hand. However we aren't ready +-- to default them fully to () or whatever, because the type-class defaulting +-- rules have yet to run. + +zonkTopTyVar tv + | k `eqKind` default_k = return tv + | otherwise + = do { tv' <- newFlexiTyVar default_k + ; writeMetaTyVar tv (mkTyVarTy tv') + ; return tv' } + where + 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 @@ -687,7 +710,6 @@ checkValidType ctxt ty ConArgCtxt _ -> Rank 1 -- We are given the type of the entire -- constructor, hence rank 1 ForSigCtxt _ -> Rank 1 - RuleSigCtxt _ -> Rank 1 SpecInstCtxt -> Rank 1 actual_kind = typeKind ty @@ -902,14 +924,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 @@ -917,10 +939,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 @@ -1013,7 +1048,9 @@ even in a scope where b is in scope. \begin{code} checkFreeness forall_tyvars theta - = mappM_ complain (filter is_free theta) + = do { gla_exts <- doptM Opt_GlasgowExts + ; if gla_exts then return () -- New! Oct06 + else mappM_ complain (filter is_free theta) } where is_free pred = not (isIPPred pred) && not (any bound_var (varSetElems (tyVarsOfPred pred))) @@ -1033,6 +1070,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) @@ -1129,14 +1169,15 @@ 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) $ - checkInstTermination theta inst_tys + mapM_ addErrTc (checkInstTermination inst_tys theta) -- The Coverage Condition ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys) (instTypeErr (pprClassPred clas inst_tys) msg) } where - msg = parens (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} Termination test: each assertion in the context satisfies @@ -1153,20 +1194,19 @@ The underlying idea is that \begin{code} -checkInstTermination :: ThetaType -> [TcType] -> TcM () -checkInstTermination theta tys - = do { mappM_ (check_nomore (fvTypes tys)) theta - ; mappM_ (check_smaller (sizeTypes tys)) theta } - -check_nomore :: [TyVar] -> PredType -> TcM () -check_nomore fvs pred - = checkTc (null (fvPred pred \\ fvs)) - (predUndecErr pred nomoreMsg $$ parens undecidableMsg) - -check_smaller :: Int -> PredType -> TcM () -check_smaller n pred - = checkTc (sizePred pred < n) - (predUndecErr pred smallerMsg $$ parens undecidableMsg) +checkInstTermination :: [TcType] -> ThetaType -> [Message] +checkInstTermination tys theta + = mapCatMaybes check theta + where + fvs = fvTypes tys + size = sizeTypes tys + check pred + | not (null (fvPred pred \\ fvs)) + = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg) + | sizePred pred >= size + = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg) + | otherwise + = Nothing predUndecErr pred msg = sep [msg, nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]