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,
+ writeWantedCoVar, readWantedCoVar,
+ newIP, newDict, newSilentGiven, isSilentEvVar,
- --------------------------------
- -- Creating new coercion variables
- newCoVars, newMetaCoVar,
+ newWantedEvVar, newWantedEvVars,
+ newTcEvBinds, addTcEvBind,
--------------------------------
-- Instantiation
- tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
- tcInstSigTyVars,
- tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
- tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
+ tcInstTyVars, tcInstSigTyVars,
+ tcInstType,
+ tcInstSkolTyVars, tcInstSuperSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
+ tcSkolDFunType, tcSuperSkolTyVars,
--------------------------------
-- Checking type validity
Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
- SourceTyCtxt(..), checkValidTheta, checkFreeness,
- checkValidInstHead, checkValidInstance,
- checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
- checkUpdateMeta, updateMeta, checkTauTvUpdate, fillBoxWithTau, unifyKindCtxt,
- unifyKindMisMatch, validDerivPred, arityErr, notMonoType, notMonoArgs,
+ SourceTyCtxt(..), checkValidTheta,
+ checkValidInstance,
+ 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
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 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 ()
+newEvVars :: TcThetaType -> TcM [EvVar]
+newEvVars theta = mapM newEvVar theta
- | 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 = ()
-
- f :: (A a -> a -> ()) -> ()
- f = \ _ -> ()
-
- x :: ()
- x = f (\ x p -> p x)
+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
-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 (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.
-
-\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 -> Maybe 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 mb_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 = mb_loc `orElse` getSrcSpan 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 (Just 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
+
+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}
%************************************************************************
\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
+newMetaTyVar meta_info kind
+ = do { uniq <- newMetaUnique
; 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
- ; 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 )
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
; 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
- = 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;
+ ; 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
- _k1 = tyVarKind tyvar
- _k2 = typeKind ty
+ tv_kind = tyVarKind tyvar
+ ty_kind = typeKind ty
\end{code}
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
-- 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}
%************************************************************************
\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
\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
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)
--
-- We leave skolem TyVars alone; they are immutable.
zonkQuantifiedTyVar tv
- | ASSERT( isTcTyVar tv )
- isSkolemTyVar tv = return tv
+ = 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) = do { loc' <- zonkGivenLoc loc; return (Given loc') }
+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:
* 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 = ()
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]
~~~~~~~~~~~~~~~~~~~~~~~~
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.
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.
-- 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
-- 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 ) do
ty' <- go ty
- return (ForAllTy tyvar ty')
+ tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
+ return (ForAllTy tyvar' ty')
go_pred (ClassP c tys) = do tys' <- mapM go tys
return (ClassP c tys')
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 *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 }
+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 }
+
+-- 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}
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}
%************************************************************************
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
- 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
+ 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
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 ty
+checkValidMonoType ty = check_mono_type MustBeMonoType ty
\end{code}
\begin{code}
-data Rank = Rank Int | Arbitrary
+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
-decRank Arbitrary = Arbitrary
-decRank (Rank n) = Rank (n-1)
+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 (Rank 0) = False
-nonZeroRank _ = True
+nonZeroRank ArbitraryRank = True
+nonZeroRank (Rank n) = n>0
+nonZeroRank _ = False
----------------------------------------
data UbxTupFlag = UT_Ok | UT_NotOk
-- The "Ok" version means "ok if UnboxedTuples is on"
----------------------------------------
-check_mono_type :: Type -> TcM () -- No foralls anywhere
- -- No unlifted types of any kind
-check_mono_type ty
- = do { check_type (Rank 0) UT_NotOk ty
+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
+-- 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
check_type rank ubx_tup ty
| not (null tvs && null theta)
- = do { checkTc (nonZeroRank rank) (forAllTyErr ty)
+ = 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
- ; 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 }
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 tys
+ mapM_ (check_mono_type SynArgMonoType) tys
else -- In the liberal case (only for closed syns), expand then check
case tcView ty of
}
| 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
- ; let rank' = if impred then rank else Rank 0
+ ; 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
-- Anyway, they are dealt with by a special case in check_tau_type
check_arg_type rank ty
- = do { impred <- doptM Opt_ImpredicativeTypes
- ; let rank' = if impred then rank else Rank 0 -- Monotype unless impredicative
+ = 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, unliftedArgErr, ubxArgTyErr :: Type -> SDoc
-forAllTyErr ty = sep [ptext (sLit "Illegal polymorphic or qualified type:"), ppr 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]
; checkTc (arity == n_tys) arity_err
-- Check the form of the argument types
- ; mapM_ check_mono_type tys
+ ; mapM_ checkValidMonoType tys
; checkTc (check_class_pred_tys dflags ctxt tys)
(predTyVarErr pred $$ how_to_allow)
}
arity_err = arityErr "Class" class_name arity n_tys
how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
-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
- ; check_mono_type ty1
- ; check_mono_type ty2
+ ; checkValidMonoType ty1
+ ; checkValidMonoType ty2
}
-check_pred_ty _ SigmaCtxt (IParam _ ty) = check_mono_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
-- 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
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 ()
= 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 &&
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") $$
+ 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 :: [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)")
- ]
+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
= 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") <+> pprPred pred
+eqPredTyErr pred = ptext (sLit "Illegal equational constraint") <+> pprPred 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)]
dupPredWarn :: [[PredType]] -> SDoc
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}
We can also have instances for functions: @instance Foo (a -> b) ...@.
\begin{code}
-checkValidInstHead :: Type -> TcM (Class, [TcType])
-
-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
- mapM_ check_mono_type tys
- 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_mono_type tys
+checkValidInstHead :: Class -> [Type] -> TcM ()
+checkValidInstHead clas tys
+ = do { dflags <- getDOpts
+
+ -- If GlasgowExts then check at least one isn't a type variable
+ ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
+ all tcInstHeadTyNotSynonym tys)
+ (instTypeErr pp_pred head_type_synonym_msg)
+ ; checkTc (xopt Opt_FlexibleInstances dflags ||
+ all tcInstHeadTyAppAllTyVars tys)
+ (instTypeErr pp_pred head_type_args_tyvars_msg)
+ ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
+ isSingleton tys)
+ (instTypeErr pp_pred 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
+ 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." $$
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."])
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}
%* *
%************************************************************************
-
\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
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
validDerivPred _ = False
\end{code}
+
%************************************************************************
%* *
Checking type instance well-formedness and termination
; 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))
}
checkTyFamFreeness :: Type -> TcM ()
checkTyFamFreeness ty
= checkTc (isTyFamFree ty) $
- tyFamInstInIndexErr ty
+ tyFamInstIllegalErr ty
-- Check that a type does not contain any type family applications.
--
-- Error messages
-tyFamInstInIndexErr :: Type -> SDoc
-tyFamInstInIndexErr ty
- = hang (ptext (sLit "Illegal type family application 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
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}
projects / ghc-hetmet.git / blobdiff