X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=2c01d2300a4505c34164414c5f746b6d8f862d7c;hp=525ba0d29ac3fc74bd6fde1c5323c6fe8b3da003;hb=febf1ced754a3996ac1a5877dcded87828560d1c;hpb=296058a1cafa80dec0b3f998348bce7c65f668b0 diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 525ba0d..2c01d23 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -18,42 +18,48 @@ module TcMType ( newFlexiTyVarTy, -- Kind -> TcM TcType newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] newKindVar, newKindVars, - lookupTcTyVar, LookupTyVarResult(..), + mkTcTyVarName, - newMetaTyVar, readMetaTyVar, writeMetaTyVar, isFilledMetaTyVar, + newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, + isFilledMetaTyVar, isFlexiMetaTyVar, -------------------------------- - -- Boxy type variables - newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, + -- Creating new evidence variables + newEvVar, newCoVar, newEvVars, + newIP, newDict, newSilentGiven, isSilentEvVar, - -------------------------------- - -- Creating new coercion variables - newCoVars, newMetaCoVar, + newWantedEvVar, newWantedEvVars, + newTcEvBinds, addTcEvBind, -------------------------------- -- Instantiation - tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, - tcInstSigType, - tcInstSkolTyVars, tcInstSkolType, - tcSkolSigType, tcSkolSigTyVars, occurCheckErr, execTcTyVarBinds, + tcInstTyVars, tcInstSigTyVars, + tcInstType, + tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType, + tcSkolDFunType, tcSuperSkolTyVars, -------------------------------- -- Checking type validity Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType, - SourceTyCtxt(..), checkValidTheta, checkFreeness, + SourceTyCtxt(..), checkValidTheta, checkValidInstHead, checkValidInstance, - checkInstTermination, checkValidTypeInst, checkTyFamFreeness, checkKinds, - checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt, - unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs, - growPredTyVars, growTyVars, growThetaTyVars, + checkInstTermination, checkValidTypeInst, checkTyFamFreeness, + arityErr, + growPredTyVars, growThetaTyVars, validDerivPred, -------------------------------- -- Zonking - zonkType, zonkTcPredType, + zonkType, mkZonkTcTyVar, zonkTcPredType, + zonkTcTypeCarefully, skolemiseUnboundMetaTyVar, zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar, zonkQuantifiedTyVar, zonkQuantifiedTyVars, zonkTcType, zonkTcTypes, zonkTcThetaType, - zonkTcKindToKind, zonkTcKind, zonkTopTyVar, + zonkTcKindToKind, zonkTcKind, + zonkImplication, zonkEvVar, zonkWantedEvVar, zonkFlavoredEvVar, + zonkWC, zonkWantedEvVars, + zonkTcTypeAndSubst, + tcGetGlobalTyVars, + readKindVar, writeKindVar ) where @@ -64,428 +70,202 @@ module TcMType ( import TypeRep import TcType import Type -import Coercion import Class import TyCon import Var -- others: -import TcRnMonad -- TcType, amongst others +import HsSyn -- HsType +import TcRnMonad -- TcType, amongst others +import Id import FunDeps import Name -import VarEnv import VarSet import ErrUtils import DynFlags import Util -import Bag import Maybes import ListSetOps -import UniqSupply +import BasicTypes import SrcLoc import Outputable import FastString +import Unique( Unique ) +import Bag import Control.Monad -import Data.List ( (\\) ) +import Data.List ( (\\) ) \end{code} %************************************************************************ %* * - Instantiation in general + Kind variables %* * %************************************************************************ \begin{code} -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; - -- (?x :: Int) => Int -> Int - (theta, tau) = tcSplitPhiTy rho - in - return ([], theta, tau) - - (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars - - ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars') - -- Either the tyvars are freshly made, by inst_tyvars, - -- or (in the call from tcSkolSigType) any nested foralls - -- have different binders. Either way, zipTopTvSubst is ok +newKindVar :: TcM TcKind +newKindVar = do { uniq <- newUnique + ; ref <- newMutVar Flexi + ; return (mkTyVarTy (mkKindVar uniq ref)) } - ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho) - ; return (tyvars', theta, tau) } +newKindVars :: Int -> TcM [TcKind] +newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ()) \end{code} %************************************************************************ %* * - Updating tau types + Evidence variables; range over constraints we can abstract over %* * %************************************************************************ -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 :: Bool -> TyVar -> Type -> TcM () -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 _ _) = 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 } - _ -> 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 = () +newEvVars :: TcThetaType -> TcM [EvVar] +newEvVars theta = mapM newEvVar theta - f :: (A a -> a -> ()) -> () - f = \ _ -> () +newWantedEvVar :: TcPredType -> TcM EvVar +newWantedEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2 +newWantedEvVar (ClassP cls tys) = newDict cls tys +newWantedEvVar (IParam ip ty) = newIP ip ty - 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). +newWantedEvVars :: TcThetaType -> TcM [EvVar] +newWantedEvVars theta = mapM newWantedEvVar theta -------------- +newEvVar :: TcPredType -> TcM EvVar +-- Creates new *rigid* variables for predicates +newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2 +newEvVar (ClassP cls tys) = newDict cls tys +newEvVar (IParam ip ty) = newIP ip ty + +newCoVar :: TcType -> TcType -> TcM CoVar +newCoVar ty1 ty2 + = do { name <- newName (mkVarOccFS (fsLit "co")) + ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) } + +newIP :: IPName Name -> TcType -> TcM IpId +newIP ip ty + = do { name <- newName (getOccName (ipNameName ip)) + ; return (mkLocalId name (mkPredTy (IParam ip ty))) } + +newDict :: Class -> [TcType] -> TcM DictId +newDict cls tys + = do { name <- newName (mkDictOcc (getOccName cls)) + ; return (mkLocalId name (mkPredTy (ClassP cls tys))) } + +newName :: OccName -> TcM Name +newName occ + = do { uniq <- newUnique + ; loc <- getSrcSpanM + ; return (mkInternalName uniq occ loc) } -Execute a bag of type variable bindings. - -\begin{code} -execTcTyVarBinds :: TcTyVarBinds -> TcM () -execTcTyVarBinds = mapM_ execTcTyVarBind . bagToList - where - execTcTyVarBind (TcTyVarBind tv ty) - = do { ASSERTM2( do { details <- readMetaTyVar tv - ; return (isFlexi details) }, ppr tv ) - ; ty' <- if isCoVar tv - then return ty - else do { maybe_ty <- checkTauTvUpdate tv ty - ; case maybe_ty of - Nothing -> pprPanic "TcRnMonad.execTcTyBind" - (ppr tv <+> text ":=" <+> ppr ty) - Just ty' -> return ty' - } - ; writeMetaTyVar tv ty' - } -\end{code} - -Error mesages in case of kind mismatch. - -\begin{code} -unifyKindMisMatch :: TcKind -> TcKind -> TcM () -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 :: Bool -> TyVar -> Type -> TidyEnv -> TcM (TidyEnv, SDoc) -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) +----------------- +newSilentGiven :: PredType -> TcM EvVar +-- Make a dictionary for a "silent" given dictionary +-- Behaves just like any EvVar except that it responds True to isSilentDict +-- This is used only to suppress confusing error reports +newSilentGiven (ClassP cls tys) + = do { uniq <- newUnique + ; let name = mkSystemName uniq (mkDictOcc (getOccName cls)) + ; return (mkLocalId name (mkPredTy (ClassP cls tys))) } +newSilentGiven (EqPred ty1 ty2) + = do { uniq <- newUnique + ; let name = mkSystemName uniq (mkTyVarOccFS (fsLit "co")) + ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) } +newSilentGiven pred@(IParam {}) + = pprPanic "newSilentDict" (ppr pred) -- Implicit parameters rejected earlier + +isSilentEvVar :: EvVar -> Bool +isSilentEvVar v = isSystemName (Var.varName v) + -- Notice that all *other* evidence variables get Internal Names \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 + SkolemTvs (immutable) %* * %************************************************************************ \begin{code} -newCoVars :: [(TcType,TcType)] -> TcM [CoVar] -newCoVars spec - = do { us <- newUniqueSupply - ; return [ mkCoVar (mkSysTvName uniq (fsLit "co")) - (mkCoKind ty1 ty2) - | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] } - -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 = mapM (\ _ -> newKindVar) (nOfThem n ()) -\end{code} +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; + -- (?x :: Int) => Int -> Int + (theta, tau) = tcSplitPhiTy rho + in + return ([], theta, tau) + (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars -%************************************************************************ -%* * - SkolemTvs (immutable) -%* * -%************************************************************************ + ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars') + -- Either the tyvars are freshly made, by inst_tyvars, + -- or any nested foralls have different binders. + -- Either way, zipTopTvSubst is ok -\begin{code} -mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar -mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info) + ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho) + ; return (tyvars', theta, tau) } -tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType) +tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType) -- Instantiate a type signature with skolem constants, but -- do *not* give them fresh names, because we want the name to --- be in the type environment -- it is lexically scoped. -tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty +-- be in the type environment: it is lexically scoped. +tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty -tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar] +tcSuperSkolTyVars :: [TyVar] -> [TcTyVar] -- Make skolem constants, but do *not* give them new names, as above -tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info - | tv <- tyvars ] +-- Moreover, make them "super skolems"; see comments with superSkolemTv +tcSuperSkolTyVars tyvars + = [ mkTcTyVar (tyVarName tv) (tyVarKind tv) superSkolemTv + | tv <- tyvars ] -tcInstSkolTyVar :: SkolemInfo -> (Name -> SrcSpan) -> TyVar -> TcM TcTyVar +tcInstSkolTyVar :: Bool -> TyVar -> TcM TcTyVar -- Instantiate the tyvar, using -- * the occ-name and kind of the supplied tyvar, -- * the unique from the monad, --- * the location either from the tyvar (mb_loc = Nothing) --- or from mb_loc (Just loc) -tcInstSkolTyVar info get_loc tyvar +-- * the location either from the tyvar (skol_info = SigSkol) +-- or from the monad (otherwise) +tcInstSkolTyVar overlappable tyvar = do { uniq <- newUnique - ; let old_name = tyVarName tyvar - kind = tyVarKind tyvar - loc = get_loc old_name - new_name = mkInternalName uniq (nameOccName old_name) loc - ; return (mkSkolTyVar new_name kind info) } - -tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] --- Get the location from the monad -tcInstSkolTyVars info tyvars - = do { span <- getSrcSpanM - ; mapM (tcInstSkolTyVar info (const span)) tyvars } - -tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType) + ; loc <- getSrcSpanM + ; let new_name = mkInternalName uniq occ loc + ; return (mkTcTyVar new_name kind (SkolemTv overlappable)) } + where + old_name = tyVarName tyvar + occ = nameOccName old_name + kind = tyVarKind tyvar + +tcInstSkolTyVars :: [TyVar] -> TcM [TcTyVar] +tcInstSkolTyVars tyvars = mapM (tcInstSkolTyVar False) tyvars + +tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar] +tcInstSuperSkolTyVars tyvars = mapM (tcInstSkolTyVar True) tyvars + +tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType) -- Instantiate a type with fresh skolem constants -- Binding location comes from the monad -tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty +tcInstSkolType ty = tcInstType tcInstSkolTyVars ty -tcInstSigType :: Bool -> SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType) --- Instantiate with skolems or meta SigTvs; depending on use_skols --- Always take location info from the supplied tyvars -tcInstSigType use_skols skol_info ty - = tcInstType (mapM inst_tyvar) ty - where - inst_tyvar | use_skols = tcInstSkolTyVar skol_info getSrcSpan - | otherwise = instMetaTyVar (SigTv skol_info) +tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar] +-- Make meta SigTv type variables for patten-bound scoped type varaibles +-- We use SigTvs for them, so that they can't unify with arbitrary types +tcInstSigTyVars = mapM tcInstSigTyVar + +tcInstSigTyVar :: TyVar -> TcM TcTyVar +tcInstSigTyVar tyvar + = do { uniq <- newMetaUnique + ; ref <- newMutVar Flexi + ; let name = setNameUnique (tyVarName tyvar) uniq + -- Use the same OccName so that the tidy-er + -- doesn't rename 'a' to 'a0' etc + kind = tyVarKind tyvar + ; return (mkTcTyVar name kind (MetaTv SigTv ref)) } \end{code} @@ -496,31 +276,22 @@ tcInstSigType use_skols skol_info ty %************************************************************************ \begin{code} -newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar +newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar -- Make a new meta tyvar out of thin air -newMetaTyVar box_info kind - = do { uniq <- newUnique - ; ref <- newMutVar Flexi - ; let name = mkSysTvName uniq fs - fs = case box_info of - BoxTv -> fsLit "t" - TauTv -> fsLit "t" - SigTv _ -> fsLit "a" - -- We give BoxTv and TauTv the same string, because - -- otherwise we get user-visible differences in error - -- messages, which are confusing. If you want to see - -- the box_info of each tyvar, use -dppr-debug - ; return (mkTcTyVar name kind (MetaTv box_info ref)) } - -instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar --- Make a new meta tyvar whose Name and Kind --- come from an existing TyVar -instMetaTyVar box_info tyvar - = do { uniq <- newUnique +newMetaTyVar meta_info kind + = do { uniq <- newMetaUnique ; ref <- newMutVar Flexi - ; let name = setNameUnique (tyVarName tyvar) uniq - kind = tyVarKind tyvar - ; return (mkTcTyVar name kind (MetaTv box_info ref)) } + ; let name = mkTcTyVarName uniq s + s = case meta_info of + TauTv -> fsLit "t" + TcsTv -> fsLit "u" + SigTv -> fsLit "a" + ; return (mkTcTyVar name kind (MetaTv meta_info ref)) } + +mkTcTyVarName :: Unique -> FastString -> Name +-- Make sure that fresh TcTyVar names finish with a digit +-- leaving the un-cluttered names free for user names +mkTcTyVarName uniq str = mkSysTvName uniq str readMetaTyVar :: TyVar -> TcM MetaDetails readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) @@ -535,26 +306,62 @@ isFilledMetaTyVar tv ; return (isIndirect details) } | otherwise = return False +isFlexiMetaTyVar :: TyVar -> TcM Bool +-- True of a un-filled-in (Flexi) meta type variable +isFlexiMetaTyVar tv + | not (isTcTyVar tv) = return False + | MetaTv _ ref <- tcTyVarDetails tv + = do { details <- readMutVar ref + ; return (isFlexi details) } + | otherwise = return False + +-------------------- writeMetaTyVar :: TcTyVar -> TcType -> TcM () +-- Write into a currently-empty MetaTyVar + writeMetaTyVar tyvar ty - | not debugIsOn = writeMutVar (metaTvRef tyvar) (Indirect ty) -writeMetaTyVar tyvar ty - | not (isMetaTyVar tyvar) - = pprTrace "writeMetaTyVar" (ppr tyvar) $ + | not debugIsOn + = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty + +-- Everything from here on only happens if DEBUG is on + | not (isTcTyVar tyvar) + = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar ) return () + + | MetaTv _ ref <- tcTyVarDetails tyvar + = writeMetaTyVarRef tyvar ref ty + + | otherwise + = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar ) + return () + +-------------------- +writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM () +-- Here the tyvar is for error checking only; +-- the ref cell must be for the same tyvar +writeMetaTyVarRef tyvar ref ty + | not debugIsOn + = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty) + ; writeMutVar ref (Indirect ty) } + +-- Everything from here on only happens if DEBUG is on + | not (isPredTy tv_kind) -- Don't check kinds for updates to coercion variables + , not (ty_kind `isSubKind` tv_kind) + = WARN( True, hang (text "Ill-kinded update to meta tyvar") + 2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) ) + return () + | otherwise - = ASSERT( isMetaTyVar tyvar ) - ASSERT2( isCoVar tyvar || typeKind ty `isSubKind` tyVarKind tyvar, - (ppr tyvar <+> ppr (tyVarKind tyvar)) - $$ (ppr ty <+> ppr (typeKind ty)) ) - do { if debugIsOn then do { details <- readMetaTyVar tyvar; --- FIXME ; ASSERT2( not (isFlexi details), ppr tyvar ) - ; WARN( not (isFlexi details), ppr tyvar ) - return () } - else return () - - ; traceTc (text "writeMetaTyVar" <+> ppr tyvar <+> text ":=" <+> ppr ty) - ; writeMutVar (metaTvRef tyvar) (Indirect ty) } + = do { meta_details <- readMutVar ref; + ; ASSERT2( isFlexi meta_details, + hang (text "Double update of meta tyvar") + 2 (ppr tyvar $$ ppr meta_details) ) + + traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty) + ; writeMutVar ref (Indirect ty) } + where + tv_kind = tyVarKind tyvar + ty_kind = typeKind ty \end{code} @@ -576,10 +383,6 @@ newFlexiTyVarTy kind = do newFlexiTyVarTys :: Int -> Kind -> TcM [TcType] newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind) -tcInstTyVar :: TyVar -> TcM TcTyVar --- Instantiate with a META type variable -tcInstTyVar tyvar = instMetaTyVar TauTv tyvar - tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst) -- Instantiate with META type variables tcInstTyVars tyvars @@ -589,6 +392,16 @@ tcInstTyVars tyvars -- Since the tyvars are freshly made, -- they cannot possibly be captured by -- any existing for-alls. Hence zipTopTvSubst + +tcInstTyVar :: TyVar -> TcM TcTyVar +-- Make a new unification variable tyvar whose Name and Kind +-- come from an existing TyVar +tcInstTyVar tyvar + = do { uniq <- newMetaUnique + ; ref <- newMutVar Flexi + ; let name = mkSystemName uniq (getOccName tyvar) + kind = tyVarKind tyvar + ; return (mkTcTyVar name kind (MetaTv TauTv ref)) } \end{code} @@ -612,126 +425,91 @@ zonkSigTyVar sig_tv \end{code} -%************************************************************************ -%* * - MetaTvs: BoxTvs -%* * -%************************************************************************ - -\begin{code} -newBoxyTyVar :: Kind -> TcM BoxyTyVar -newBoxyTyVar kind = newMetaTyVar BoxTv kind - -newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar] -newBoxyTyVars kinds = mapM newBoxyTyVar kinds - -newBoxyTyVarTys :: [Kind] -> TcM [BoxyType] -newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) } - -readFilledBox :: BoxyTyVar -> TcM TcType --- Read the contents of the box, which should be filled in by now -readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv ) - do { cts <- readMetaTyVar box_tv - ; case cts of - Flexi -> pprPanic "readFilledBox" (ppr box_tv) - Indirect ty -> return ty } - -tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar --- Instantiate with a BOXY type variable -tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar -\end{code} - %************************************************************************ %* * -\subsection{Putting and getting mutable type variables} +\subsection{Zonking -- the exernal interfaces} %* * %************************************************************************ -But it's more fun to short out indirections on the way: If this -version returns a TyVar, then that TyVar is unbound. If it returns -any other type, then there might be bound TyVars embedded inside it. - -We return Nothing iff the original box was unbound. +@tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment. +To improve subsequent calls to the same function it writes the zonked set back into +the environment. \begin{code} -data LookupTyVarResult -- The result of a lookupTcTyVar call - = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv - | IndirectTv TcType - -lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult -lookupTcTyVar tyvar - = ASSERT2( isTcTyVar tyvar, ppr tyvar ) - case details of - SkolemTv _ -> return (DoneTv details) - MetaTv _ ref -> do { meta_details <- readMutVar ref - ; case meta_details of - Indirect ty -> return (IndirectTv ty) - Flexi -> return (DoneTv details) } - where - details = tcTyVarDetails tyvar - -{- --- gaw 2004 We aren't shorting anything out anymore, at least for now -getTcTyVar tyvar - | not (isTcTyVar tyvar) - = pprTrace "getTcTyVar" (ppr tyvar) $ - return (Just (mkTyVarTy tyvar)) - - | otherwise - = ASSERT2( isTcTyVar tyvar, ppr tyvar ) do - maybe_ty <- readMetaTyVar tyvar - case maybe_ty of - Just ty -> do ty' <- short_out ty - writeMetaTyVar tyvar (Just ty') - return (Just ty') - - Nothing -> return Nothing - -short_out :: TcType -> TcM TcType -short_out ty@(TyVarTy tyvar) - | not (isTcTyVar tyvar) - = return ty - - | otherwise = do - maybe_ty <- readMetaTyVar tyvar - case maybe_ty of - Just ty' -> do ty' <- short_out ty' - writeMetaTyVar tyvar (Just ty') - return ty' - - other -> return ty - -short_out other_ty = return other_ty --} +tcGetGlobalTyVars :: TcM TcTyVarSet +tcGetGlobalTyVars + = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv + ; gbl_tvs <- readMutVar gtv_var + ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs + ; writeMutVar gtv_var gbl_tvs' + ; return gbl_tvs' } \end{code} - -%************************************************************************ -%* * -\subsection{Zonking -- the exernal interfaces} -%* * -%************************************************************************ - ----------------- Type variables \begin{code} zonkTcTyVars :: [TcTyVar] -> TcM [TcType] zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars -zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet -zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar tyvars - -zonkTcTyVar :: TcTyVar -> TcM TcType -zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar) - zonk_tc_tyvar (\ tv -> return (TyVarTy tv)) tyvar -\end{code} +zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet +zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars) ----------------- Types +zonkTcTypeCarefully :: TcType -> TcM TcType +-- Do not zonk type variables free in the environment +zonkTcTypeCarefully ty + = do { env_tvs <- tcGetGlobalTyVars + ; zonkType (zonk_tv env_tvs) ty } + where + zonk_tv env_tvs tv + | tv `elemVarSet` env_tvs + = return (TyVarTy tv) + | otherwise + = ASSERT( isTcTyVar tv ) + case tcTyVarDetails tv of + SkolemTv {} -> return (TyVarTy tv) + RuntimeUnk {} -> return (TyVarTy tv) + FlatSkol ty -> zonkType (zonk_tv env_tvs) ty + MetaTv _ ref -> do { cts <- readMutVar ref + ; case cts of + Flexi -> return (TyVarTy tv) + Indirect ty -> zonkType (zonk_tv env_tvs) ty } -\begin{code} zonkTcType :: TcType -> TcM TcType -zonkTcType ty = zonkType (\ tv -> return (TyVarTy tv)) ty +-- Simply look through all Flexis +zonkTcType ty = zonkType zonkTcTyVar ty + +zonkTcTyVar :: TcTyVar -> TcM TcType +-- Simply look through all Flexis +zonkTcTyVar tv + = ASSERT2( isTcTyVar tv, ppr tv ) + case tcTyVarDetails tv of + SkolemTv {} -> return (TyVarTy tv) + RuntimeUnk {} -> return (TyVarTy tv) + FlatSkol ty -> zonkTcType ty + MetaTv _ ref -> do { cts <- readMutVar ref + ; case cts of + Flexi -> return (TyVarTy tv) + Indirect ty -> zonkTcType ty } + +zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType +-- Zonk, and simultaneously apply a non-necessarily-idempotent substitution +zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty + where + zonk_tv tv + = case tcTyVarDetails tv of + SkolemTv {} -> return (TyVarTy tv) + RuntimeUnk {} -> return (TyVarTy tv) + FlatSkol ty -> zonkType zonk_tv ty + MetaTv _ ref -> do { cts <- readMutVar ref + ; case cts of + Flexi -> zonk_flexi tv + Indirect ty -> zonkType zonk_tv ty } + zonk_flexi tv + = case lookupTyVar subst tv of + Just ty -> zonkType zonk_tv ty + Nothing -> return (TyVarTy tv) zonkTcTypes :: [TcType] -> TcM [TcType] zonkTcTypes tys = mapM zonkTcType tys @@ -749,36 +527,10 @@ zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2 are used at the end of type checking \begin{code} -zonkTopTyVar :: TcTyVar -> TcM TcTyVar --- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables --- to default the kind of ? and ?? etc to *. This is important to ensure that --- instance declarations match. For example consider --- instance Show (a->b) --- foo x = show (\_ -> True) --- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??), --- and that won't match the typeKind (*) in the instance decl. --- --- Because we are at top level, no further constraints are going to affect these --- type variables, so it's time to do it by hand. However we aren't ready --- to default them fully to () or whatever, because the type-class defaulting --- rules have yet to run. - -zonkTopTyVar tv - | k `eqKind` default_k = return tv - | otherwise - = do { tv' <- newFlexiTyVar default_k - ; writeMetaTyVar tv (mkTyVarTy tv') - ; return tv' } - where - k = tyVarKind tv - default_k = defaultKind k - zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar] zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar 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) @@ -789,36 +541,101 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- -- We leave skolem TyVars alone; they are immutable. zonkQuantifiedTyVar tv - | ASSERT2( isTcTyVar tv, ppr tv ) - isSkolemTyVar tv - = do { kind <- zonkTcType (tyVarKind tv) - ; return $ setTyVarKind tv kind - } + = ASSERT2( isTcTyVar tv, ppr tv ) + case tcTyVarDetails tv of + SkolemTv {} -> WARN( True, ppr tv ) -- Dec10: Can this really happen? + do { kind <- zonkTcType (tyVarKind tv) + ; return $ setTyVarKind tv kind } -- It might be a skolem type variable, -- for example from a user type signature - | otherwise -- It's a meta-type-variable - = do { details <- readMetaTyVar tv - - -- Create the new, frozen, skolem type variable - -- We zonk to a skolem, not to a regular TcVar - -- See Note [Zonking to Skolem] + MetaTv _ _ref -> +#ifdef DEBUG + -- [Sept 04] Check for non-empty. + -- See note [Silly Type Synonym] + (readMutVar _ref >>= \cts -> + case cts of + Flexi -> return () + Indirect ty -> WARN( True, ppr tv $$ ppr ty ) + return ()) >> +#endif + skolemiseUnboundMetaTyVar tv vanillaSkolemTv + _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk + +skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar +-- We have a Meta tyvar with a ref-cell inside it +-- Skolemise it, including giving it a new Name, so that +-- we are totally out of Meta-tyvar-land +-- We create a skolem TyVar, not a regular TyVar +-- See Note [Zonking to Skolem] +skolemiseUnboundMetaTyVar tv details + = ASSERT2( isMetaTyVar tv, ppr tv ) + do { span <- getSrcSpanM -- Get the location from "here" + -- ie where we are generalising + ; uniq <- newUnique -- Remove it from TcMetaTyVar unique land ; let final_kind = defaultKind (tyVarKind tv) - final_tv = mkSkolTyVar (tyVarName tv) final_kind UnkSkol - - -- Bind the meta tyvar to the new tyvar - ; case details of - Indirect ty -> WARN( True, ppr tv $$ ppr ty ) - return () - -- [Sept 04] I don't think this should happen - -- See note [Silly Type Synonym] - - Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv) - - -- Return the new tyvar + final_name = mkInternalName uniq (getOccName tv) span + final_tv = mkTcTyVar final_name final_kind details + ; writeMetaTyVar tv (mkTyVarTy final_tv) ; return final_tv } \end{code} +\begin{code} +zonkImplication :: Implication -> TcM Implication +zonkImplication implic@(Implic { ic_given = given + , ic_wanted = wanted + , ic_loc = loc }) + = do { -- No need to zonk the skolems + ; given' <- mapM zonkEvVar given + ; loc' <- zonkGivenLoc loc + ; wanted' <- zonkWC wanted + ; return (implic { ic_given = given' + , ic_wanted = wanted' + , ic_loc = loc' }) } + +zonkEvVar :: EvVar -> TcM EvVar +zonkEvVar var = do { ty' <- zonkTcType (varType var) + ; return (setVarType var ty') } + +zonkFlavoredEvVar :: FlavoredEvVar -> TcM FlavoredEvVar +zonkFlavoredEvVar (EvVarX ev fl) + = do { ev' <- zonkEvVar ev + ; fl' <- zonkFlavor fl + ; return (EvVarX ev' fl') } + +zonkWC :: WantedConstraints -> TcM WantedConstraints +zonkWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol }) + = do { flat' <- zonkWantedEvVars flat + ; implic' <- mapBagM zonkImplication implic + ; insol' <- mapBagM zonkFlavoredEvVar insol + ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) } + +zonkWantedEvVars :: Bag WantedEvVar -> TcM (Bag WantedEvVar) +zonkWantedEvVars = mapBagM zonkWantedEvVar + +zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar +zonkWantedEvVar (EvVarX v l) = do { v' <- zonkEvVar v; return (EvVarX v' l) } + +zonkFlavor :: CtFlavor -> TcM CtFlavor +zonkFlavor (Given loc gk) = do { loc' <- zonkGivenLoc loc; return (Given loc' gk) } +zonkFlavor fl = return fl + +zonkGivenLoc :: GivenLoc -> TcM GivenLoc +-- GivenLocs may have unification variables inside them! +zonkGivenLoc (CtLoc skol_info span ctxt) + = do { skol_info' <- zonkSkolemInfo skol_info + ; return (CtLoc skol_info' span ctxt) } + +zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo +zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty + ; return (SigSkol cx ty') } +zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys + ; return (InferSkol ntys') } + where + do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') } +zonkSkolemInfo skol_info = return skol_info +\end{code} + Note [Silly Type Synonyms] ~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: @@ -865,9 +682,9 @@ leads to problems. Consider this program from the regression test suite: evalRHS :: Int -> a evalRHS 0 root actual = eval 0 root actual -It leads to the deferral of an equality +It leads to the deferral of an equality (wrapped in an implication constraint) - (String -> String -> String) ~ a + forall a. (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. @@ -882,7 +699,7 @@ 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 +(which we require for a quantified variable), but is still a TcTyVar that the simplifier knows how to deal with. @@ -899,11 +716,9 @@ simplifier knows how to deal with. -- For tyvars bound at a for-all, zonkType zonks them to an immutable -- type variable and zonks the kind too -zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables - -- see zonkTcType, and zonkTcTypeToType - -> TcType - -> TcM Type -zonkType unbound_var_fn ty +zonkType :: (TcTyVar -> TcM Type) -- What to do with TcTyVars + -> TcType -> TcM Type +zonkType zonk_tc_tyvar ty = go ty where go (TyConApp tc tys) = do tys' <- mapM go tys @@ -924,14 +739,13 @@ zonkType unbound_var_fn ty -- to pull the TyConApp to the top. -- The two interesting cases! - go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar - | otherwise = liftM TyVarTy $ - zonkTyVar unbound_var_fn tyvar + go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar + | otherwise = return (TyVarTy tyvar) -- Ordinary (non Tc) tyvars occur inside quantified types go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do ty' <- go ty - tyvar' <- zonkTyVar unbound_var_fn tyvar + tyvar' <- return tyvar return (ForAllTy tyvar' ty') go_pred (ClassP c tys) = do tys' <- mapM go tys @@ -942,29 +756,18 @@ zonkType unbound_var_fn ty ty2' <- go ty2 return (EqPred ty1' ty2') -zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var +mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var -> TcTyVar -> TcM TcType -zonk_tc_tyvar unbound_var_fn tyvar - | not (isMetaTyVar tyvar) -- Skolems - = return (TyVarTy tyvar) - - | otherwise -- Mutables - = do { cts <- readMetaTyVar tyvar - ; case cts of - Flexi -> unbound_var_fn tyvar -- Unbound meta type variable - Indirect ty -> zonkType unbound_var_fn ty } - --- Zonk the kind of a non-TC tyvar in case it is a coercion variable (their --- kind contains types). --- -zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var - -> TyVar -> TcM TyVar -zonkTyVar unbound_var_fn tv - | isCoVar tv - = do { kind <- zonkType unbound_var_fn (tyVarKind tv) - ; return $ setTyVarKind tv kind - } - | otherwise = return tv +mkZonkTcTyVar unbound_var_fn tyvar + = ASSERT( isTcTyVar tyvar ) + case tcTyVarDetails tyvar of + SkolemTv {} -> return (TyVarTy tyvar) + RuntimeUnk {} -> return (TyVarTy tyvar) + FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty + MetaTv _ ref -> do { cts <- readMutVar ref + ; case cts of + Flexi -> unbound_var_fn tyvar + Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty } \end{code} @@ -989,7 +792,8 @@ zonkTcKind k = zonkTcType k zonkTcKindToKind :: TcKind -> TcM Kind -- When zonking a TcKind to a kind, we need to instantiate kind variables, -- Haskell specifies that * is to be used, so we follow that. -zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k +zonkTcKindToKind k + = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k \end{code} %************************************************************************ @@ -1030,11 +834,11 @@ This might not necessarily show up in kind checking. checkValidType :: UserTypeCtxt -> Type -> TcM () -- Checks that the type is valid for the given context 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 + traceTc "checkValidType" (ppr ty) + unboxed <- xoptM Opt_UnboxedTuples + rank2 <- xoptM Opt_Rank2Types + rankn <- xoptM Opt_RankNTypes + polycomp <- xoptM Opt_PolymorphicComponents let gen_rank n | rankn = ArbitraryRank | rank2 = Rank 2 @@ -1059,11 +863,15 @@ checkValidType ctxt ty = do ForSigCtxt _ -> gen_rank 1 SpecInstCtxt -> gen_rank 1 + ThBrackCtxt -> gen_rank 1 + GenSigCtxt -> panic "checkValidType" + -- Can't happen; GenSigCtxt not used for *user* sigs actual_kind = typeKind ty kind_ok = case ctxt of TySynCtxt _ -> True -- Any kind will do + ThBrackCtxt -> True -- Any kind will do ResSigCtxt -> isSubOpenTypeKind actual_kind ExprSigCtxt -> isSubOpenTypeKind actual_kind GenPatCtxt -> isLiftedTypeKind actual_kind @@ -1073,15 +881,18 @@ checkValidType ctxt ty = do ubx_tup = case ctxt of TySynCtxt _ | unboxed -> UT_Ok ExprSigCtxt | unboxed -> UT_Ok + ThBrackCtxt | unboxed -> UT_Ok _ -> UT_NotOk - -- Check that the thing has kind Type, and is lifted if necessary - checkTc kind_ok (kindErr actual_kind) - -- Check the internal validity of the type itself check_type rank ubx_tup ty - traceTc (text "checkValidType done" <+> ppr ty) + -- Check that the thing has kind Type, and is lifted if necessary + -- Do this second, becuase we can't usefully take the kind of an + -- ill-formed type such as (a~Int) + checkTc kind_ok (kindErr actual_kind) + + traceTc "checkValidType done" (ppr ty) checkValidMonoType :: Type -> TcM () checkValidMonoType ty = check_mono_type MustBeMonoType ty @@ -1130,20 +941,16 @@ check_type rank ubx_tup ty -- 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 --- 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_type _ _ (PredTy sty) - = do { dflags <- getDOpts - ; check_pred_ty dflags TypeCtxt sty } +-- Naked PredTys should, I think, have been rejected before now +check_type _ _ ty@(PredTy {}) + = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type") check_type _ _ (TyVarTy _) = return () + check_type rank _ (FunTy arg_ty res_ty) = do { check_type (decRank rank) UT_NotOk arg_ty ; check_type rank UT_Ok res_ty } @@ -1163,8 +970,8 @@ check_type rank ubx_tup ty@(TyConApp tc tys) checkTc (tyConArity tc <= length tys) arity_msg -- See Note [Liberal type synonyms] - ; liberal <- doptM Opt_LiberalTypeSynonyms - ; if not liberal || isOpenSynTyCon tc then + ; liberal <- xoptM Opt_LiberalTypeSynonyms + ; if not liberal || isSynFamilyTyCon tc then -- For H98 and synonym families, do check the type args mapM_ (check_mono_type SynArgMonoType) tys @@ -1175,10 +982,10 @@ check_type rank ubx_tup ty@(TyConApp tc tys) } | isUnboxedTupleTyCon tc - = do { ub_tuples_allowed <- doptM Opt_UnboxedTuples + = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg - ; impred <- doptM Opt_ImpredicativeTypes + ; impred <- xoptM Opt_ImpredicativeTypes ; let rank' = if impred then ArbitraryRank else TyConArgMonoType -- c.f. check_arg_type -- However, args are allowed to be unlifted, or @@ -1222,14 +1029,15 @@ check_arg_type :: Rank -> Type -> TcM () -- 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 ArbitraryRank -- Arg of tycon can have arby rank, regardless - else case rank of -- Predictive => must be monotype - MustBeMonoType -> MustBeMonoType - _ -> TyConArgMonoType + = do { impred <- xoptM Opt_ImpredicativeTypes + ; let rank' = case rank of -- Predictive => must be monotype + MustBeMonoType -> MustBeMonoType -- Monotype, regardless + _other | impred -> ArbitraryRank + | otherwise -> TyConArgMonoType -- Make sure that MustBeMonoType is propagated, -- so that we don't suggest -XImpredicativeTypes in -- (Ord (forall a.a)) => a -> a + -- and so that if it Must be a monotype, we check that it is! ; check_type rank' UT_NotOk ty ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } @@ -1330,7 +1138,7 @@ check_valid_theta ctxt theta = do warnTc (notNull dups) (dupPredWarn dups) mapM_ (check_pred_ty dflags ctxt) theta where - (_,dups) = removeDups tcCmpPred theta + (_,dups) = removeDups cmpPred theta ------------------------- check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM () @@ -1350,18 +1158,13 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys) arity_err = arityErr "Class" class_name arity n_tys how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this")) -check_pred_ty _ (ClassSCCtxt _) (EqPred _ _) - = -- We do not yet support superclass equalities. - failWithTc $ - sep [ ptext (sLit "The current implementation of type families does not") - , ptext (sLit "support equality constraints in superclass contexts.") - , ptext (sLit "They are planned for a future release.") - ] -check_pred_ty dflags _ pred@(EqPred ty1 ty2) +check_pred_ty dflags ctxt pred@(EqPred ty1 ty2) = do { -- Equational constraints are valid in all contexts if type -- families are permitted - ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred) + ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred) + ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True) + (eqSuperClassErr pred) -- Check the form of the argument types ; checkValidMonoType ty1 @@ -1392,8 +1195,8 @@ check_class_pred_tys dflags ctxt tys -- checkInstTermination _ -> flexible_contexts || all tyvar_head tys where - flexible_contexts = dopt Opt_FlexibleContexts dflags - undecidable_ok = dopt Opt_UndecidableInstances dflags + flexible_contexts = xopt Opt_FlexibleContexts dflags + undecidable_ok = xopt Opt_UndecidableInstances dflags ------------------------- tyvar_head :: Type -> Bool @@ -1435,6 +1238,10 @@ 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). +In addition, GHC insists that at least one type variable +in each constraint is in V. So we disallow a type like + forall a. Eq b => b -> b +even in a scope where b is in scope. \begin{code} checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM () @@ -1453,59 +1260,60 @@ checkAmbiguity forall_tyvars theta tau_tyvars ambigErr :: PredType -> SDoc ambigErr pred - = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred), - nest 4 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$ + = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPredTy pred), + nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$ ptext (sLit "must be reachable from the type after the '=>'"))] +\end{code} + +Note [Growing the tau-tvs using constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +(growInstsTyVars insts tvs) is the result of extending the set + of tyvars tvs using all conceivable links from pred --------------------------- --- For this 'grow' stuff see Note [Growing the tau-tvs using constraints] in Inst +E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e} +Then grow precs tvs = {a,b,c} +\begin{code} growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet --- Finds a fixpoint +-- See Note [Growing the tau-tvs using constraints] growThetaTyVars theta tvs | null theta = tvs | otherwise = fixVarSet mk_next tvs where - mk_next tvs = foldr growPredTyVars tvs theta - - -growPredTyVars :: TcPredType -> TyVarSet -> TyVarSet --- Here is where the special case for inplicit parameters happens -growPredTyVars (IParam _ ty) tvs = tvs `unionVarSet` tyVarsOfType ty -growPredTyVars pred tvs = growTyVars (tyVarsOfPred pred) tvs - -growTyVars :: TyVarSet -> TyVarSet -> TyVarSet -growTyVars new_tvs tvs - | new_tvs `intersectsVarSet` tvs = tvs `unionVarSet` new_tvs - | otherwise = tvs + mk_next tvs = foldr grow_one tvs theta + grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs + +growPredTyVars :: TcPredType + -> TyVarSet -- The set to extend + -> TyVarSet -- TyVars of the predicate if it intersects + -- the set, or is implicit parameter +growPredTyVars pred tvs + | IParam {} <- pred = pred_tvs -- See Note [Implicit parameters and ambiguity] + | pred_tvs `intersectsVarSet` tvs = pred_tvs + | otherwise = emptyVarSet + where + pred_tvs = tyVarsOfPred pred \end{code} -In addition, GHC insists that at least one type variable -in each constraint is in V. So we disallow a type like - forall a. Eq b => b -> b -even in a scope where b is in scope. +Note [Implicit parameters and ambiguity] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +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' + +Furthermore, the type variables fixed by an implicit parameter +propagate to the others. E.g. + foo :: (Show a, ?x::[a]) => Int + foo = show (?x++?x) +The type of foo looks ambiguous. But it isn't, because at a call site +we might have + let ?x = 5::Int in foo +and all is well. In effect, implicit parameters are, well, parameters, +so we can take their type variables into account as part of the +"tau-tvs" stuff. This is done in the function 'FunDeps.grow'. -\begin{code} -checkFreeness :: [Var] -> [PredType] -> TcM () -checkFreeness forall_tyvars theta - = do { flexible_contexts <- doptM Opt_FlexibleContexts - ; unless flexible_contexts $ mapM_ complain (filter is_free theta) } - where - is_free pred = not (isIPPred pred) - && not (any bound_var (varSetElems (tyVarsOfPred pred))) - bound_var ct_var = ct_var `elem` forall_tyvars - complain pred = addErrTc (freeErr pred) - -freeErr :: PredType -> SDoc -freeErr pred - = 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} checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc @@ -1513,44 +1321,32 @@ checkThetaCtxt ctxt theta = vcat [ptext (sLit "In the context:") <+> pprTheta theta, ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ] +eqSuperClassErr :: PredType -> SDoc +eqSuperClassErr pred + = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:")) + 2 (ppr pred) + badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc -badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty -eqPredTyErr sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty - $$ - parens (ptext (sLit "Use -XTypeFamilies to permit this")) +badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPredTy pred +eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPredTy pred + $$ + 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)] + nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)] dupPredWarn :: [[PredType]] -> SDoc -dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups) +dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPredTy (map head dups) arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc arityErr kind name n m = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"), - n_arguments <> comma, text "but has been given", int m] + n_arguments <> comma, text "but has been given", + if m==0 then text "none" else int m] where n_arguments | n == 0 = ptext (sLit "no arguments") | n == 1 = ptext (sLit "1 argument") | True = hsep [int n, ptext (sLit "arguments")] - ------------------ -notMonoType :: TcType -> TcM a -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 :: TcType -> TcM a -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} - %************************************************************************ %* * \subsection{Checking for a decent instance head type} @@ -1567,34 +1363,20 @@ compiled elsewhere). In these cases, we let them go through anyway. We can also have instances for functions: @instance Foo (a -> b) ...@. \begin{code} -checkValidInstHead :: Type -> TcM (Class, [TcType]) +checkValidInstHead :: Class -> [Type] -> TcM () +checkValidInstHead clas tys + = do { dflags <- getDOpts -checkValidInstHead ty -- Should be a source type - = case tcSplitPredTy_maybe ty of { - Nothing -> failWithTc (instTypeErr (ppr ty) empty) ; - Just pred -> - - case getClassPredTys_maybe pred of { - Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ; - Just (clas,tys) -> do - - dflags <- getDOpts - check_inst_head dflags clas tys - return (clas, tys) - }} - -check_inst_head :: DynFlags -> Class -> [Type] -> TcM () -check_inst_head dflags clas tys - = do { -- If GlasgowExts then check at least one isn't a type variable - ; checkTc (dopt Opt_TypeSynonymInstances dflags || + -- If GlasgowExts then check at least one isn't a type variable + ; checkTc (xopt Opt_TypeSynonymInstances dflags || all tcInstHeadTyNotSynonym tys) - (instTypeErr (pprClassPred clas tys) head_type_synonym_msg) - ; checkTc (dopt Opt_FlexibleInstances dflags || + (instTypeErr pp_pred head_type_synonym_msg) + ; checkTc (xopt Opt_FlexibleInstances dflags || all tcInstHeadTyAppAllTyVars tys) - (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg) - ; checkTc (dopt Opt_MultiParamTypeClasses dflags || + (instTypeErr pp_pred head_type_args_tyvars_msg) + ; checkTc (xopt Opt_MultiParamTypeClasses dflags || isSingleton tys) - (instTypeErr (pprClassPred clas tys) head_one_type_msg) + (instTypeErr pp_pred head_one_type_msg) -- May not contain type family applications ; mapM_ checkTyFamFreeness tys @@ -1607,6 +1389,7 @@ check_inst_head dflags clas tys } where + pp_pred = pprClassPred clas tys head_type_synonym_msg = parens ( text "All instance types must be of the form (T t1 ... tn)" $$ text "where T is not a synonym." $$ @@ -1614,7 +1397,7 @@ check_inst_head dflags clas tys 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 "where a1 ... an are *distinct type variables*,", text "and each type variable appears at most once in the instance head.", text "Use -XFlexibleInstances if you want to disable this."]) @@ -1625,7 +1408,7 @@ check_inst_head dflags clas tys instTypeErr :: SDoc -> SDoc -> SDoc instTypeErr pp_ty msg = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty, - nest 4 msg] + nest 2 msg] \end{code} @@ -1635,28 +1418,34 @@ instTypeErr pp_ty msg %* * %************************************************************************ - \begin{code} -checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM () -checkValidInstance tyvars theta clas inst_tys - = do { undecidable_ok <- doptM Opt_UndecidableInstances - - ; checkValidTheta InstThetaCtxt theta +checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType + -> Class -> [TcType] -> TcM () +checkValidInstance hs_type tyvars theta clas inst_tys + = setSrcSpan (getLoc hs_type) $ + do { setSrcSpan head_loc (checkValidInstHead clas inst_tys) + ; checkValidTheta InstThetaCtxt theta ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys) -- Check that instance inference will terminate (if we care) -- For Haskell 98 this will already have been done by checkValidTheta, -- but as we may be using other extensions we need to check. - ; unless undecidable_ok $ + ; undecidable_ok <- xoptM Opt_UndecidableInstances + ; unless undecidable_ok $ mapM_ addErrTc (checkInstTermination inst_tys theta) -- The Coverage Condition ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys) (instTypeErr (pprClassPred clas inst_tys) msg) - } + } where msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"), undecidableMsg]) + + -- The location of the "head" of the instance + head_loc = case hs_type of + L _ (HsForAllTy _ _ _ (L loc _)) -> loc + L loc _ -> loc \end{code} Termination test: the so-called "Paterson conditions" (see Section 5 of @@ -1693,7 +1482,7 @@ checkInstTermination tys theta predUndecErr :: PredType -> SDoc -> SDoc predUndecErr pred msg = sep [msg, - nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)] + nest 2 (ptext (sLit "in the constraint:") <+> pprPredTy pred)] nomoreMsg, smallerMsg, undecidableMsg :: SDoc nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head") @@ -1701,64 +1490,9 @@ smallerMsg = ptext (sLit "Constraint is no smaller than the instance head") undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this") \end{code} - -%************************************************************************ -%* * - Checking the context of a derived instance declaration -%* * -%************************************************************************ - -Note [Exotic derived instance contexts] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In a 'derived' instance declaration, we *infer* the context. It's a -bit unclear what rules we should apply for this; the Haskell report is -silent. Obviously, constraints like (Eq a) are fine, but what about - data T f a = MkT (f a) deriving( Eq ) -where we'd get an Eq (f a) constraint. That's probably fine too. - -One could go further: consider - data T a b c = MkT (Foo a b c) deriving( Eq ) - instance (C Int a, Eq b, Eq c) => Eq (Foo a b c) - -Notice that this instance (just) satisfies the Paterson termination -conditions. Then we *could* derive an instance decl like this: - - instance (C Int a, Eq b, Eq c) => Eq (T a b c) - -even though there is no instance for (C Int a), because there just -*might* be an instance for, say, (C Int Bool) at a site where we -need the equality instance for T's. - -However, this seems pretty exotic, and it's quite tricky to allow -this, and yet give sensible error messages in the (much more common) -case where we really want that instance decl for C. - -So for now we simply require that the derived instance context -should have only type-variable constraints. - -Here is another example: - data Fix f = In (f (Fix f)) deriving( Eq ) -Here, if we are prepared to allow -XUndecidableInstances 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. +validDeivPred checks for OK 'deriving' context. See Note [Exotic +derived instance contexts] in TcSimplify. However the predicate is +here because it uses sizeTypes, fvTypes. \begin{code} validDerivPred :: PredType -> Bool @@ -1767,6 +1501,7 @@ validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs validDerivPred _ = False \end{code} + %************************************************************************ %* * Checking type instance well-formedness and termination @@ -1787,7 +1522,7 @@ checkValidTypeInst typats rhs ; checkValidMonoType rhs -- we have a decidable instance unless otherwise permitted - ; undecidable_ok <- doptM Opt_UndecidableInstances + ; undecidable_ok <- xoptM Opt_UndecidableInstances ; unless undecidable_ok $ mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs)) } @@ -1834,7 +1569,7 @@ isTyFamFree = null . tyFamInsts tyFamInstIllegalErr :: Type -> SDoc tyFamInstIllegalErr ty = hang (ptext (sLit "Illegal type synonym family application in instance") <> - colon) 4 $ + colon) 2 $ ppr ty famInstUndecErr :: Type -> SDoc -> SDoc @@ -1888,8 +1623,14 @@ sizeType (ForAllTy _ ty) = sizeType ty sizeTypes :: [Type] -> Int sizeTypes xs = sum (map sizeType xs) +-- Size of a predicate +-- +-- We are considering whether *class* constraints terminate +-- Once we get into an implicit parameter or equality we +-- can't get back to a class constraint, so it's safe +-- to say "size 0". See Trac #4200. sizePred :: PredType -> Int sizePred (ClassP _ tys') = sizeTypes tys' -sizePred (IParam _ ty) = sizeType ty -sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2 +sizePred (IParam {}) = 0 +sizePred (EqPred {}) = 0 \end{code}