newFlexiTyVarTy, -- Kind -> TcM TcType
newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
newKindVar, newKindVars,
- lookupTcTyVar, LookupTyVarResult(..),
- newMetaTyVar, readMetaTyVar, writeMetaTyVar,
- --------------------------------
- -- Boxy type variables
- newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox,
+ newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
+ isFilledMetaTyVar, isFlexiMetaTyVar,
--------------------------------
- -- Creating new coercion variables
- newCoVars,
+ -- Creating new evidence variables
+ newEvVar, newCoVar, newEvVars,
+ newWantedCoVar, writeWantedCoVar, readWantedCoVar,
+ newIP, newDict, newSelfDict, isSelfDict,
+
+ newWantedEvVar, newWantedEvVars,
+ newKindConstraint,
+ newTcEvBinds, addTcEvBind,
--------------------------------
-- Instantiation
- tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
- tcInstSigTyVars, zonkSigTyVar,
- tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType,
- tcSkolSigType, tcSkolSigTyVars,
+ tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
+ tcInstType, tcInstSigType,
+ tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType,
+ tcSkolSigType, tcSkolSigTyVars,
--------------------------------
-- Checking type validity
- Rank, UserTypeCtxt(..), checkValidType,
- SourceTyCtxt(..), checkValidTheta, checkFreeness,
- checkValidInstHead, checkValidInstance, checkAmbiguity,
- checkInstTermination,
+ Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
+ SourceTyCtxt(..), checkValidTheta,
+ checkValidInstHead, checkValidInstance,
+ checkInstTermination, checkValidTypeInst, checkTyFamFreeness,
arityErr,
+ growPredTyVars, growThetaTyVars, validDerivPred,
--------------------------------
-- Zonking
- zonkType, zonkTcPredType,
- zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV,
+ zonkType, mkZonkTcTyVar, zonkTcPredType,
+ zonkTcTypeCarefully,
+ zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
zonkQuantifiedTyVar, zonkQuantifiedTyVars,
- zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
- zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
+ zonkTcType, zonkTcTypes, zonkTcThetaType,
+ zonkTcKindToKind, zonkTcKind,
+ zonkImplication, zonkWanted, zonkEvVar, zonkWantedEvVar,
+ zonkTcTypeAndSubst,
+ tcGetGlobalTyVars,
readKindVar, writeKindVar
-
) where
#include "HsVersions.h"
import Var
-- others:
-import TcRnMonad -- TcType, amongst others
+import HsSyn -- HsType
+import TcRnMonad -- TcType, amongst others
+import Id
import FunDeps
import Name
import VarSet
import Util
import Maybes
import ListSetOps
-import UniqSupply
+import BasicTypes
import SrcLoc
import Outputable
+import FastString
+import Bag
-import Control.Monad ( when, unless )
+import Control.Monad
import Data.List ( (\\) )
\end{code}
%************************************************************************
%* *
- Instantiation in general
+ Kind variables
%* *
%************************************************************************
\begin{code}
-tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
- -> TcType -- Type to instantiate
- -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
-tcInstType inst_tyvars ty
- = case tcSplitForAllTys ty of
- ([], rho) -> let -- There may be overloading despite no type variables;
- -- (?x :: Int) => Int -> Int
- (theta, tau) = tcSplitPhiTy rho
- in
- return ([], theta, tau)
-
- (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
-
- ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
- -- Either the tyvars are freshly made, by inst_tyvars,
- -- or (in the call from tcSkolSigType) any nested foralls
- -- have different binders. Either way, zipTopTvSubst is ok
+newKindVar :: TcM TcKind
+newKindVar = do { uniq <- newUnique
+ ; ref <- newMutVar Flexi
+ ; return (mkTyVarTy (mkKindVar uniq ref)) }
- ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
- ; return (tyvars', theta, tau) }
+newKindVars :: Int -> TcM [TcKind]
+newKindVars n = mapM (\ _ -> newKindVar) (nOfThem n ())
\end{code}
%************************************************************************
%* *
- Kind variables
+ Evidence variables; range over constraints we can abstract over
%* *
%************************************************************************
\begin{code}
-newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
-newCoVars spec
- = do { us <- newUniqueSupply
- ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
- (mkCoKind ty1 ty2)
- | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
-
-newKindVar :: TcM TcKind
-newKindVar = do { uniq <- newUnique
- ; ref <- newMutVar Flexi
- ; return (mkTyVarTy (mkKindVar uniq ref)) }
+newEvVars :: TcThetaType -> TcM [EvVar]
+newEvVars theta = mapM newEvVar theta
+
+newWantedEvVar :: TcPredType -> TcM EvVar
+newWantedEvVar (EqPred ty1 ty2) = newWantedCoVar ty1 ty2
+newWantedEvVar (ClassP cls tys) = newDict cls tys
+newWantedEvVar (IParam ip ty) = newIP ip ty
+
+newWantedEvVars :: TcThetaType -> TcM [EvVar]
+newWantedEvVars theta = mapM newWantedEvVar theta
+
+newWantedCoVar :: TcType -> TcType -> TcM CoVar
+newWantedCoVar ty1 ty2 = newCoVar ty1 ty2
+
+-- We used to create a mutable co-var
+{-
+-- A wanted coercion variable is a MetaTyVar
+-- that can be filled in with its binding
+ = do { uniq <- newUnique
+ ; ref <- newMutVar Flexi
+ ; let name = mkSysTvName uniq (fsLit "c")
+ kind = mkPredTy (EqPred ty1 ty2)
+ ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }
+-}
-newKindVars :: Int -> TcM [TcKind]
-newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
+--------------
+newEvVar :: TcPredType -> TcM EvVar
+-- Creates new *rigid* variables for predicates
+newEvVar (EqPred ty1 ty2) = newCoVar ty1 ty2
+newEvVar (ClassP cls tys) = newDict cls tys
+newEvVar (IParam ip ty) = newIP ip ty
+
+newCoVar :: TcType -> TcType -> TcM CoVar
+newCoVar ty1 ty2
+ = do { name <- newName (mkTyVarOccFS (fsLit "co"))
+ ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
+
+newIP :: IPName Name -> TcType -> TcM IpId
+newIP ip ty
+ = do { name <- newName (getOccName (ipNameName ip))
+ ; return (mkLocalId name (mkPredTy (IParam ip ty))) }
+
+newDict :: Class -> [TcType] -> TcM DictId
+newDict cls tys
+ = do { name <- newName (mkDictOcc (getOccName cls))
+ ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
+
+newName :: OccName -> TcM Name
+newName occ
+ = do { uniq <- newUnique
+ ; loc <- getSrcSpanM
+ ; return (mkInternalName uniq occ loc) }
+
+-----------------
+newKindConstraint :: Type -> Kind -> TcM (CoVar, Type)
+-- Create a new wanted CoVar that constrains the type
+-- to have the specified kind
+newKindConstraint ty kind
+ = do { ty_k <- newFlexiTyVarTy kind
+ ; co_var <- newWantedCoVar ty ty_k
+ ; return (co_var, ty_k) }
+
+-----------------
+newSelfDict :: Class -> [TcType] -> TcM DictId
+-- Make a dictionary for "self". It behaves just like a normal DictId
+-- except that it responds True to isSelfDict
+-- This is used only to suppress confusing error reports
+newSelfDict cls tys
+ = do { uniq <- newUnique
+ ; let name = mkSystemName uniq selfDictOcc
+ ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
+
+selfDictOcc :: OccName
+selfDictOcc = mkVarOcc "self"
+
+isSelfDict :: EvVar -> Bool
+isSelfDict v = isSystemName (Var.varName v)
+ -- Notice that all *other* evidence variables get Internal Names
\end{code}
%************************************************************************
\begin{code}
+tcInstType :: ([TyVar] -> TcM [TcTyVar]) -- How to instantiate the type variables
+ -> TcType -- Type to instantiate
+ -> TcM ([TcTyVar], TcThetaType, TcType) -- Result
+ -- (type vars (excl coercion vars), preds (incl equalities), rho)
+tcInstType inst_tyvars ty
+ = case tcSplitForAllTys ty of
+ ([], rho) -> let -- There may be overloading despite no type variables;
+ -- (?x :: Int) => Int -> Int
+ (theta, tau) = tcSplitPhiTy rho
+ in
+ return ([], theta, tau)
+
+ (tyvars, rho) -> do { tyvars' <- inst_tyvars tyvars
+
+ ; let tenv = zipTopTvSubst tyvars (mkTyVarTys tyvars')
+ -- Either the tyvars are freshly made, by inst_tyvars,
+ -- or (in the call from tcSkolSigType) any nested foralls
+ -- have different binders. Either way, zipTopTvSubst is ok
+
+ ; let (theta, tau) = tcSplitPhiTy (substTy tenv rho)
+ ; return (tyvars', theta, tau) }
+
mkSkolTyVar :: Name -> Kind -> SkolemInfo -> TcTyVar
mkSkolTyVar name kind info = mkTcTyVar name kind (SkolemTv info)
tcSkolSigType :: SkolemInfo -> Type -> TcM ([TcTyVar], TcThetaType, TcType)
-- Instantiate a type signature with skolem constants, but
-- do *not* give them fresh names, because we want the name to
--- be in the type environment -- it is lexically scoped.
+-- be in the type environment: it is lexically scoped.
tcSkolSigType info ty = tcInstType (\tvs -> return (tcSkolSigTyVars info tvs)) ty
tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
| tv <- tyvars ]
-tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar
+tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
-- Instantiate the tyvar, using
-- * the occ-name and kind of the supplied tyvar,
-- * the unique from the monad,
--- * the location either from the tyvar (mb_loc = Nothing)
--- or from mb_loc (Just loc)
-tcInstSkolTyVar info mb_loc tyvar
+-- * the location either from the tyvar (skol_info = SigSkol)
+-- or from the monad (otehrwise)
+tcInstSkolTyVar skol_info tyvar
= do { uniq <- newUnique
- ; let old_name = tyVarName tyvar
- kind = tyVarKind tyvar
- loc = mb_loc `orElse` getSrcSpan old_name
- new_name = mkInternalName uniq (nameOccName old_name) loc
- ; return (mkSkolTyVar new_name kind info) }
+ ; loc <- case skol_info of
+ SigSkol {} -> return (getSrcSpan old_name)
+ _ -> getSrcSpanM
+ ; let new_name = mkInternalName uniq occ loc
+ ; return (mkSkolTyVar new_name kind skol_info) }
+ where
+ old_name = tyVarName tyvar
+ occ = nameOccName old_name
+ kind = tyVarKind tyvar
tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
-- Get the location from the monad
tcInstSkolTyVars info tyvars
- = do { span <- getSrcSpanM
- ; mapM (tcInstSkolTyVar info (Just span)) tyvars }
+ = mapM (tcInstSkolTyVar info) tyvars
tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
-- Instantiate a type with fresh skolem constants
-- Binding location comes from the monad
tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
+
+tcInstSigType :: Bool -> Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType)
+-- Instantiate with skolems or meta SigTvs; depending on use_skols
+-- Always take location info from the supplied tyvars
+tcInstSigType use_skols name ty
+ | use_skols
+ = tcInstType (tcInstSkolTyVars (SigSkol (FunSigCtxt name))) ty
+ | otherwise
+ = tcInstType tcInstSigTyVars ty
+
+tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
+-- Make meta SigTv type variables for patten-bound scoped type varaibles
+-- We use SigTvs for them, so that they can't unify with arbitrary types
+tcInstSigTyVars = mapM (\tv -> instMetaTyVar (SigTv (tyVarName tv)) tv)
+ -- ToDo: the "function binding site is bogus
\end{code}
%************************************************************************
\begin{code}
-newMetaTyVar :: BoxInfo -> Kind -> TcM TcTyVar
+newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
-- Make a new meta tyvar out of thin air
-newMetaTyVar box_info kind
+newMetaTyVar meta_info kind
= do { uniq <- newUnique
- ; ref <- newMutVar Flexi ;
+ ; ref <- newMutVar Flexi
; let name = mkSysTvName uniq fs
- fs = case box_info of
- BoxTv -> FSLIT("t")
- TauTv -> FSLIT("t")
- SigTv _ -> FSLIT("a")
- -- We give BoxTv and TauTv the same string, because
- -- otherwise we get user-visible differences in error
- -- messages, which are confusing. If you want to see
- -- the box_info of each tyvar, use -dppr-debug
- ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
-
-instMetaTyVar :: BoxInfo -> TyVar -> TcM TcTyVar
+ fs = case meta_info of
+ TauTv -> fsLit "t"
+ SigTv _ -> fsLit "a"
+ ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
+
+instMetaTyVar :: MetaInfo -> TyVar -> TcM TcTyVar
-- Make a new meta tyvar whose Name and Kind
-- come from an existing TyVar
-instMetaTyVar box_info tyvar
+instMetaTyVar meta_info tyvar
= do { uniq <- newUnique
- ; ref <- newMutVar Flexi ;
+ ; ref <- newMutVar Flexi
; let name = setNameUnique (tyVarName tyvar) uniq
kind = tyVarKind tyvar
- ; return (mkTcTyVar name kind (MetaTv box_info ref)) }
+ ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
readMutVar (metaTvRef tyvar)
+readWantedCoVar :: CoVar -> TcM MetaDetails
+readWantedCoVar covar = ASSERT2( isMetaTyVar covar, ppr covar )
+ readMutVar (metaTvRef covar)
+
+
+
+isFilledMetaTyVar :: TyVar -> TcM Bool
+-- True of a filled-in (Indirect) meta type variable
+isFilledMetaTyVar tv
+ | not (isTcTyVar tv) = return False
+ | MetaTv _ ref <- tcTyVarDetails tv
+ = do { details <- readMutVar ref
+ ; return (isIndirect details) }
+ | otherwise = return False
+
+isFlexiMetaTyVar :: TyVar -> TcM Bool
+-- True of a un-filled-in (Flexi) meta type variable
+isFlexiMetaTyVar tv
+ | not (isTcTyVar tv) = return False
+ | MetaTv _ ref <- tcTyVarDetails tv
+ = do { details <- readMutVar ref
+ ; return (isFlexi details) }
+ | otherwise = return False
+
+--------------------
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
-#ifndef DEBUG
-writeMetaTyVar tyvar ty = writeMutVar (metaTvRef tyvar) (Indirect ty)
-#else
+-- Write into a currently-empty MetaTyVar
+
writeMetaTyVar tyvar ty
- | not (isMetaTyVar tyvar)
- = pprTrace "writeMetaTyVar" (ppr tyvar) $
- returnM ()
+ | not debugIsOn
+ = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
+
+-- Everything from here on only happens if DEBUG is on
+ | not (isTcTyVar tyvar)
+ = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
+ return ()
+
+ | MetaTv _ ref <- tcTyVarDetails tyvar
+ = writeMetaTyVarRef tyvar ref ty
+
+ | otherwise
+ = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
+ return ()
+
+writeWantedCoVar :: CoVar -> Coercion -> TcM ()
+writeWantedCoVar cv co = writeMetaTyVar cv co
+
+--------------------
+writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
+-- Here the tyvar is for error checking only;
+-- the ref cell must be for the same tyvar
+writeMetaTyVarRef tyvar ref ty
+ | not debugIsOn
+ = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
+ ; writeMutVar ref (Indirect ty) }
+
+-- Everything from here on only happens if DEBUG is on
+ | not (isPredTy tv_kind) -- Don't check kinds for updates to coercion variables
+ , not (ty_kind `isSubKind` tv_kind)
+ = WARN( True, hang (text "Ill-kinded update to meta tyvar")
+ 2 (ppr tyvar $$ ppr tv_kind $$ ppr ty $$ ppr ty_kind) )
+ return ()
| otherwise
- = 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) }
+ = do { meta_details <- readMutVar ref;
+ ; WARN( not (isFlexi meta_details),
+ hang (text "Double update of meta tyvar")
+ 2 (ppr tyvar $$ ppr meta_details) )
+
+ traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
+ ; writeMutVar ref (Indirect ty) }
where
- k1 = tyVarKind tyvar
- k2 = typeKind ty
-#endif
+ tv_kind = tyVarKind tyvar
+ ty_kind = typeKind ty
\end{code}
newFlexiTyVar kind = newMetaTyVar TauTv kind
newFlexiTyVarTy :: Kind -> TcM TcType
-newFlexiTyVarTy kind
- = newFlexiTyVar kind `thenM` \ tc_tyvar ->
- returnM (TyVarTy tc_tyvar)
+newFlexiTyVarTy kind = do
+ tc_tyvar <- newFlexiTyVar kind
+ return (TyVarTy tc_tyvar)
newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
-newFlexiTyVarTys n kind = mappM newFlexiTyVarTy (nOfThem n kind)
+newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
tcInstTyVar :: TyVar -> TcM TcTyVar
-- Instantiate with a META type variable
tcInstTyVars tyvars
= do { tc_tvs <- mapM tcInstTyVar tyvars
; let tys = mkTyVarTys tc_tvs
- ; returnM (tc_tvs, tys, zipTopTvSubst tyvars tys) }
+ ; return (tc_tvs, tys, zipTopTvSubst tyvars tys) }
-- Since the tyvars are freshly made,
-- they cannot possibly be captured by
-- any existing for-alls. Hence zipTopTvSubst
%************************************************************************
\begin{code}
-tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar]
--- Instantiate with skolems or meta SigTvs; depending on use_skols
--- Always take location info from the supplied tyvars
-tcInstSigTyVars use_skols skol_info tyvars
- | use_skols
- = mapM (tcInstSkolTyVar skol_info Nothing) tyvars
-
- | otherwise
- = mapM (instMetaTyVar (SigTv skol_info)) tyvars
-
zonkSigTyVar :: TcTyVar -> TcM TcTyVar
zonkSigTyVar sig_tv
| isSkolemTyVar sig_tv
\end{code}
-%************************************************************************
-%* *
- MetaTvs: BoxTvs
-%* *
-%************************************************************************
-
-\begin{code}
-newBoxyTyVar :: Kind -> TcM BoxyTyVar
-newBoxyTyVar kind = newMetaTyVar BoxTv kind
-
-newBoxyTyVars :: [Kind] -> TcM [BoxyTyVar]
-newBoxyTyVars kinds = mapM newBoxyTyVar kinds
-
-newBoxyTyVarTys :: [Kind] -> TcM [BoxyType]
-newBoxyTyVarTys kinds = do { tvs <- mapM newBoxyTyVar kinds; return (mkTyVarTys tvs) }
-
-readFilledBox :: BoxyTyVar -> TcM TcType
--- Read the contents of the box, which should be filled in by now
-readFilledBox box_tv = ASSERT( isBoxyTyVar box_tv )
- do { cts <- readMetaTyVar box_tv
- ; case cts of
- Flexi -> pprPanic "readFilledBox" (ppr box_tv)
- Indirect ty -> return ty }
-
-tcInstBoxyTyVar :: TyVar -> TcM BoxyTyVar
--- Instantiate with a BOXY type variable
-tcInstBoxyTyVar tyvar = instMetaTyVar BoxTv tyvar
-\end{code}
-
%************************************************************************
%* *
-\subsection{Putting and getting mutable type variables}
+\subsection{Zonking -- the exernal interfaces}
%* *
%************************************************************************
-But it's more fun to short out indirections on the way: If this
-version returns a TyVar, then that TyVar is unbound. If it returns
-any other type, then there might be bound TyVars embedded inside it.
-
-We return Nothing iff the original box was unbound.
+@tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
+To improve subsequent calls to the same function it writes the zonked set back into
+the environment.
\begin{code}
-data LookupTyVarResult -- The result of a lookupTcTyVar call
- = DoneTv TcTyVarDetails -- SkolemTv or virgin MetaTv
- | IndirectTv TcType
-
-lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
-lookupTcTyVar tyvar
- = ASSERT2( isTcTyVar tyvar, ppr tyvar )
- case details of
- SkolemTv _ -> return (DoneTv details)
- MetaTv _ ref -> do { meta_details <- readMutVar ref
- ; case meta_details of
- Indirect ty -> return (IndirectTv ty)
- Flexi -> return (DoneTv details) }
- where
- details = tcTyVarDetails tyvar
-
-{-
--- gaw 2004 We aren't shorting anything out anymore, at least for now
-getTcTyVar tyvar
- | not (isTcTyVar tyvar)
- = pprTrace "getTcTyVar" (ppr tyvar) $
- returnM (Just (mkTyVarTy tyvar))
-
- | otherwise
- = ASSERT2( isTcTyVar tyvar, ppr tyvar )
- readMetaTyVar tyvar `thenM` \ maybe_ty ->
- case maybe_ty of
- Just ty -> short_out ty `thenM` \ ty' ->
- writeMetaTyVar tyvar (Just ty') `thenM_`
- returnM (Just ty')
-
- Nothing -> returnM Nothing
-
-short_out :: TcType -> TcM TcType
-short_out ty@(TyVarTy tyvar)
- | not (isTcTyVar tyvar)
- = returnM ty
-
- | otherwise
- = readMetaTyVar tyvar `thenM` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> short_out ty' `thenM` \ ty' ->
- writeMetaTyVar tyvar (Just ty') `thenM_`
- returnM ty'
-
- other -> returnM ty
-
-short_out other_ty = returnM other_ty
--}
+tcGetGlobalTyVars :: TcM TcTyVarSet
+tcGetGlobalTyVars
+ = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
+ ; gbl_tvs <- readMutVar gtv_var
+ ; gbl_tvs' <- zonkTcTyVarsAndFV gbl_tvs
+ ; writeMutVar gtv_var gbl_tvs'
+ ; return gbl_tvs' }
\end{code}
-
-%************************************************************************
-%* *
-\subsection{Zonking -- the exernal interfaces}
-%* *
-%************************************************************************
-
----------------- Type variables
\begin{code}
zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
-zonkTcTyVars tyvars = mappM zonkTcTyVar tyvars
+zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
-zonkTcTyVarsAndFV :: [TcTyVar] -> TcM TcTyVarSet
-zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
- returnM (tyVarsOfTypes tys)
-
-zonkTcTyVar :: TcTyVar -> TcM TcType
-zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar)
- zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
-\end{code}
+zonkTcTyVarsAndFV :: TcTyVarSet -> TcM TcTyVarSet
+zonkTcTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTcTyVar (varSetElems tyvars)
----------------- Types
-\begin{code}
+zonkTcTypeCarefully :: TcType -> TcM TcType
+-- Do not zonk type variables free in the environment
+zonkTcTypeCarefully ty
+ = do { env_tvs <- tcGetGlobalTyVars
+ ; zonkType (zonk_tv env_tvs) ty }
+ where
+ zonk_tv env_tvs tv
+ | tv `elemVarSet` env_tvs
+ = return (TyVarTy tv)
+ | otherwise
+ = ASSERT( isTcTyVar tv )
+ case tcTyVarDetails tv of
+ SkolemTv {} -> return (TyVarTy tv)
+ FlatSkol ty -> zonkType (zonk_tv env_tvs) ty
+ MetaTv _ ref -> do { cts <- readMutVar ref
+ ; case cts of
+ Flexi -> return (TyVarTy tv)
+ Indirect ty -> zonkType (zonk_tv env_tvs) ty }
+
zonkTcType :: TcType -> TcM TcType
-zonkTcType ty = zonkType (\ tv -> returnM (TyVarTy tv)) ty
+-- Simply look through all Flexis
+zonkTcType ty = zonkType zonkTcTyVar ty
-zonkTcTypes :: [TcType] -> TcM [TcType]
-zonkTcTypes tys = mappM zonkTcType tys
+zonkTcTyVar :: TcTyVar -> TcM TcType
+-- Simply look through all Flexis
+zonkTcTyVar tv
+ = ASSERT2( isTcTyVar tv, ppr tv )
+ case tcTyVarDetails tv of
+ SkolemTv {} -> return (TyVarTy tv)
+ FlatSkol ty -> zonkTcType ty
+ MetaTv _ ref -> do { cts <- readMutVar ref
+ ; case cts of
+ Flexi -> return (TyVarTy tv)
+ Indirect ty -> zonkTcType ty }
+
+zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
+-- Zonk, and simultaneously apply a non-necessarily-idempotent substitution
+zonkTcTypeAndSubst subst ty = zonkType zonk_tv ty
+ where
+ zonk_tv tv
+ = case tcTyVarDetails tv of
+ SkolemTv {} -> return (TyVarTy tv)
+ FlatSkol ty -> zonkType zonk_tv ty
+ MetaTv _ ref -> do { cts <- readMutVar ref
+ ; case cts of
+ Flexi -> zonk_flexi tv
+ Indirect ty -> zonkType zonk_tv ty }
+ zonk_flexi tv
+ = case lookupTyVar subst tv of
+ Just ty -> zonkType zonk_tv ty
+ Nothing -> return (TyVarTy tv)
-zonkTcClassConstraints cts = mappM zonk cts
- where zonk (clas, tys)
- = zonkTcTypes tys `thenM` \ new_tys ->
- returnM (clas, new_tys)
+zonkTcTypes :: [TcType] -> TcM [TcType]
+zonkTcTypes tys = mapM zonkTcType tys
zonkTcThetaType :: TcThetaType -> TcM TcThetaType
-zonkTcThetaType theta = mappM zonkTcPredType theta
+zonkTcThetaType theta = mapM zonkTcPredType theta
zonkTcPredType :: TcPredType -> TcM TcPredType
-zonkTcPredType (ClassP c ts)
- = zonkTcTypes ts `thenM` \ new_ts ->
- returnM (ClassP c new_ts)
-zonkTcPredType (IParam n t)
- = zonkTcType t `thenM` \ new_t ->
- returnM (IParam n new_t)
-zonkTcPredType (EqPred t1 t2)
- = zonkTcType t1 `thenM` \ new_t1 ->
- zonkTcType t2 `thenM` \ new_t2 ->
- returnM (EqPred new_t1 new_t2)
+zonkTcPredType (ClassP c ts) = ClassP c <$> zonkTcTypes ts
+zonkTcPredType (IParam n t) = IParam n <$> zonkTcType t
+zonkTcPredType (EqPred t1 t2) = EqPred <$> zonkTcType t1 <*> zonkTcType t2
\end{code}
------------------- These ...ToType, ...ToKind versions
are used at the end of type checking
\begin{code}
-zonkTopTyVar :: TcTyVar -> TcM TcTyVar
--- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables
--- to default the kind of ? and ?? etc to *. This is important to ensure that
--- instance declarations match. For example consider
--- instance Show (a->b)
--- foo x = show (\_ -> True)
--- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
--- and that won't match the typeKind (*) in the instance decl.
---
--- Because we are at top level, no further constraints are going to affect these
--- type variables, so it's time to do it by hand. However we aren't ready
--- to default them fully to () or whatever, because the type-class defaulting
--- rules have yet to run.
+zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
+zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
-zonkTopTyVar tv
- | k `eqKind` default_k = return tv
- | otherwise
- = do { tv' <- newFlexiTyVar default_k
- ; writeMetaTyVar tv (mkTyVarTy tv')
- ; return tv' }
- where
- k = tyVarKind tv
- default_k = defaultKind k
-
-zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TyVar]
-zonkQuantifiedTyVars = mappM zonkQuantifiedTyVar
-
-zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
+zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
-- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
--
-- The quantified type variables often include meta type variables
-- we want to freeze them into ordinary type variables, and
-- default their kind (e.g. from OpenTypeKind to TypeKind)
-- -- see notes with Kind.defaultKind
--- The meta tyvar is updated to point to the new regular TyVar. Now any
+-- The meta tyvar is updated to point to the new skolem 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
- | ASSERT( isTcTyVar tv )
- isSkolemTyVar tv = return tv
+ | ASSERT2( isTcTyVar tv, ppr tv )
+ isSkolemTyVar tv
+ = do { kind <- zonkTcType (tyVarKind tv)
+ ; return $ setTyVarKind tv kind
+ }
-- It might be a skolem type variable,
-- for example from a user type signature
| otherwise -- It's a meta-type-variable
= do { details <- readMetaTyVar tv
- -- Create the new, frozen, regular type variable
+ -- Create the new, frozen, skolem type variable
+ -- We zonk to a skolem, not to a regular TcVar
+ -- See Note [Zonking to Skolem]
; let final_kind = defaultKind (tyVarKind tv)
- final_tv = mkTyVar (tyVarName tv) final_kind
+ final_tv = mkSkolTyVar (tyVarName tv) final_kind UnkSkol
-- Bind the meta tyvar to the new tyvar
; case details of
; return final_tv }
\end{code}
-[Silly Type Synonyms]
+\begin{code}
+zonkImplication :: Implication -> TcM Implication
+zonkImplication implic@(Implic { ic_untch = env_tvs, ic_given = given
+ , ic_wanted = wanted })
+ = do { env_tvs' <- zonkTcTyVarsAndFV env_tvs
+ ; given' <- mapM zonkEvVar given
+ ; wanted' <- mapBagM zonkWanted wanted
+ ; return (implic { ic_untch = env_tvs', ic_given = given'
+ , ic_wanted = wanted' }) }
+
+zonkEvVar :: EvVar -> TcM EvVar
+zonkEvVar var = do { ty' <- zonkTcType (varType var)
+ ; return (setVarType var ty') }
+
+zonkWanted :: WantedConstraint -> TcM WantedConstraint
+zonkWanted (WcImplic imp) = do { imp' <- zonkImplication imp; return (WcImplic imp') }
+zonkWanted (WcEvVar ev) = do { ev' <- zonkWantedEvVar ev; return (WcEvVar ev') }
+
+zonkWantedEvVar :: WantedEvVar -> TcM WantedEvVar
+zonkWantedEvVar (WantedEvVar v l) = do { v' <- zonkEvVar v; return (WantedEvVar v' l) }
+\end{code}
+
+Note [Silly Type Synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
type C u a = u -- Note 'a' unused
* Now abstract over the 'a', but float out the Num (C d a) constraint
because it does not 'really' mention a. (see exactTyVarsOfType)
The arg to foo becomes
- /\a -> \t -> t+t
+ \/\a -> \t -> t+t
* So we get a dict binding for Num (C d a), which is zonked to give
a = ()
quantification, so the floated dict will still have type (C d a).
Which renders this whole note moot; happily!]
-* Then the /\a abstraction has a zonked 'a' in it.
+* Then the \/\a abstraction has a zonked 'a' in it.
All very silly. I think its harmless to ignore the problem. We'll end up with
-a /\a in the final result but all the occurrences of a will be zonked to ()
+a \/\a in the final result but all the occurrences of a will be zonked to ()
+
+Note [Zonking to Skolem]
+~~~~~~~~~~~~~~~~~~~~~~~~
+We used to zonk quantified type variables to regular TyVars. However, this
+leads to problems. Consider this program from the regression test suite:
+
+ eval :: Int -> String -> String -> String
+ eval 0 root actual = evalRHS 0 root actual
+
+ evalRHS :: Int -> a
+ evalRHS 0 root actual = eval 0 root actual
+
+It leads to the deferral of an equality (wrapped in an implication constraint)
+
+ forall a. (String -> String -> String) ~ a
+
+which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
+In the meantime `a' is zonked and quantified to form `evalRHS's signature.
+This has the *side effect* of also zonking the `a' in the deferred equality
+(which at this point is being handed around wrapped in an implication
+constraint).
+
+Finally, the equality (with the zonked `a') will be handed back to the
+simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
+If we zonk `a' with a regular type variable, we will have this regular type
+variable now floating around in the simplifier, which in many places assumes to
+only see proper TcTyVars.
+
+We can avoid this problem by zonking with a skolem. The skolem is rigid
+(which we require for a quantified variable), but is still a TcTyVar that the
+simplifier knows how to deal with.
%************************************************************************
-- see zonkTcType, and zonkTcTypeToType
-> TcType
-> TcM Type
-zonkType unbound_var_fn ty
+zonkType zonk_tc_tyvar ty
= go ty
where
- go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations
-
- go (TyConApp tc tys) = mappM go tys `thenM` \ tys' ->
- returnM (TyConApp tc tys')
-
- go (PredTy p) = go_pred p `thenM` \ p' ->
- returnM (PredTy p')
-
- go (FunTy arg res) = go arg `thenM` \ arg' ->
- go res `thenM` \ res' ->
- returnM (FunTy arg' res')
-
- go (AppTy fun arg) = go fun `thenM` \ fun' ->
- go arg `thenM` \ arg' ->
- returnM (mkAppTy fun' arg')
+ go (TyConApp tc tys) = do tys' <- mapM go tys
+ return (TyConApp tc tys')
+
+ go (PredTy p) = do p' <- go_pred p
+ return (PredTy p')
+
+ go (FunTy arg res) = do arg' <- go arg
+ res' <- go res
+ return (FunTy arg' res')
+
+ go (AppTy fun arg) = do fun' <- go fun
+ arg' <- go arg
+ return (mkAppTy fun' arg')
-- NB the mkAppTy; we might have instantiated a
-- type variable to a type constructor, so we need
-- to pull the TyConApp to the top.
-- The two interesting cases!
- go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar unbound_var_fn tyvar
- | otherwise = return (TyVarTy tyvar)
+ go (TyVarTy tyvar) | isTcTyVar tyvar = zonk_tc_tyvar tyvar
+ | otherwise = liftM TyVarTy $
+ zonkTyVar zonk_tc_tyvar tyvar
-- Ordinary (non Tc) tyvars occur inside quantified types
- go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar )
- go ty `thenM` \ ty' ->
- returnM (ForAllTy tyvar ty')
+ go (ForAllTy tyvar ty) = ASSERT( isImmutableTyVar tyvar ) do
+ ty' <- go ty
+ tyvar' <- zonkTyVar zonk_tc_tyvar tyvar
+ return (ForAllTy tyvar' ty')
- go_pred (ClassP c tys) = mappM go tys `thenM` \ tys' ->
- returnM (ClassP c tys')
- go_pred (IParam n ty) = go ty `thenM` \ ty' ->
- returnM (IParam n ty')
- go_pred (EqPred ty1 ty2) = go ty1 `thenM` \ ty1' ->
- go ty2 `thenM` \ ty2' ->
- returnM (EqPred ty1' ty2')
+ go_pred (ClassP c tys) = do tys' <- mapM go tys
+ return (ClassP c tys')
+ go_pred (IParam n ty) = do ty' <- go ty
+ return (IParam n ty')
+ go_pred (EqPred ty1 ty2) = do ty1' <- go ty1
+ ty2' <- go ty2
+ return (EqPred ty1' ty2')
-zonk_tc_tyvar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable variable
+mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var
-> TcTyVar -> TcM TcType
-zonk_tc_tyvar unbound_var_fn tyvar
- | not (isMetaTyVar tyvar) -- Skolems
- = returnM (TyVarTy tyvar)
-
- | otherwise -- Mutables
- = do { cts <- readMetaTyVar tyvar
- ; case cts of
- Flexi -> unbound_var_fn tyvar -- Unbound meta type variable
- Indirect ty -> zonkType unbound_var_fn ty }
+mkZonkTcTyVar unbound_var_fn tyvar
+ = ASSERT( isTcTyVar tyvar )
+ case tcTyVarDetails tyvar of
+ SkolemTv {} -> return (TyVarTy tyvar)
+ FlatSkol ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty
+ MetaTv _ ref -> do { cts <- readMutVar ref
+ ; case cts of
+ Flexi -> unbound_var_fn tyvar
+ Indirect ty -> zonkType (mkZonkTcTyVar unbound_var_fn) ty }
+
+-- Zonk the kind of a non-TC tyvar in case it is a coercion variable
+-- (their kind contains types).
+zonkTyVar :: (TcTyVar -> TcM Type) -- What to do for a TcTyVar
+ -> TyVar -> TcM TyVar
+zonkTyVar zonk_tc_tyvar tv
+ | isCoVar tv
+ = do { kind <- zonkType zonk_tc_tyvar (tyVarKind tv)
+ ; return $ setTyVarKind tv kind }
+ | otherwise = return tv
\end{code}
zonkTcKindToKind :: TcKind -> TcM Kind
-- When zonking a TcKind to a kind, we need to instantiate kind variables,
-- Haskell specifies that * is to be used, so we follow that.
-zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
+zonkTcKindToKind k
+ = zonkType (mkZonkTcTyVar (\ _ -> return liftedTypeKind)) k
\end{code}
%************************************************************************
\begin{code}
checkValidType :: UserTypeCtxt -> Type -> TcM ()
-- Checks that the type is valid for the given context
-checkValidType ctxt ty
- = traceTc (text "checkValidType" <+> ppr ty) `thenM_`
- doptM Opt_GlasgowExts `thenM` \ gla_exts ->
+checkValidType ctxt ty = do
+ traceTc "checkValidType" (ppr ty)
+ unboxed <- xoptM Opt_UnboxedTuples
+ rank2 <- xoptM Opt_Rank2Types
+ rankn <- xoptM Opt_RankNTypes
+ polycomp <- xoptM Opt_PolymorphicComponents
let
- rank | gla_exts = Arbitrary
- | otherwise
- = case ctxt of -- Haskell 98
- GenPatCtxt -> Rank 0
- LamPatSigCtxt -> Rank 0
- BindPatSigCtxt -> Rank 0
- DefaultDeclCtxt-> Rank 0
- ResSigCtxt -> Rank 0
- TySynCtxt _ -> Rank 0
- ExprSigCtxt -> Rank 1
- FunSigCtxt _ -> Rank 1
- ConArgCtxt _ -> Rank 1 -- We are given the type of the entire
- -- constructor, hence rank 1
- ForSigCtxt _ -> Rank 1
- SpecInstCtxt -> Rank 1
+ gen_rank n | rankn = ArbitraryRank
+ | rank2 = Rank 2
+ | otherwise = Rank n
+ rank
+ = case ctxt of
+ DefaultDeclCtxt-> MustBeMonoType
+ ResSigCtxt -> MustBeMonoType
+ LamPatSigCtxt -> gen_rank 0
+ BindPatSigCtxt -> gen_rank 0
+ TySynCtxt _ -> gen_rank 0
+ GenPatCtxt -> gen_rank 1
+ -- This one is a bit of a hack
+ -- See the forall-wrapping in TcClassDcl.mkGenericInstance
+
+ ExprSigCtxt -> gen_rank 1
+ FunSigCtxt _ -> gen_rank 1
+ ConArgCtxt _ | polycomp -> gen_rank 2
+ -- We are given the type of the entire
+ -- constructor, hence rank 1
+ | otherwise -> gen_rank 1
+
+ ForSigCtxt _ -> gen_rank 1
+ SpecInstCtxt -> gen_rank 1
+ ThBrackCtxt -> gen_rank 1
actual_kind = typeKind ty
kind_ok = case ctxt of
- TySynCtxt _ -> True -- Any kind will do
- ResSigCtxt -> isSubOpenTypeKind actual_kind
- ExprSigCtxt -> isSubOpenTypeKind actual_kind
+ TySynCtxt _ -> True -- Any kind will do
+ ThBrackCtxt -> True -- Any kind will do
+ ResSigCtxt -> isSubOpenTypeKind actual_kind
+ ExprSigCtxt -> isSubOpenTypeKind actual_kind
GenPatCtxt -> isLiftedTypeKind actual_kind
ForSigCtxt _ -> isLiftedTypeKind actual_kind
- other -> isSubArgTypeKind actual_kind
+ _ -> isSubArgTypeKind actual_kind
- ubx_tup | 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
- -- Check that the thing has kind Type, and is lifted if necessary
- checkTc kind_ok (kindErr actual_kind) `thenM_`
+ ubx_tup = case ctxt of
+ TySynCtxt _ | unboxed -> UT_Ok
+ ExprSigCtxt | unboxed -> UT_Ok
+ ThBrackCtxt | unboxed -> UT_Ok
+ _ -> UT_NotOk
-- Check the internal validity of the type itself
- check_poly_type rank ubx_tup ty `thenM_`
+ check_type rank ubx_tup ty
+
+ -- Check that the thing has kind Type, and is lifted if necessary
+ -- Do this second, becuase we can't usefully take the kind of an
+ -- ill-formed type such as (a~Int)
+ checkTc kind_ok (kindErr actual_kind)
+
+ traceTc "checkValidType done" (ppr ty)
- traceTc (text "checkValidType done" <+> ppr ty)
+checkValidMonoType :: Type -> TcM ()
+checkValidMonoType ty = check_mono_type MustBeMonoType ty
\end{code}
\begin{code}
-data Rank = Rank Int | Arbitrary
-
-decRank :: Rank -> Rank
-decRank Arbitrary = Arbitrary
-decRank (Rank n) = Rank (n-1)
+data Rank = ArbitraryRank -- Any rank ok
+ | MustBeMonoType -- Monotype regardless of flags
+ | TyConArgMonoType -- Monotype but could be poly if -XImpredicativeTypes
+ | SynArgMonoType -- Monotype but could be poly if -XLiberalTypeSynonyms
+ | Rank Int -- Rank n, but could be more with -XRankNTypes
+
+decRank :: Rank -> Rank -- Function arguments
+decRank (Rank 0) = Rank 0
+decRank (Rank n) = Rank (n-1)
+decRank other_rank = other_rank
+
+nonZeroRank :: Rank -> Bool
+nonZeroRank ArbitraryRank = True
+nonZeroRank (Rank n) = n>0
+nonZeroRank _ = False
----------------------------------------
data UbxTupFlag = UT_Ok | UT_NotOk
- -- The "Ok" version means "ok if -fglasgow-exts is on"
+ -- The "Ok" version means "ok if UnboxedTuples is on"
----------------------------------------
-check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
-check_poly_type (Rank 0) ubx_tup ty
- = check_tau_type (Rank 0) ubx_tup ty
-
-check_poly_type rank ubx_tup ty
- | null tvs && null theta
- = check_tau_type rank ubx_tup ty
- | otherwise
- = do { check_valid_theta SigmaCtxt theta
- ; check_poly_type rank ubx_tup tau -- Allow foralls to right of arrow
- ; checkFreeness tvs theta
+check_mono_type :: Rank -> Type -> TcM () -- No foralls anywhere
+ -- No unlifted types of any kind
+check_mono_type rank ty
+ = do { check_type rank UT_NotOk ty
+ ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
+
+check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
+-- The args say what the *type context* requires, independent
+-- of *flag* settings. You test the flag settings at usage sites.
+--
+-- Rank is allowed rank for function args
+-- Rank 0 means no for-alls anywhere
+
+check_type rank ubx_tup ty
+ | not (null tvs && null theta)
+ = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
+ -- Reject e.g. (Maybe (?x::Int => Int)),
+ -- with a decent error message
+ ; check_valid_theta SigmaCtxt theta
+ ; check_type rank ubx_tup tau -- Allow foralls to right of arrow
; checkAmbiguity tvs theta (tyVarsOfType tau) }
where
(tvs, theta, tau) = tcSplitSigmaTy ty
+-- Naked PredTys should, I think, have been rejected before now
+check_type _ _ ty@(PredTy {})
+ = failWithTc (text "Predicate" <+> ppr ty <+> text "used as a type")
+
+check_type _ _ (TyVarTy _) = return ()
+
+check_type rank _ (FunTy arg_ty res_ty)
+ = do { check_type (decRank rank) UT_NotOk arg_ty
+ ; check_type rank UT_Ok res_ty }
+
+check_type rank _ (AppTy ty1 ty2)
+ = do { check_arg_type rank ty1
+ ; check_arg_type rank ty2 }
+
+check_type rank ubx_tup ty@(TyConApp tc tys)
+ | isSynTyCon tc
+ = do { -- Check that the synonym has enough args
+ -- This applies equally to open and closed synonyms
+ -- It's OK to have an *over-applied* type synonym
+ -- data Tree a b = ...
+ -- type Foo a = Tree [a]
+ -- f :: Foo a b -> ...
+ checkTc (tyConArity tc <= length tys) arity_msg
+
+ -- See Note [Liberal type synonyms]
+ ; liberal <- xoptM Opt_LiberalTypeSynonyms
+ ; if not liberal || isSynFamilyTyCon tc then
+ -- For H98 and synonym families, do check the type args
+ mapM_ (check_mono_type SynArgMonoType) tys
+
+ else -- In the liberal case (only for closed syns), expand then check
+ case tcView ty of
+ Just ty' -> check_type rank ubx_tup ty'
+ Nothing -> pprPanic "check_tau_type" (ppr ty)
+ }
+
+ | isUnboxedTupleTyCon tc
+ = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples
+ ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
+
+ ; impred <- xoptM Opt_ImpredicativeTypes
+ ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
+ -- c.f. check_arg_type
+ -- However, args are allowed to be unlifted, or
+ -- more unboxed tuples, so can't use check_arg_ty
+ ; mapM_ (check_type rank' UT_Ok) tys }
+
+ | otherwise
+ = mapM_ (check_arg_type rank) tys
+
+ where
+ ubx_tup_ok ub_tuples_allowed = case ubx_tup of
+ UT_Ok -> ub_tuples_allowed
+ _ -> False
+
+ n_args = length tys
+ tc_arity = tyConArity tc
+
+ arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
+ ubx_tup_msg = ubxArgTyErr ty
+
+check_type _ _ ty = pprPanic "check_type" (ppr ty)
+
----------------------------------------
-check_arg_type :: Type -> TcM ()
+check_arg_type :: Rank -> Type -> TcM ()
-- The sort of type that can instantiate a type variable,
-- or be the argument of a type constructor.
-- Not an unboxed tuple, but now *can* be a forall (since impredicativity)
-- But not in user code.
-- Anyway, they are dealt with by a special case in check_tau_type
-check_arg_type ty
- = check_poly_type Arbitrary UT_NotOk ty `thenM_`
- checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
-
-----------------------------------------
-check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
--- Rank is allowed rank for function args
--- No foralls otherwise
-
-check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
-check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty)
- -- Reject e.g. (Maybe (?x::Int => Int)), with a decent error message
-
--- Naked PredTys don't usually show up, but they can as a result of
--- {-# SPECIALISE instance Ord Char #-}
--- The Right Thing would be to fix the way that SPECIALISE instance pragmas
--- are handled, but the quick thing is just to permit PredTys here.
-check_tau_type rank ubx_tup (PredTy sty) = getDOpts `thenM` \ dflags ->
- check_pred_ty dflags TypeCtxt sty
-
-check_tau_type rank ubx_tup (TyVarTy _) = returnM ()
-check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
- = check_poly_type (decRank rank) UT_NotOk arg_ty `thenM_`
- check_poly_type rank UT_Ok res_ty
-
-check_tau_type rank ubx_tup (AppTy ty1 ty2)
- = check_arg_type ty1 `thenM_` check_arg_type ty2
+check_arg_type rank ty
+ = do { impred <- xoptM Opt_ImpredicativeTypes
+ ; let rank' = case rank of -- Predictive => must be monotype
+ MustBeMonoType -> MustBeMonoType -- Monotype, regardless
+ _other | impred -> ArbitraryRank
+ | otherwise -> TyConArgMonoType
+ -- Make sure that MustBeMonoType is propagated,
+ -- so that we don't suggest -XImpredicativeTypes in
+ -- (Ord (forall a.a)) => a -> a
+ -- and so that if it Must be a monotype, we check that it is!
-check_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 -> unless (isOpenTyCon tc -- No expansion if open
- && tyConArity tc <= length tys) $
- failWithTc arity_msg
-
- ; gla_exts <- doptM Opt_GlasgowExts
- ; if gla_exts && not (isOpenTyCon tc) then
- -- If -fglasgow-exts then don't check the type arguments of
- -- *closed* synonyms.
- -- This allows us to instantiate a synonym defn with a
- -- for-all type, or with a partially-applied type synonym.
- -- e.g. type T a b = a
- -- type S m = m ()
- -- f :: S (T Int)
- -- Here, T is partially applied, so it's illegal in H98.
- -- But if you expand S first, then T we get just
- -- f :: Int
- -- which is fine.
- returnM ()
- else
- -- For H98, do check the type args
- mappM_ check_arg_type tys
- }
-
- | isUnboxedTupleTyCon tc
- = 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
- = mappM_ check_arg_type tys
+ ; check_type rank' UT_NotOk ty
+ ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
+----------------------------------------
+forAllTyErr :: Rank -> Type -> SDoc
+forAllTyErr rank ty
+ = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
+ , suggestion ]
where
- ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
+ suggestion = case rank of
+ Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
+ TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
+ SynArgMonoType -> ptext (sLit "Perhaps you intended to use -XLiberalTypeSynonyms")
+ _ -> empty -- Polytype is always illegal
+
+unliftedArgErr, ubxArgTyErr :: Type -> SDoc
+unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
+ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
+
+kindErr :: Kind -> SDoc
+kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
+\end{code}
- n_args = length tys
- tc_arity = tyConArity tc
+Note [Liberal type synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If -XLiberalTypeSynonyms is on, expand closed type synonyms *before*
+doing validity checking. This allows us to instantiate a synonym defn
+with a for-all type, or with a partially-applied type synonym.
+ e.g. type T a b = a
+ type S m = m ()
+ f :: S (T Int)
+Here, T is partially applied, so it's illegal in H98. But if you
+expand S first, then T we get just
+ f :: Int
+which is fine.
- arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
- ubx_tup_msg = ubxArgTyErr ty
+IMPORTANT: suppose T is a type synonym. Then we must do validity
+checking on an appliation (T ty1 ty2)
-----------------------------------------
-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}
+ *either* before expansion (i.e. check ty1, ty2)
+ *or* after expansion (i.e. expand T ty1 ty2, and then check)
+ BUT NOT BOTH
+
+If we do both, we get exponential behaviour!!
+ data TIACons1 i r c = c i ::: r c
+ type TIACons2 t x = TIACons1 t (TIACons1 t x)
+ type TIACons3 t x = TIACons2 t (TIACons1 t x)
+ type TIACons4 t x = TIACons2 t (TIACons2 t x)
+ type TIACons7 t x = TIACons4 t (TIACons3 t x)
%************************************************************************
| InstThetaCtxt -- Context 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 TypeCtxt = ptext SLIT("the context of a type")
+pprSourceTyCtxt :: SourceTyCtxt -> SDoc
+pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
+pprSourceTyCtxt SigmaCtxt = ptext (sLit "the context of a polymorphic type")
+pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
+pprSourceTyCtxt InstThetaCtxt = ptext (sLit "the context of an instance declaration")
+pprSourceTyCtxt TypeCtxt = ptext (sLit "the context of a type")
\end{code}
\begin{code}
= addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
-------------------------
-check_valid_theta ctxt []
- = returnM ()
-check_valid_theta ctxt theta
- = getDOpts `thenM` \ dflags ->
- warnTc (notNull dups) (dupPredWarn dups) `thenM_`
- mappM_ (check_pred_ty dflags ctxt) theta
+check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
+check_valid_theta _ []
+ = return ()
+check_valid_theta ctxt theta = do
+ dflags <- getDOpts
+ warnTc (notNull dups) (dupPredWarn dups)
+ mapM_ (check_pred_ty dflags ctxt) theta
where
(_,dups) = removeDups tcCmpPred theta
-------------------------
+check_pred_ty :: DynFlags -> SourceTyCtxt -> PredType -> TcM ()
check_pred_ty dflags ctxt pred@(ClassP cls tys)
= do { -- Class predicates are valid in all contexts
; checkTc (arity == n_tys) arity_err
-- Check the form of the argument types
- ; mappM_ check_arg_type tys
+ ; mapM_ checkValidMonoType tys
; checkTc (check_class_pred_tys dflags ctxt tys)
(predTyVarErr pred $$ how_to_allow)
}
arity = classArity cls
n_tys = length tys
arity_err = arityErr "Class" class_name arity n_tys
- how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
+ how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
-check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
+
+check_pred_ty dflags _ pred@(EqPred ty1 ty2)
= do { -- Equational constraints are valid in all contexts if type
-- families are permitted
- ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
+ ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
-- Check the form of the argument types
- ; check_eq_arg_type ty1
- ; check_eq_arg_type ty2
+ ; checkValidMonoType ty1
+ ; checkValidMonoType ty2
}
- where
- check_eq_arg_type = check_poly_type (Rank 0) UT_NotOk
-check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
+check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
-- Implicit parameters only allowed in type
-- signatures; not in instance decls, superclasses etc
-- The reason for not allowing implicit params in instances is a bit
-- instance decl would show up two uses of ?x.
-- Catch-all
-check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
+check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
-------------------------
+check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
check_class_pred_tys dflags ctxt tys
= case ctxt of
TypeCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine
- InstThetaCtxt -> gla_exts || undecidable_ok || all tcIsTyVarTy tys
+ InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
-- Further checks on head and theta in
-- checkInstTermination
- other -> gla_exts || all tyvar_head tys
+ _ -> flexible_contexts || all tyvar_head tys
where
- gla_exts = dopt Opt_GlasgowExts dflags
- undecidable_ok = dopt Opt_AllowUndecidableInstances dflags
+ flexible_contexts = xopt Opt_FlexibleContexts dflags
+ undecidable_ok = xopt Opt_UndecidableInstances dflags
-------------------------
+tyvar_head :: Type -> Bool
tyvar_head ty -- Haskell 98 allows predicates of form
| tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
| otherwise -- where a is a type variable
don't need to check for ambiguity either, because the test can't fail
(see is_ambig).
+In addition, GHC insists that at least one type variable
+in each constraint is in V. So we disallow a type like
+ forall a. Eq b => b -> b
+even in a scope where b is in scope.
+
\begin{code}
checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
checkAmbiguity forall_tyvars theta tau_tyvars
- = mappM_ complain (filter is_ambig theta)
+ = mapM_ complain (filter is_ambig theta)
where
complain pred = addErrTc (ambigErr pred)
- extended_tau_vars = grow theta tau_tyvars
+ extended_tau_vars = growThetaTyVars theta tau_tyvars
- -- 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'
+ -- See Note [Implicit parameters and ambiguity] in TcSimplify
is_ambig pred = isClassPred pred &&
any ambig_var (varSetElems (tyVarsOfPred pred))
ambig_var ct_var = (ct_var `elem` forall_tyvars) &&
not (ct_var `elemVarSet` extended_tau_vars)
+ambigErr :: PredType -> SDoc
ambigErr pred
- = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
- nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
- ptext SLIT("must be reachable from the type after the '=>'"))]
+ = sep [ptext (sLit "Ambiguous constraint") <+> quotes (pprPred pred),
+ nest 2 (ptext (sLit "At least one of the forall'd type variables mentioned by the constraint") $$
+ ptext (sLit "must be reachable from the type after the '=>'"))]
\end{code}
-
-In addition, GHC insists that at least one type variable
-in each constraint is in V. So we disallow a type like
- forall a. Eq b => b -> b
-even in a scope where b is in scope.
+
+Note [Growing the tau-tvs using constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(growInstsTyVars insts tvs) is the result of extending the set
+ of tyvars tvs using all conceivable links from pred
+
+E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
+Then grow precs tvs = {a,b,c}
\begin{code}
-checkFreeness forall_tyvars theta
- = do { gla_exts <- doptM Opt_GlasgowExts
- ; if gla_exts then return () -- New! Oct06
- else mappM_ complain (filter is_free theta) }
- where
- is_free pred = not (isIPPred pred)
- && not (any bound_var (varSetElems (tyVarsOfPred pred)))
- bound_var ct_var = ct_var `elem` forall_tyvars
- complain pred = addErrTc (freeErr pred)
-
-freeErr pred
- = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
- ptext SLIT("are already in scope"),
- nest 4 (ptext SLIT("(at least one must be universally quantified here)"))
- ]
+growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
+-- See Note [Growing the tau-tvs using constraints]
+growThetaTyVars theta tvs
+ | null theta = tvs
+ | otherwise = fixVarSet mk_next tvs
+ where
+ mk_next tvs = foldr grow_one tvs theta
+ grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
+
+growPredTyVars :: TcPredType
+ -> TyVarSet -- The set to extend
+ -> TyVarSet -- TyVars of the predicate if it intersects
+ -- the set, or is implicit parameter
+growPredTyVars pred tvs
+ | IParam {} <- pred = pred_tvs -- See Note [Implicit parameters and ambiguity]
+ | pred_tvs `intersectsVarSet` tvs = pred_tvs
+ | otherwise = emptyVarSet
+ where
+ pred_tvs = tyVarsOfPred pred
\end{code}
+
+Note [Implicit parameters and ambiguity]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Only a *class* predicate can give rise to ambiguity
+An *implicit parameter* cannot. For example:
+ foo :: (?x :: [a]) => Int
+ foo = length ?x
+is fine. The call site will suppply a particular 'x'
+
+Furthermore, the type variables fixed by an implicit parameter
+propagate to the others. E.g.
+ foo :: (Show a, ?x::[a]) => Int
+ foo = show (?x++?x)
+The type of foo looks ambiguous. But it isn't, because at a call site
+we might have
+ let ?x = 5::Int in foo
+and all is well. In effect, implicit parameters are, well, parameters,
+so we can take their type variables into account as part of the
+"tau-tvs" stuff. This is done in the function 'FunDeps.grow'.
+
\begin{code}
+checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
checkThetaCtxt ctxt theta
- = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
- ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
+ = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
+ ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
-badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
-eqPredTyErr sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
+badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
+badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty
+eqPredTyErr sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty
$$
- parens (ptext SLIT("Use -ftype-families to permit this"))
-predTyVarErr pred = sep [ptext SLIT("Non type-variable argument"),
- nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
-dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
+ parens (ptext (sLit "Use -XTypeFamilies to permit this"))
+predTyVarErr pred = sep [ptext (sLit "Non type-variable argument"),
+ nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
+dupPredWarn :: [[PredType]] -> SDoc
+dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
+arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
arityErr kind name n m
- = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
- n_arguments <> comma, text "but has been given", int m]
+ = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
+ n_arguments <> comma, text "but has been given",
+ if m==0 then text "none" else int m]
where
- n_arguments | n == 0 = ptext SLIT("no arguments")
- | n == 1 = ptext SLIT("1 argument")
- | True = hsep [int n, ptext SLIT("arguments")]
+ n_arguments | n == 0 = ptext (sLit "no arguments")
+ | n == 1 = ptext (sLit "1 argument")
+ | True = hsep [int n, ptext (sLit "arguments")]
\end{code}
-
%************************************************************************
%* *
\subsection{Checking for a decent instance head type}
case getClassPredTys_maybe pred of {
Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
- Just (clas,tys) ->
+ Just (clas,tys) -> do
- getDOpts `thenM` \ dflags ->
- mappM_ check_arg_type tys `thenM_`
- check_inst_head dflags clas tys `thenM_`
- returnM (clas, tys)
+ dflags <- getDOpts
+ check_inst_head dflags clas tys
+ return (clas, tys)
}}
+check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
check_inst_head dflags clas tys
- -- If GlasgowExts then check at least one isn't a type variable
- | dopt Opt_GlasgowExts dflags
- = mapM_ check_one tys
-
- -- WITH HASKELL 98, MUST HAVE C (T a b c)
- | otherwise
- = checkTc (isSingleton tys && tcValidInstHeadTy first_ty)
- (instTypeErr (pprClassPred clas tys) head_shape_msg)
-
- where
- (first_ty : _) = tys
-
- head_shape_msg = parens (text "The instance type must be of form (T a1 ... an)" $$
- text "where T is not a synonym, and a1 ... an are distinct type *variables*")
-
+ = do { -- If GlasgowExts then check at least one isn't a type variable
+ ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
+ all tcInstHeadTyNotSynonym tys)
+ (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
+ ; checkTc (xopt Opt_FlexibleInstances dflags ||
+ all tcInstHeadTyAppAllTyVars tys)
+ (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
+ ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
+ isSingleton tys)
+ (instTypeErr (pprClassPred clas tys) head_one_type_msg)
+ -- May not contain type family applications
+ ; mapM_ checkTyFamFreeness tys
+
+ ; mapM_ checkValidMonoType tys
-- For now, I only allow tau-types (not polytypes) in
-- the head of an instance decl.
-- E.g. instance C (forall a. a->a) is rejected
-- One could imagine generalising that, but I'm not sure
-- what all the consequences might be
- check_one ty = do { check_tau_type (Rank 0) UT_NotOk ty
- ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
+ }
+ where
+ head_type_synonym_msg = parens (
+ text "All instance types must be of the form (T t1 ... tn)" $$
+ text "where T is not a synonym." $$
+ text "Use -XTypeSynonymInstances if you want to disable this.")
+
+ head_type_args_tyvars_msg = parens (vcat [
+ text "All instance types must be of the form (T a1 ... an)",
+ text "where a1 ... an are type *variables*,",
+ text "and each type variable appears at most once in the instance head.",
+ text "Use -XFlexibleInstances if you want to disable this."])
+
+ head_one_type_msg = parens (
+ text "Only one type can be given in an instance head." $$
+ text "Use -XMultiParamTypeClasses if you want to allow more.")
+
+instTypeErr :: SDoc -> SDoc -> SDoc
instTypeErr pp_ty msg
- = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
- nest 4 msg]
+ = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty,
+ nest 2 msg]
\end{code}
%* *
%************************************************************************
-
\begin{code}
-checkValidInstance :: [TyVar] -> ThetaType -> Class -> [TcType] -> TcM ()
-checkValidInstance tyvars theta clas inst_tys
- = do { gla_exts <- doptM Opt_GlasgowExts
- ; undecidable_ok <- doptM Opt_AllowUndecidableInstances
+checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type
+ -> TcM (Class, [TcType])
+checkValidInstance hs_type tyvars theta tau
+ = setSrcSpan (getLoc hs_type) $
+ do { (clas, inst_tys) <- setSrcSpan head_loc $
+ checkValidInstHead tau
+
+ ; undecidable_ok <- xoptM Opt_UndecidableInstances
; checkValidTheta InstThetaCtxt theta
; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
-- Check that instance inference will terminate (if we care)
- -- For Haskell 98, checkValidTheta has already done that
- ; when (gla_exts && not undecidable_ok) $
+ -- For Haskell 98 this will already have been done by checkValidTheta,
+ -- but as we may be using other extensions we need to check.
+ ; unless undecidable_ok $
mapM_ addErrTc (checkInstTermination inst_tys theta)
-- The Coverage Condition
; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
(instTypeErr (pprClassPred clas inst_tys) msg)
+
+ ; return (clas, inst_tys)
}
where
- msg = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"),
+ msg = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
undecidableMsg])
+
+ -- The location of the "head" of the instance
+ head_loc = case hs_type of
+ L _ (HsForAllTy _ _ _ (L loc _)) -> loc
+ L loc _ -> loc
\end{code}
Termination test: the so-called "Paterson conditions" (see Section 5 of
| otherwise
= Nothing
+predUndecErr :: PredType -> SDoc -> SDoc
predUndecErr pred msg = sep [msg,
- nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
+ nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
-nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
-smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
-undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
+nomoreMsg, smallerMsg, undecidableMsg :: SDoc
+nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
+smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
+undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
+\end{code}
+
+validDeivPred checks for OK 'deriving' context. See Note [Exotic
+derived instance contexts] in TcSimplify. However the predicate is
+here because it uses sizeTypes, fvTypes.
+
+\begin{code}
+validDerivPred :: PredType -> Bool
+validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
+ where fvs = fvTypes tys
+validDerivPred _ = False
+\end{code}
+
+%************************************************************************
+%* *
+ Checking type instance well-formedness and termination
+%* *
+%************************************************************************
+
+\begin{code}
+-- Check that a "type instance" is well-formed (which includes decidability
+-- unless -XUndecidableInstances is given).
+--
+checkValidTypeInst :: [Type] -> Type -> TcM ()
+checkValidTypeInst typats rhs
+ = do { -- left-hand side contains no type family applications
+ -- (vanilla synonyms are fine, though)
+ ; mapM_ checkTyFamFreeness typats
+
+ -- the right-hand side is a tau type
+ ; checkValidMonoType rhs
+
+ -- we have a decidable instance unless otherwise permitted
+ ; undecidable_ok <- xoptM Opt_UndecidableInstances
+ ; unless undecidable_ok $
+ mapM_ addErrTc (checkFamInst typats (tyFamInsts rhs))
+ }
+
+-- Make sure that each type family instance is
+-- (1) strictly smaller than the lhs,
+-- (2) mentions no type variable more often than the lhs, and
+-- (3) does not contain any further type family instances.
+--
+checkFamInst :: [Type] -- lhs
+ -> [(TyCon, [Type])] -- type family instances
+ -> [Message]
+checkFamInst lhsTys famInsts
+ = mapCatMaybes check famInsts
+ where
+ size = sizeTypes lhsTys
+ fvs = fvTypes lhsTys
+ check (tc, tys)
+ | not (all isTyFamFree tys)
+ = Just (famInstUndecErr famInst nestedMsg $$ parens undecidableMsg)
+ | not (null (fvTypes tys \\ fvs))
+ = Just (famInstUndecErr famInst nomoreVarMsg $$ parens undecidableMsg)
+ | size <= sizeTypes tys
+ = Just (famInstUndecErr famInst smallerAppMsg $$ parens undecidableMsg)
+ | otherwise
+ = Nothing
+ where
+ famInst = TyConApp tc tys
+
+-- Ensure that no type family instances occur in a type.
+--
+checkTyFamFreeness :: Type -> TcM ()
+checkTyFamFreeness ty
+ = checkTc (isTyFamFree ty) $
+ tyFamInstIllegalErr ty
+
+-- Check that a type does not contain any type family applications.
+--
+isTyFamFree :: Type -> Bool
+isTyFamFree = null . tyFamInsts
+
+-- Error messages
+
+tyFamInstIllegalErr :: Type -> SDoc
+tyFamInstIllegalErr ty
+ = hang (ptext (sLit "Illegal type synonym family application in instance") <>
+ colon) 2 $
+ ppr ty
+
+famInstUndecErr :: Type -> SDoc -> SDoc
+famInstUndecErr ty msg
+ = sep [msg,
+ nest 2 (ptext (sLit "in the type family application:") <+>
+ pprType ty)]
+
+nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
+nestedMsg = ptext (sLit "Nested type family application")
+nomoreVarMsg = ptext (sLit "Variable occurs more often than in instance head")
+smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{Auxiliary functions}
+%* *
+%************************************************************************
+
+\begin{code}
-- Free variables of a type, retaining repetitions, and expanding synonyms
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
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
sizeTypes :: [Type] -> Int
sizeTypes xs = sum (map sizeType xs)
+-- Size of a predicate
+--
+-- We are considering whether *class* constraints terminate
+-- Once we get into an implicit parameter or equality we
+-- can't get back to a class constraint, so it's safe
+-- to say "size 0". See Trac #4200.
sizePred :: PredType -> Int
sizePred (ClassP _ tys') = sizeTypes tys'
-sizePred (IParam _ ty) = sizeType ty
-sizePred (EqPred ty1 ty2) = sizeType ty1 + sizeType ty2
+sizePred (IParam {}) = 0
+sizePred (EqPred {}) = 0
\end{code}
projects / ghc-hetmet.git / blobdiff