X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=30917eff83083f91c82f4a7a5dd0495494e01c03;hp=767dbc236992d4eaf69a624e5bab86499991d54c;hb=49f976f35373adb95e8b7043ba1666d48e7f33f7;hpb=ad94d40948668032189ad22a0ad741ac1f645f50 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 767dbc2..30917ef 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -13,7 +13,7 @@ mutable type variables -- 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/CodingStyle#Warnings +-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings -- for details module TcMType ( @@ -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 @@ -34,27 +35,28 @@ module TcMType ( -------------------------------- -- Creating new coercion variables - newCoVars, + newCoVars, newMetaCoVar, -------------------------------- -- Instantiation tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, - tcInstSigTyVars, zonkSigTyVar, + tcInstSigTyVars, tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, - tcSkolSigType, tcSkolSigTyVars, + tcSkolSigType, tcSkolSigTyVars, occurCheckErr, -------------------------------- -- Checking type validity - Rank, UserTypeCtxt(..), checkValidType, + Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType, SourceTyCtxt(..), checkValidTheta, checkFreeness, - checkValidInstHead, checkValidInstance, checkAmbiguity, + checkValidInstHead, checkValidInstance, checkInstTermination, checkValidTypeInst, checkTyFamFreeness, - arityErr, + checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt, + unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs, -------------------------------- -- Zonking zonkType, zonkTcPredType, - zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar, zonkQuantifiedTyVar, zonkQuantifiedTyVars, zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType, zonkTcKindToKind, zonkTcKind, zonkTopTyVar, @@ -102,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; @@ -124,6 +127,265 @@ tcInstType inst_tyvars ty %************************************************************************ %* * + Updating tau types +%* * +%************************************************************************ + +Can't be in TcUnify, as we also need it in TcTyFuns. + +\begin{code} +type SwapFlag = Bool + -- False <=> the two args are (actual, expected) respectively + -- True <=> the two args are (expected, actual) respectively + +checkUpdateMeta :: SwapFlag + -> TcTyVar -> IORef MetaDetails -> TcType -> TcM () +-- Update tv1, which is flexi; occurs check is alrady done +-- The 'check' version does a kind check too +-- We do a sub-kind check here: we might unify (a b) with (c d) +-- where b::*->* and d::*; this should fail + +checkUpdateMeta swapped tv1 ref1 ty2 + = do { checkKinds swapped tv1 ty2 + ; updateMeta tv1 ref1 ty2 } + +updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM () +updateMeta tv1 ref1 ty2 + = ASSERT( isMetaTyVar tv1 ) + ASSERT( isBoxyTyVar tv1 || isTauTy ty2 ) + do { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 ) + ; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2) + ; writeMutVar ref1 (Indirect ty2) + } + +---------------- +checkKinds swapped tv1 ty2 +-- We're about to unify a type variable tv1 with a non-tyvar-type ty2. +-- ty2 has been zonked at this stage, which ensures that +-- its kind has as much boxity information visible as possible. + | tk2 `isSubKind` tk1 = return () + + | otherwise + -- Either the kinds aren't compatible + -- (can happen if we unify (a b) with (c d)) + -- or we are unifying a lifted type variable with an + -- unlifted type: e.g. (id 3#) is illegal + = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $ + unifyKindMisMatch k1 k2 + where + (k1,k2) | swapped = (tk2,tk1) + | otherwise = (tk1,tk2) + tk1 = tyVarKind tv1 + tk2 = typeKind ty2 + +---------------- +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) +-- (b) that ty is a monotype +-- Furthermore, in the interest of (b), if you find an +-- empty box (BoxTv that is Flexi), fill it in with a TauTv +-- +-- 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 + = 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' <- mapM go tys + ; return $ occurs (TyConApp tc) tys' } + 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 = return $ Left False -- (a) + | isTcTyVar tv = go_tyvar tv (tcTyVarDetails 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 $ 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 $ 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 -> do { ty <- fillBoxWithTau tv ref + ; return $ Right ty } + other -> return $ Right (TyVarTy tv) + } + + -- go_syn is called for synonyms only + -- See Note [Type synonyms and the occur check] + go_syn tc tys + | not (isTauTyCon tc) + = notMonoType orig_ty -- (b) again + | otherwise + = do { (msgs, mb_tys') <- tryTc (mapM go tys) + ; case mb_tys' of + + -- 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) + } + + -- 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 +-- tau-type meta-variable, whose print-name is the same as tv +-- Choosing the same name is good: when we instantiate a function +-- we allocate boxy tyvars with the same print-name as the quantified +-- tyvar; and then we often fill the box with a tau-tyvar, and again +-- we want to choose the same name. +fillBoxWithTau tv ref + = do { tv' <- tcInstTyVar tv -- Do not gratuitously forget + ; let tau = mkTyVarTy tv' -- name of the type variable + ; writeMutVar ref (Indirect tau) + ; 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} +unifyKindMisMatch ty1 ty2 = do + ty1' <- zonkTcKind ty1 + ty2' <- zonkTcKind ty2 + let + msg = hang (ptext SLIT("Couldn't match kind")) + 2 (sep [quotes (ppr ty1'), + ptext SLIT("against"), + quotes (ppr ty2')]) + failWithTc msg + +unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred + -- tv1 and ty2 are zonked already + = return msg + where + msg = (env2, ptext SLIT("When matching the kinds of") <+> + sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual]) + + (pp_expected, pp_actual) | swapped = (pp2, pp1) + | otherwise = (pp1, pp2) + (env1, tv1') = tidyOpenTyVar tidy_env tv1 + (env2, ty2') = tidyOpenType env1 ty2 + pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1) + pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2) +\end{code} + +Error message for failure due to an occurs check. + +\begin{code} +occurCheckErr :: TcType -> TcType -> TcM a +occurCheckErr ty containingTy + = do { env0 <- tcInitTidyEnv + ; ty' <- zonkTcType ty + ; containingTy' <- zonkTcType containingTy + ; let (env1, tidy_ty1) = tidyOpenType env0 ty' + (env2, tidy_ty2) = tidyOpenType env1 containingTy' + extra = sep [ppr tidy_ty1, char '=', ppr tidy_ty2] + ; failWithTcM (env2, hang msg 2 extra) } + where + msg = ptext SLIT("Occurs check: cannot construct the infinite type:") +\end{code} + +%************************************************************************ +%* * Kind variables %* * %************************************************************************ @@ -136,13 +398,16 @@ newCoVars spec (mkCoKind ty1 ty2) | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] } +newMetaCoVar :: TcType -> TcType -> TcM TcTyVar +newMetaCoVar ty1 ty2 = newMetaTyVar TauTv (mkCoKind ty1 ty2) + newKindVar :: TcM TcKind newKindVar = do { uniq <- newUnique ; ref <- newMutVar Flexi ; return (mkTyVarTy (mkKindVar uniq ref)) } newKindVars :: Int -> TcM [TcKind] -newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ()) +newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ()) \end{code} @@ -231,15 +496,22 @@ 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) -#else +writeMetaTyVar tyvar ty + | not debugIsOn = writeMutVar (metaTvRef tyvar) (Indirect ty) writeMetaTyVar tyvar ty | not (isMetaTyVar tyvar) = pprTrace "writeMetaTyVar" (ppr tyvar) $ - returnM () - + return () | otherwise = ASSERT( isMetaTyVar tyvar ) -- TOM: It should also work for coercions @@ -249,7 +521,6 @@ writeMetaTyVar tyvar ty where k1 = tyVarKind tyvar k2 = typeKind ty -#endif \end{code} @@ -264,12 +535,12 @@ newFlexiTyVar :: Kind -> TcM TcTyVar newFlexiTyVar kind = newMetaTyVar TauTv kind newFlexiTyVarTy :: Kind -> TcM TcType -newFlexiTyVarTy kind - = newFlexiTyVar kind `thenM` \ tc_tyvar -> - returnM (TyVarTy tc_tyvar) +newFlexiTyVarTy kind = do + tc_tyvar <- newFlexiTyVar kind + return (TyVarTy tc_tyvar) newFlexiTyVarTys :: Int -> Kind -> TcM [TcType] -newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind) +newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind) tcInstTyVar :: TyVar -> TcM TcTyVar -- Instantiate with a META type variable @@ -280,7 +551,7 @@ tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst) tcInstTyVars tyvars = do { tc_tvs <- mapM tcInstTyVar tyvars ; let tys = mkTyVarTys tc_tvs - ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) } + ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) } -- Since the tyvars are freshly made, -- they cannot possibly be captured by -- any existing for-alls. Hence zipTopTvSubst @@ -381,33 +652,33 @@ lookupTcTyVar tyvar getTcTyVar tyvar | not (isTcTyVar tyvar) = pprTrace "getTcTyVar" (ppr tyvar) $ - returnM (Just (mkTyVarTy tyvar)) + return (Just (mkTyVarTy tyvar)) | otherwise - = ASSERT2( isTcTyVar tyvar, ppr tyvar ) - readMetaTyVar tyvar `thenM` \ maybe_ty -> + = ASSERT2( isTcTyVar tyvar, ppr tyvar ) do + maybe_ty <- readMetaTyVar tyvar case maybe_ty of - Just ty -> short_out ty `thenM` \ ty' -> - writeMetaTyVar tyvar (Just ty') `thenM_` - returnM (Just ty') + Just ty -> do ty' <- short_out ty + writeMetaTyVar tyvar (Just ty') + return (Just ty') - Nothing -> returnM Nothing + Nothing -> return Nothing short_out :: TcType -> TcM TcType short_out ty@(TyVarTy tyvar) | not (isTcTyVar tyvar) - = returnM ty + = return ty - | otherwise - = readMetaTyVar tyvar `thenM` \ maybe_ty -> + | otherwise = do + maybe_ty <- readMetaTyVar tyvar case maybe_ty of - Just ty' -> short_out ty' `thenM` \ ty' -> - writeMetaTyVar tyvar (Just ty') `thenM_` - returnM ty' + Just ty' -> do ty' <- short_out ty' + writeMetaTyVar tyvar (Just ty') + return ty' - other -> returnM ty + other -> return ty -short_out other_ty = returnM other_ty +short_out other_ty = return other_ty -} \end{code} @@ -422,45 +693,37 @@ short_out other_ty = returnM other_ty \begin{code} zonkTcTyVars :: [TcTyVar] -> TcM [TcType] -zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars +zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet -zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys -> - returnM (tyVarsOfTypes tys) +zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar tyvars zonkTcTyVar :: TcTyVar -> TcM TcType zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar) - zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar + zonk_tc_tyvar (\ tv -> return (TyVarTy tv)) tyvar \end{code} ----------------- Types \begin{code} zonkTcType :: TcType -> TcM TcType -zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty +zonkTcType ty = zonkType (\ tv -> return (TyVarTy tv)) ty zonkTcTypes :: [TcType] -> TcM [TcType] -zonkTcTypes tys = mappM zonkTcType tys +zonkTcTypes tys = mapM zonkTcType tys -zonkTcClassConstraints cts = mappM zonk cts - where zonk (clas, tys) - = zonkTcTypes tys `thenM` \ new_tys -> - returnM (clas, new_tys) +zonkTcClassConstraints cts = mapM zonk cts + where zonk (clas, tys) = do + new_tys <- zonkTcTypes tys + return (clas, new_tys) zonkTcThetaType :: TcThetaType -> TcM TcThetaType -zonkTcThetaType theta = mappM zonkTcPredType theta +zonkTcThetaType theta = mapM zonkTcPredType theta zonkTcPredType :: TcPredType -> TcM TcPredType -zonkTcPredType (ClassP c ts) - = zonkTcTypes ts `thenM` \ new_ts -> - returnM (ClassP c new_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) +zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts +zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t +zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2 \end{code} ------------------- These ...ToType, ...ToKind versions @@ -491,17 +754,17 @@ zonkTopTyVar tv k = tyVarKind tv default_k = defaultKind k -zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar] -zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar +zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar] +zonkQuantifiedTyVars = mapM 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. -- @@ -515,9 +778,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 @@ -532,8 +797,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 @@ -567,6 +832,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. + %************************************************************************ %* * @@ -588,21 +884,19 @@ zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type varia zonkType unbound_var_fn ty = go ty where - go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations - - go (TyConApp tc tys) = mappM go tys `thenM` \ tys' -> - returnM (TyConApp tc tys') - - go (PredTy p) = go_pred p `thenM` \ p' -> - returnM (PredTy p') - - go (FunTy arg res) = go arg `thenM` \ arg' -> - go res `thenM` \ res' -> - returnM (FunTy arg' res') - - go (AppTy fun arg) = go fun `thenM` \ fun' -> - go arg `thenM` \ arg' -> - returnM (mkAppTy fun' arg') + go (TyConApp tc tys) = do tys' <- mapM go tys + return (TyConApp tc tys') + + 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') -- NB the mkAppTy; we might have instantiated a -- type variable to a type constructor, so we need -- to pull the TyConApp to the top. @@ -612,23 +906,23 @@ zonkType unbound_var_fn ty | otherwise = return (TyVarTy tyvar) -- Ordinary (non Tc) tyvars occur inside quantified types - go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) - go ty `thenM` \ ty' -> - returnM (ForAllTy tyvar ty') + go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do + ty' <- go ty + return (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 (EqPred ty1 ty2) = go ty1 `thenM` \ ty1' -> - go ty2 `thenM` \ ty2' -> - returnM (EqPred ty1' ty2') + 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 ty1 ty2) = do ty1' <- go ty1 + ty2' <- go ty2 + return (EqPred ty1' ty2') zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable -> TcTyVar -> TcM TcType zonk_tc_tyvar unbound_var_fn tyvar | not (isMetaTyVar tyvar) -- Skolems - = returnM (TyVarTy tyvar) + = return (TyVarTy tyvar) | otherwise -- Mutables = do { cts <- readMetaTyVar tyvar @@ -699,12 +993,12 @@ This might not necessarily show up in kind checking. \begin{code} 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_PolymorphicComponents `thenM` \ polycomp -> +checkValidType ctxt ty = do + traceTc (text "checkValidType" <+> ppr ty) + unboxed <- doptM Opt_UnboxedTuples + rank2 <- doptM Opt_Rank2Types + rankn <- doptM Opt_RankNTypes + polycomp <- doptM Opt_PolymorphicComponents let rank | rankn = Arbitrary | rank2 = Rank 2 @@ -740,14 +1034,17 @@ checkValidType ctxt ty 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_` + checkTc kind_ok (kindErr actual_kind) -- Check the internal validity of the type itself - check_poly_type rank ubx_tup ty `thenM_` + check_type rank ubx_tup ty traceTc (text "checkValidType done" <+> ppr ty) + +checkValidMonoType :: Type -> TcM () +checkValidMonoType ty = check_mono_type ty \end{code} @@ -758,116 +1055,92 @@ 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 _) = return () +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 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 + mapM_ 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 + ; mapM_ (check_type rank' UT_Ok) tys } | otherwise - = mappM_ check_arg_type tys + = mapM_ (check_arg_type rank) tys where ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False } @@ -879,12 +1152,65 @@ 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) %************************************************************************ @@ -926,21 +1252,22 @@ checkValidTheta ctxt theta ------------------------- check_valid_theta ctxt [] - = returnM () -check_valid_theta ctxt theta - = getDOpts `thenM` \ dflags -> - warnTc (notNull dups) (dupPredWarn dups) `thenM_` - mappM_ (check_pred_ty dflags ctxt) theta + = return () +check_valid_theta ctxt theta = do + dflags <- getDOpts + warnTc (notNull dups) (dupPredWarn dups) + mapM_ (check_pred_ty dflags ctxt) theta where (_,dups) = removeDups tcCmpPred theta ------------------------- +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 + ; mapM_ check_mono_type tys ; checkTc (check_class_pred_tys dflags ctxt tys) (predTyVarErr pred $$ how_to_allow) } @@ -957,13 +1284,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 @@ -978,6 +1303,7 @@ check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty 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 @@ -1028,19 +1354,16 @@ 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 - = mappM_ complain (filter is_ambig theta) + = mapM_ complain (filter is_ambig theta) where 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)) @@ -1061,7 +1384,7 @@ even in a scope where b is in scope. \begin{code} checkFreeness forall_tyvars theta = do { flexible_contexts <- doptM Opt_FlexibleContexts - ; unless flexible_contexts $ mappM_ complain (filter is_free theta) } + ; unless flexible_contexts $ mapM_ complain (filter is_free theta) } where is_free pred = not (isIPPred pred) && not (any bound_var (varSetElems (tyVarsOfPred pred))) @@ -1069,10 +1392,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} @@ -1083,7 +1409,7 @@ checkThetaCtxt ctxt theta badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty eqPredTyErr sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty $$ - parens (ptext SLIT("Use -ftype-families to permit this")) + 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) @@ -1095,6 +1421,21 @@ arityErr kind name n m n_arguments | n == 0 = ptext SLIT("no arguments") | n == 1 = ptext SLIT("1 argument") | True = hsep [int n, ptext SLIT("arguments")] + +----------------- +notMonoType ty + = do { ty' <- zonkTcType ty + ; env0 <- tcInitTidyEnv + ; let (env1, tidy_ty) = tidyOpenType env0 ty' + msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty) + ; failWithTcM (env1, msg) } + +notMonoArgs ty + = do { ty' <- zonkTcType ty + ; env0 <- tcInitTidyEnv + ; let (env1, tidy_ty) = tidyOpenType env0 ty' + msg = ptext SLIT("Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty) + ; failWithTcM (env1, msg) } \end{code} @@ -1123,12 +1464,12 @@ checkValidInstHead ty -- Should be a source type case getClassPredTys_maybe pred of { Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ; - Just (clas,tys) -> + Just (clas,tys) -> do - getDOpts `thenM` \ dflags -> - mappM_ check_arg_type tys `thenM_` - check_inst_head dflags clas tys `thenM_` - returnM (clas, tys) + dflags <- getDOpts + mapM_ check_mono_type tys + check_inst_head dflags clas tys + return (clas, tys) }} check_inst_head dflags clas tys @@ -1142,30 +1483,29 @@ 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)" $$ 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_type_args_tyvars_msg = parens (vcat [ + text "All instance types must be of the form (T a1 ... an)", + text "where a1 ... an are type *variables*,", + text "and each type variable appears at most once in the instance head.", + text "Use -XFlexibleInstances if you want to disable this."]) 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. - -- 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] @@ -1245,7 +1585,72 @@ undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this") %************************************************************************ %* * -\subsection{Checking type instance well-formedness and termination} + 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 %* * %************************************************************************ @@ -1257,7 +1662,7 @@ checkValidTypeInst :: [Type] -> Type -> TcM () checkValidTypeInst typats rhs = do { -- left-hand side contains no type family applications -- (vanilla synonyms are fine, though) - ; mappM_ checkTyFamFreeness typats + ; mapM_ checkTyFamFreeness typats -- the right-hand side is a tau type ; checkTc (isTauTy rhs) $ @@ -1340,7 +1745,6 @@ fvType :: Type -> [TyVar] fvType ty | Just exp_ty <- tcView ty = fvType exp_ty fvType (TyVarTy tv) = [tv] fvType (TyConApp _ tys) = fvTypes tys -fvType (NoteTy _ ty) = fvType ty fvType (PredTy pred) = fvPred pred fvType (FunTy arg res) = fvType arg ++ fvType res fvType (AppTy fun arg) = fvType fun ++ fvType arg @@ -1359,7 +1763,6 @@ sizeType :: Type -> Int sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty sizeType (TyVarTy _) = 1 sizeType (TyConApp _ tys) = sizeTypes tys + 1 -sizeType (NoteTy _ ty) = sizeType ty sizeType (PredTy pred) = sizePred pred sizeType (FunTy arg res) = sizeType arg + sizeType res + 1 sizeType (AppTy fun arg) = sizeType fun + sizeType arg @@ -1372,16 +1775,4 @@ sizePred :: PredType -> Int sizePred (ClassP _ tys') = sizeTypes tys' sizePred (IParam _ ty) = sizeType ty sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 - --- Type family instances occuring in a type after expanding synonyms -tyFamInsts :: Type -> [(TyCon, [Type])] -tyFamInsts ty - | Just exp_ty <- tcView ty = tyFamInsts exp_ty -tyFamInsts (TyVarTy _) = [] -tyFamInsts (TyConApp tc tys) - | isOpenSynTyCon tc = [(tc, tys)] - | otherwise = concat (map tyFamInsts tys) -tyFamInsts (FunTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 -tyFamInsts (AppTy ty1 ty2) = tyFamInsts ty1 ++ tyFamInsts ty2 -tyFamInsts (ForAllTy _ ty) = tyFamInsts ty \end{code}