X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=f7cbb2c81a819a527258cc37b935757ea5680bec;hb=3787d9878e4d62829a555f01b2a4c5866f24f303;hp=f14cf59af46b497fa9984f2c2f7a1f0f3be177bd;hpb=1b6b0ba3b93351045e19df9fa9cb0f8baf033afc;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index f14cf59..f7cbb2c 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -26,7 +26,8 @@ module TcMType ( newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] newKindVar, newKindVars, lookupTcTyVar, LookupTyVarResult(..), - newMetaTyVar, readMetaTyVar, writeMetaTyVar, + + newMetaTyVar, readMetaTyVar, writeMetaTyVar, isFilledMetaTyVar, -------------------------------- -- Boxy type variables @@ -39,13 +40,13 @@ module TcMType ( -------------------------------- -- Instantiation tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, - tcInstSigTyVars, zonkSigTyVar, + tcInstSigTyVars, tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, tcSkolSigType, tcSkolSigTyVars, occurCheckErr, -------------------------------- -- Checking type validity - Rank, UserTypeCtxt(..), checkValidType, + Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType, SourceTyCtxt(..), checkValidTheta, checkFreeness, checkValidInstHead, checkValidInstance, checkInstTermination, checkValidTypeInst, checkTyFamFreeness, @@ -55,7 +56,7 @@ module TcMType ( -------------------------------- -- Zonking zonkType, zonkTcPredType, - zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar, zonkQuantifiedTyVar, zonkQuantifiedTyVars, zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType, zonkTcKindToKind, zonkTcKind, zonkTopTyVar, @@ -103,6 +104,7 @@ import Data.List ( (\\) ) tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables -> TcType -- Type to instantiate -> TcM ([TcTyVar], TcThetaType, TcType) -- Result + -- (type vars (excl coercion vars), preds (incl equalities), rho) tcInstType inst_tyvars ty = case tcSplitForAllTys ty of ([], rho) -> let -- There may be overloading despite no type variables; @@ -496,6 +498,15 @@ readMetaTyVar :: TyVar -> TcM MetaDetails readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) readMutVar (metaTvRef tyvar) +isFilledMetaTyVar :: TyVar -> TcM Bool +-- True of a filled-in (Indirect) meta type variable +isFilledMetaTyVar tv + | not (isTcTyVar tv) = return False + | MetaTv _ ref <- tcTyVarDetails tv + = do { details <- readMutVar ref + ; return (isIndirect details) } + | otherwise = return False + writeMetaTyVar :: TcTyVar -> TcType -> TcM () #ifndef DEBUG writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty) @@ -756,17 +767,17 @@ zonkTopTyVar tv k = tyVarKind tv default_k = defaultKind k -zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar] +zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar] zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar -zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar +zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it. -- -- 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 +-- The meta tyvar is updated to point to the new skolem TyVar. Now any -- bound occurences of the original type variable will get zonked to -- the immutable version. -- @@ -780,9 +791,11 @@ zonkQuantifiedTyVar tv | otherwise -- It's a meta-type-variable = do { details <- readMetaTyVar tv - -- Create the new, frozen, regular type variable + -- Create the new, frozen, skolem type variable + -- We zonk to a skolem, not to a regular TcVar + -- See Note [Zonking to Skolem] ; let final_kind = defaultKind (tyVarKind tv) - final_tv = mkTyVar (tyVarName tv) final_kind + final_tv = mkSkolTyVar (tyVarName tv) final_kind UnkSkol -- Bind the meta tyvar to the new tyvar ; case details of @@ -797,8 +810,8 @@ zonkQuantifiedTyVar tv ; return final_tv } \end{code} -[Silly Type Synonyms] - +Note [Silly Type Synonyms] +~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: type C u a = u -- Note 'a' unused @@ -832,6 +845,37 @@ Consider this: All very silly. I think its harmless to ignore the problem. We'll end up with a /\a in the final result but all the occurrences of a will be zonked to () +Note [Zonking to Skolem] +~~~~~~~~~~~~~~~~~~~~~~~~ +We used to zonk quantified type variables to regular TyVars. However, this +leads to problems. Consider this program from the regression test suite: + + eval :: Int -> String -> String -> String + eval 0 root actual = evalRHS 0 root actual + + evalRHS :: Int -> a + evalRHS 0 root actual = eval 0 root actual + +It leads to the deferral of an equality + + (String -> String -> String) ~ a + +which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck). +In the meantime `a' is zonked and quantified to form `evalRHS's signature. +This has the *side effect* of also zonking the `a' in the deferred equality +(which at this point is being handed around wrapped in an implication +constraint). + +Finally, the equality (with the zonked `a') will be handed back to the +simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop. +If we zonk `a' with a regular type variable, we will have this regular type +variable now floating around in the simplifier, which in many places assumes to +only see proper TcTyVars. + +We can avoid this problem by zonking with a skolem. The skolem is rigid +(which we requirefor a quantified variable), but is still a TcTyVar that the +simplifier knows how to deal with. + %************************************************************************ %* * @@ -966,9 +1010,9 @@ 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_UnboxedTuples `thenM` \ unboxed -> - doptM Opt_Rank2Types `thenM` \ rank2 -> - doptM Opt_RankNTypes `thenM` \ rankn -> + doptM Opt_UnboxedTuples `thenM` \ unboxed -> + doptM Opt_Rank2Types `thenM` \ rank2 -> + doptM Opt_RankNTypes `thenM` \ rankn -> doptM Opt_PolymorphicComponents `thenM` \ polycomp -> let rank | rankn = Arbitrary @@ -1010,9 +1054,12 @@ checkValidType ctxt ty checkTc kind_ok (kindErr actual_kind) `thenM_` -- Check the internal validity of the type itself - check_poly_type rank ubx_tup ty `thenM_` + check_type rank ubx_tup ty `thenM_` traceTc (text "checkValidType done" <+> ppr ty) + +checkValidMonoType :: Type -> TcM () +checkValidMonoType ty = check_mono_type ty \end{code} @@ -1023,116 +1070,95 @@ decRank :: Rank -> Rank decRank Arbitrary = Arbitrary decRank (Rank n) = Rank (n-1) +nonZeroRank :: Rank -> Bool +nonZeroRank (Rank 0) = False +nonZeroRank _ = True + ---------------------------------------- data UbxTupFlag = UT_Ok | UT_NotOk -- The "Ok" version means "ok if -fglasgow-exts is on" ---------------------------------------- -check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM () -check_poly_type (Rank 0) ubx_tup ty - = check_tau_type (Rank 0) ubx_tup ty - -check_poly_type rank ubx_tup ty - | 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 +check_mono_type :: Type -> TcM () -- No foralls anywhere + -- No unlifted types of any kind +check_mono_type ty + = do { check_type (Rank 0) UT_NotOk ty + ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } + +check_type :: Rank -> UbxTupFlag -> Type -> TcM () +-- The args say what the *type* context requires, independent +-- of *flag* settings. You test the flag settings at usage sites. +-- +-- Rank is allowed rank for function args +-- Rank 0 means no for-alls anywhere + +check_type rank ubx_tup ty + | not (null tvs && null theta) + = do { checkTc (nonZeroRank rank) (forAllTyErr ty) + -- Reject e.g. (Maybe (?x::Int => Int)), + -- with a decent error message + ; check_valid_theta SigmaCtxt theta + ; check_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, --- or be the argument of a type constructor. --- Not an unboxed tuple, but now *can* be a forall (since impredicativity) --- Other unboxed types are very occasionally allowed as type --- arguments depending on the kind of the type constructor --- --- For example, we want to reject things like: --- --- instance Ord a => Ord (forall s. T s a) --- and --- g :: T s (forall b.b) --- --- NB: unboxed tuples can have polymorphic or unboxed args. --- This happens in the workers for functions returning --- product types with polymorphic components. --- But not in user code. --- Anyway, they are dealt with by a special case in check_tau_type - -check_arg_type ty - = check_poly_type Arbitrary UT_NotOk ty `thenM_` - checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) - ----------------------------------------- -check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM () --- Rank is allowed rank for function args --- No foralls otherwise - -check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty) -check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty) - -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message - -- Naked PredTys don't usually show up, but they can as a result of -- {-# SPECIALISE instance Ord Char #-} -- 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_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 (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 - -check_tau_type rank ubx_tup (NoteTy other_note ty) - = check_tau_type rank ubx_tup ty - -check_tau_type rank ubx_tup ty@(TyConApp tc tys) - | isSynTyCon tc - = do { -- It's OK to have an *over-applied* type synonym +check_type rank ubx_tup (PredTy sty) + = do { dflags <- getDOpts + ; check_pred_ty dflags TypeCtxt sty } + +check_type rank ubx_tup (TyVarTy _) = returnM () +check_type rank ubx_tup ty@(FunTy arg_ty res_ty) + = do { check_type (decRank rank) UT_NotOk arg_ty + ; check_type rank UT_Ok res_ty } + +check_type rank ubx_tup (AppTy ty1 ty2) + = do { check_arg_type rank ty1 + ; check_arg_type rank ty2 } + +check_type rank ubx_tup (NoteTy other_note ty) + = check_type rank ubx_tup ty + +check_type rank ubx_tup ty@(TyConApp tc tys) + | isSynTyCon tc + = do { -- Check that the synonym has enough args + -- This applies equally to open and closed synonyms + -- 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 -> 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 - -- 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 - } + checkTc (tyConArity tc <= length tys) arity_msg + + -- See Note [Liberal type synonyms] + ; liberal <- doptM Opt_LiberalTypeSynonyms + ; if not liberal || isOpenSynTyCon tc then + -- For H98 and synonym families, do check the type args + mappM_ check_mono_type tys + + else -- In the liberal case (only for closed syns), expand then check + case tcView ty of + Just ty' -> check_type rank ubx_tup ty' + Nothing -> pprPanic "check_tau_type" (ppr ty) + } | isUnboxedTupleTyCon tc - = 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 + = do { ub_tuples_allowed <- doptM Opt_UnboxedTuples + ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg + + ; impred <- doptM Opt_ImpredicativeTypes + ; let rank' = if impred then rank else Rank 0 + -- c.f. check_arg_type + -- However, args are allowed to be unlifted, or -- more unboxed tuples, so can't use check_arg_ty + ; mappM_ (check_type rank' UT_Ok) tys } | otherwise - = mappM_ check_arg_type tys + = mappM_ (check_arg_type rank) tys where ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False } @@ -1144,12 +1170,66 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) ubx_tup_msg = ubxArgTyErr ty ---------------------------------------- +check_arg_type :: Rank -> Type -> TcM () +-- The sort of type that can instantiate a type variable, +-- or be the argument of a type constructor. +-- Not an unboxed tuple, but now *can* be a forall (since impredicativity) +-- Other unboxed types are very occasionally allowed as type +-- arguments depending on the kind of the type constructor +-- +-- For example, we want to reject things like: +-- +-- instance Ord a => Ord (forall s. T s a) +-- and +-- g :: T s (forall b.b) +-- +-- NB: unboxed tuples can have polymorphic or unboxed args. +-- This happens in the workers for functions returning +-- product types with polymorphic components. +-- But not in user code. +-- Anyway, they are dealt with by a special case in check_tau_type + +check_arg_type rank ty + = do { impred <- doptM Opt_ImpredicativeTypes + ; let rank' = if impred then rank else Rank 0 -- Monotype unless impredicative + ; check_type rank' UT_NotOk ty + ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } + +---------------------------------------- forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty -unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty +unliftedArgErr ty = ptext SLIT("Illegal unlifted type:") <+> ppr ty ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind \end{code} +Note [Liberal type synonyms] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If -XLiberalTypeSynonyms is on, expand closed type synonyms *before* +doing validity checking. 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. + +IMPORTANT: suppose T is a type synonym. Then we must do validity +checking on an appliation (T ty1 ty2) + + *either* before expansion (i.e. check ty1, ty2) + *or* after expansion (i.e. expand T ty1 ty2, and then check) + BUT NOT BOTH + +If we do both, we get exponential behaviour!! + + data TIACons1 i r c = c i ::: r c + type TIACons2 t x = TIACons1 t (TIACons1 t x) + type TIACons3 t x = TIACons2 t (TIACons1 t x) + type TIACons4 t x = TIACons2 t (TIACons2 t x) + type TIACons7 t x = TIACons4 t (TIACons3 t x) + %************************************************************************ %* * @@ -1205,7 +1285,7 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys) ; checkTc (arity == n_tys) arity_err -- Check the form of the argument types - ; mappM_ check_arg_type tys + ; mappM_ check_mono_type tys ; checkTc (check_class_pred_tys dflags ctxt tys) (predTyVarErr pred $$ how_to_allow) } @@ -1222,13 +1302,11 @@ check_pred_ty dflags ctxt pred@(EqPred ty1 ty2) ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred) -- Check the form of the argument types - ; check_eq_arg_type ty1 - ; check_eq_arg_type ty2 + ; check_mono_type ty1 + ; check_mono_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 +check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_mono_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 @@ -1407,7 +1485,7 @@ checkValidInstHead ty -- Should be a source type Just (clas,tys) -> getDOpts `thenM` \ dflags -> - mappM_ check_arg_type tys `thenM_` + mappM_ check_mono_type tys `thenM_` check_inst_head dflags clas tys `thenM_` returnM (clas, tys) }} @@ -1423,7 +1501,13 @@ check_inst_head dflags clas tys checkTc (dopt Opt_MultiParamTypeClasses dflags || isSingleton tys) (instTypeErr (pprClassPred clas tys) head_one_type_msg) - mapM_ check_one tys + mapM_ check_mono_type tys + -- For now, I only allow tau-types (not polytypes) in + -- the head of an instance decl. + -- E.g. instance C (forall a. a->a) is rejected + -- One could imagine generalising that, but I'm not sure + -- what all the consequences might be + where head_type_synonym_msg = parens ( text "All instance types must be of the form (T t1 ... tn)" $$ @@ -1439,14 +1523,6 @@ check_inst_head dflags clas tys 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. - -- E.g. instance C (forall a. a->a) is rejected - -- One could imagine generalising that, but I'm not sure - -- what all the consequences might be - check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty - ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } - instTypeErr pp_ty msg = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, nest 4 msg]