X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcMType.lhs;h=7ac2677e5b7b9f7ed6a49760d660ebaf6e5c84e5;hb=4dd415e9d8e564ca09937042b5c5605f7f2991c9;hp=2a3dc75dbc63841f9a92bba52e069ec5a0e182ad;hpb=8e67f5502e2e316245806ee3735a2f41a844b611;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index 2a3dc75..7ac2677 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -29,7 +29,7 @@ module TcMType ( Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt, SourceTyCtxt(..), checkValidTheta, checkFreeness, checkValidInstHead, instTypeErr, checkAmbiguity, - arityErr, isRigidType, + arityErr, -------------------------------- -- Zonking @@ -47,23 +47,23 @@ module TcMType ( -- friends: import HsSyn ( LHsType ) -import TypeRep ( Type(..), PredType(..), TyNote(..), -- Friend; can see representation - Kind, ThetaType +import TypeRep ( Type(..), PredType(..), -- Friend; can see representation + ThetaType ) import TcType ( TcType, TcThetaType, TcTauType, TcPredType, TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef, - tcCmpPred, isClassPred, + tcCmpPred, tcEqType, isClassPred, tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, - tcSplitTyConApp_maybe, tcSplitForAllTys, - tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy, + tcValidInstHeadTy, tcSplitForAllTys, + tcIsTyVarTy, tcSplitSigmaTy, isUnLiftedType, isIPPred, isImmutableTyVar, typeKind, isFlexi, isSkolemTyVar, mkAppTy, mkTyVarTy, mkTyVarTys, tyVarsOfPred, getClassPredTys_maybe, - tyVarsOfType, tyVarsOfTypes, + tyVarsOfType, tyVarsOfTypes, tcView, pprPred, pprTheta, pprClassPred ) -import Kind ( Kind(..), KindVar(..), mkKindVar, isSubKind, +import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar, isSubKind, isLiftedTypeKind, isArgTypeKind, isOpenTypeKind, liftedTypeKind, defaultKind ) @@ -77,13 +77,13 @@ import Var ( TyVar, tyVarKind, tyVarName, -- others: import TcRnMonad -- TcType, amongst others import FunDeps ( grow ) -import Name ( Name, setNameUnique, mkSysTvName, mkSystemName, getOccName ) +import Name ( Name, setNameUnique, mkSysTvName ) import VarSet import VarEnv -import CmdLineOpts ( dopt, DynFlag(..) ) +import DynFlags ( dopt, DynFlag(..) ) import UniqSupply ( uniqsFromSupply ) -import Util ( nOfThem, isSingleton, equalLength, notNull ) -import ListSetOps ( removeDups ) +import Util ( nOfThem, isSingleton, notNull ) +import ListSetOps ( removeDups, findDupsEq ) import SrcLoc ( unLoc ) import Outputable \end{code} @@ -122,22 +122,6 @@ newTyFlexiVarTy kind newTyFlexiVarTys :: Int -> Kind -> TcM [TcType] newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind) -isRigidType :: TcType -> TcM Bool --- Check that the type is rigid, *taking the type refinement into account* --- In other words if a rigid type variable tv is refined to a wobbly type, --- the answer should be False --- ToDo: can this happen? -isRigidType ty - = do { rigids <- mapM is_rigid (varSetElems (tyVarsOfType ty)) - ; return (and rigids) } - where - is_rigid tv = do { details <- lookupTcTyVar tv - ; case details of - RigidTv -> return True - IndirectTv True ty -> isRigidType ty - other -> return False - } - newKindVar :: TcM TcKind newKindVar = do { uniq <- newUnique ; ref <- newMutVar Nothing @@ -177,11 +161,9 @@ tcInstTyVars tyvars -- they cannot possibly be captured by -- any existing for-alls. Hence zipTopTvSubst -tcInstTyVar tyvar -- Use the OccName of the tyvar we are instantiating - -- but make a System Name, so that it's updated in - -- preference to a tcInstSigTyVar +tcInstTyVar tyvar -- Freshen the Name of the tyvar = do { uniq <- newUnique - ; newMetaTyVar (mkSystemName uniq (getOccName tyvar)) + ; newMetaTyVar (setNameUnique (tyVarName tyvar) uniq) (tyVarKind tyvar) Flexi } tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType) @@ -192,25 +174,38 @@ tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty --------------------------------------------- -tcInstSigType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType) --- Instantiate a type with fresh meta type variables, but --- ones which have the same Name as the original type --- variable. This is used for type signatures, where we must --- instantiate with meta type variables, but we'd like to avoid --- instantiating them were possible; and the unifier unifies --- tyvars with System Names by preference +tcInstSigType :: Name -> [Name] -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) +-- Instantiate a type with fresh SigSkol variables +-- See Note [Signature skolems] in TcType. -- --- We don't need a fresh unique, because the renamer has made them +-- Tne new type variables have the sane Name as the original *iff* they are scoped. +-- For scoped tyvars, we don't need a fresh unique, because the renamer has made them -- unique, and it's better not to do so because we extend the envt -- with them as scoped type variables, and we'd like to avoid spurious -- 's = s' bindings in error messages -tcInstSigType ty = tc_inst_type tcInstSigTyVars ty +-- +-- For non-scoped ones, we *must* instantiate fresh ones: +-- +-- type T = forall a. [a] -> [a] +-- f :: T; +-- f = g where { g :: T; g = } +-- +-- We must not use the same 'a' from the defn of T at both places!! + +tcInstSigType id_name scoped_names ty = tc_inst_type (tcInstSigTyVars id_name scoped_names) ty -tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar] -tcInstSigTyVars tyvars +tcInstSigTyVars :: Name -> [Name] -> [TyVar] -> TcM [TcTyVar] +tcInstSigTyVars id_name scoped_names tyvars = mapM new_tv tyvars where - new_tv tv = newMetaTyVar (tyVarName tv) (tyVarKind tv) Flexi + new_tv tv + = do { let name = tyVarName tv + ; ref <- newMutVar Flexi + ; name' <- if name `elem` scoped_names + then return name + else do { uniq <- newUnique; return (setNameUnique name uniq) } + ; return (mkTcTyVar name' (tyVarKind tv) + (SigSkolTv id_name ref)) } --------------------------------------------- @@ -299,8 +294,7 @@ We return Nothing iff the original box was unbound. \begin{code} data LookupTyVarResult -- The result of a lookupTcTyVar call - = FlexiTv - | RigidTv + = DoneTv TcTyVarDetails -- Unrefined SkolemTv or virgin MetaTv/SigSkolTv | IndirectTv Bool TcType -- True => This is a non-wobbly type refinement, -- gotten from GADT match unification @@ -310,34 +304,48 @@ data LookupTyVarResult -- The result of a lookupTcTyVar call lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult -- This function is the ONLY PLACE that we consult the -- type refinement carried by the monad --- --- The boolean returned with Indirect lookupTcTyVar tyvar - = case tcTyVarDetails tyvar of + = let + details = tcTyVarDetails tyvar + in + case details of + MetaTv ref -> lookup_wobbly details ref + SkolemTv _ -> do { type_reft <- getTypeRefinement ; case lookupVarEnv type_reft tyvar of Just ty -> return (IndirectTv True ty) - Nothing -> return RigidTv - } - MetaTv ref -> do { details <- readMutVar ref - ; case details of - Indirect ty -> return (IndirectTv False ty) - Flexi -> return FlexiTv + Nothing -> return (DoneTv details) } + -- For SigSkolTvs try the refinement, and, failing that + -- see if it's been unified to anything. It's a combination + -- of SkolemTv and MetaTv + SigSkolTv _ ref -> do { type_reft <- getTypeRefinement + ; case lookupVarEnv type_reft tyvar of + Just ty -> return (IndirectTv True ty) + Nothing -> lookup_wobbly details ref + } + -- Look up a meta type variable, conditionally consulting -- the current type refinement condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult condLookupTcTyVar use_refinement tyvar | use_refinement = lookupTcTyVar tyvar | otherwise - = case tcTyVarDetails tyvar of - SkolemTv _ -> return RigidTv - MetaTv ref -> do { details <- readMutVar ref - ; case details of - Indirect ty -> return (IndirectTv False ty) - Flexi -> return FlexiTv - } + = case details of + MetaTv ref -> lookup_wobbly details ref + SkolemTv _ -> return (DoneTv details) + SigSkolTv _ ref -> lookup_wobbly details ref + where + details = tcTyVarDetails tyvar + +lookup_wobbly :: TcTyVarDetails -> IORef MetaDetails -> TcM LookupTyVarResult +lookup_wobbly details ref + = do { meta_details <- readMutVar ref + ; case meta_details of + Indirect ty -> return (IndirectTv False ty) + Flexi -> return (DoneTv details) + } {- -- gaw 2004 We aren't shorting anything out anymore, at least for now @@ -519,11 +527,7 @@ zonkType unbound_var_fn rflag ty go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' -> returnM (TyConApp tycon tys') - go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' -> - go ty2 `thenM` \ ty2' -> - returnM (NoteTy (SynNote ty1') ty2') - - go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations + go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations go (PredTy p) = go_pred p `thenM` \ p' -> returnM (PredTy p') @@ -565,9 +569,9 @@ zonkTyVar unbound_var_fn rflag tyvar -- If b is true, the variable was refined, and therefore it is okay -- to continue refining inside. Otherwise it was wobbly and we should -- not refine further inside. - IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid - FlexiTv -> unbound_var_fn tyvar -- Unbound flexi - RigidTv -> return (TyVarTy tyvar) -- Rigid, no zonking necessary + IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid + DoneTv (MetaTv _) -> unbound_var_fn tyvar -- Unbound meta type variable + DoneTv other -> return (TyVarTy tyvar) -- Rigid, no zonking necessary \end{code} @@ -581,8 +585,8 @@ zonkTyVar unbound_var_fn rflag tyvar \begin{code} readKindVar :: KindVar -> TcM (Maybe TcKind) writeKindVar :: KindVar -> TcKind -> TcM () -readKindVar (KVar _ ref) = readMutVar ref -writeKindVar (KVar _ ref) val = writeMutVar ref (Just val) +readKindVar kv = readMutVar (kindVarRef kv) +writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val) ------------- zonkTcKind :: TcKind -> TcM TcKind @@ -647,6 +651,7 @@ This might not necessarily show up in kind checking. \begin{code} data UserTypeCtxt = FunSigCtxt Name -- Function type signature + -- Also used for types in SPECIALISE pragmas | ExprSigCtxt -- Expression type signature | ConArgCtxt Name -- Data constructor argument | TySynCtxt Name -- RHS of a type synonym decl @@ -659,6 +664,7 @@ data UserTypeCtxt | ForSigCtxt Name -- Foreign inport or export signature | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE | DefaultDeclCtxt -- Types in a default declaration + | SpecInstCtxt -- SPECIALISE instance pragma -- Notes re TySynCtxt -- We allow type synonyms that aren't types; e.g. type List = [] @@ -685,6 +691,7 @@ pprUserTypeCtxt ty ResSigCtxt = sep [ptext SLIT("In a result type signature pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty] pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty] pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)] +pprUserTypeCtxt ty SpecInstCtxt = sep [ptext SLIT("In a SPECIALISE instance pragma:"), nest 2 (ppr ty)] pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty) \end{code} @@ -710,6 +717,7 @@ checkValidType ctxt ty -- constructor, hence rank 1 ForSigCtxt _ -> Rank 1 RuleSigCtxt _ -> Rank 1 + SpecInstCtxt -> Rank 1 actual_kind = typeKind ty @@ -719,7 +727,7 @@ checkValidType ctxt ty ExprSigCtxt -> isOpenTypeKind actual_kind GenPatCtxt -> isLiftedTypeKind actual_kind ForSigCtxt _ -> isLiftedTypeKind actual_kind - other -> isArgTypeKind actual_kind + other -> isArgTypeKind actual_kind ubx_tup | not gla_exts = UT_NotOk | otherwise = case ctxt of @@ -813,29 +821,6 @@ check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty) check_tau_type rank ubx_tup (AppTy ty1 ty2) = check_arg_type ty1 `thenM_` check_arg_type ty2 -check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty) - -- Synonym notes are built only when the synonym is - -- saturated (see Type.mkSynTy) - = doptM Opt_GlasgowExts `thenM` \ gla_exts -> - (if gla_exts then - -- If -fglasgow-exts then don't check the 'note' part. - -- 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 - -- type S m = m () - -- f :: S (T Int) - -- Here, T is partially applied, so it's illegal in H98. - -- But if you expand S first, then T we get just - -- f :: Int - -- which is fine. - returnM () - else - -- For H98, do check the un-expanded part - check_tau_type rank ubx_tup syn - ) `thenM_` - - check_tau_type rank ubx_tup ty - check_tau_type rank ubx_tup (NoteTy other_note ty) = check_tau_type rank ubx_tup ty @@ -844,8 +829,31 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) = -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated -- synonym application, leaving it to checkValidType (i.e. right here) -- to find the error - checkTc syn_arity_ok arity_msg `thenM_` - mappM_ check_arg_type tys + do { -- It's OK to have an *over-applied* type synonym + -- data Tree a b = ... + -- 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 + -- 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 + -- type S m = m () + -- f :: S (T Int) + -- Here, T is partially applied, so it's illegal in H98. + -- But if you expand S first, then T we get just + -- f :: Int + -- which is fine. + returnM () + else + -- For H98, do check the type args + mappM_ check_arg_type tys + } | isUnboxedTupleTyCon tc = doptM Opt_GlasgowExts `thenM` \ gla_exts -> @@ -860,11 +868,6 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) where ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False } - syn_arity_ok = tc_arity <= n_args - -- It's OK to have an *over-applied* type synonym - -- data Tree a b = ... - -- type Foo a = Tree [a] - -- f :: Foo a b -> ... n_args = length tys tc_arity = tyConArity tc @@ -971,15 +974,20 @@ check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty) ------------------------- check_class_pred_tys dflags ctxt tys = case ctxt of + TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine InstHeadCtxt -> True -- We check for instance-head -- formation in checkValidInstHead - InstThetaCtxt -> undecidable_ok || all tcIsTyVarTy tys + InstThetaCtxt -> undecidable_ok || distinct_tyvars tys other -> gla_exts || all tyvar_head tys where undecidable_ok = dopt Opt_AllowUndecidableInstances dflags gla_exts = dopt Opt_GlasgowExts dflags ------------------------- +distinct_tyvars tys -- Check that the types are all distinct type variables + = all tcIsTyVarTy tys && null (findDupsEq tcEqType tys) + +------------------------- tyvar_head ty -- Haskell 98 allows predicates of form | tcIsTyVarTy ty = True -- C (a ty1 .. tyn) | otherwise -- where a is a type variable @@ -1070,7 +1078,8 @@ checkThetaCtxt ctxt theta ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ] badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty -predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred +predTyVarErr pred = sep [ptext SLIT("Non-type variables, or repeated type variables,"), + 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 @@ -1121,20 +1130,16 @@ check_inst_head dflags clas tys | dopt Opt_GlasgowExts dflags = check_tyvars dflags clas tys - -- WITH HASKELL 1.4, MUST HAVE C (T a b c) + -- WITH HASKELL 98, MUST HAVE C (T a b c) | isSingleton tys, - Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty, - not (isSynTyCon tycon), -- ...but not a synonym - all tcIsTyVarTy arg_tys, -- Applied to type variables - equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys - -- This last condition checks that all the type variables are distinct + tcValidInstHeadTy first_ty = returnM () | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg) where - (first_ty : _) = tys + (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")