--------------------------------
-- Creating new mutable type variables
newTyVar,
- newTyVarTy, -- Kind -> NF_TcM TcType
- newTyVarTys, -- Int -> Kind -> NF_TcM [TcType]
- newKindVar, newKindVars, newBoxityVar,
+ newTyVarTy, -- Kind -> TcM TcType
+ newTyVarTys, -- Int -> Kind -> TcM [TcType]
+ newKindVar, newKindVars, newOpenTypeKind,
putTcTyVar, getTcTyVar,
+ newMutTyVar, readMutTyVar, writeMutTyVar,
newHoleTyVarTy, readHoleResult, zapToType,
SourceTyCtxt(..), checkValidTheta,
checkValidTyCon, checkValidClass,
checkValidInstHead, instTypeErr, checkAmbiguity,
+ arityErr,
--------------------------------
-- Zonking
+ zonkType,
zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
- zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
+ zonkTcPredType, zonkTcTyVarToTyVar, zonkKindEnv,
) where
-- friends:
import TypeRep ( Type(..), SourceType(..), TyNote(..), -- Friend; can see representation
- Kind, ThetaType
+ Kind, ThetaType, typeCon
)
import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
- tcEqType, tcCmpPred,
+ tcEqType, tcCmpPred, isClassPred,
tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
tcSplitTyConApp_maybe, tcSplitForAllTys,
- tcIsTyVarTy, tcSplitSigmaTy,
- isUnLiftedType, isIPPred, isHoleTyVar,
+ tcIsTyVarTy, tcSplitSigmaTy, mkTyConApp,
+ isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy,
mkAppTy, mkTyVarTy, mkTyVarTys,
tyVarsOfPred, getClassPredTys_maybe,
liftedTypeKind, openTypeKind, defaultKind, superKind,
superBoxity, liftedBoxity, typeKind,
tyVarsOfType, tyVarsOfTypes,
- eqKind, isTypeKind, isAnyTypeKind,
-
+ eqKind, isTypeKind,
isFFIArgumentTy, isFFIImportResultTy
)
-import qualified Type ( splitFunTys )
import Subst ( Subst, mkTopTyVarSubst, substTy )
import Class ( Class, DefMeth(..), classArity, className, classBigSig )
-import TyCon ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
- tyConArity, tyConName, tyConKind, tyConTheta,
+import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
+ tyConArity, tyConName, tyConTheta,
getSynTyConDefn, tyConDataCons )
import DataCon ( DataCon, dataConWrapId, dataConName, dataConSig, dataConFieldLabels )
import FieldLabel ( fieldLabelName, fieldLabelType )
-import PrimRep ( PrimRep(VoidRep) )
-import Var ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
+import Var ( TyVar, idType, idName, tyVarKind, tyVarName, isTyVar,
+ mkTyVar, mkMutTyVar, isMutTyVar, mutTyVarRef )
-- others:
import Generics ( validGenericMethodType )
-import TcMonad -- TcType, amongst others
-import TysWiredIn ( voidTy, listTyCon, tupleTyCon )
+import TcRnMonad -- TcType, amongst others
import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
import ForeignCall ( Safety(..) )
import FunDeps ( grow )
import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
-import Name ( Name, NamedThing(..), setNameUnique, mkSystemName,
- mkInternalName, mkDerivedTyConOcc
- )
+import Name ( Name, setNameUnique, mkSystemTvNameEncoded )
import VarSet
-import BasicTypes ( Boxity(Boxed) )
import CmdLineOpts ( dopt, DynFlag(..) )
-import Unique ( Uniquable(..) )
-import SrcLoc ( noSrcLoc )
import Util ( nOfThem, isSingleton, equalLength, notNull )
import ListSetOps ( equivClasses, removeDups )
import Outputable
%************************************************************************
\begin{code}
-newTyVar :: Kind -> NF_TcM TcTyVar
+newMutTyVar :: Name -> Kind -> TyVarDetails -> TcM TyVar
+newMutTyVar name kind details
+ = do { ref <- newMutVar Nothing ;
+ return (mkMutTyVar name kind details ref) }
+
+readMutTyVar :: TyVar -> TcM (Maybe Type)
+readMutTyVar tyvar = readMutVar (mutTyVarRef tyvar)
+
+writeMutTyVar :: TyVar -> Maybe Type -> TcM ()
+writeMutTyVar tyvar val = writeMutVar (mutTyVarRef tyvar) val
+
+newTyVar :: Kind -> TcM TcTyVar
newTyVar kind
- = tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutTyVar (mkSystemName uniq FSLIT("t")) kind VanillaTv
+ = newUnique `thenM` \ uniq ->
+ newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
-newTyVarTy :: Kind -> NF_TcM TcType
+newTyVarTy :: Kind -> TcM TcType
newTyVarTy kind
- = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
- returnNF_Tc (TyVarTy tc_tyvar)
+ = newTyVar kind `thenM` \ tc_tyvar ->
+ returnM (TyVarTy tc_tyvar)
-newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
-newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
+newTyVarTys :: Int -> Kind -> TcM [TcType]
+newTyVarTys n kind = mappM newTyVarTy (nOfThem n kind)
-newKindVar :: NF_TcM TcKind
+newKindVar :: TcM TcKind
newKindVar
- = tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutTyVar (mkSystemName uniq FSLIT("k")) superKind VanillaTv `thenNF_Tc` \ kv ->
- returnNF_Tc (TyVarTy kv)
-
-newKindVars :: Int -> NF_TcM [TcKind]
-newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
-
-newBoxityVar :: NF_TcM TcKind
-newBoxityVar
- = tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutTyVar (mkSystemName uniq FSLIT("bx")) superBoxity VanillaTv `thenNF_Tc` \ kv ->
- returnNF_Tc (TyVarTy kv)
+ = newUnique `thenM` \ uniq ->
+ newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("k")) superKind VanillaTv `thenM` \ kv ->
+ returnM (TyVarTy kv)
+
+newKindVars :: Int -> TcM [TcKind]
+newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
+
+newOpenTypeKind :: TcM TcKind -- Returns the kind (Type bx), where bx is fresh
+newOpenTypeKind
+ = newUnique `thenM` \ uniq ->
+ newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("bx")) superBoxity VanillaTv `thenM` \ kv ->
+ returnM (mkTyConApp typeCon [TyVarTy kv])
\end{code}
%************************************************************************
\begin{code}
-newHoleTyVarTy :: NF_TcM TcType
- = tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutTyVar (mkSystemName uniq FSLIT("h")) openTypeKind HoleTv `thenNF_Tc` \ tv ->
- returnNF_Tc (TyVarTy tv)
+newHoleTyVarTy :: TcM TcType
+ = newUnique `thenM` \ uniq ->
+ newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("h")) openTypeKind HoleTv `thenM` \ tv ->
+ returnM (TyVarTy tv)
-readHoleResult :: TcType -> NF_TcM TcType
+readHoleResult :: TcType -> TcM TcType
-- Read the answer out of a hole, constructed by newHoleTyVarTy
readHoleResult (TyVarTy tv)
= ASSERT( isHoleTyVar tv )
- getTcTyVar tv `thenNF_Tc` \ maybe_res ->
+ getTcTyVar tv `thenM` \ maybe_res ->
case maybe_res of
- Just ty -> returnNF_Tc ty
+ Just ty -> returnM ty
Nothing -> pprPanic "readHoleResult: empty" (ppr tv)
readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
-zapToType :: TcType -> NF_TcM TcType
+zapToType :: TcType -> TcM TcType
zapToType (TyVarTy tv)
| isHoleTyVar tv
- = getTcTyVar tv `thenNF_Tc` \ maybe_res ->
+ = getTcTyVar tv `thenM` \ maybe_res ->
case maybe_res of
- Nothing -> newTyVarTy openTypeKind `thenNF_Tc` \ ty ->
- putTcTyVar tv ty `thenNF_Tc_`
- returnNF_Tc ty
- Just ty -> returnNF_Tc ty -- No need to loop; we never
+ Nothing -> newTyVarTy openTypeKind `thenM` \ ty ->
+ putTcTyVar tv ty `thenM_`
+ returnM ty
+ Just ty -> returnM ty -- No need to loop; we never
-- have chains of holes
-zapToType other_ty = returnNF_Tc other_ty
+zapToType other_ty = returnM other_ty
\end{code}
%************************************************************************
\begin{code}
tcInstTyVars :: TyVarDetails -> [TyVar]
- -> NF_TcM ([TcTyVar], [TcType], Subst)
+ -> TcM ([TcTyVar], [TcType], Subst)
tcInstTyVars tv_details tyvars
- = mapNF_Tc (tcInstTyVar tv_details) tyvars `thenNF_Tc` \ tc_tyvars ->
+ = mappM (tcInstTyVar tv_details) tyvars `thenM` \ tc_tyvars ->
let
tys = mkTyVarTys tc_tyvars
in
- returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
+ returnM (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
-- Since the tyvars are freshly made,
-- they cannot possibly be captured by
-- any existing for-alls. Hence mkTopTyVarSubst
tcInstTyVar tv_details tyvar
- = tcGetUnique `thenNF_Tc` \ uniq ->
+ = newUnique `thenM` \ uniq ->
let
name = setNameUnique (tyVarName tyvar) uniq
-- Note that we don't change the print-name
-- Better watch out for this. If worst comes to worst, just
-- use mkSystemName.
in
- tcNewMutTyVar name (tyVarKind tyvar) tv_details
+ newMutTyVar name (tyVarKind tyvar) tv_details
-tcInstType :: TyVarDetails -> TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
+tcInstType :: TyVarDetails -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-- tcInstType instantiates the outer-level for-alls of a TcType with
-- fresh (mutable) type variables, splits off the dictionary part,
-- and returns the pieces.
let
(theta, tau) = tcSplitPhiTy rho
in
- returnNF_Tc ([], theta, tau)
+ returnM ([], theta, tau)
- (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
+ (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenM` \ (tyvars', _, tenv) ->
let
(theta, tau) = tcSplitPhiTy (substTy tenv rho)
in
- returnNF_Tc (tyvars', theta, tau)
+ returnM (tyvars', theta, tau)
\end{code}
%************************************************************************
\begin{code}
-putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
-getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
+putTcTyVar :: TcTyVar -> TcType -> TcM TcType
+getTcTyVar :: TcTyVar -> TcM (Maybe TcType)
\end{code}
Putting is easy:
putTcTyVar tyvar ty
| not (isMutTyVar tyvar)
= pprTrace "putTcTyVar" (ppr tyvar) $
- returnNF_Tc ty
+ returnM ty
| otherwise
= ASSERT( isMutTyVar tyvar )
- tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
- returnNF_Tc ty
+ writeMutTyVar tyvar (Just ty) `thenM_`
+ returnM ty
\end{code}
Getting is more interesting. The easy thing to do is just to read, thus:
\begin{verbatim}
-getTcTyVar tyvar = tcReadMutTyVar tyvar
+getTcTyVar tyvar = readMutTyVar tyvar
\end{verbatim}
But it's more fun to short out indirections on the way: If this
getTcTyVar tyvar
| not (isMutTyVar tyvar)
= pprTrace "getTcTyVar" (ppr tyvar) $
- returnNF_Tc (Just (mkTyVarTy tyvar))
+ returnM (Just (mkTyVarTy tyvar))
| otherwise
= ASSERT2( isMutTyVar tyvar, ppr tyvar )
- tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ readMutTyVar tyvar `thenM` \ maybe_ty ->
case maybe_ty of
- Just ty -> short_out ty `thenNF_Tc` \ ty' ->
- tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
- returnNF_Tc (Just ty')
+ Just ty -> short_out ty `thenM` \ ty' ->
+ writeMutTyVar tyvar (Just ty') `thenM_`
+ returnM (Just ty')
- Nothing -> returnNF_Tc Nothing
+ Nothing -> returnM Nothing
-short_out :: TcType -> NF_TcM TcType
+short_out :: TcType -> TcM TcType
short_out ty@(TyVarTy tyvar)
| not (isMutTyVar tyvar)
- = returnNF_Tc ty
+ = returnM ty
| otherwise
- = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ = readMutTyVar tyvar `thenM` \ maybe_ty ->
case maybe_ty of
- Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
- tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
- returnNF_Tc ty'
+ Just ty' -> short_out ty' `thenM` \ ty' ->
+ writeMutTyVar tyvar (Just ty') `thenM_`
+ returnM ty'
- other -> returnNF_Tc ty
+ other -> returnM ty
-short_out other_ty = returnNF_Tc other_ty
+short_out other_ty = returnM other_ty
\end{code}
----------------- Type variables
\begin{code}
-zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
-zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
+zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
+zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
-zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
-zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
- returnNF_Tc (tyVarsOfTypes tys)
+zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
+zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
+ returnM (tyVarsOfTypes tys)
-zonkTcTyVar :: TcTyVar -> NF_TcM TcType
-zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
+zonkTcTyVar :: TcTyVar -> TcM TcType
+zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) tyvar
\end{code}
----------------- Types
\begin{code}
-zonkTcType :: TcType -> NF_TcM TcType
-zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
+zonkTcType :: TcType -> TcM TcType
+zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
-zonkTcTypes :: [TcType] -> NF_TcM [TcType]
-zonkTcTypes tys = mapNF_Tc zonkTcType tys
+zonkTcTypes :: [TcType] -> TcM [TcType]
+zonkTcTypes tys = mappM zonkTcType tys
-zonkTcClassConstraints cts = mapNF_Tc zonk cts
+zonkTcClassConstraints cts = mappM zonk cts
where zonk (clas, tys)
- = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
- returnNF_Tc (clas, new_tys)
+ = zonkTcTypes tys `thenM` \ new_tys ->
+ returnM (clas, new_tys)
-zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
-zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
+zonkTcThetaType :: TcThetaType -> TcM TcThetaType
+zonkTcThetaType theta = mappM zonkTcPredType theta
-zonkTcPredType :: TcPredType -> NF_TcM TcPredType
+zonkTcPredType :: TcPredType -> TcM TcPredType
zonkTcPredType (ClassP c ts)
- = zonkTcTypes ts `thenNF_Tc` \ new_ts ->
- returnNF_Tc (ClassP c new_ts)
+ = zonkTcTypes ts `thenM` \ new_ts ->
+ returnM (ClassP c new_ts)
zonkTcPredType (IParam n t)
- = zonkTcType t `thenNF_Tc` \ new_t ->
- returnNF_Tc (IParam n new_t)
+ = zonkTcType t `thenM` \ new_t ->
+ returnM (IParam n new_t)
\end{code}
------------------- These ...ToType, ...ToKind versions
are used at the end of type checking
\begin{code}
-zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
+zonkKindEnv :: [(Name, TcKind)] -> TcM [(Name, Kind)]
zonkKindEnv pairs
- = mapNF_Tc zonk_it pairs
+ = mappM zonk_it pairs
where
- zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
- returnNF_Tc (name, kind)
+ zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenM` \ kind ->
+ returnM (name, kind)
-- When zonking a kind, we want to
-- zonk a *kind* variable to (Type *)
| tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
| otherwise = pprPanic "zonkKindEnv" (ppr kv)
-zonkTcTypeToType :: TcType -> NF_TcM Type
-zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
- where
- -- Zonk a mutable but unbound type variable to an arbitrary type
- -- We know it's unbound even though we don't carry an environment,
- -- because at the binding site for a type variable we bind the
- -- mutable tyvar to a fresh immutable one. So the mutable store
- -- plays the role of an environment. If we come across a mutable
- -- type variable that isn't so bound, it must be completely free.
- zonk_unbound_tyvar tv = putTcTyVar tv (mkArbitraryType tv)
-
-
--- When the type checker finds a type variable with no binding,
--- which means it can be instantiated with an arbitrary type, it
--- usually instantiates it to Void. Eg.
---
--- length []
--- ===>
--- length Void (Nil Void)
---
--- But in really obscure programs, the type variable might have
--- a kind other than *, so we need to invent a suitably-kinded type.
---
--- This commit uses
--- Void for kind *
--- List for kind *->*
--- Tuple for kind *->...*->*
---
--- which deals with most cases. (Previously, it only dealt with
--- kind *.)
---
--- In the other cases, it just makes up a TyCon with a suitable
--- kind. If this gets into an interface file, anyone reading that
--- file won't understand it. This is fixable (by making the client
--- of the interface file make up a TyCon too) but it is tiresome and
--- never happens, so I am leaving it
-
-mkArbitraryType :: TcTyVar -> Type
--- Make up an arbitrary type whose kind is the same as the tyvar.
--- We'll use this to instantiate the (unbound) tyvar.
-mkArbitraryType tv
- | isAnyTypeKind kind = voidTy -- The vastly common case
- | otherwise = TyConApp tycon []
- where
- kind = tyVarKind tv
- (args,res) = Type.splitFunTys kind -- Kinds are simple; use Type.splitFunTys
-
- tycon | kind `eqKind` tyConKind listTyCon -- *->*
- = listTyCon -- No tuples this size
-
- | all isTypeKind args && isTypeKind res
- = tupleTyCon Boxed (length args) -- *-> ... ->*->*
-
- | otherwise
- = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
- mkPrimTyCon tc_name kind 0 [] VoidRep
- -- Same name as the tyvar, apart from making it start with a colon (sigh)
- -- I dread to think what will happen if this gets out into an
- -- interface file. Catastrophe likely. Major sigh.
-
- tc_name = mkInternalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
-
-- zonkTcTyVarToTyVar is applied to the *binding* occurrence
-- of a type variable, at the *end* of type checking. It changes
-- the *mutable* type variable into an *immutable* one.
-- Now any bound occurences of the original type variable will get
-- zonked to the immutable version.
-zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
+zonkTcTyVarToTyVar :: TcTyVar -> TcM TyVar
zonkTcTyVarToTyVar tv
= let
-- Make an immutable version, defaulting
in
-- If the type variable is mutable, then bind it to immut_tv_ty
-- so that all other occurrences of the tyvar will get zapped too
- zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
+ zonkTyVar zap tv `thenM` \ ty2 ->
+ -- This warning shows up if the allegedly-unbound tyvar is
+ -- already bound to something. It can actually happen, and
+ -- in a harmless way (see [Silly Type Synonyms] below) so
+ -- it's only a warning
WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
- returnNF_Tc immut_tv
+ returnM immut_tv
\end{code}
+[Silly Type Synonyms]
+
+Consider this:
+ type C u a = u -- Note 'a' unused
+
+ foo :: (forall a. C u a -> C u a) -> u
+ foo x = ...
+
+ bar :: Num u => u
+ bar = foo (\t -> t + t)
+
+* From the (\t -> t+t) we get type {Num d} => d -> d
+ where d is fresh.
+
+* Now unify with type of foo's arg, and we get:
+ {Num (C d a)} => C d a -> C d a
+ where a is fresh.
+
+* Now abstract over the 'a', but float out the Num (C d a) constraint
+ because it does not 'really' mention a. (see Type.tyVarsOfType)
+ The arg to foo becomes
+ /\a -> \t -> t+t
+
+* So we get a dict binding for Num (C d a), which is zonked to give
+ a = ()
+
+* Then the /\a abstraction has a zonked 'a' in it.
+
+All very silly. I think its harmless to ignore the problem.
+
%************************************************************************
%* *
-- For tyvars bound at a for-all, zonkType zonks them to an immutable
-- type variable and zonks the kind too
-zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
+zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
-- see zonkTcType, and zonkTcTypeToType
-> TcType
- -> NF_TcM Type
+ -> TcM Type
zonkType unbound_var_fn ty
= go ty
where
- go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
- returnNF_Tc (TyConApp tycon tys')
+ go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
+ returnM (TyConApp tycon tys')
- go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
- go ty2 `thenNF_Tc` \ ty2' ->
- returnNF_Tc (NoteTy (SynNote ty1') ty2')
+ go (NoteTy (SynNote ty1) ty2) = go ty1 `thenM` \ ty1' ->
+ go ty2 `thenM` \ ty2' ->
+ returnM (NoteTy (SynNote ty1') ty2')
go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
- go (SourceTy p) = go_pred p `thenNF_Tc` \ p' ->
- returnNF_Tc (SourceTy p')
+ go (SourceTy p) = go_pred p `thenM` \ p' ->
+ returnM (SourceTy p')
- go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
- go res `thenNF_Tc` \ res' ->
- returnNF_Tc (FunTy arg' res')
+ go (FunTy arg res) = go arg `thenM` \ arg' ->
+ go res `thenM` \ res' ->
+ returnM (FunTy arg' res')
- go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
- go arg `thenNF_Tc` \ arg' ->
- returnNF_Tc (mkAppTy fun' arg')
+ go (AppTy fun arg) = go fun `thenM` \ fun' ->
+ go arg `thenM` \ arg' ->
+ returnM (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) = zonkTyVar unbound_var_fn tyvar
- go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
- go ty `thenNF_Tc` \ ty' ->
- returnNF_Tc (ForAllTy tyvar' ty')
+ go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenM` \ tyvar' ->
+ go ty `thenM` \ ty' ->
+ returnM (ForAllTy tyvar' ty')
- go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
- returnNF_Tc (ClassP c tys')
- go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
- returnNF_Tc (NType tc tys')
- go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
- returnNF_Tc (IParam n ty')
+ go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
+ returnM (ClassP c tys')
+ go_pred (NType tc tys) = mappM go tys `thenM` \ tys' ->
+ returnM (NType tc tys')
+ go_pred (IParam n ty) = go ty `thenM` \ ty' ->
+ returnM (IParam n ty')
-zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
- -> TcTyVar -> NF_TcM TcType
+zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
+ -> TcTyVar -> TcM TcType
zonkTyVar unbound_var_fn tyvar
| not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
-- zonking a forall type, when the bound type variable
-- needn't be mutable
= ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
- returnNF_Tc (TyVarTy tyvar)
+ returnM (TyVarTy tyvar)
| otherwise
- = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ = getTcTyVar tyvar `thenM` \ maybe_ty ->
case maybe_ty of
Nothing -> unbound_var_fn tyvar -- Mutable and unbound
Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
checkValidType :: UserTypeCtxt -> Type -> TcM ()
-- Checks that the type is valid for the given context
checkValidType ctxt ty
- = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
+ = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
let
rank | gla_exts = Arbitrary
| otherwise
-- but for type synonyms we allow them even at
-- top level
in
- tcAddErrCtxt (checkTypeCtxt ctxt ty) $
+ addErrCtxt (checkTypeCtxt ctxt ty) $
-- Check that the thing has kind Type, and is lifted if necessary
- checkTc kind_ok (kindErr actual_kind) `thenTc_`
+ checkTc kind_ok (kindErr actual_kind) `thenM_`
-- Check the internal validity of the type itself
check_poly_type rank ubx_tup ty
= let
(tvs, theta, tau) = tcSplitSigmaTy ty
in
- check_valid_theta SigmaCtxt theta `thenTc_`
- check_tau_type (decRank rank) ubx_tup tau `thenTc_`
- checkFreeness tvs theta `thenTc_`
+ check_valid_theta SigmaCtxt theta `thenM_`
+ check_tau_type (decRank rank) ubx_tup tau `thenM_`
+ checkFreeness tvs theta `thenM_`
checkAmbiguity tvs theta (tyVarsOfType tau)
----------------------------------------
-- Anyway, they are dealt with by a special case in check_tau_type
check_arg_type ty
- = check_tau_type (Rank 0) UT_NotOk ty `thenTc_`
+ = check_tau_type (Rank 0) UT_NotOk ty `thenM_`
checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
----------------------------------------
-- No foralls otherwise
check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
-check_tau_type rank ubx_tup (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
+check_tau_type rank ubx_tup (SourceTy sty) = getDOpts `thenM` \ dflags ->
check_source_ty dflags TypeCtxt sty
-check_tau_type rank ubx_tup (TyVarTy _) = returnTc ()
+check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
- = check_poly_type rank UT_NotOk arg_ty `thenTc_`
+ = check_poly_type rank UT_NotOk arg_ty `thenM_`
check_tau_type rank UT_Ok res_ty
check_tau_type rank ubx_tup (AppTy ty1 ty2)
- = check_arg_type ty1 `thenTc_` check_arg_type ty2
+ = check_arg_type ty1 `thenM_` check_arg_type ty2
-check_tau_type rank ubx_tup (NoteTy note ty)
- = check_tau_type rank ubx_tup ty
+check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
-- Synonym notes are built only when the synonym is
-- saturated (see Type.mkSynTy)
- -- Not checking the 'note' part allows us to instantiate a synonym
- -- defn with a for-all type, or with a partially-applied type synonym,
- -- but that seems OK too
+ = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
+ (if gla_exts then
+ -- If -fglasgow-exts then don't check the 'note' part.
+ -- This allows us to instantiate a synonym defn with a
+ -- for-all type, or with a partially-applied type synonym.
+ -- e.g. type T a b = a
+ -- type S m = m ()
+ -- f :: S (T Int)
+ -- Here, T is partially applied, so it's illegal in H98.
+ -- But if you expand S first, then T we get just
+ -- f :: Int
+ -- which is fine.
+ returnM ()
+ else
+ -- For H98, do check the un-expanded part
+ check_tau_type rank ubx_tup syn
+ ) `thenM_`
+
+ check_tau_type rank ubx_tup ty
+
+check_tau_type rank ubx_tup (NoteTy other_note ty)
+ = check_tau_type rank ubx_tup ty
check_tau_type rank ubx_tup ty@(TyConApp tc tys)
| isSynTyCon tc
= -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
- -- synonym application, leaving it to checkValidType (i.e. right here
+ -- synonym application, leaving it to checkValidType (i.e. right here)
-- to find the error
- checkTc syn_arity_ok arity_msg `thenTc_`
- mapTc_ check_arg_type tys
+ checkTc syn_arity_ok arity_msg `thenM_`
+ mappM_ check_arg_type tys
| isUnboxedTupleTyCon tc
- = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
- checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenTc_`
- mapTc_ (check_tau_type (Rank 0) UT_Ok) tys
+ = doptM Opt_GlasgowExts `thenM` \ gla_exts ->
+ checkTc (ubx_tup_ok gla_exts) ubx_tup_msg `thenM_`
+ mappM_ (check_tau_type (Rank 0) UT_Ok) tys
-- Args are allowed to be unlifted, or
-- more unboxed tuples, so can't use check_arg_ty
| otherwise
- = mapTc_ check_arg_type tys
+ = mappM_ check_arg_type tys
where
ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
\end{code}
-Check for ambiguity
-~~~~~~~~~~~~~~~~~~~
- forall V. P => tau
-is ambiguous if P contains generic variables
-(i.e. one of the Vs) that are not mentioned in tau
-
-However, we need to take account of functional dependencies
-when we speak of 'mentioned in tau'. Example:
- class C a b | a -> b where ...
-Then the type
- forall x y. (C x y) => x
-is not ambiguous because x is mentioned and x determines y
-
-NB; the ambiguity check is only used for *user* types, not for types
-coming from inteface files. The latter can legitimately have
-ambiguous types. Example
-
- class S a where s :: a -> (Int,Int)
- instance S Char where s _ = (1,1)
- f:: S a => [a] -> Int -> (Int,Int)
- f (_::[a]) x = (a*x,b)
- where (a,b) = s (undefined::a)
-
-Here the worker for f gets the type
- fw :: forall a. S a => Int -> (# Int, Int #)
-
-If the list of tv_names is empty, we have a monotype, and then we
-don't need to check for ambiguity either, because the test can't fail
-(see is_ambig).
-
-\begin{code}
-checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
-checkAmbiguity forall_tyvars theta tau_tyvars
- = mapTc_ complain (filter is_ambig theta)
- where
- complain pred = addErrTc (ambigErr pred)
- extended_tau_vars = grow theta tau_tyvars
- is_ambig pred = any ambig_var (varSetElems (tyVarsOfPred pred))
-
- ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
- not (ct_var `elemVarSet` extended_tau_vars)
-
- is_free ct_var = not (ct_var `elem` forall_tyvars)
-
-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 '=>'"))]
-\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.
-
-\begin{code}
-checkFreeness forall_tyvars theta
- = mapTc_ 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"),
- nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
- ]
-\end{code}
%************************************************************************
\begin{code}
checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
checkValidTheta ctxt theta
- = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
+ = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
-------------------------
check_valid_theta ctxt []
- = returnTc ()
+ = returnM ()
check_valid_theta ctxt theta
- = getDOptsTc `thenNF_Tc` \ dflags ->
- warnTc (notNull dups) (dupPredWarn dups) `thenNF_Tc_`
- mapTc_ (check_source_ty dflags ctxt) theta
+ = getDOpts `thenM` \ dflags ->
+ warnTc (notNull dups) (dupPredWarn dups) `thenM_`
+ -- Actually, in instance decls and type signatures,
+ -- duplicate constraints are eliminated by TcMonoType.hoistForAllTys,
+ -- so this error can only fire for the context of a class or
+ -- data type decl.
+ mappM_ (check_source_ty dflags ctxt) theta
where
(_,dups) = removeDups tcCmpPred theta
-------------------------
check_source_ty dflags ctxt pred@(ClassP cls tys)
= -- Class predicates are valid in all contexts
- mapTc_ check_arg_type tys `thenTc_`
- checkTc (arity == n_tys) arity_err `thenTc_`
- checkTc (all tyvar_head tys || arby_preds_ok)
+ mappM_ check_arg_type tys `thenM_`
+ checkTc (arity == n_tys) arity_err `thenM_`
+ checkTc (check_class_pred_tys dflags ctxt tys)
(predTyVarErr pred $$ how_to_allow)
where
n_tys = length tys
arity_err = arityErr "Class" class_name arity n_tys
- arby_preds_ok = case ctxt of
- InstHeadCtxt -> True -- We check for instance-head formation
- -- in checkValidInstHead
- InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
- other -> dopt Opt_GlasgowExts dflags
-
how_to_allow = case ctxt of
InstHeadCtxt -> empty -- Should not happen
InstThetaCtxt -> parens undecidableMsg
-- constraint Foo [Int] might come out of e,and applying the
-- instance decl would show up two uses of ?x.
-check_source_ty dflags TypeCtxt (NType tc tys) = mapTc_ check_arg_type tys
+check_source_ty dflags TypeCtxt (NType tc tys) = mappM_ check_arg_type tys
-- Catch-all
check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
-------------------------
+check_class_pred_tys dflags ctxt tys
+ = case ctxt of
+ InstHeadCtxt -> True -- We check for instance-head
+ -- formation in checkValidInstHead
+ InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
+ other -> gla_exts || all tyvar_head tys
+ where
+ undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
+ gla_exts = dopt Opt_GlasgowExts dflags
+
+-------------------------
tyvar_head ty -- Haskell 98 allows predicates of form
| tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
| otherwise -- where a is a type variable
Nothing -> False
\end{code}
+Check for ambiguity
+~~~~~~~~~~~~~~~~~~~
+ forall V. P => tau
+is ambiguous if P contains generic variables
+(i.e. one of the Vs) that are not mentioned in tau
+
+However, we need to take account of functional dependencies
+when we speak of 'mentioned in tau'. Example:
+ class C a b | a -> b where ...
+Then the type
+ forall x y. (C x y) => x
+is not ambiguous because x is mentioned and x determines y
+
+NB; the ambiguity check is only used for *user* types, not for types
+coming from inteface files. The latter can legitimately have
+ambiguous types. Example
+
+ class S a where s :: a -> (Int,Int)
+ instance S Char where s _ = (1,1)
+ f:: S a => [a] -> Int -> (Int,Int)
+ f (_::[a]) x = (a*x,b)
+ where (a,b) = s (undefined::a)
+
+Here the worker for f gets the type
+ fw :: forall a. S a => Int -> (# Int, Int #)
+
+If the list of tv_names is empty, we have a monotype, and then we
+don't need to check for ambiguity either, because the test can't fail
+(see is_ambig).
+
\begin{code}
-badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
-predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
-dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
+checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
+checkAmbiguity forall_tyvars theta tau_tyvars
+ = mappM_ complain (filter is_ambig theta)
+ where
+ complain pred = addErrTc (ambigErr pred)
+ extended_tau_vars = grow theta tau_tyvars
+
+ -- Only a *class* predicate can give rise to ambiguity
+ -- An *implicit parameter* cannot. For example:
+ -- foo :: (?x :: [a]) => Int
+ -- foo = length ?x
+ -- is fine. The call site will suppply a particular 'x'
+ is_ambig pred = isClassPred pred &&
+ any ambig_var (varSetElems (tyVarsOfPred pred))
+
+ ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
+ not (ct_var `elemVarSet` extended_tau_vars)
+
+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 '=>'"))]
+\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.
+\begin{code}
+checkFreeness forall_tyvars theta
+ = 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"),
+ nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
+ ]
+\end{code}
+
+\begin{code}
checkThetaCtxt ctxt theta
= vcat [ptext SLIT("In the context:") <+> pprTheta theta,
ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
+
+badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
+predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
+dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
+
+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]
+ where
+ n_arguments | n == 0 = ptext SLIT("no arguments")
+ | n == 1 = ptext SLIT("1 argument")
+ | True = hsep [int n, ptext SLIT("arguments")]
\end{code}
| isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
| otherwise
= -- Check the context on the data decl
- checkValidTheta (DataTyCtxt name) (tyConTheta tc) `thenTc_`
+ checkValidTheta (DataTyCtxt name) (tyConTheta tc) `thenM_`
-- Check arg types of data constructors
- mapTc_ checkValidDataCon data_cons `thenTc_`
+ mappM_ checkValidDataCon data_cons `thenM_`
-- Check that fields with the same name share a type
- mapTc_ check_fields groups
+ mappM_ check_fields groups
where
name = tyConName tc
checkValidDataCon :: DataCon -> TcM ()
checkValidDataCon con
- = checkValidType ctxt (idType (dataConWrapId con)) `thenTc_`
+ = checkValidType ctxt (idType (dataConWrapId con)) `thenM_`
-- This checks the argument types and
-- ambiguity of the existential context (if any)
- tcAddErrCtxt (existentialCtxt con)
- (checkFreeness ex_tvs ex_theta)
+ addErrCtxt (existentialCtxt con)
+ (checkFreeness ex_tvs ex_theta)
where
ctxt = ConArgCtxt (dataConName con)
(_, _, ex_tvs, ex_theta, _, _) = dataConSig con
checkValidClass :: Class -> TcM ()
checkValidClass cls
= -- CHECK ARITY 1 FOR HASKELL 1.4
- doptsTc Opt_GlasgowExts `thenTc` \ gla_exts ->
+ doptM Opt_GlasgowExts `thenM` \ gla_exts ->
-- Check that the class is unary, unless GlaExs
- checkTc (notNull tyvars) (nullaryClassErr cls) `thenTc_`
- checkTc (gla_exts || unary) (classArityErr cls) `thenTc_`
+ checkTc (notNull tyvars) (nullaryClassErr cls) `thenM_`
+ checkTc (gla_exts || unary) (classArityErr cls) `thenM_`
-- Check the super-classes
- checkValidTheta (ClassSCCtxt (className cls)) theta `thenTc_`
+ checkValidTheta (ClassSCCtxt (className cls)) theta `thenM_`
-- Check the class operations
- mapTc_ check_op op_stuff `thenTc_`
+ mappM_ check_op op_stuff `thenM_`
-- Check that if the class has generic methods, then the
-- class has only one parameter. We can't do generic
no_generics = null [() | (_, GenDefMeth) <- op_stuff]
check_op (sel_id, dm)
- = checkValidTheta SigmaCtxt (tail theta) `thenTc_`
+ = checkValidTheta SigmaCtxt (tail theta) `thenM_`
-- The 'tail' removes the initial (C a) from the
-- class itself, leaving just the method type
- checkValidType (FunSigCtxt op_name) tau `thenTc_`
+ checkValidType (FunSigCtxt op_name) tau `thenM_`
-- Check that for a generic method, the type of
-- the method is sufficiently simple
Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
Just (clas,tys) ->
- getDOptsTc `thenNF_Tc` \ dflags ->
- mapTc_ check_arg_type tys `thenTc_`
- check_inst_head dflags clas tys `thenTc_`
- returnTc (clas, tys)
+ getDOpts `thenM` \ dflags ->
+ mappM_ check_arg_type tys `thenM_`
+ check_inst_head dflags clas tys `thenM_`
+ returnM (clas, tys)
}}
check_inst_head dflags clas tys
all tcIsTyVarTy arg_tys, -- Applied to type variables
equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
-- This last condition checks that all the type variables are distinct
- = returnTc ()
+ = returnM ()
| otherwise
= failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
check_tyvars dflags clas tys
-- Check that at least one isn't a type variable
-- unless -fallow-undecideable-instances
- | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
- | not (all tcIsTyVarTy tys) = returnTc ()
+ | dopt Opt_AllowUndecidableInstances dflags = returnM ()
+ | not (all tcIsTyVarTy tys) = returnM ()
| otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
where
msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")