X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=3357004df441aedb86d08f6ae57b5aa1faf7fde9;hp=13fbf557d100728e4da90085e83f3b448ea4918c;hb=3f1b316d7035c55cd712cd39a9981339bcef2e8c;hpb=6d2b0ae3ae3296cb6cdd496cbf85b897c7ce150b diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 13fbf55..3357004 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,7 +40,7 @@ module TcMType ( -------------------------------- -- Instantiation tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, - tcInstSigTyVars, zonkSigTyVar, + tcInstSigTyVars, tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, tcSkolSigType, tcSkolSigTyVars, occurCheckErr, @@ -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, @@ -177,7 +178,7 @@ checkKinds swapped tv1 ty2 tk2 = typeKind ty2 ---------------- -checkTauTvUpdate :: TcTyVar -> TcType -> TcM TcType +checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType) -- (checkTauTvUpdate tv ty) -- We are about to update the TauTv tv with ty. -- Check (a) that tv doesn't occur in ty (occurs check) @@ -185,42 +186,79 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM TcType -- Furthermore, in the interest of (b), if you find an -- empty box (BoxTv that is Flexi), fill it in with a TauTv -- --- Returns the (non-boxy) type to update the type variable with, or fails +-- We have three possible outcomes: +-- (1) Return the (non-boxy) type to update the type variable with, +-- [we know the update is ok!] +-- (2) return Nothing, or +-- [we cannot tell whether the update is ok right now] +-- (3) fails. +-- [the update is definitely invalid] +-- We return Nothing in case the tv occurs in ty *under* a type family +-- application. In this case, we must not update tv (to avoid a cyclic type +-- term), but we also cannot fail claiming an infinite type. Given +-- type family F a +-- type instance F Int = Int +-- consider +-- a ~ F a +-- This is perfectly reasonable, if we later get a ~ Int. checkTauTvUpdate orig_tv orig_ty - = go orig_ty + = do { result <- go orig_ty + ; case result of + Right ty -> return $ Just ty + Left True -> return $ Nothing + Left False -> occurCheckErr (mkTyVarTy orig_tv) orig_ty + } where + go :: TcType -> TcM (Either Bool TcType) + -- go returns + -- Right ty if everything is fine + -- Left True if orig_tv occurs in orig_ty, but under a type family app + -- Left False if orig_tv occurs in orig_ty (with no type family app) + -- It fails if it encounters a forall type, except as an argument for a + -- closed type synonym that expands to a tau type. go (TyConApp tc tys) | isSynTyCon tc = go_syn tc tys - | otherwise = do { tys' <- mappM go tys; return (TyConApp tc tys') } + | otherwise = do { tys' <- mappM go tys + ; return $ occurs (TyConApp tc) tys' } go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations - go (PredTy p) = do { p' <- go_pred p; return (PredTy p') } - go (FunTy arg res) = do { arg' <- go arg; res' <- go res; return (FunTy arg' res') } - go (AppTy fun arg) = do { fun' <- go fun; arg' <- go arg; return (mkAppTy fun' arg') } + go (PredTy p) = do { p' <- go_pred p + ; return $ occurs1 PredTy p' } + go (FunTy arg res) = do { arg' <- go arg + ; res' <- go res + ; return $ occurs2 FunTy arg' res' } + go (AppTy fun arg) = do { fun' <- go fun + ; arg' <- go arg + ; return $ occurs2 mkAppTy fun' arg' } -- NB the mkAppTy; we might have instantiated a -- type variable to a type constructor, so we need -- to pull the TyConApp to the top. go (ForAllTy tv ty) = notMonoType orig_ty -- (b) go (TyVarTy tv) - | orig_tv == tv = occurCheck tv -- (a) + | orig_tv == tv = return $ Left False -- (a) | isTcTyVar tv = go_tyvar tv (tcTyVarDetails tv) - | otherwise = return (TyVarTy tv) + | otherwise = return $ Right (TyVarTy tv) -- Ordinary (non Tc) tyvars -- occur inside quantified types - go_pred (ClassP c tys) = do { tys' <- mapM go tys; return (ClassP c tys') } - go_pred (IParam n ty) = do { ty' <- go ty; return (IParam n ty') } - go_pred (EqPred t1 t2) = do { t1' <- go t1; t2' <- go t2; return (EqPred t1' t2') } + go_pred (ClassP c tys) = do { tys' <- mapM go tys + ; return $ occurs (ClassP c) tys' } + go_pred (IParam n ty) = do { ty' <- go ty + ; return $ occurs1 (IParam n) ty' } + go_pred (EqPred t1 t2) = do { t1' <- go t1 + ; t2' <- go t2 + ; return $ occurs2 EqPred t1' t2' } - go_tyvar tv (SkolemTv _) = return (TyVarTy tv) + go_tyvar tv (SkolemTv _) = return $ Right (TyVarTy tv) go_tyvar tv (MetaTv box ref) = do { cts <- readMutVar ref ; case cts of Indirect ty -> go ty Flexi -> case box of - BoxTv -> fillBoxWithTau tv ref - other -> return (TyVarTy tv) + BoxTv -> do { ty <- fillBoxWithTau tv ref + ; return $ Right ty } + other -> return $ Right (TyVarTy tv) } -- go_syn is called for synonyms only @@ -231,18 +269,40 @@ checkTauTvUpdate orig_tv orig_ty | otherwise = do { (msgs, mb_tys') <- tryTc (mapM go tys) ; case mb_tys' of - Just tys' -> return (TyConApp tc tys') - -- Retain the synonym (the common case) - Nothing | isOpenTyCon tc - -> notMonoArgs (TyConApp tc tys) - -- Synonym families must have monotype args - | otherwise - -> go (expectJust "checkTauTvUpdate" - (tcView (TyConApp tc tys))) - -- Try again, expanding the synonym + + -- we had a type error => forall in type parameters + Nothing + | isOpenTyCon tc -> notMonoArgs (TyConApp tc tys) + -- Synonym families must have monotype args + | otherwise -> go (expectJust "checkTauTvUpdate(1)" + (tcView (TyConApp tc tys))) + -- Try again, expanding the synonym + + -- no type error, but need to test whether occurs check happend + Just tys' -> + case occurs id tys' of + Left _ + | isOpenTyCon tc -> return $ Left True + -- Variable occured under type family application + | otherwise -> go (expectJust "checkTauTvUpdate(2)" + (tcView (TyConApp tc tys))) + -- Try again, expanding the synonym + Right raw_tys' -> return $ Right (TyConApp tc raw_tys') + -- Retain the synonym (the common case) } - occurCheck tv = occurCheckErr (mkTyVarTy tv) orig_ty + -- Left results (= occurrence of orig_ty) dominate and + -- (Left False) (= fatal occurrence) dominates over (Left True) + occurs :: ([a] -> b) -> [Either Bool a] -> Either Bool b + occurs c = either Left (Right . c) . foldr combine (Right []) + where + combine (Left famInst1) (Left famInst2) = Left (famInst1 && famInst2) + combine (Right _ ) (Left famInst) = Left famInst + combine (Left famInst) (Right _) = Left famInst + combine (Right arg) (Right args) = Right (arg:args) + + occurs1 c x = occurs (\[x'] -> c x') [x] + occurs2 c x y = occurs (\[x', y'] -> c x' y') [x, y] fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType -- (fillBoxWithTau tv ref) fills ref with a freshly allocated @@ -258,6 +318,28 @@ fillBoxWithTau tv ref ; return tau } \end{code} +Note [Type synonyms and the occur check] +~~~~~~~~~~~~~~~~~~~~ +Basically we want to update tv1 := ps_ty2 +because ps_ty2 has type-synonym info, which improves later error messages + +But consider + type A a = () + + f :: (A a -> a -> ()) -> () + f = \ _ -> () + + x :: () + x = f (\ x p -> p x) + +In the application (p x), we try to match "t" with "A t". If we go +ahead and bind t to A t (= ps_ty2), we'll lead the type checker into +an infinite loop later. +But we should not reject the program, because A t = (). +Rather, we should bind t to () (= non_var_ty2). + +-------------- + Error mesages in case of kind mismatch. \begin{code} @@ -415,6 +497,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) @@ -675,17 +766,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. -- @@ -699,9 +790,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 @@ -716,8 +809,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 @@ -751,6 +844,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. + %************************************************************************ %* * @@ -1014,34 +1138,26 @@ 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 + | 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 + 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_arg_type tys - } + + else -- In the liberal case (only for closed syns), expand then check + case tcView ty of + Just ty' -> check_tau_type rank ubx_tup ty' + Nothing -> pprPanic "check_tau_type" (ppr ty) + } | isUnboxedTupleTyCon tc = doptM Opt_UnboxedTuples `thenM` \ ub_tuples_allowed -> @@ -1069,6 +1185,34 @@ ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument 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) + %************************************************************************ %* *