X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=84fb1b81ede9cce659a7bf3faa03f3218449bbc4;hp=3357004df441aedb86d08f6ae57b5aa1faf7fde9;hb=5de363ca9ebdb7d85e3c353c1cffdf0a1c11128e;hpb=6ac37f3bfd72d6fdc819821bfaea1aa70d46f53c diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 3357004..84fb1b8 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -9,13 +9,6 @@ This module contains monadic operations over types that contain mutable type variables \begin{code} -{-# OPTIONS -w #-} --- 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/Commentary/CodingStyle#Warnings --- for details - module TcMType ( TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet, @@ -25,41 +18,47 @@ module TcMType ( newFlexiTyVarTy, -- Kind -> TcM TcType newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] newKindVar, newKindVars, - lookupTcTyVar, LookupTyVarResult(..), - newMetaTyVar, readMetaTyVar, writeMetaTyVar, isFilledMetaTyVar, + newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, + isFilledMetaTyVar, isFlexiMetaTyVar, -------------------------------- - -- Boxy type variables - newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, + -- Creating new evidence variables + newEvVar, newCoVar, newEvVars, + newWantedCoVar, writeWantedCoVar, readWantedCoVar, + newIP, newDict, newSelfDict, isSelfDict, - -------------------------------- - -- Creating new coercion variables - newCoVars, newMetaCoVar, + newWantedEvVar, newWantedEvVars, + newKindConstraint, + newTcEvBinds, addTcEvBind, -------------------------------- -- Instantiation - tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar, - tcInstSigTyVars, - tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, - tcSkolSigType, tcSkolSigTyVars, occurCheckErr, + tcInstTyVar, tcInstTyVars, tcInstSigTyVars, + tcInstType, tcInstSigType, + tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType, + tcSkolSigType, tcSkolSigTyVars, -------------------------------- -- Checking type validity - Rank, UserTypeCtxt(..), checkValidType, - SourceTyCtxt(..), checkValidTheta, checkFreeness, + Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType, + SourceTyCtxt(..), checkValidTheta, checkValidInstHead, checkValidInstance, - checkInstTermination, checkValidTypeInst, checkTyFamFreeness, - checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt, - unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs, + checkInstTermination, checkValidTypeInst, checkTyFamFreeness, + arityErr, + growPredTyVars, growThetaTyVars, validDerivPred, -------------------------------- -- Zonking - zonkType, zonkTcPredType, + zonkType, mkZonkTcTyVar, zonkTcPredType, + zonkTcTypeCarefully, zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar, zonkQuantifiedTyVar, zonkQuantifiedTyVars, - zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType, - zonkTcKindToKind, zonkTcKind, zonkTopTyVar, + zonkTcType, zonkTcTypes, zonkTcThetaType, + zonkTcKindToKind, zonkTcKind, + zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar, + zonkTcTypeAndSubst, + tcGetGlobalTyVars, readKindVar, writeKindVar ) where @@ -76,7 +75,9 @@ 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 VarSet @@ -85,347 +86,158 @@ import DynFlags import Util import Maybes import ListSetOps -import UniqSupply +import BasicTypes import SrcLoc import Outputable +import FastString +import Bag -import Control.Monad ( when, unless ) +import Control.Monad 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 -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 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 = returnM () - - | 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' <- mappM go tys - ; return $ occurs (TyConApp tc) tys' } - go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations - go (PredTy p) = do { p' <- go_pred p - ; return $ 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). +newEvVars :: TcThetaType -> TcM [EvVar] +newEvVars theta = mapM newEvVar theta + +newWantedEvVar :: TcPredType -> TcM EvVar +newWantedEvVar (EqPred ty1 ty2) = newWantedCoVar ty1 ty2 +newWantedEvVar (ClassP cls tys) = newDict cls tys +newWantedEvVar (IParam ip ty) = newIP ip ty + +newWantedEvVars :: TcThetaType -> TcM [EvVar] +newWantedEvVars theta = mapM newWantedEvVar theta + +newWantedCoVar :: TcType -> TcType -> TcM CoVar +newWantedCoVar ty1 ty2 = newCoVar ty1 ty2 + +-- We used to create a mutable co-var +{- +-- A wanted coercion variable is a MetaTyVar +-- that can be filled in with its binding + = do { uniq <- newUnique + ; ref <- newMutVar Flexi + ; let name = mkSysTvName uniq (fsLit "c") + kind = mkPredTy (EqPred ty1 ty2) + ; return (mkTcTyVar name kind (MetaTv TauTv ref)) } +-} -------------- +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 (mkTyVarOccFS (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) } -Error mesages in case of kind mismatch. +----------------- +newKindConstraint :: Type -> Kind -> TcM (CoVar, Type) +-- Create a new wanted CoVar that constrains the type +-- to have the specified kind +newKindConstraint ty kind + = do { ty_k <- newFlexiTyVarTy kind + ; co_var <- newWantedCoVar ty ty_k + ; return (co_var, ty_k) } -\begin{code} -unifyKindMisMatch ty1 ty2 - = zonkTcKind ty1 `thenM` \ ty1' -> - zonkTcKind ty2 `thenM` \ ty2' -> - let - msg = hang (ptext SLIT("Couldn't match kind")) - 2 (sep [quotes (ppr ty1'), - ptext SLIT("against"), - quotes (ppr ty2')]) - in - failWithTc msg - -unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred - -- tv1 and ty2 are zonked already - = returnM 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) +----------------- +newSelfDict :: Class -> [TcType] -> TcM DictId +-- Make a dictionary for "self". It behaves just like a normal DictId +-- except that it responds True to isSelfDict +-- This is used only to suppress confusing error reports +newSelfDict cls tys + = do { uniq <- newUnique + ; let name = mkSystemName uniq selfDictOcc + ; return (mkLocalId name (mkPredTy (ClassP cls tys))) } + +selfDictOcc :: OccName +selfDictOcc = mkVarOcc "self" + +isSelfDict :: EvVar -> Bool +isSelfDict 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)) } +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) -newKindVars :: Int -> TcM [TcKind] -newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ()) -\end{code} + (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 -%************************************************************************ -%* * - SkolemTvs (immutable) -%* * -%************************************************************************ + ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho) + ; return (tyvars', theta, tau) } -\begin{code} mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info) tcSkolSigType :: SkolemInfo -> 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. +-- be in the type environment: it is lexically scoped. tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar] @@ -433,30 +245,48 @@ tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar] tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info | tv <- tyvars ] -tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar +tcInstSkolTyVar :: SkolemInfo -> 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 mb_loc tyvar +-- * the location either from the tyvar (skol_info = SigSkol) +-- or from the monad (otehrwise) +tcInstSkolTyVar skol_info tyvar = do { uniq <- newUnique - ; let old_name = tyVarName tyvar - kind = tyVarKind tyvar - loc = mb_loc `orElse` getSrcSpan old_name - new_name = mkInternalName uniq (nameOccName old_name) loc - ; return (mkSkolTyVar new_name kind info) } + ; loc <- case skol_info of + SigSkol {} -> return (getSrcSpan old_name) + _ -> getSrcSpanM + ; let new_name = mkInternalName uniq occ loc + ; return (mkSkolTyVar new_name kind skol_info) } + where + old_name = tyVarName tyvar + occ = nameOccName old_name + kind = tyVarKind tyvar tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar] -- Get the location from the monad tcInstSkolTyVars info tyvars - = do { span <- getSrcSpanM - ; mapM (tcInstSkolTyVar info (Just span)) tyvars } + = mapM (tcInstSkolTyVar info) tyvars tcInstSkolType :: SkolemInfo -> 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 + +tcInstSigType :: Bool -> Name -> 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 name ty + | use_skols + = tcInstType (tcInstSkolTyVars (SigSkol (FunSigCtxt name))) ty + | otherwise + = tcInstType tcInstSigTyVars ty + +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 (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv) + -- ToDo: the "function binding site is bogus \end{code} @@ -467,36 +297,37 @@ tcInstSkolType info ty = tcInstType (tcInstSkolTyVars 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 +newMetaTyVar meta_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 + fs = case meta_info of + TauTv -> fsLit "t" + SigTv _ -> fsLit "a" + ; return (mkTcTyVar name kind (MetaTv meta_info ref)) } + +instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar -- Make a new meta tyvar whose Name and Kind -- come from an existing TyVar -instMetaTyVar box_info tyvar +instMetaTyVar meta_info tyvar = do { uniq <- newUnique ; ref <- newMutVar Flexi ; let name = setNameUnique (tyVarName tyvar) uniq kind = tyVarKind tyvar - ; return (mkTcTyVar name kind (MetaTv box_info ref)) } + ; return (mkTcTyVar name kind (MetaTv meta_info ref)) } readMetaTyVar :: TyVar -> TcM MetaDetails readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) readMutVar (metaTvRef tyvar) +readWantedCoVar :: CoVar -> TcM MetaDetails +readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar ) + readMutVar (metaTvRef covar) + + + isFilledMetaTyVar :: TyVar -> TcM Bool -- True of a filled-in (Indirect) meta type variable isFilledMetaTyVar tv @@ -506,25 +337,65 @@ 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 () -#ifndef DEBUG -writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty) -#else +-- Write into a currently-empty MetaTyVar + writeMetaTyVar tyvar ty - | not (isMetaTyVar tyvar) - = pprTrace "writeMetaTyVar" (ppr tyvar) $ - returnM () + | 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 - = ASSERT( isMetaTyVar tyvar ) - -- TOM: It should also work for coercions - -- ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) ) - do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar ) - ; writeMutVar (metaTvRef tyvar) (Indirect ty) } + = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar ) + return () + +writeWantedCoVar :: CoVar -> Coercion -> TcM () +writeWantedCoVar cv co = writeMetaTyVar cv co + +-------------------- +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 + = do { meta_details <- readMutVar ref; + ; WARN( not (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 - k1 = tyVarKind tyvar - k2 = typeKind ty -#endif + tv_kind = tyVarKind tyvar + ty_kind = typeKind ty \end{code} @@ -539,12 +410,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 @@ -555,7 +426,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 @@ -569,16 +440,6 @@ tcInstTyVars tyvars %************************************************************************ \begin{code} -tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar] --- Instantiate with skolems or meta SigTvs; depending on use_skols --- Always take location info from the supplied tyvars -tcInstSigTyVars use_skols skol_info tyvars - | use_skols - = mapM (tcInstSkolTyVar skol_info Nothing) tyvars - - | otherwise - = mapM (instMetaTyVar (SigTv skol_info)) tyvars - zonkSigTyVar :: TcTyVar -> TcM TcTyVar zonkSigTyVar sig_tv | isSkolemTyVar sig_tv @@ -592,182 +453,108 @@ 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) $ - returnM (Just (mkTyVarTy tyvar)) - - | otherwise - = ASSERT2( isTcTyVar tyvar, ppr tyvar ) - readMetaTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Just ty -> short_out ty `thenM` \ ty' -> - writeMetaTyVar tyvar (Just ty') `thenM_` - returnM (Just ty') - - Nothing -> returnM Nothing - -short_out :: TcType -> TcM TcType -short_out ty@(TyVarTy tyvar) - | not (isTcTyVar tyvar) - = returnM ty - - | otherwise - = readMetaTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Just ty' -> short_out ty' `thenM` \ ty' -> - writeMetaTyVar tyvar (Just ty') `thenM_` - returnM ty' - - other -> returnM ty - -short_out other_ty = returnM 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 = mappM zonkTcTyVar tyvars +zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars -zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet -zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys -> - returnM (tyVarsOfTypes tys) - -zonkTcTyVar :: TcTyVar -> TcM TcType -zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar) - zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar -\end{code} +zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet +zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars) ----------------- Types -\begin{code} +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) + 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 } + zonkTcType :: TcType -> TcM TcType -zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty +-- Simply look through all Flexis +zonkTcType ty = zonkType zonkTcTyVar ty -zonkTcTypes :: [TcType] -> TcM [TcType] -zonkTcTypes tys = mappM zonkTcType tys +zonkTcTyVar :: TcTyVar -> TcM TcType +-- Simply look through all Flexis +zonkTcTyVar tv + = ASSERT2( isTcTyVar tv, ppr tv ) + case tcTyVarDetails tv of + SkolemTv {} -> 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) + 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) -zonkTcClassConstraints cts = mappM zonk cts - where zonk (clas, tys) - = zonkTcTypes tys `thenM` \ new_tys -> - returnM (clas, new_tys) +zonkTcTypes :: [TcType] -> TcM [TcType] +zonkTcTypes tys = mapM zonkTcType 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 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 = mappM zonkQuantifiedTyVar +zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it. @@ -782,8 +569,11 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar -- -- We leave skolem TyVars alone; they are immutable. zonkQuantifiedTyVar tv - | ASSERT( isTcTyVar tv ) - isSkolemTyVar tv = return tv + | ASSERT2( isTcTyVar tv, ppr tv ) + isSkolemTyVar tv + = do { kind <- zonkTcType (tyVarKind tv) + ; return $ setTyVarKind tv kind + } -- It might be a skolem type variable, -- for example from a user type signature @@ -809,6 +599,29 @@ zonkQuantifiedTyVar tv ; return final_tv } \end{code} +\begin{code} +zonkImplication :: Implication -> TcM Implication +zonkImplication implic@(Implic { ic_untch = env_tvs, ic_given = given + , ic_wanted = wanted }) + = do { env_tvs' <- zonkTcTyVarsAndFV env_tvs + ; given' <- mapM zonkEvVar given + ; wanted' <- mapBagM zonkWanted wanted + ; return (implic { ic_untch = env_tvs', ic_given = given' + , ic_wanted = wanted' }) } + +zonkEvVar :: EvVar -> TcM EvVar +zonkEvVar var = do { ty' <- zonkTcType (varType var) + ; return (setVarType var ty') } + +zonkWanted :: WantedConstraint -> TcM WantedConstraint +zonkWanted (WcImplic imp) = do { imp' <- zonkImplication imp; return (WcImplic imp') } +zonkWanted (WcEvVar ev) = do { ev' <- zonkWantedEvVar ev; return (WcEvVar ev') } + +zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar +zonkWantedEvVar (WantedEvVar v l) = do { v' <- zonkEvVar v; return (WantedEvVar v' l) } +\end{code} + + Note [Silly Type Synonyms] ~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this: @@ -830,7 +643,7 @@ Consider this: * Now abstract over the 'a', but float out the Num (C d a) constraint because it does not 'really' mention a. (see exactTyVarsOfType) The arg to foo becomes - /\a -> \t -> t+t + \/\a -> \t -> t+t * So we get a dict binding for Num (C d a), which is zonked to give a = () @@ -839,10 +652,10 @@ Consider this: quantification, so the floated dict will still have type (C d a). Which renders this whole note moot; happily!] -* Then the /\a abstraction has a zonked 'a' in it. +* Then the \/\a abstraction has a zonked 'a' in it. 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 () +a \/\a in the final result but all the occurrences of a will be zonked to () Note [Zonking to Skolem] ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -855,9 +668,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. @@ -872,7 +685,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. @@ -893,56 +706,66 @@ zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type varia -- see zonkTcType, and zonkTcTypeToType -> TcType -> TcM Type -zonkType unbound_var_fn ty +zonkType zonk_tc_tyvar 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. -- The two interesting cases! - go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar - | otherwise = return (TyVarTy tyvar) + go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar + | otherwise = liftM TyVarTy $ + zonkTyVar zonk_tc_tyvar 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 + tyvar' <- zonkTyVar zonk_tc_tyvar tyvar + 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 +mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var -> TcTyVar -> TcM TcType -zonk_tc_tyvar unbound_var_fn tyvar - | not (isMetaTyVar tyvar) -- Skolems - = returnM (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 } +mkZonkTcTyVar unbound_var_fn tyvar + = ASSERT( isTcTyVar tyvar ) + case tcTyVarDetails tyvar of + SkolemTv {} -> 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 } + +-- 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 a TcTyVar + -> TyVar -> TcM TyVar +zonkTyVar zonk_tc_tyvar tv + | isCoVar tv + = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv) + ; return $ setTyVarKind tv kind } + | otherwise = return tv \end{code} @@ -967,7 +790,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} %************************************************************************ @@ -1007,137 +831,131 @@ 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 "checkValidType" (ppr ty) + unboxed <- xoptM Opt_UnboxedTuples + rank2 <- xoptM Opt_Rank2Types + rankn <- xoptM Opt_RankNTypes + polycomp <- xoptM Opt_PolymorphicComponents let - rank | rankn = Arbitrary - | rank2 = Rank 2 - | otherwise - = case ctxt of -- Haskell 98 - GenPatCtxt -> Rank 0 - LamPatSigCtxt -> Rank 0 - BindPatSigCtxt -> Rank 0 - DefaultDeclCtxt-> Rank 0 - ResSigCtxt -> Rank 0 - TySynCtxt _ -> Rank 0 - ExprSigCtxt -> Rank 1 - FunSigCtxt _ -> Rank 1 - ConArgCtxt _ -> if polycomp - then Rank 2 + gen_rank n | rankn = ArbitraryRank + | rank2 = Rank 2 + | otherwise = Rank n + rank + = case ctxt of + DefaultDeclCtxt-> MustBeMonoType + ResSigCtxt -> MustBeMonoType + LamPatSigCtxt -> gen_rank 0 + BindPatSigCtxt -> gen_rank 0 + TySynCtxt _ -> gen_rank 0 + GenPatCtxt -> gen_rank 1 + -- This one is a bit of a hack + -- See the forall-wrapping in TcClassDcl.mkGenericInstance + + ExprSigCtxt -> gen_rank 1 + FunSigCtxt _ -> gen_rank 1 + ConArgCtxt _ | polycomp -> gen_rank 2 -- We are given the type of the entire -- constructor, hence rank 1 - else Rank 1 - ForSigCtxt _ -> Rank 1 - SpecInstCtxt -> Rank 1 + | otherwise -> gen_rank 1 + + ForSigCtxt _ -> gen_rank 1 + SpecInstCtxt -> gen_rank 1 + ThBrackCtxt -> gen_rank 1 actual_kind = typeKind ty kind_ok = case ctxt of - TySynCtxt _ -> True -- Any kind will do - ResSigCtxt -> isSubOpenTypeKind actual_kind - ExprSigCtxt -> isSubOpenTypeKind actual_kind + TySynCtxt _ -> True -- Any kind will do + ThBrackCtxt -> True -- Any kind will do + ResSigCtxt -> isSubOpenTypeKind actual_kind + ExprSigCtxt -> isSubOpenTypeKind actual_kind GenPatCtxt -> isLiftedTypeKind actual_kind ForSigCtxt _ -> isLiftedTypeKind actual_kind - other -> isSubArgTypeKind actual_kind + _ -> isSubArgTypeKind actual_kind ubx_tup = case ctxt of TySynCtxt _ | unboxed -> UT_Ok ExprSigCtxt | unboxed -> UT_Ok + ThBrackCtxt | 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_` -- 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) + -- 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 \end{code} \begin{code} -data Rank = Rank Int | Arbitrary - -decRank :: Rank -> Rank -decRank Arbitrary = Arbitrary -decRank (Rank n) = Rank (n-1) +data Rank = ArbitraryRank -- Any rank ok + | MustBeMonoType -- Monotype regardless of flags + | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes + | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms + | Rank Int -- Rank n, but could be more with -XRankNTypes + +decRank :: Rank -> Rank -- Function arguments +decRank (Rank 0) = Rank 0 +decRank (Rank n) = Rank (n-1) +decRank other_rank = other_rank + +nonZeroRank :: Rank -> Bool +nonZeroRank ArbitraryRank = True +nonZeroRank (Rank n) = n>0 +nonZeroRank _ = False ---------------------------------------- data UbxTupFlag = UT_Ok | UT_NotOk - -- The "Ok" version means "ok if -fglasgow-exts is on" + -- The "Ok" version means "ok if UnboxedTuples 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 - ; checkFreeness tvs theta +check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere + -- No unlifted types of any kind +check_mono_type rank ty + = do { check_type rank 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 rank 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 ; 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 +-- 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_arg_type ty - = check_poly_type Arbitrary UT_NotOk ty `thenM_` - checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) +check_type _ _ (TyVarTy _) = return () ----------------------------------------- -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_type rank _ (FunTy arg_ty res_ty) + = do { check_type (decRank rank) UT_NotOk arg_ty + ; check_type rank UT_Ok res_ty } -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_type rank _ (AppTy ty1 ty2) + = do { check_arg_type rank ty1 + ; check_arg_type rank ty2 } -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) +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 @@ -1148,29 +966,35 @@ check_tau_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 - mappM_ check_arg_type tys + mapM_ (check_mono_type SynArgMonoType) tys else -- In the liberal case (only for closed syns), expand then check case tcView ty of - Just ty' -> check_tau_type rank ubx_tup ty' + 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 <- xoptM Opt_UnboxedTuples + ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg + + ; 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 -- 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 } + ubx_tup_ok ub_tuples_allowed = case ubx_tup of + UT_Ok -> ub_tuples_allowed + _ -> False n_args = length tys tc_arity = tyConArity tc @@ -1178,11 +1002,60 @@ check_tau_type rank ubx_tup ty@(TyConApp tc tys) arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args ubx_tup_msg = ubxArgTyErr ty +check_type _ _ ty = pprPanic "check_type" (ppr ty) + ---------------------------------------- -forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty -unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> 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 +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 <- 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) } + +---------------------------------------- +forAllTyErr :: Rank -> Type -> SDoc +forAllTyErr rank ty + = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty) + , suggestion ] + where + suggestion = case rank of + Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types") + TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes") + SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms") + _ -> empty -- Polytype is always illegal + +unliftedArgErr, ubxArgTyErr :: Type -> SDoc +unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty] +ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty] + +kindErr :: Kind -> SDoc +kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind] \end{code} Note [Liberal type synonyms] @@ -1239,11 +1112,12 @@ data SourceTyCtxt | InstThetaCtxt -- Context of an instance decl -- instance => C [a] where ... -pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c) -pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type") -pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc) -pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration") -pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type") +pprSourceTyCtxt :: SourceTyCtxt -> SDoc +pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c) +pprSourceTyCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type") +pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc) +pprSourceTyCtxt InstThetaCtxt = ptext (sLit "the context of an instance declaration") +pprSourceTyCtxt TypeCtxt = ptext (sLit "the context of a type") \end{code} \begin{code} @@ -1252,12 +1126,13 @@ checkValidTheta ctxt theta = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta 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 +check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM () +check_valid_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 @@ -1268,7 +1143,7 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys) ; checkTc (arity == n_tys) arity_err -- Check the form of the argument types - ; mappM_ check_arg_type tys + ; mapM_ checkValidMonoType tys ; checkTc (check_class_pred_tys dflags ctxt tys) (predTyVarErr pred $$ how_to_allow) } @@ -1277,21 +1152,20 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys) arity = classArity cls n_tys = length tys arity_err = arityErr "Class" class_name arity n_tys - how_to_allow = parens (ptext SLIT("Use -XFlexibleContexts to permit this")) + how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this")) -check_pred_ty dflags ctxt pred@(EqPred ty1 ty2) + +check_pred_ty dflags _ 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) -- Check the form of the argument types - ; check_eq_arg_type ty1 - ; check_eq_arg_type ty2 + ; checkValidMonoType ty1 + ; checkValidMonoType 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 _ SigmaCtxt (IParam _ ty) = checkValidMonoType 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 @@ -1303,7 +1177,7 @@ check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty -- instance decl would show up two uses of ?x. -- Catch-all -check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty) +check_pred_ty _ _ sty = failWithTc (badPredTyErr sty) ------------------------- check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool @@ -1313,12 +1187,13 @@ check_class_pred_tys dflags ctxt tys InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys -- Further checks on head and theta in -- checkInstTermination - other -> flexible_contexts || all tyvar_head tys + _ -> 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 tyvar_head ty -- Haskell 98 allows predicates of form | tcIsTyVarTy ty = True -- C (a ty1 .. tyn) | otherwise -- where a is a type variable @@ -1357,14 +1232,18 @@ 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 () 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 + extended_tau_vars = growThetaTyVars theta tau_tyvars -- See Note [Implicit parameters and ambiguity] in TcSimplify is_ambig pred = isClassPred pred && @@ -1373,75 +1252,90 @@ checkAmbiguity forall_tyvars theta tau_tyvars ambig_var ct_var = (ct_var `elem` forall_tyvars) && not (ct_var `elemVarSet` extended_tau_vars) +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") $$ - ptext SLIT("must be reachable from the type after the '=>'"))] + = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred 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} - -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 [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 + +E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e} +Then grow precs tvs = {a,b,c} \begin{code} -checkFreeness forall_tyvars theta - = do { flexible_contexts <- doptM Opt_FlexibleContexts - ; unless flexible_contexts $ mappM_ 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 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)") - ] +growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet +-- See Note [Growing the tau-tvs using constraints] +growThetaTyVars theta tvs + | null theta = tvs + | otherwise = fixVarSet mk_next tvs + where + 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} + +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} +checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc checkThetaCtxt ctxt theta - = vcat [ptext SLIT("In the context:") <+> pprTheta theta, - ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ] + = vcat [ptext (sLit "In the context:") <+> pprTheta theta, + ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ] -badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty -eqPredTyErr sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty +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")) -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) + 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 :: [[PredType]] -> SDoc +dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (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] + = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"), + 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 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) } + n_arguments | n == 0 = ptext (sLit "no arguments") + | n == 1 = ptext (sLit "1 argument") + | True = hsep [int n, ptext (sLit "arguments")] \end{code} - %************************************************************************ %* * \subsection{Checking for a decent instance head type} @@ -1467,52 +1361,56 @@ 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 + check_inst_head dflags clas tys + return (clas, tys) }} +check_inst_head :: DynFlags -> Class -> [Type] -> TcM () check_inst_head dflags clas tys - -- If GlasgowExts then check at least one isn't a type variable - = do checkTc (dopt Opt_TypeSynonymInstances dflags || - all tcInstHeadTyNotSynonym tys) - (instTypeErr (pprClassPred clas tys) head_type_synonym_msg) - checkTc (dopt Opt_FlexibleInstances dflags || - all tcInstHeadTyAppAllTyVars tys) - (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg) - checkTc (dopt Opt_MultiParamTypeClasses dflags || - isSingleton tys) - (instTypeErr (pprClassPred clas tys) head_one_type_msg) - mapM_ check_one tys + = do { -- 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 (xopt Opt_FlexibleInstances dflags || + all tcInstHeadTyAppAllTyVars tys) + (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg) + ; checkTc (xopt Opt_MultiParamTypeClasses dflags || + isSingleton tys) + (instTypeErr (pprClassPred clas tys) head_one_type_msg) + -- May not contain type family applications + ; mapM_ checkTyFamFreeness tys + + ; mapM_ checkValidMonoType 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 :: SDoc -> SDoc -> SDoc instTypeErr pp_ty msg - = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, - nest 4 msg] + = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty, + nest 2 msg] \end{code} @@ -1522,11 +1420,15 @@ instTypeErr pp_ty msg %* * %************************************************************************ - \begin{code} -checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM () -checkValidInstance tyvars theta clas inst_tys - = do { undecidable_ok <- doptM Opt_UndecidableInstances +checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type + -> TcM (Class, [TcType]) +checkValidInstance hs_type tyvars theta tau + = setSrcSpan (getLoc hs_type) $ + do { (clas, inst_tys) <- setSrcSpan head_loc $ + checkValidInstHead tau + + ; undecidable_ok <- xoptM Opt_UndecidableInstances ; checkValidTheta InstThetaCtxt theta ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys) @@ -1540,10 +1442,17 @@ checkValidInstance tyvars theta clas inst_tys -- The Coverage Condition ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys) (instTypeErr (pprClassPred clas inst_tys) msg) + + ; return (clas, inst_tys) } where - msg = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"), + 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 @@ -1578,80 +1487,28 @@ checkInstTermination tys theta | otherwise = Nothing +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:") <+> pprPred pred)] -nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head") -smallerMsg = ptext SLIT("Constraint is no smaller than the instance head") -undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this") +nomoreMsg, smallerMsg, undecidableMsg :: SDoc +nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head") +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 -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. +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 -validDerivPred (ClassP cls tys) = hasNoDups fvs && sizeTypes tys == length fvs - where fvs = fvTypes tys -validDerivPred otehr = False +validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs + where fvs = fvTypes tys +validDerivPred _ = False \end{code} + %************************************************************************ %* * Checking type instance well-formedness and termination @@ -1660,20 +1517,19 @@ validDerivPred otehr = False \begin{code} -- Check that a "type instance" is well-formed (which includes decidability --- unless -fallow-undecidable-instances is given). +-- unless -XUndecidableInstances is given). -- 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) $ - polyTyErr 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)) } @@ -1708,7 +1564,7 @@ checkFamInst lhsTys famInsts checkTyFamFreeness :: Type -> TcM () checkTyFamFreeness ty = checkTc (isTyFamFree ty) $ - tyFamInstInIndexErr ty + tyFamInstIllegalErr ty -- Check that a type does not contain any type family applications. -- @@ -1717,23 +1573,22 @@ isTyFamFree = null . tyFamInsts -- Error messages -tyFamInstInIndexErr ty - = hang (ptext SLIT("Illegal type family application in type instance") <> - colon) 4 $ - ppr ty - -polyTyErr ty - = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $ +tyFamInstIllegalErr :: Type -> SDoc +tyFamInstIllegalErr ty + = hang (ptext (sLit "Illegal type synonym family application in instance") <> + colon) 2 $ ppr ty +famInstUndecErr :: Type -> SDoc -> SDoc famInstUndecErr ty msg = sep [msg, - nest 2 (ptext SLIT("in the type family application:") <+> + nest 2 (ptext (sLit "in the type family application:") <+> pprType ty)] -nestedMsg = ptext SLIT("Nested type family application") -nomoreVarMsg = ptext SLIT("Variable occurs more often than in instance head") -smallerAppMsg = ptext SLIT("Application is no smaller than the instance head") +nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc +nestedMsg = ptext (sLit "Nested type family application") +nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head") +smallerAppMsg = ptext (sLit "Application is no smaller than the instance head") \end{code} @@ -1749,7 +1604,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 @@ -1768,7 +1622,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 @@ -1777,8 +1630,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}