--------------------------------
-- Creating new mutable type variables
- newTyVar,
- newTyVarTy, -- Kind -> NF_TcM TcType
- newTyVarTys, -- Int -> Kind -> NF_TcM [TcType]
- newKindVar, newKindVars, newBoxityVar,
- putTcTyVar, getTcTyVar,
+ newFlexiTyVar,
+ newFlexiTyVarTy, -- Kind -> TcM TcType
+ newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
+ newKindVar, newKindVars,
+ lookupTcTyVar, LookupTyVarResult(..),
+ newMetaTyVar, readMetaTyVar, writeMetaTyVar,
- newHoleTyVarTy, readHoleResult, zapToType,
+ --------------------------------
+ -- Boxy type variables
+ newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
--------------------------------
-- Instantiation
- tcInstTyVar, tcInstTyVars, tcInstType,
+ tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar,
+ tcInstSigTyVars, zonkSigTyVar,
+ tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
+ tcSkolSigType, tcSkolSigTyVars,
--------------------------------
-- Checking type validity
- Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
- SourceTyCtxt(..), checkValidTheta,
- checkValidTyCon, checkValidClass,
+ Rank, UserTypeCtxt(..), checkValidType,
+ SourceTyCtxt(..), checkValidTheta, checkFreeness,
checkValidInstHead, instTypeErr, checkAmbiguity,
+ checkInstTermination,
+ arityErr,
--------------------------------
-- Zonking
- zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
+ zonkType, zonkTcPredType,
+ zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
- zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
+ zonkTcKindToKind, zonkTcKind,
+
+ readKindVar, writeKindVar
) where
-- friends:
-import TypeRep ( Type(..), SourceType(..), TyNote(..), -- Friend; can see representation
- Kind, ThetaType
+import TypeRep ( Type(..), PredType(..), -- Friend; can see representation
+ ThetaType
)
import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
- TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
- tcEqType, tcCmpPred,
+ TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..),
+ MetaDetails(..), SkolemInfo(..), BoxInfo(..),
+ BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType,
+ UserTypeCtxt(..),
+ isMetaTyVar, isSigTyVar, metaTvRef,
+ tcCmpPred, isClassPred, tcGetTyVar,
tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
- tcSplitTyConApp_maybe, tcSplitForAllTys,
+ tcValidInstHeadTy, tcSplitForAllTys,
tcIsTyVarTy, tcSplitSigmaTy,
- isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy,
-
+ isUnLiftedType, isIPPred,
+ typeKind, isSkolemTyVar,
mkAppTy, mkTyVarTy, mkTyVarTys,
tyVarsOfPred, getClassPredTys_maybe,
-
- liftedTypeKind, openTypeKind, defaultKind, superKind,
- superBoxity, liftedBoxity, typeKind,
- tyVarsOfType, tyVarsOfTypes,
- eqKind, isTypeKind, isAnyTypeKind,
-
- isFFIArgumentTy, isFFIImportResultTy
+ tyVarsOfType, tyVarsOfTypes, tcView,
+ pprPred, pprTheta, pprClassPred )
+import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar,
+ isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
+ liftedTypeKind, defaultKind
)
-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,
- 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 Type ( TvSubst, zipTopTvSubst, substTy )
+import Class ( Class, classArity, className )
+import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
+ tyConArity, tyConName )
+import Var ( TyVar, tyVarKind, tyVarName, isTcTyVar,
+ mkTyVar, mkTcTyVar, tcTyVarDetails )
+
+ -- Assertions
+#ifdef DEBUG
+import TcType ( isFlexi, isBoxyTyVar, isImmutableTyVar )
+import Kind ( isSubKind )
+#endif
-- others:
-import Generics ( validGenericMethodType )
-import TcMonad -- TcType, amongst others
-import TysWiredIn ( voidTy, listTyCon, tupleTyCon )
-import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
-import ForeignCall ( Safety(..) )
+import TcRnMonad -- TcType, amongst others
import FunDeps ( grow )
-import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
-import Name ( Name, NamedThing(..), setNameUnique,
- mkInternalName, mkDerivedTyConOcc,
- mkSystemTvNameEncoded,
- )
+import Name ( Name, setNameUnique, mkSysTvName )
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 DynFlags ( dopt, DynFlag(..) )
+import Util ( nOfThem, isSingleton, notNull )
+import ListSetOps ( removeDups )
import Outputable
+
+import Data.List ( (\\) )
\end{code}
%************************************************************************
%* *
-\subsection{New type variables}
+ Instantiation in general
%* *
%************************************************************************
\begin{code}
-newTyVar :: Kind -> NF_TcM TcTyVar
-newTyVar kind
- = tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("t")) kind VanillaTv
-
-newTyVarTy :: Kind -> NF_TcM TcType
-newTyVarTy kind
- = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
- returnNF_Tc (TyVarTy tc_tyvar)
-
-newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
-newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
-
-newKindVar :: NF_TcM TcKind
-newKindVar
- = tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutTyVar (mkSystemTvNameEncoded 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 (mkSystemTvNameEncoded uniq FSLIT("bx")) superBoxity VanillaTv `thenNF_Tc` \ kv ->
- returnNF_Tc (TyVarTy kv)
+tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
+ -> TcType -- Type to instantiate
+ -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
+tcInstType inst_tyvars ty
+ = case tcSplitForAllTys ty of
+ ([], rho) -> let -- There may be overloading despite no type variables;
+ -- (?x :: Int) => Int -> Int
+ (theta, tau) = tcSplitPhiTy rho
+ in
+ return ([], theta, tau)
+
+ (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
+
+ ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
+ -- Either the tyvars are freshly made, by inst_tyvars,
+ -- or (in the call from tcSkolSigType) any nested foralls
+ -- have different binders. Either way, zipTopTvSubst is ok
+
+ ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
+ ; return (tyvars', theta, tau) }
\end{code}
%************************************************************************
%* *
-\subsection{'hole' type variables}
+ Kind variables
%* *
%************************************************************************
\begin{code}
-newHoleTyVarTy :: NF_TcM TcType
- = tcGetUnique `thenNF_Tc` \ uniq ->
- tcNewMutTyVar (mkSystemTvNameEncoded uniq FSLIT("h")) openTypeKind HoleTv `thenNF_Tc` \ tv ->
- returnNF_Tc (TyVarTy tv)
-
-readHoleResult :: TcType -> NF_TcM TcType
--- Read the answer out of a hole, constructed by newHoleTyVarTy
-readHoleResult (TyVarTy tv)
- = ASSERT( isHoleTyVar tv )
- getTcTyVar tv `thenNF_Tc` \ maybe_res ->
- case maybe_res of
- Just ty -> returnNF_Tc ty
- Nothing -> pprPanic "readHoleResult: empty" (ppr tv)
-readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
-
-zapToType :: TcType -> NF_TcM TcType
-zapToType (TyVarTy tv)
- | isHoleTyVar tv
- = getTcTyVar tv `thenNF_Tc` \ 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
- -- have chains of holes
-
-zapToType other_ty = returnNF_Tc other_ty
-\end{code}
+newKindVar :: TcM TcKind
+newKindVar = do { uniq <- newUnique
+ ; ref <- newMutVar Nothing
+ ; return (KindVar (mkKindVar uniq ref)) }
+
+newKindVars :: Int -> TcM [TcKind]
+newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
+\end{code}
+
%************************************************************************
%* *
-\subsection{Type instantiation}
+ SkolemTvs (immutable)
%* *
%************************************************************************
-Instantiating a bunch of type variables
+\begin{code}
+mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
+mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
+
+tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type signature with skolem constants, but
+-- do *not* give them fresh names, because we want the name to
+-- be in the type environment -- it is lexically scoped.
+tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
+
+tcSkolSigTyVars :: SkolemInfo -> [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 ]
+
+tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh skolem constants
+tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
+
+tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
+tcInstSkolTyVar info tyvar
+ = do { uniq <- newUnique
+ ; let name = setNameUnique (tyVarName tyvar) uniq
+ kind = tyVarKind tyvar
+ ; return (mkSkolTyVar name kind info) }
+
+tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
+tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
+\end{code}
+
+
+%************************************************************************
+%* *
+ MetaTvs (meta type variables; mutable)
+%* *
+%************************************************************************
\begin{code}
-tcInstTyVars :: TyVarDetails -> [TyVar]
- -> NF_TcM ([TcTyVar], [TcType], Subst)
+newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
+-- Make a new meta tyvar out of thin air
+newMetaTyVar box_info kind
+ = do { uniq <- newUnique
+ ; ref <- newMutVar Flexi ;
+ ; let name = mkSysTvName uniq fs
+ fs = case box_info of
+ BoxTv -> FSLIT("bx")
+ TauTv -> FSLIT("t")
+ SigTv _ -> FSLIT("a")
+ ; 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)) }
+
+readMetaTyVar :: TyVar -> TcM MetaDetails
+readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
+ readMutVar (metaTvRef tyvar)
+
+writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
+#ifndef DEBUG
+writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
+#else
+writeMetaTyVar tyvar ty
+ | not (isMetaTyVar tyvar)
+ = pprTrace "writeMetaTyVar" (ppr tyvar) $
+ returnM ()
-tcInstTyVars tv_details tyvars
- = mapNF_Tc (tcInstTyVar tv_details) tyvars `thenNF_Tc` \ tc_tyvars ->
- let
- tys = mkTyVarTys tc_tyvars
- in
- returnNF_Tc (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 ->
- let
- name = setNameUnique (tyVarName tyvar) uniq
- -- Note that we don't change the print-name
- -- This won't confuse the type checker but there's a chance
- -- that two different tyvars will print the same way
- -- in an error message. -dppr-debug will show up the difference
- -- Better watch out for this. If worst comes to worst, just
- -- use mkSystemName.
- in
- tcNewMutTyVar name (tyVarKind tyvar) tv_details
+ | otherwise
+ = ASSERT( isMetaTyVar tyvar )
+ 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) }
+ where
+ k1 = tyVarKind tyvar
+ k2 = typeKind ty
+#endif
+\end{code}
-tcInstType :: TyVarDetails -> TcType -> NF_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.
-tcInstType tv_details ty
- = case tcSplitForAllTys ty of
- ([], rho) -> -- There may be overloading despite no type variables;
- -- (?x :: Int) => Int -> Int
- let
- (theta, tau) = tcSplitPhiTy rho
- in
- returnNF_Tc ([], theta, tau)
- (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
- let
- (theta, tau) = tcSplitPhiTy (substTy tenv rho)
- in
- returnNF_Tc (tyvars', theta, tau)
+%************************************************************************
+%* *
+ MetaTvs: TauTvs
+%* *
+%************************************************************************
+
+\begin{code}
+newFlexiTyVar :: Kind -> TcM TcTyVar
+newFlexiTyVar kind = newMetaTyVar TauTv kind
+
+newFlexiTyVarTy :: Kind -> TcM TcType
+newFlexiTyVarTy kind
+ = newFlexiTyVar kind `thenM` \ tc_tyvar ->
+ returnM (TyVarTy tc_tyvar)
+
+newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
+newFlexiTyVarTys n kind = mappM 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
+ = do { tc_tvs <- mapM tcInstTyVar tyvars
+ ; let tys = mkTyVarTys tc_tvs
+ ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
+ -- Since the tyvars are freshly made,
+ -- they cannot possibly be captured by
+ -- any existing for-alls. Hence zipTopTvSubst
\end{code}
%************************************************************************
%* *
-\subsection{Putting and getting mutable type variables}
+ MetaTvs: SigTvs
%* *
%************************************************************************
\begin{code}
-putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
-getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
+tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
+-- Instantiate with meta SigTvs
+tcInstSigTyVars skol_info tyvars
+ = mapM (instMetaTyVar (SigTv skol_info)) tyvars
+
+zonkSigTyVar :: TcTyVar -> TcM TcTyVar
+zonkSigTyVar sig_tv
+ | isSkolemTyVar sig_tv
+ = return sig_tv -- Happens in the call in TcBinds.checkDistinctTyVars
+ | otherwise
+ = ASSERT( isSigTyVar sig_tv )
+ do { ty <- zonkTcTyVar sig_tv
+ ; return (tcGetTyVar "zonkSigTyVar" ty) }
+ -- 'ty' is bound to be a type variable, because SigTvs
+ -- can only be unified with type variables
\end{code}
-Putting is easy:
+
+%************************************************************************
+%* *
+ MetaTvs: BoxTvs
+%* *
+%************************************************************************
\begin{code}
-putTcTyVar tyvar ty
- | not (isMutTyVar tyvar)
- = pprTrace "putTcTyVar" (ppr tyvar) $
- returnNF_Tc ty
+newBoxyTyVar :: Kind -> TcM BoxyTyVar
+newBoxyTyVar kind = newMetaTyVar BoxTv kind
- | otherwise
- = ASSERT( isMutTyVar tyvar )
- tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
- returnNF_Tc ty
+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
+
+tcInstBoxy :: TcType -> TcM ([BoxyTyVar], BoxyThetaType, BoxySigmaType)
+-- tcInstType instantiates the outer-level for-alls of a TcType with
+-- fresh BOXY type variables, splits off the dictionary part,
+-- and returns the pieces.
+tcInstBoxy ty = tcInstType (mapM tcInstBoxyTyVar) ty
\end{code}
-Getting is more interesting. The easy thing to do is just to read, thus:
-\begin{verbatim}
-getTcTyVar tyvar = tcReadMutTyVar tyvar
-\end{verbatim}
+%************************************************************************
+%* *
+\subsection{Putting and getting mutable type variables}
+%* *
+%************************************************************************
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
We return Nothing iff the original box was unbound.
\begin{code}
+data LookupTyVarResult -- The result of a lookupTcTyVar call
+ = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
+ | IndirectTv TcType
+
+lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
+lookupTcTyVar 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 (isMutTyVar tyvar)
+ | not (isTcTyVar 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 ->
+ = ASSERT2( isTcTyVar tyvar, ppr tyvar )
+ readMetaTyVar 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' ->
+ writeMetaTyVar 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
+ | not (isTcTyVar tyvar)
+ = returnM ty
| otherwise
- = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
+ = readMetaTyVar 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' ->
+ writeMetaTyVar 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 = ASSERT( isTcTyVar tyvar )
+ zonk_tc_tyvar (\ 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 pairs
- = mapNF_Tc zonk_it pairs
- where
- zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
- returnNF_Tc (name, kind)
-
- -- When zonking a kind, we want to
- -- zonk a *kind* variable to (Type *)
- -- zonk a *boxity* variable to *
- zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
- | 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 $$ ppr kind) $
- 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.
---
--- It does this by making an immutable version of tv and binds tv to it.
--- Now any bound occurences of the original type variable will get
--- zonked to the immutable version.
-
-zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
-zonkTcTyVarToTyVar tv
- = let
- -- Make an immutable version, defaulting
- -- the kind to lifted if necessary
- immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
- immut_tv_ty = mkTyVarTy immut_tv
-
- zap tv = putTcTyVar tv immut_tv_ty
- -- Bind the mutable version to the immutable one
- 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 ->
-
- -- 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
+zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
+-- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
+-- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
+-- When we do this, we also default the kind -- see notes with Kind.defaultKind
+-- The meta tyvar is updated to point to the new regular TyVar. Now any
+-- bound occurences of the original type variable will get zonked to
+-- the immutable version.
+--
+-- We leave skolem TyVars alone; they are immutable.
+zonkQuantifiedTyVar tv
+ | isSkolemTyVar tv = return tv
+ -- 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, regular type variable
+ ; let final_kind = defaultKind (tyVarKind tv)
+ final_tv = mkTyVar (tyVarName tv) final_kind
+
+ -- 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
+ ; return final_tv }
\end{code}
[Silly Type Synonyms]
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)
+ because it does not 'really' mention a. (see exactTyVarsOfType)
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 = ()
+ [Note Sept 04: now that we are zonking quantified type variables
+ on construction, the 'a' will be frozen as a regular tyvar on
+ 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.
-All very silly. I think its harmless to ignore the problem.
+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 ()
%************************************************************************
%************************************************************************
\begin{code}
--- zonkType is used for Kinds as well
-
-- For unbound, mutable tyvars, zonkType uses the function given to it
-- 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
+ -> TcType
+ -> 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 (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
- go ty2 `thenNF_Tc` \ ty2' ->
- returnNF_Tc (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 (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
- go res `thenNF_Tc` \ res' ->
- returnNF_Tc (FunTy arg' res')
-
- go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
- go arg `thenNF_Tc` \ arg' ->
- returnNF_Tc (mkAppTy fun' arg')
+ go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
+
+ go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
+ returnM (TyConApp tc tys')
+
+ go (PredTy p) = go_pred p `thenM` \ p' ->
+ returnM (PredTy p')
+
+ go (FunTy arg res) = go arg `thenM` \ arg' ->
+ go res `thenM` \ res' ->
+ returnM (FunTy arg' res')
+
+ go (AppTy fun arg) = go fun `thenM` \ fun' ->
+ go arg `thenM` \ arg' ->
+ returnM (mkAppTy fun' arg')
-- 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_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')
-
-zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
- -> TcTyVar -> NF_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)
-
- | otherwise
- = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
- case maybe_ty of
- Nothing -> unbound_var_fn tyvar -- Mutable and unbound
- Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
+ go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
+ | otherwise = return (TyVarTy tyvar)
+ -- Ordinary (non Tc) tyvars occur inside quantified types
+
+ go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
+ go ty `thenM` \ ty' ->
+ returnM (ForAllTy tyvar ty')
+
+ go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
+ returnM (ClassP c tys')
+ go_pred (IParam n ty) = go ty `thenM` \ ty' ->
+ returnM (IParam n ty')
+
+zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
+ -> TcTyVar -> TcM TcType
+zonk_tc_tyvar unbound_var_fn tyvar
+ | not (isMetaTyVar tyvar) -- Skolems
+ = returnM (TyVarTy tyvar)
+
+ | 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 }
\end{code}
%************************************************************************
%* *
+ Zonking kinds
+%* *
+%************************************************************************
+
+\begin{code}
+readKindVar :: KindVar -> TcM (Maybe TcKind)
+writeKindVar :: KindVar -> TcKind -> TcM ()
+readKindVar kv = readMutVar (kindVarRef kv)
+writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
+
+-------------
+zonkTcKind :: TcKind -> TcM TcKind
+zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
+ ; k2' <- zonkTcKind k2
+ ; returnM (FunKind k1' k2') }
+zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv
+ ; case mb_kind of
+ Nothing -> returnM k
+ Just k -> zonkTcKind k }
+zonkTcKind other_kind = returnM other_kind
+
+-------------
+zonkTcKindToKind :: TcKind -> TcM Kind
+zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
+ ; k2' <- zonkTcKindToKind k2
+ ; returnM (FunKind k1' k2') }
+
+zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv
+ ; case mb_kind of
+ Nothing -> return liftedTypeKind
+ Just k -> zonkTcKindToKind k }
+
+zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
+zonkTcKindToKind other_kind = returnM other_kind
+\end{code}
+
+%************************************************************************
+%* *
\subsection{Checking a user type}
%* *
%************************************************************************
\begin{code}
-data UserTypeCtxt
- = FunSigCtxt Name -- Function type signature
- | ExprSigCtxt -- Expression type signature
- | ConArgCtxt Name -- Data constructor argument
- | TySynCtxt Name -- RHS of a type synonym decl
- | GenPatCtxt -- Pattern in generic decl
- -- f{| a+b |} (Inl x) = ...
- | PatSigCtxt -- Type sig in pattern
- -- f (x::t) = ...
- | ResSigCtxt -- Result type sig
- -- f x :: t = ....
- | ForSigCtxt Name -- Foreign inport or export signature
- | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
-
--- Notes re TySynCtxt
--- We allow type synonyms that aren't types; e.g. type List = []
---
--- If the RHS mentions tyvars that aren't in scope, we'll
--- quantify over them:
--- e.g. type T = a->a
--- will become type T = forall a. a->a
---
--- With gla-exts that's right, but for H98 we should complain.
-
-
-pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
-pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
-pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
-pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
-pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
-pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
-pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
-pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
-pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
-\end{code}
-
-\begin{code}
checkValidType :: UserTypeCtxt -> Type -> TcM ()
-- Checks that the type is valid for the given context
checkValidType ctxt ty
- = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
+ = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
+ doptM Opt_GlasgowExts `thenM` \ gla_exts ->
let
rank | gla_exts = Arbitrary
| otherwise
= case ctxt of -- Haskell 98
GenPatCtxt -> Rank 0
- PatSigCtxt -> Rank 0
+ LamPatSigCtxt -> Rank 0
+ BindPatSigCtxt -> Rank 0
+ DefaultDeclCtxt-> Rank 0
ResSigCtxt -> Rank 0
TySynCtxt _ -> Rank 0
ExprSigCtxt -> Rank 1
-- constructor, hence rank 1
ForSigCtxt _ -> Rank 1
RuleSigCtxt _ -> Rank 1
+ SpecInstCtxt -> Rank 1
actual_kind = typeKind ty
- actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
-
kind_ok = case ctxt of
TySynCtxt _ -> True -- Any kind will do
- GenPatCtxt -> actual_kind_is_lifted
- ForSigCtxt _ -> actual_kind_is_lifted
- other -> isTypeKind actual_kind
+ ResSigCtxt -> isOpenTypeKind actual_kind
+ ExprSigCtxt -> isOpenTypeKind actual_kind
+ GenPatCtxt -> isLiftedTypeKind actual_kind
+ ForSigCtxt _ -> isLiftedTypeKind actual_kind
+ other -> isArgTypeKind actual_kind
ubx_tup | not gla_exts = UT_NotOk
| otherwise = case ctxt of
TySynCtxt _ -> UT_Ok
+ ExprSigCtxt -> UT_Ok
other -> UT_NotOk
-- Unboxed tuples ok in function results,
-- but for type synonyms we allow them even at
-- top level
in
- tcAddErrCtxt (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
-
-
-checkTypeCtxt ctxt ty
- = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
- ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
-
- -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
- -- something strange like {Eq k} -> k -> k, because there is no
- -- ForAll at the top of the type. Since this is going to the user
- -- we want it to look like a proper Haskell type even then; hence the hack
- --
- -- This shows up in the complaint about
- -- case C a where
- -- op :: Eq a => a -> a
-ppr_ty ty | null forall_tvs && notNull theta = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
- | otherwise = ppr ty
- where
- (forall_tvs, theta, tau) = tcSplitSigmaTy ty
+ check_poly_type rank ubx_tup ty `thenM_`
+
+ traceTc (text "checkValidType done" <+> ppr ty)
\end{code}
= 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)
----------------------------------------
check_arg_type :: Type -> TcM ()
-- The sort of type that can instantiate a type variable,
-- or be the argument of a type constructor.
--- Not an unboxed tuple, not a forall.
+-- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
-- Other unboxed types are very occasionally allowed as type
-- arguments depending on the kind of the type constructor
--
-- 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_poly_type Arbitrary UT_NotOk ty `thenM_`
checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
----------------------------------------
-- Rank is allowed rank for function args
-- No foralls otherwise
-check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
-check_tau_type rank ubx_tup (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
- check_source_ty dflags TypeCtxt sty
-check_tau_type rank ubx_tup (TyVarTy _) = returnTc ()
+check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
+check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
+ -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
+
+-- Naked PredTys don't usually show up, but they can as a result of
+-- {-# SPECIALISE instance Ord Char #-}
+-- The Right Thing would be to fix the way that SPECIALISE instance pragmas
+-- are handled, but the quick thing is just to permit PredTys here.
+check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
+ check_source_ty dflags TypeCtxt sty
+
+check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
- = check_poly_type rank UT_NotOk arg_ty `thenTc_`
- check_tau_type rank UT_Ok res_ty
+ = check_poly_type rank UT_NotOk arg_ty `thenM_`
+ check_poly_type rank UT_Ok res_ty
check_tau_type rank ubx_tup (AppTy ty1 ty2)
- = check_arg_type ty1 `thenTc_` check_arg_type ty2
-
-check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
- -- Synonym notes are built only when the synonym is
- -- saturated (see Type.mkSynTy)
- = doptsTc Opt_GlasgowExts `thenNF_Tc` \ 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
+ = check_arg_type ty1 `thenM_` check_arg_type ty2
+
+check_tau_type rank ubx_tup (NoteTy other_note ty)
+ = check_tau_type rank ubx_tup ty
+
+check_tau_type rank ubx_tup ty@(TyConApp tc tys)
+ | isSynTyCon tc
+ = do { -- It's OK to have an *over-applied* type synonym
+ -- data Tree a b = ...
+ -- type Foo a = Tree [a]
+ -- f :: Foo a b -> ...
+ ; case tcView ty of
+ Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
+ Nothing -> failWithTc arity_msg
+
+ ; gla_exts <- doptM Opt_GlasgowExts
+ ; if gla_exts then
+ -- If -fglasgow-exts then don't check the type arguments
+ -- 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 ()
-- But if you expand S first, then T we get just
-- f :: Int
-- which is fine.
- returnTc ()
- else
- -- For H98, do check the un-expanded part
- check_tau_type rank ubx_tup syn
- ) `thenTc_`
-
- 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)
- -- to find the error
- checkTc syn_arity_ok arity_msg `thenTc_`
- mapTc_ check_arg_type tys
+ returnM ()
+ else
+ -- For H98, do check the type args
+ 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
- -- Args are allowed to be unlifted, or
- -- more unboxed tuples, so can't use check_arg_ty
+ = 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 }
- syn_arity_ok = tc_arity <= n_args
- -- It's OK to have an *over-applied* type synonym
- -- data Tree a b = ...
- -- type Foo a = Tree [a]
- -- f :: Foo a b -> ...
n_args = length tys
tc_arity = tyConArity tc
ubx_tup_msg = ubxArgTyErr ty
----------------------------------------
-forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
-unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
-ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
+forAllTyErr ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
+unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
+ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
\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}
+-- Enumerate the contexts in which a "source type", <S>, can occur
+-- Eq a
+-- or ?x::Int
+-- or r <: {x::Int}
+-- or (N a) where N is a newtype
+
data SourceTyCtxt
= ClassSCCtxt Name -- Superclasses of clas
- | SigmaCtxt -- Context of a normal for-all type
- | DataTyCtxt Name -- Context of a data decl
+ -- class <S> => C a where ...
+ | SigmaCtxt -- Theta part of a normal for-all type
+ -- f :: <S> => a -> a
+ | DataTyCtxt Name -- Theta part of a data decl
+ -- data <S> => T a = MkT a
| TypeCtxt -- Source type in an ordinary type
+ -- f :: N a -> N a
| InstThetaCtxt -- Context of an instance decl
- | InstHeadCtxt -- Head of an instance decl
+ -- instance <S> => C [a] where ...
pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
-pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
\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_`
+ 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 (arity == n_tys) arity_err `thenM_`
+
+ -- Check the form of the argument types
+ mappM_ check_arg_type tys `thenM_`
checkTc (check_class_pred_tys dflags ctxt tys)
(predTyVarErr pred $$ how_to_allow)
-- 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
-
-- Catch-all
check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
-------------------------
check_class_pred_tys dflags ctxt tys
= case ctxt of
+ TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
InstHeadCtxt -> True -- We check for instance-head
-- formation in checkValidInstHead
- InstThetaCtxt -> undecidable_ok || all isTyVarTy tys
+ InstThetaCtxt -> undecidable_ok || distinct_tyvars tys
other -> gla_exts || all tyvar_head tys
where
- undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
gla_exts = dopt Opt_GlasgowExts dflags
-------------------------
Nothing -> False
\end{code}
-\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)
-
-checkThetaCtxt ctxt theta
- = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
- ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
-\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
-%************************************************************************
-%* *
-\subsection{Validity check for TyCons}
-%* *
-%************************************************************************
+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
-checkValidTyCon is called once the mutually-recursive knot has been
-tied, so we can look at things freely.
+ 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)
-\begin{code}
-checkValidTyCon :: TyCon -> TcM ()
-checkValidTyCon tc
- | isSynTyCon tc = checkValidType (TySynCtxt name) syn_rhs
- | otherwise
- = -- Check the context on the data decl
- checkValidTheta (DataTyCtxt name) (tyConTheta tc) `thenTc_`
-
- -- Check arg types of data constructors
- mapTc_ checkValidDataCon data_cons `thenTc_`
+Here the worker for f gets the type
+ fw :: forall a. S a => Int -> (# Int, Int #)
- -- Check that fields with the same name share a type
- mapTc_ check_fields groups
+If the list of tv_names is empty, we have a monotype, and then we
+don't need to check for ambiguity either, because the test can't fail
+(see is_ambig).
+\begin{code}
+checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
+checkAmbiguity forall_tyvars theta tau_tyvars
+ = mappM_ complain (filter is_ambig theta)
where
- name = tyConName tc
- (_, syn_rhs) = getSynTyConDefn tc
- data_cons = tyConDataCons tc
-
- fields = [field | con <- data_cons, field <- dataConFieldLabels con]
- groups = equivClasses cmp_name fields
- cmp_name field1 field2 = fieldLabelName field1 `compare` fieldLabelName field2
-
- check_fields fields@(first_field_label : other_fields)
- -- These fields all have the same name, but are from
- -- different constructors in the data type
- = -- Check that all the fields in the group have the same type
- -- NB: this check assumes that all the constructors of a given
- -- data type use the same type variables
- checkTc (all (tcEqType field_ty) other_tys) (fieldTypeMisMatch field_name)
- where
- field_ty = fieldLabelType first_field_label
- field_name = fieldLabelName first_field_label
- other_tys = map fieldLabelType other_fields
-
-checkValidDataCon :: DataCon -> TcM ()
-checkValidDataCon con
- = checkValidType ctxt (idType (dataConWrapId con)) `thenTc_`
- -- This checks the argument types and
- -- ambiguity of the existential context (if any)
- tcAddErrCtxt (existentialCtxt con)
- (checkFreeness ex_tvs ex_theta)
- where
- ctxt = ConArgCtxt (dataConName con)
- (_, _, ex_tvs, ex_theta, _, _) = dataConSig con
+ 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))
-fieldTypeMisMatch field_name
- = sep [ptext SLIT("Different constructors give different types for field"), quotes (ppr field_name)]
+ ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
+ not (ct_var `elemVarSet` extended_tau_vars)
-existentialCtxt con = ptext SLIT("When checking the existential context of constructor")
- <+> quotes (ppr con)
+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}
-
-
-checkValidClass is called once the mutually-recursive knot has been
-tied, so we can look at things freely.
+
+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}
-checkValidClass :: Class -> TcM ()
-checkValidClass cls
- = -- CHECK ARITY 1 FOR HASKELL 1.4
- doptsTc Opt_GlasgowExts `thenTc` \ gla_exts ->
-
- -- Check that the class is unary, unless GlaExs
- checkTc (notNull tyvars) (nullaryClassErr cls) `thenTc_`
- checkTc (gla_exts || unary) (classArityErr cls) `thenTc_`
+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)
- -- Check the super-classes
- checkValidTheta (ClassSCCtxt (className cls)) theta `thenTc_`
+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}
- -- Check the class operations
- mapTc_ check_op op_stuff `thenTc_`
+\begin{code}
+checkThetaCtxt ctxt theta
+ = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
+ ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
- -- Check that if the class has generic methods, then the
- -- class has only one parameter. We can't do generic
- -- multi-parameter type classes!
- checkTc (unary || no_generics) (genericMultiParamErr cls)
+badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
+predTyVarErr pred = sep [ptext SLIT("Non-type variable argument"),
+ nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
+dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
- where
- (tyvars, theta, _, op_stuff) = classBigSig cls
- unary = isSingleton tyvars
- no_generics = null [() | (_, GenDefMeth) <- op_stuff]
-
- check_op (sel_id, dm)
- = checkValidTheta SigmaCtxt (tail theta) `thenTc_`
- -- The 'tail' removes the initial (C a) from the
- -- class itself, leaving just the method type
-
- checkValidType (FunSigCtxt op_name) tau `thenTc_`
-
- -- Check that for a generic method, the type of
- -- the method is sufficiently simple
- checkTc (dm /= GenDefMeth || validGenericMethodType op_ty)
- (badGenericMethodType op_name op_ty)
- where
- op_name = idName sel_id
- op_ty = idType sel_id
- (_,theta,tau) = tcSplitSigmaTy op_ty
-
-nullaryClassErr cls
- = ptext SLIT("No parameters for class") <+> quotes (ppr cls)
-
-classArityErr cls
- = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
- parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
-
-genericMultiParamErr clas
- = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
- ptext SLIT("cannot have generic methods")
-
-badGenericMethodType op op_ty
- = hang (ptext SLIT("Generic method type is too complex"))
- 4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
- ptext SLIT("You can only use type variables, arrows, and tuples")])
+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}
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
- | -- CCALL CHECK
- -- A user declaration of a CCallable/CReturnable instance
- -- must be for a "boxed primitive" type.
- (clas `hasKey` cCallableClassKey
- && not (ccallable_type first_ty))
- || (clas `hasKey` cReturnableClassKey
- && not (creturnable_type first_ty))
- = failWithTc (nonBoxedPrimCCallErr clas first_ty)
-
-- If GlasgowExts then check at least one isn't a type variable
| dopt Opt_GlasgowExts dflags
- = check_tyvars dflags clas tys
+ = returnM ()
- -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
+ -- WITH HASKELL 98, MUST HAVE C (T a b c)
| isSingleton tys,
- Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
- not (isSynTyCon tycon), -- ...but not a synonym
- 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 ()
+ tcValidInstHeadTy first_ty
+ = returnM ()
| otherwise
= failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
where
- (first_ty : _) = tys
+ (first_ty : _) = tys
- ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
- creturnable_type ty = isFFIImportResultTy dflags ty
-
head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
text "where T is not a synonym, and a,b,c are distinct type variables")
-
-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 ()
- | 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")
- $$ undecidableMsg)
-
-undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
\end{code}
\begin{code}
instTypeErr pp_ty msg
= sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
nest 4 msg]
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{Checking instance for termination}
+%* *
+%************************************************************************
+
+Termination test: each assertion in the context satisfies
+ (1) no variable has more occurrences in the assertion than in the head, and
+ (2) the assertion has fewer constructors and variables (taken together
+ and counting repetitions) than the head.
+This is only needed with -fglasgow-exts, as Haskell 98 restrictions
+(which have already been checked) guarantee termination.
+
+\begin{code}
+checkInstTermination :: ThetaType -> [TcType] -> TcM ()
+checkInstTermination theta tys
+ = do
+ dflags <- getDOpts
+ check_inst_termination dflags theta tys
+
+check_inst_termination dflags theta tys
+ | not (dopt Opt_GlasgowExts dflags) = returnM ()
+ | dopt Opt_AllowUndecidableInstances dflags = returnM ()
+ | otherwise = do
+ mappM_ (check_nomore (fvTypes tys)) theta
+ mappM_ (check_smaller (sizeTypes tys)) theta
+
+check_nomore :: [TyVar] -> PredType -> TcM ()
+check_nomore fvs pred
+ = checkTc (null (fvPred pred \\ fvs))
+ (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
+
+check_smaller :: Int -> PredType -> TcM ()
+check_smaller n pred
+ = checkTc (sizePred pred < n)
+ (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+
+predUndecErr pred msg = sep [msg,
+ nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
+
+nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
+smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
+undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
-nonBoxedPrimCCallErr clas inst_ty
- = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
- 4 (pprClassPred clas [inst_ty])
+-- free variables of a type, retaining repetitions
+fvType :: Type -> [TyVar]
+fvType ty | Just exp_ty <- tcView ty = fvType exp_ty
+fvType (TyVarTy tv) = [tv]
+fvType (TyConApp _ tys) = fvTypes tys
+fvType (NoteTy _ ty) = fvType ty
+fvType (PredTy pred) = fvPred pred
+fvType (FunTy arg res) = fvType arg ++ fvType res
+fvType (AppTy fun arg) = fvType fun ++ fvType arg
+fvType (ForAllTy tyvar ty) = filter (/= tyvar) (fvType ty)
+
+fvTypes :: [Type] -> [TyVar]
+fvTypes tys = concat (map fvType tys)
+
+fvPred :: PredType -> [TyVar]
+fvPred (ClassP _ tys') = fvTypes tys'
+fvPred (IParam _ ty) = fvType ty
+
+-- size of a type: the number of variables and constructors
+sizeType :: Type -> Int
+sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty
+sizeType (TyVarTy _) = 1
+sizeType (TyConApp _ tys) = sizeTypes tys + 1
+sizeType (NoteTy _ ty) = sizeType ty
+sizeType (PredTy pred) = sizePred pred
+sizeType (FunTy arg res) = sizeType arg + sizeType res + 1
+sizeType (AppTy fun arg) = sizeType fun + sizeType arg
+sizeType (ForAllTy _ ty) = sizeType ty
+
+sizeTypes :: [Type] -> Int
+sizeTypes xs = sum (map sizeType xs)
+
+sizePred :: PredType -> Int
+sizePred (ClassP _ tys') = sizeTypes tys'
+sizePred (IParam _ ty) = sizeType ty
\end{code}
projects / ghc-hetmet.git / blobdiff