--------------------------------
-- Creating new mutable type variables
newFlexiTyVar,
- newTyFlexiVarTy, -- Kind -> TcM TcType
- newTyFlexiVarTys, -- Int -> Kind -> TcM [TcType]
+ newFlexiTyVarTy, -- Kind -> TcM TcType
+ newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
newKindVar, newKindVars,
- lookupTcTyVar, condLookupTcTyVar, LookupTyVarResult(..),
- newMetaTyVar, readMetaTyVar, writeMetaTyVar, putMetaTyVar,
+ lookupTcTyVar, LookupTyVarResult(..),
+ newMetaTyVar, readMetaTyVar, writeMetaTyVar,
+
+ --------------------------------
+ -- Boxy type variables
+ newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
--------------------------------
-- Instantiation
- tcInstTyVar, tcInstTyVars, tcInstType,
- tcSkolTyVar, tcSkolTyVars, tcSkolType,
+ tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxy, tcInstBoxyTyVar,
+ tcInstSigTyVars, zonkSigTyVar,
+ tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
+ tcSkolSigType, tcSkolSigTyVars,
--------------------------------
-- Checking type validity
- Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
+ Rank, UserTypeCtxt(..), checkValidType,
SourceTyCtxt(..), checkValidTheta, checkFreeness,
checkValidInstHead, instTypeErr, checkAmbiguity,
- arityErr, isRigidType,
+ checkInstTermination,
+ arityErr,
--------------------------------
-- Zonking
-- friends:
-import HsSyn ( LHsType )
-import TypeRep ( Type(..), PredType(..), 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, TcTyVarDetails(..),
- MetaDetails(..), SkolemInfo(..), isMetaTyVar, metaTvRef,
- tcCmpPred, isClassPred,
+ MetaDetails(..), SkolemInfo(..), BoxInfo(..),
+ BoxyTyVar, BoxyType, BoxyThetaType, BoxySigmaType,
+ UserTypeCtxt(..),
+ isMetaTyVar, isSigTyVar, metaTvRef,
+ tcCmpPred, isClassPred, tcGetTyVar,
tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
- tcSplitTyConApp_maybe, tcSplitForAllTys,
- tcIsTyVarTy, tcSplitSigmaTy, tcIsTyVarTy,
- isUnLiftedType, isIPPred, isImmutableTyVar,
- typeKind, isFlexi, isSkolemTyVar,
+ tcValidInstHeadTy, tcSplitForAllTys,
+ tcIsTyVarTy, tcSplitSigmaTy,
+ isUnLiftedType, isIPPred,
+ typeKind, isSkolemTyVar,
mkAppTy, mkTyVarTy, mkTyVarTys,
tyVarsOfPred, getClassPredTys_maybe,
- tyVarsOfType, tyVarsOfTypes,
+ tyVarsOfType, tyVarsOfTypes, tcView,
pprPred, pprTheta, pprClassPred )
-import Kind ( Kind(..), KindVar(..), mkKindVar, isSubKind,
+import Kind ( Kind(..), KindVar, kindVarRef, mkKindVar,
isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
liftedTypeKind, defaultKind
)
import Class ( Class, classArity, className )
import TyCon ( TyCon, isSynTyCon, isUnboxedTupleTyCon,
tyConArity, tyConName )
-import Var ( TyVar, tyVarKind, tyVarName,
- mkTyVar, mkTcTyVar, tcTyVarDetails, isTcTyVar )
+import Var ( TyVar, tyVarKind, tyVarName, isTcTyVar,
+ mkTyVar, mkTcTyVar, tcTyVarDetails )
+
+ -- Assertions
+#ifdef DEBUG
+import TcType ( isFlexi, isBoxyTyVar, isImmutableTyVar )
+import Kind ( isSubKind )
+#endif
-- others:
import TcRnMonad -- TcType, amongst others
import FunDeps ( grow )
import Name ( Name, setNameUnique, mkSysTvName )
import VarSet
-import VarEnv
-import CmdLineOpts ( dopt, DynFlag(..) )
-import Util ( nOfThem, isSingleton, equalLength, notNull )
+import DynFlags ( dopt, DynFlag(..) )
+import Util ( nOfThem, isSingleton, notNull )
import ListSetOps ( removeDups )
-import SrcLoc ( unLoc )
import Outputable
+
+import Data.List ( (\\) )
\end{code}
%************************************************************************
%* *
-\subsection{New type variables}
+ Instantiation in general
%* *
%************************************************************************
\begin{code}
-newMetaTyVar :: Name -> Kind -> MetaDetails -> TcM TyVar
-newMetaTyVar name kind details
- = do { ref <- newMutVar details ;
- return (mkTcTyVar name kind (MetaTv ref)) }
+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)
-readMetaTyVar :: TyVar -> TcM MetaDetails
-readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
- readMutVar (metaTvRef tyvar)
+ (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
-writeMetaTyVar :: TyVar -> MetaDetails -> TcM ()
-writeMetaTyVar tyvar val = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
- writeMutVar (metaTvRef tyvar) val
+ ; 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
-newFlexiTyVar :: Kind -> TcM TcTyVar
-newFlexiTyVar kind
- = newUnique `thenM` \ uniq ->
- newMetaTyVar (mkSysTvName uniq FSLIT("t")) kind Flexi
+ ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
+ ; return (tyvars', theta, tau) }
+\end{code}
-newTyFlexiVarTy :: Kind -> TcM TcType
-newTyFlexiVarTy kind
- = newFlexiTyVar kind `thenM` \ tc_tyvar ->
- returnM (TyVarTy tc_tyvar)
-newTyFlexiVarTys :: Int -> Kind -> TcM [TcType]
-newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind)
-
-isRigidType :: TcType -> TcM Bool
--- Check that the type is rigid, *taking the type refinement into account*
--- In other words if a rigid type variable tv is refined to a wobbly type,
--- the answer should be False
--- ToDo: can this happen?
-isRigidType ty
- = do { rigids <- mapM is_rigid (varSetElems (tyVarsOfType ty))
- ; return (and rigids) }
- where
- is_rigid tv = do { details <- lookupTcTyVar tv
- ; case details of
- RigidTv -> return True
- IndirectTv True ty -> isRigidType ty
- other -> return False
- }
+%************************************************************************
+%* *
+ Kind variables
+%* *
+%************************************************************************
+\begin{code}
newKindVar :: TcM TcKind
newKindVar = do { uniq <- newUnique
; ref <- newMutVar Nothing
%************************************************************************
%* *
-\subsection{Type instantiation}
+ SkolemTvs (immutable)
%* *
%************************************************************************
-Instantiating a bunch of type variables
-
-Note [TyVarName]
-~~~~~~~~~~~~~~~~
-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.
-
-
\begin{code}
------------------------
-tcInstTyVars :: [TyVar] -> TcM ([TcTyVar], [TcType], TvSubst)
-tcInstTyVars tyvars
- = do { tc_tvs <- mappM 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
-
-tcInstTyVar tyvar
- = do { uniq <- newUnique
- ; let name = setNameUnique (tyVarName tyvar) uniq
- -- See Note [TyVarName]
- ; newMetaTyVar name (tyVarKind tyvar) Flexi }
-
-tcInstType :: 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.
-tcInstType ty
- = case tcSplitForAllTys ty of
- ([], rho) -> -- There may be overloading despite no type variables;
- -- (?x :: Int) => Int -> Int
- let
- (theta, tau) = tcSplitPhiTy rho
- in
- returnM ([], theta, tau)
-
- (tyvars, rho) -> tcInstTyVars tyvars `thenM` \ (tyvars', _, tenv) ->
- let
- (theta, tau) = tcSplitPhiTy (substTy tenv rho)
- in
- returnM (tyvars', theta, tau)
-
----------------------------------------------
--- Similar functions but for skolem constants
-
-tcSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
-tcSkolTyVars info tyvars = mappM (tcSkolTyVar info) tyvars
-
-tcSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
-tcSkolTyVar info tyvar
+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
- -- See Note [TyVarName]
- ; return (mkTcTyVar name (tyVarKind tyvar)
- (SkolemTv info)) }
-
-tcSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-tcSkolType info ty
- = case tcSplitForAllTys ty of
- ([], rho) -> let
- (theta, tau) = tcSplitPhiTy rho
- in
- returnM ([], theta, tau)
+ kind = tyVarKind tyvar
+ ; return (mkSkolTyVar name kind info) }
- (tyvars, rho) -> tcSkolTyVars info tyvars `thenM` \ tyvars' ->
- let
- tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
- (theta, tau) = tcSplitPhiTy (substTy tenv rho)
- in
- returnM (tyvars', theta, tau)
+tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
+tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
\end{code}
%************************************************************************
%* *
-\subsection{Putting and getting mutable type variables}
+ MetaTvs (meta type variables; mutable)
%* *
%************************************************************************
\begin{code}
-putMetaTyVar :: TcTyVar -> TcType -> TcM ()
+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
-putMetaTyVar tyvar ty = writeMetaTyVar tyvar (Indirect ty)
+writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
#else
-putMetaTyVar tyvar ty
+writeMetaTyVar tyvar ty
| not (isMetaTyVar tyvar)
- = pprTrace "putTcTyVar" (ppr tyvar) $
+ = pprTrace "writeMetaTyVar" (ppr tyvar) $
returnM ()
| otherwise
= ASSERT( isMetaTyVar tyvar )
ASSERT2( k2 `isSubKind` k1, (ppr tyvar <+> ppr k1) $$ (ppr ty <+> ppr k2) )
- do { ASSERTM( do { details <- readMetaTyVar tyvar; return (isFlexi details) } )
- ; writeMetaTyVar tyvar (Indirect ty) }
+ 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}
+
+%************************************************************************
+%* *
+ 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}
+
+
+%************************************************************************
+%* *
+ MetaTvs: SigTvs
+%* *
+%************************************************************************
+
+\begin{code}
+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}
+
+
+%************************************************************************
+%* *
+ MetaTvs: BoxTvs
+%* *
+%************************************************************************
+
+\begin{code}
+newBoxyTyVar :: Kind -> TcM BoxyTyVar
+newBoxyTyVar kind = newMetaTyVar BoxTv kind
+
+newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
+newBoxyTyVars kinds = mapM newBoxyTyVar kinds
+
+newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
+newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
+
+readFilledBox :: BoxyTyVar -> TcM TcType
+-- Read the contents of the box, which should be filled in by now
+readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
+ do { cts <- readMetaTyVar box_tv
+ ; case cts of
+ Flexi -> pprPanic "readFilledBox" (ppr box_tv)
+ Indirect ty -> return ty }
+
+tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
+-- Instantiate with a BOXY type variable
+tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
+
+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}
+
+
+%************************************************************************
+%* *
+\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
any other type, then there might be bound TyVars embedded inside it.
\begin{code}
data LookupTyVarResult -- The result of a lookupTcTyVar call
- = FlexiTv
- | RigidTv
- | IndirectTv Bool TcType
- -- True => This is a non-wobbly type refinement,
- -- gotten from GADT match unification
- -- False => This is a wobbly type,
- -- gotten from inference unification
+ = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
+ | IndirectTv TcType
lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
--- This function is the ONLY PLACE that we consult the
--- type refinement carried by the monad
---
--- The boolean returned with Indirect
lookupTcTyVar tyvar
- = case tcTyVarDetails tyvar of
- SkolemTv _ -> do { type_reft <- getTypeRefinement
- ; case lookupVarEnv type_reft tyvar of
- Just ty -> return (IndirectTv True ty)
- Nothing -> return RigidTv
- }
- MetaTv ref -> do { details <- readMutVar ref
- ; case details of
- Indirect ty -> return (IndirectTv False ty)
- Flexi -> return FlexiTv
- }
-
--- Look up a meta type variable, conditionally consulting
--- the current type refinement
-condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
-condLookupTcTyVar use_refinement tyvar
- | use_refinement = lookupTcTyVar tyvar
- | otherwise
- = case tcTyVarDetails tyvar of
- SkolemTv _ -> return RigidTv
- MetaTv ref -> do { details <- readMutVar ref
- ; case details of
- Indirect ty -> return (IndirectTv False ty)
- Flexi -> return FlexiTv
- }
+ = 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
returnM (tyVarsOfTypes tys)
zonkTcTyVar :: TcTyVar -> TcM TcType
-zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnM (TyVarTy tv)) True tyvar
+zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar )
+ zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
\end{code}
----------------- Types
\begin{code}
zonkTcType :: TcType -> TcM TcType
-zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) True ty
+zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
zonkTcTypes :: [TcType] -> TcM [TcType]
zonkTcTypes tys = mappM zonkTcType tys
\begin{code}
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 inot ano ordinary TyVar.
+-- 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 imutable.
+-- We leave skolem TyVars alone; they are immutable.
zonkQuantifiedTyVar tv
| isSkolemTyVar tv = return tv
-- It might be a skolem type variable,
-- [Sept 04] I don't think this should happen
-- See note [Silly Type Synonym]
- other -> writeMetaTyVar tv (Indirect (mkTyVarTy final_tv))
+ Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
-- Return the new tyvar
; return final_tv }
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
zonkType :: (TcTyVar -> TcM Type) -- What to do with unbound mutable type variables
-- see zonkTcType, and zonkTcTypeToType
- -> Bool -- Should we consult the current type refinement?
-> TcType
-> TcM Type
-zonkType unbound_var_fn rflag ty
+zonkType unbound_var_fn ty
= go ty
where
- go (TyConApp tycon tys) = mappM go tys `thenM` \ tys' ->
- returnM (TyConApp tycon tys')
-
- go (NewTcApp tycon tys) = mappM go tys `thenM` \ tys' ->
- returnM (NewTcApp tycon tys')
-
- 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 (PredTy p) = go_pred p `thenM` \ p' ->
- returnM (PredTy p')
-
- go (FunTy arg res) = go arg `thenM` \ arg' ->
- go res `thenM` \ res' ->
- returnM (FunTy arg' res')
-
- go (AppTy fun arg) = go fun `thenM` \ fun' ->
- go arg `thenM` \ arg' ->
- returnM (mkAppTy fun' arg')
+ go (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 rflag tyvar
+ 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' ->
go_pred (IParam n ty) = go ty `thenM` \ ty' ->
returnM (IParam n ty')
-zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
- -> Bool -- Consult the type refinement?
- -> TcTyVar -> TcM TcType
-zonkTyVar unbound_var_fn rflag tyvar
- | not (isTcTyVar tyvar) -- This can happen when
- -- zonking a forall type, when the bound type variable
- -- needn't be mutable
+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
- = condLookupTcTyVar rflag tyvar `thenM` \ details ->
- case details of
- -- If b is true, the variable was refined, and therefore it is okay
- -- to continue refining inside. Otherwise it was wobbly and we should
- -- not refine further inside.
- IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
- FlexiTv -> unbound_var_fn tyvar -- Unbound flexi
- RigidTv -> return (TyVarTy tyvar) -- Rigid, no zonking necessary
+ | 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}
\begin{code}
readKindVar :: KindVar -> TcM (Maybe TcKind)
writeKindVar :: KindVar -> TcKind -> TcM ()
-readKindVar (KVar _ ref) = readMutVar ref
-writeKindVar (KVar _ ref) val = writeMutVar ref (Just val)
+readKindVar kv = readMutVar (kindVarRef kv)
+writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
-------------
zonkTcKind :: TcKind -> TcM TcKind
\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
- | DefaultDeclCtxt -- Types in a default declaration
-
--- 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.
-
-
-pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
-pprHsSigCtxt ctxt hs_ty = pprUserTypeCtxt (unLoc hs_ty) ctxt
-
-pprUserTypeCtxt ty (FunSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
-pprUserTypeCtxt ty ExprSigCtxt = sep [ptext SLIT("In an expression type signature:"), nest 2 (ppr ty)]
-pprUserTypeCtxt ty (ConArgCtxt c) = sep [ptext SLIT("In the type of the constructor"), pp_sig c ty]
-pprUserTypeCtxt ty (TySynCtxt c) = sep [ptext SLIT("In the RHS of the type synonym") <+> quotes (ppr c) <> comma,
- nest 2 (ptext SLIT(", namely") <+> ppr ty)]
-pprUserTypeCtxt ty GenPatCtxt = sep [ptext SLIT("In the type pattern of a generic definition:"), nest 2 (ppr ty)]
-pprUserTypeCtxt ty PatSigCtxt = sep [ptext SLIT("In a pattern type signature:"), nest 2 (ppr ty)]
-pprUserTypeCtxt ty ResSigCtxt = sep [ptext SLIT("In a result type signature:"), nest 2 (ppr ty)]
-pprUserTypeCtxt ty (ForSigCtxt n) = sep [ptext SLIT("In the foreign declaration:"), pp_sig n ty]
-pprUserTypeCtxt ty (RuleSigCtxt n) = sep [ptext SLIT("In the type signature:"), pp_sig n ty]
-pprUserTypeCtxt ty DefaultDeclCtxt = sep [ptext SLIT("In a type in a `default' declaration:"), nest 2 (ppr ty)]
-
-pp_sig n ty = nest 2 (ppr n <+> dcolon <+> ppr ty)
-\end{code}
-
-\begin{code}
checkValidType :: UserTypeCtxt -> Type -> TcM ()
-- Checks that the type is valid for the given context
checkValidType ctxt ty
| 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
-- constructor, hence rank 1
ForSigCtxt _ -> Rank 1
RuleSigCtxt _ -> Rank 1
+ SpecInstCtxt -> Rank 1
actual_kind = typeKind ty
ExprSigCtxt -> isOpenTypeKind actual_kind
GenPatCtxt -> isLiftedTypeKind actual_kind
ForSigCtxt _ -> isLiftedTypeKind actual_kind
- other -> isArgTypeKind actual_kind
+ other -> isArgTypeKind actual_kind
ubx_tup | not gla_exts = UT_NotOk
| otherwise = case ctxt of
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 `thenM_`
+ = 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 (PredTy sty) = getDOpts `thenM` \ dflags ->
- check_source_ty dflags TypeCtxt sty
+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 `thenM_`
- check_tau_type rank UT_Ok res_ty
+ check_poly_type rank UT_Ok res_ty
check_tau_type rank ubx_tup (AppTy ty1 ty2)
= check_arg_type ty1 `thenM_` check_arg_type ty2
-check_tau_type rank ubx_tup (NoteTy (SynNote syn) ty)
- -- Synonym notes are built only when the synonym is
- -- saturated (see Type.mkSynTy)
- = 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
+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.
- 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 (NewTcApp tc tys)
- = mappM_ check_arg_type tys
-
-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 `thenM_`
- mappM_ check_arg_type tys
+ returnM ()
+ else
+ -- For H98, do check the type args
+ mappM_ check_arg_type tys
+ }
| isUnboxedTupleTyCon tc
= doptM Opt_GlasgowExts `thenM` \ gla_exts ->
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
+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
-- f :: N a -> N a
| InstThetaCtxt -- Context of an instance decl
-- instance <S> => C [a] where ...
- | InstHeadCtxt -- Head of an instance decl
- -- instance ... => Eq 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}
check_valid_theta ctxt theta
= getDOpts `thenM` \ dflags ->
warnTc (notNull dups) (dupPredWarn dups) `thenM_`
- -- Actually, in instance decls and type signatures,
- -- duplicate constraints are eliminated by TcHsType.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_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 tcIsTyVarTy 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
-------------------------
ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
-predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
+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)
arityErr kind name n m
check_inst_head dflags clas tys
-- 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
+ tcValidInstHeadTy first_ty
= returnM ()
| otherwise
= failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
where
- (first_ty : _) = tys
+ (first_ty : _) = tys
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 = 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")
- $$ undecidableMsg)
-
-undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
\end{code}
\begin{code}
= 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")
+
+-- 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}