X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=34375495277bb9f18fd70cc437c0cb2e6e6b7ed0;hp=fa129d3927fd04c2a6beb0372160927c648cca42;hb=acdff50c263a13d1048ab87bea5508c5c9e51146;hpb=0065d5ab628975892cea1ec7303f968c3338cbe1 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index fa129d3..3437549 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -1,11 +1,21 @@ % +% (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} +{-# OPTIONS -w #-} +-- The above warning supression flag is a temporary kludge. +-- While working on this module you are encouraged to remove it and fix +-- any warnings in the module. See +-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings +-- for details + module TcMType ( TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet, @@ -23,8 +33,12 @@ module TcMType ( newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, -------------------------------- + -- Creating new coercion variables + newCoVars, + + -------------------------------- -- Instantiation - tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar, + tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, tcInstSigTyVars, zonkSigTyVar, tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, tcSkolSigType, tcSkolSigTyVars, @@ -33,72 +47,47 @@ module TcMType ( -- Checking type validity Rank, UserTypeCtxt(..), checkValidType, SourceTyCtxt(..), checkValidTheta, checkFreeness, - checkValidInstHead, checkValidInstance, checkAmbiguity, - checkInstTermination, - arityErr, + checkValidInstHead, checkValidInstance, + checkInstTermination, checkValidTypeInst, checkTyFamFreeness, + validDerivPred, arityErr, -------------------------------- -- Zonking zonkType, zonkTcPredType, - zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar, + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, + zonkQuantifiedTyVar, zonkQuantifiedTyVars, zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType, - zonkTcKindToKind, zonkTcKind, + zonkTcKindToKind, zonkTcKind, zonkTopTyVar, readKindVar, writeKindVar - ) where #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, BoxyThetaType, BoxySigmaType, - UserTypeCtxt(..), - 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 Kind ( Kind(..), KindVar, kindVarRef, mkKindVar, - isLiftedTypeKind, isArgTypeKind, isOpenTypeKind, - liftedTypeKind, defaultKind - ) -import Type ( TvSubst, zipTopTvSubst, substTy ) -import Class ( Class, classArity, className ) -import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon, - tyConArity, tyConName ) -import Var ( TyVar, tyVarKind, tyVarName, isTcTyVar, - mkTyVar, mkTcTyVar, tcTyVarDetails ) - - -- Assertions -#ifdef DEBUG -import TcType ( isFlexi, isBoxyTyVar, isImmutableTyVar ) -import Kind ( 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 ErrUtils +import DynFlags +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} @@ -140,10 +129,17 @@ tcInstType inst_tyvars ty %************************************************************************ \begin{code} +newCoVars :: [(TcType,TcType)] -> TcM [CoVar] +newCoVars spec + = do { us <- newUniqueSupply + ; return [ mkCoVar (mkSysTvName uniq FSLIT("co")) + (mkCoKind ty1 ty2) + | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] } + newKindVar :: TcM TcKind newKindVar = do { uniq <- newUnique - ; ref <- newMutVar Nothing - ; return (KindVar (mkKindVar uniq ref)) } + ; ref <- newMutVar Flexi + ; return (mkTyVarTy (mkKindVar uniq ref)) } newKindVars :: Int -> TcM [TcKind] newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ()) @@ -171,19 +167,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} @@ -198,12 +205,16 @@ newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar -- Make a new meta tyvar out of thin air newMetaTyVar box_info kind = do { uniq <- newUnique - ; ref <- newMutVar Flexi ; + ; ref <- newMutVar Flexi ; let name = mkSysTvName uniq fs fs = case box_info of - BoxTv -> FSLIT("bx") + 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 + -- the box_info of each tyvar, use -dppr-debug ; return (mkTcTyVar name kind (MetaTv box_info ref)) } instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar @@ -211,7 +222,7 @@ instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar -- come from an existing TyVar instMetaTyVar box_info tyvar = do { uniq <- newUnique - ; ref <- newMutVar Flexi ; + ; ref <- newMutVar Flexi ; let name = setNameUnique (tyVarName tyvar) uniq kind = tyVarKind tyvar ; return (mkTcTyVar name kind (MetaTv box_info ref)) } @@ -231,7 +242,8 @@ writeMetaTyVar tyvar ty | otherwise = ASSERT( isMetaTyVar tyvar ) - ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) ) + -- TOM: It should also work for coercions + -- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) ) do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar ) ; writeMutVar (metaTvRef tyvar) (Indirect ty) } where @@ -282,9 +294,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 @@ -321,18 +338,12 @@ readFilledBox :: BoxyTyVar -> TcM TcType readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv ) do { cts <- readMetaTyVar box_tv ; case cts of - Flexi -> pprPanic "readFilledBox" (ppr box_tv) + Flexi -> pprPanic "readFilledBox" (ppr box_tv) Indirect ty -> return ty } tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar -- Instantiate with a BOXY type variable tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar - -tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType) --- tcInstType instantiates the outer-level for-alls of a TcType with --- fresh BOXY type variables, splits off the dictionary part, --- and returns the pieces. -tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty \end{code} @@ -355,12 +366,13 @@ 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 Indirect ty -> return (IndirectTv ty) - Flexi -> return (DoneTv details) } + Flexi -> return (DoneTv details) } where details = tcTyVarDetails tyvar @@ -417,7 +429,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} @@ -445,23 +457,58 @@ zonkTcPredType (ClassP c 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) \end{code} ------------------- These ...ToType, ...ToKind versions 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 @@ -569,10 +616,13 @@ zonkType unbound_var_fn ty go ty `thenM` \ ty' -> returnM (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 (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') zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable -> TcTyVar -> TcM TcType @@ -596,35 +646,20 @@ zonk_tc_tyvar unbound_var_fn tyvar %************************************************************************ \begin{code} -readKindVar :: KindVar -> TcM (Maybe TcKind) +readKindVar :: KindVar -> TcM (MetaDetails) writeKindVar :: KindVar -> TcKind -> TcM () readKindVar kv = readMutVar (kindVarRef kv) -writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val) +writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val) ------------- zonkTcKind :: TcKind -> TcM TcKind -zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1 - ; k2' <- zonkTcKind k2 - ; returnM (FunKind k1' k2') } -zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv - ; case mb_kind of - Nothing -> returnM k - Just k -> zonkTcKind k } -zonkTcKind other_kind = returnM other_kind +zonkTcKind k = zonkTcType k ------------- zonkTcKindToKind :: TcKind -> TcM Kind -zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1 - ; k2' <- zonkTcKindToKind k2 - ; returnM (FunKind k1' k2') } - -zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv - ; case mb_kind of - Nothing -> return liftedTypeKind - Just k -> zonkTcKindToKind k } - -zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to * -zonkTcKindToKind other_kind = returnM other_kind +-- When zonking a TcKind to a kind, we need to instantiate kind variables, +-- Haskell specifies that * is to be used, so we follow that. +zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k \end{code} %************************************************************************ @@ -666,9 +701,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 @@ -679,30 +718,28 @@ 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 kind_ok = case ctxt of TySynCtxt _ -> True -- Any kind will do - ResSigCtxt -> isOpenTypeKind actual_kind - ExprSigCtxt -> isOpenTypeKind actual_kind + ResSigCtxt -> isSubOpenTypeKind actual_kind + ExprSigCtxt -> isSubOpenTypeKind actual_kind GenPatCtxt -> isLiftedTypeKind actual_kind ForSigCtxt _ -> isLiftedTypeKind actual_kind - other -> isArgTypeKind 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_` @@ -731,14 +768,16 @@ check_poly_type (Rank 0) ubx_tup ty = check_tau_type (Rank 0) ubx_tup ty check_poly_type rank ubx_tup ty - = let - (tvs, theta, tau) = tcSplitSigmaTy ty - in - check_valid_theta SigmaCtxt theta `thenM_` - check_tau_type (decRank rank) ubx_tup tau `thenM_` - checkFreeness tvs theta `thenM_` - checkAmbiguity tvs theta (tyVarsOfType tau) - + | 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 + ; 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, @@ -777,12 +816,12 @@ check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty -- 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_source_ty dflags TypeCtxt sty + 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 rank UT_NotOk arg_ty `thenM_` - check_poly_type rank UT_Ok res_ty + = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_` + check_poly_type rank UT_Ok res_ty check_tau_type rank ubx_tup (AppTy ty1 ty2) = check_arg_type ty1 `thenM_` check_arg_type ty2 @@ -797,12 +836,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 @@ -819,8 +860,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 @@ -829,7 +870,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 @@ -889,31 +930,45 @@ check_valid_theta ctxt [] check_valid_theta ctxt theta = getDOpts `thenM` \ dflags -> warnTc (notNull dups) (dupPredWarn dups) `thenM_` - mappM_ (check_source_ty dflags ctxt) theta + mappM_ (check_pred_ty dflags ctxt) theta where (_,dups) = removeDups tcCmpPred theta ------------------------- -check_source_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) - +check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM () +check_pred_ty dflags ctxt pred@(ClassP cls tys) + = 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")) - -check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty - -- Implicit parameters only allows in type + 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 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 @@ -921,19 +976,20 @@ check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty -- instance decl would show up two uses of ?x. -- Catch-all -check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty) +check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty) ------------------------- +check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool 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 - undecidable_ok = dopt Opt_AllowUndecidableInstances dflags + flexible_contexts = dopt Opt_FlexibleContexts dflags + undecidable_ok = dopt Opt_UndecidableInstances dflags ------------------------- tyvar_head ty -- Haskell 98 allows predicates of form @@ -974,6 +1030,7 @@ If the list of tv_names is empty, we have a monotype, and then we don't need to check for ambiguity either, because the test can't fail (see is_ambig). + \begin{code} checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM () checkAmbiguity forall_tyvars theta tau_tyvars @@ -982,11 +1039,7 @@ checkAmbiguity forall_tyvars theta tau_tyvars complain pred = addErrTc (ambigErr pred) extended_tau_vars = grow theta tau_tyvars - -- Only a *class* predicate can give rise to ambiguity - -- An *implicit parameter* cannot. For example: - -- foo :: (?x :: [a]) => Int - -- foo = length ?x - -- is fine. The call site will suppply a particular 'x' + -- See Note [Implicit parameters and ambiguity] in TcSimplify is_ambig pred = isClassPred pred && any ambig_var (varSetElems (tyVarsOfPred pred)) @@ -1006,7 +1059,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))) @@ -1014,10 +1068,13 @@ checkFreeness forall_tyvars theta complain pred = addErrTc (freeErr pred) freeErr pred - = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+> - ptext SLIT("are already in scope"), - nest 4 (ptext SLIT("(at least one must be universally quantified here)")) - ] + = 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)") + , nest 4 $ + ptext SLIT("(Use -XFlexibleContexts to lift this restriction)") + ] \end{code} \begin{code} @@ -1025,7 +1082,10 @@ checkThetaCtxt ctxt theta = vcat [ptext SLIT("In the context:") <+> pprTheta theta, ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ] -badSourceTyErr sty = ptext SLIT("Illegal 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) @@ -1075,19 +1135,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. @@ -1113,26 +1184,31 @@ 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_UndecidableInstances ; 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) $ - checkInstTermination theta inst_tys + -- 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) (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 +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. @@ -1146,20 +1222,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)] @@ -1167,7 +1242,166 @@ predUndecErr pred msg = sep [msg, 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} + + +%************************************************************************ +%* * + Checking the context of a derived instance declaration +%* * +%************************************************************************ + +Note [Exotic derived instance contexts] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +In a 'derived' instance declaration, we *infer* the context. It's a +bit unclear what rules we should apply for this; the Haskell report is +silent. Obviously, constraints like (Eq a) are fine, but what about + data T f a = MkT (f a) deriving( Eq ) +where we'd get an Eq (f a) constraint. That's probably fine too. + +One could go further: consider + data T a b c = MkT (Foo a b c) deriving( Eq ) + instance (C Int a, Eq b, Eq c) => Eq (Foo a b c) + +Notice that this instance (just) satisfies the Paterson termination +conditions. Then we *could* derive an instance decl like this: + + instance (C Int a, Eq b, Eq c) => Eq (T a b c) + +even though there is no instance for (C Int a), because there just +*might* be an instance for, say, (C Int Bool) at a site where we +need the equality instance for T's. + +However, this seems pretty exotic, and it's quite tricky to allow +this, and yet give sensible error messages in the (much more common) +case where we really want that instance decl for C. + +So for now we simply require that the derived instance context +should have only type-variable constraints. + +Here is another example: + data Fix f = In (f (Fix f)) deriving( Eq ) +Here, if we are prepared to allow -fallow-undecidable-instances we +could derive the instance + instance Eq (f (Fix f)) => Eq (Fix f) +but this is so delicate that I don't think it should happen inside +'deriving'. If you want this, write it yourself! + +NB: if you want to lift this condition, make sure you still meet the +termination conditions! If not, the deriving mechanism generates +larger and larger constraints. Example: + data Succ a = S a + data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show + +Note the lack of a Show instance for Succ. First we'll generate + instance (Show (Succ a), Show a) => Show (Seq a) +and then + instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a) +and so on. Instead we want to complain of no instance for (Show (Succ a)). + +The bottom line +~~~~~~~~~~~~~~~ +Allow constraints which consist only of type variables, with no repeats. + +\begin{code} +validDerivPred :: PredType -> Bool +validDerivPred (ClassP cls tys) = hasNoDups fvs && sizeTypes tys == length fvs + where fvs = fvTypes tys +validDerivPred otehr = False +\end{code} + +%************************************************************************ +%* * + Checking type instance well-formedness and termination +%* * +%************************************************************************ +\begin{code} +-- Check that a "type instance" is well-formed (which includes decidability +-- unless -fallow-undecidable-instances is given). +-- +checkValidTypeInst :: [Type] -> Type -> TcM () +checkValidTypeInst typats rhs + = do { -- left-hand side contains no type family applications + -- (vanilla synonyms are fine, though) + ; mappM_ checkTyFamFreeness typats + + -- the right-hand side is a tau type + ; checkTc (isTauTy rhs) $ + polyTyErr rhs + + -- we have a decidable instance unless otherwise permitted + ; undecidable_ok <- doptM Opt_UndecidableInstances + ; unless undecidable_ok $ + mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs)) + } + +-- Make sure that each type family instance is +-- (1) strictly smaller than the lhs, +-- (2) mentions no type variable more often than the lhs, and +-- (3) does not contain any further type family instances. +-- +checkFamInst :: [Type] -- lhs + -> [(TyCon, [Type])] -- type family instances + -> [Message] +checkFamInst lhsTys famInsts + = mapCatMaybes check famInsts + where + size = sizeTypes lhsTys + fvs = fvTypes lhsTys + check (tc, tys) + | not (all isTyFamFree tys) + = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg) + | not (null (fvTypes tys \\ fvs)) + = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg) + | size <= sizeTypes tys + = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg) + | otherwise + = Nothing + where + famInst = TyConApp tc tys + +-- Ensure that no type family instances occur in a type. +-- +checkTyFamFreeness :: Type -> TcM () +checkTyFamFreeness ty + = checkTc (isTyFamFree ty) $ + tyFamInstInIndexErr ty + +-- Check that a type does not contain any type family applications. +-- +isTyFamFree :: Type -> Bool +isTyFamFree = null . tyFamInsts + +-- Error messages + +tyFamInstInIndexErr ty + = 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 $ + ppr ty + +famInstUndecErr ty msg + = sep [msg, + 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") +\end{code} + + +%************************************************************************ +%* * +\subsection{Auxiliary functions} +%* * +%************************************************************************ + +\begin{code} -- Free variables of a type, retaining repetitions, and expanding synonyms fvType :: Type -> [TyVar] fvType ty | Just exp_ty <- tcView ty = fvType exp_ty @@ -1185,6 +1419,7 @@ fvTypes tys = concat (map fvType tys) fvPred :: PredType -> [TyVar] fvPred (ClassP _ tys') = fvTypes tys' fvPred (IParam _ ty) = fvType ty +fvPred (EqPred ty1 ty2) = fvType ty1 ++ fvType ty2 -- Size of a type: the number of variables and constructors sizeType :: Type -> Int @@ -1203,4 +1438,5 @@ sizeTypes xs = sum (map sizeType xs) sizePred :: PredType -> Int sizePred (ClassP _ tys') = sizeTypes tys' sizePred (IParam _ ty) = sizeType ty +sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 \end{code}