%
% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 19921998
%
\section[TcType]{Types used in the typechecker}
This module provides the Type interface for frontend parts of the
compiler. These parts
* treat "source types" as opaque:
newtypes, and predicates are meaningful.
* look through usage types
The "tc" prefix is for "TypeChecker", because the type checker
is the principal client.
\begin{code}
module TcType (
TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
TcTyVar, TcTyVarSet, TcKind, TcCoVar,
UserTypeCtxt(..), pprUserTypeCtxt,
TcTyVarDetails(..), pprTcTyVarDetails,
MetaDetails(Flexi, Indirect), MetaInfo(..),
SkolemInfo(..), pprSkolTvBinding, pprSkolInfo,
isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy,
isSigTyVar, isExistentialTyVar, isTyConableTyVar,
metaTvRef,
isFlexi, isIndirect, isUnkSkol, isRuntimeUnkSkol,
mkPhiTy, mkSigmaTy,
tcView,
tcSplitForAllTys, tcSplitPhiTy, tcSplitPredFunTy_maybe,
tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, repSplitAppTy_maybe,
tcInstHeadTyNotSynonym, tcInstHeadTyAppAllTyVars,
tcGetTyVar_maybe, tcGetTyVar,
tcSplitSigmaTy, tcDeepSplitSigmaTy_maybe,
tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
eqKind,
isSigmaTy, isOverloadedTy, isRigidTy,
isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
isIntegerTy, isBoolTy, isUnitTy, isCharTy,
isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
isSynFamilyTyConApp,
deNoteType,
tyClsNamesOfType, tyClsNamesOfDFunHead,
getDFunTyKey,
getClassPredTys_maybe, getClassPredTys,
isClassPred, isTyVarClassPred, isEqPred,
mkClassPred, mkIPPred, tcSplitPredTy_maybe,
mkDictTy, evVarPred,
isPredTy, isDictTy, isDictLikeTy,
tcSplitDFunTy, tcSplitDFunHead, predTyUnique,
isIPPred,
isRefineableTy, isRefineablePred,
tidyType, tidyTypes,
tidyOpenType, tidyOpenTypes,
tidyTyVarBndr, tidyFreeTyVars,
tidyOpenTyVar, tidyOpenTyVars,
tidyTopType, tidyPred,
tidyKind, tidySkolemTyVar,
isFFIArgumentTy,
isFFIImportResultTy,
isFFIExportResultTy,
isFFIExternalTy,
isFFIDynArgumentTy,
isFFIDynResultTy,
isFFIPrimArgumentTy,
isFFIPrimResultTy,
isFFILabelTy,
isFFIDotnetTy,
isFFIDotnetObjTy,
isFFITy,
isFunPtrTy,
tcSplitIOType_maybe,
typeKind,
Kind,
unliftedTypeKind, liftedTypeKind, argTypeKind,
openTypeKind, mkArrowKind, mkArrowKinds,
isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind,
isSubArgTypeKind, isSubKind, splitKindFunTys, defaultKind,
kindVarRef, mkKindVar,
Type, PredType(..), ThetaType,
mkForAllTy, mkForAllTys,
mkFunTy, mkFunTys, zipFunTys,
mkTyConApp, mkAppTy, mkAppTys, applyTy, applyTys,
mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
TvSubst(..),
TvSubstEnv, emptyTvSubst, substEqSpec,
mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst,
mkTopTvSubst, notElemTvSubst, unionTvSubst,
getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, lookupTyVar,
extendTvSubst, extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
substTy, substTys, substTyWith, substTheta, substTyVar, substTyVars, substTyVarBndr,
isUnLiftedType,
isUnboxedTupleType,
isPrimitiveType,
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
tcTyVarsOfType, tcTyVarsOfTypes, tcTyVarsOfPred, exactTyVarsOfType,
exactTyVarsOfTypes,
pprKind, pprParendKind,
pprType, pprParendType, pprTypeApp, pprTyThingCategory,
pprPred, pprTheta, pprThetaArrow, pprClassPred
) where
#include "HsVersions.h"
import TypeRep
import DataCon
import Class
import Var
import ForeignCall
import VarSet
import Type
import Coercion
import TyCon
import HsExpr( HsMatchContext )
import DynFlags
import Name
import NameSet
import VarEnv
import PrelNames
import TysWiredIn
import BasicTypes
import Util
import Maybes
import ListSetOps
import Outputable
import FastString
import Data.List( mapAccumL )
import Data.IORef
\end{code}
%************************************************************************
%* *
\subsection{Types}
%* *
%************************************************************************
The type checker divides the generic Type world into the
following more structured beasts:
sigma ::= forall tyvars. phi
phi :: theta => rho
rho ::= sigma -> rho
| tau
tau ::= tyvar
| tycon tau_1 .. tau_n
| tau_1 tau_2
| tau_1 -> tau_2
\begin{code}
type TcTyVar = TyVar
type TcCoVar = CoVar
type TcType = Type
type TcPredType = PredType
type TcThetaType = ThetaType
type TcSigmaType = TcType
type TcRhoType = TcType
type TcTauType = TcType
type TcKind = Kind
type TcTyVarSet = TyVarSet
\end{code}
%************************************************************************
%* *
\subsection{TyVarDetails}
%* *
%************************************************************************
TyVarDetails gives extra info about type variables, used during type
checking. It's attached to mutable type variables only.
It's knottied back to Var.lhs. There is no reason in principle
why Var.lhs shouldn't actually have the definition, but it "belongs" here.
Note [Signature skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
Consider this
x :: [a]
y :: b
(x,y,z) = ([y,z], z, head x)
Here, x and y have type sigs, which go into the environment. We used to
instantiate their types with skolem constants, and push those types into
the RHS, so we'd typecheck the RHS with type
( [a*], b*, c )
where a*, b* are skolem constants, and c is an ordinary meta type varible.
The trouble is that the occurrences of z in the RHS force a* and b* to
be the *same*, so we can't make them into skolem constants that don't unify
with each other. Alas.
One solution would be insist that in the above defn the programmer uses
the same type variable in both type signatures. But that takes explanation.
The alternative (currently implemented) is to have a special kind of skolem
constant, SigTv, which can unify with other SigTvs. These are *not* treated
as righd for the purposes of GADTs. And they are used *only* for pattern
bindings and mutually recursive function bindings. See the function
TcBinds.tcInstSig, and its use_skols parameter.
\begin{code}
data TcTyVarDetails
= SkolemTv SkolemInfo
| FlatSkol TcType
| MetaTv MetaInfo (IORef MetaDetails)
data MetaDetails
= Flexi
| Indirect TcType
data MetaInfo
= TauTv
| SigTv Name
| TcsTv
data SkolemInfo
= SigSkol UserTypeCtxt
| ClsSkol Class
| InstSkol
| FamInstSkol
| PatSkol
DataCon
(HsMatchContext Name)
| ArrowSkol
| IPSkol [IPName Name]
| RuleSkol RuleName
| GenSkol TcType
| RuntimeUnkSkol
| NoScSkol
| UnkSkol
data UserTypeCtxt
= FunSigCtxt Name
| ExprSigCtxt
| ConArgCtxt Name
| TySynCtxt Name
| GenPatCtxt
| LamPatSigCtxt
| BindPatSigCtxt
| ResSigCtxt
| ForSigCtxt Name
| DefaultDeclCtxt
| SpecInstCtxt
| ThBrackCtxt
mkKindName :: Unique -> Name
mkKindName unique = mkSystemName unique kind_var_occ
kindVarRef :: KindVar -> IORef MetaDetails
kindVarRef tc =
ASSERT ( isTcTyVar tc )
case tcTyVarDetails tc of
MetaTv TauTv ref -> ref
_ -> pprPanic "kindVarRef" (ppr tc)
mkKindVar :: Unique -> IORef MetaDetails -> KindVar
mkKindVar u r
= mkTcTyVar (mkKindName u)
tySuperKind
(MetaTv TauTv r)
kind_var_occ :: OccName
kind_var_occ = mkOccName tvName "k"
\end{code}
%************************************************************************
%* *
Prettyprinting
%* *
%************************************************************************
\begin{code}
pprTcTyVarDetails :: TcTyVarDetails -> SDoc
pprTcTyVarDetails (SkolemTv _) = ptext (sLit "sk")
pprTcTyVarDetails (FlatSkol {}) = ptext (sLit "fsk")
pprTcTyVarDetails (MetaTv TauTv _) = ptext (sLit "tau")
pprTcTyVarDetails (MetaTv TcsTv _) = ptext (sLit "tcs")
pprTcTyVarDetails (MetaTv (SigTv _) _) = ptext (sLit "sig")
pprUserTypeCtxt :: UserTypeCtxt -> SDoc
pprUserTypeCtxt (FunSigCtxt n) = ptext (sLit "the type signature for") <+> quotes (ppr n)
pprUserTypeCtxt ExprSigCtxt = ptext (sLit "an expression type signature")
pprUserTypeCtxt (ConArgCtxt c) = ptext (sLit "the type of the constructor") <+> quotes (ppr c)
pprUserTypeCtxt (TySynCtxt c) = ptext (sLit "the RHS of the type synonym") <+> quotes (ppr c)
pprUserTypeCtxt GenPatCtxt = ptext (sLit "the type pattern of a generic definition")
pprUserTypeCtxt ThBrackCtxt = ptext (sLit "a Template Haskell quotation [t|...|]")
pprUserTypeCtxt LamPatSigCtxt = ptext (sLit "a pattern type signature")
pprUserTypeCtxt BindPatSigCtxt = ptext (sLit "a pattern type signature")
pprUserTypeCtxt ResSigCtxt = ptext (sLit "a result type signature")
pprUserTypeCtxt (ForSigCtxt n) = ptext (sLit "the foreign declaration for") <+> quotes (ppr n)
pprUserTypeCtxt DefaultDeclCtxt = ptext (sLit "a type in a `default' declaration")
pprUserTypeCtxt SpecInstCtxt = ptext (sLit "a SPECIALISE instance pragma")
pprSkolTvBinding :: TcTyVar -> SDoc
pprSkolTvBinding tv
= ASSERT ( isTcTyVar tv )
quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
where
ppr_details (SkolemTv info) = ppr_skol info
ppr_details (FlatSkol {}) = ptext (sLit "is a flattening type variable")
ppr_details (MetaTv (SigTv n) _) = ptext (sLit "is bound by the type signature for")
<+> quotes (ppr n)
ppr_details (MetaTv _ _) = ptext (sLit "is a meta type variable")
ppr_skol UnkSkol = ptext (sLit "is an unknown type variable")
ppr_skol RuntimeUnkSkol = ptext (sLit "is an unknown runtime type")
ppr_skol info = sep [ptext (sLit "is a rigid type variable bound by"),
sep [pprSkolInfo info,
nest 2 (ptext (sLit "at") <+> ppr (getSrcLoc tv))]]
instance Outputable SkolemInfo where
ppr = pprSkolInfo
pprSkolInfo :: SkolemInfo -> SDoc
pprSkolInfo (SigSkol ctxt) = pprUserTypeCtxt ctxt
pprSkolInfo (IPSkol ips) = ptext (sLit "the implicit-parameter bindings for")
<+> pprWithCommas ppr ips
pprSkolInfo (ClsSkol cls) = ptext (sLit "the class declaration for") <+> quotes (ppr cls)
pprSkolInfo InstSkol = ptext (sLit "the instance declaration")
pprSkolInfo NoScSkol = ptext (sLit "the instance declaration (self)")
pprSkolInfo FamInstSkol = ptext (sLit "the family instance declaration")
pprSkolInfo (RuleSkol name) = ptext (sLit "the RULE") <+> doubleQuotes (ftext name)
pprSkolInfo ArrowSkol = ptext (sLit "the arrow form")
pprSkolInfo (PatSkol dc _) = sep [ ptext (sLit "a pattern with constructor")
, ppr dc <+> dcolon <+> ppr (dataConUserType dc) ]
pprSkolInfo (GenSkol ty) = sep [ ptext (sLit "the polymorphic type")
, quotes (ppr ty) ]
pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) ptext (sLit "UnkSkol")
pprSkolInfo RuntimeUnkSkol = WARN( True, text "pprSkolInfo: RuntimeUnkSkol" ) ptext (sLit "RuntimeUnkSkol")
instance Outputable MetaDetails where
ppr Flexi = ptext (sLit "Flexi")
ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty
\end{code}
%************************************************************************
%* *
\subsection{TidyType}
%* *
%************************************************************************
\begin{code}
tidyTyVarBndr :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
tidyTyVarBndr env@(tidy_env, subst) tyvar
= case tidyOccName tidy_env (getOccName name) of
(tidy', occ') -> ((tidy', subst'), tyvar'')
where
subst' = extendVarEnv subst tyvar tyvar''
tyvar' = setTyVarName tyvar name'
name' = tidyNameOcc name occ'
tyvar'' | isCoVar tyvar = setTyVarKind tyvar' kind'
| otherwise = tyvar'
kind' = tidyType env (tyVarKind tyvar)
where
name = tyVarName tyvar
tidyFreeTyVars :: TidyEnv -> TyVarSet -> TidyEnv
tidyFreeTyVars env tyvars = fst (tidyOpenTyVars env (varSetElems tyvars))
tidyOpenTyVars :: TidyEnv -> [TyVar] -> (TidyEnv, [TyVar])
tidyOpenTyVars env tyvars = mapAccumL tidyOpenTyVar env tyvars
tidyOpenTyVar :: TidyEnv -> TyVar -> (TidyEnv, TyVar)
tidyOpenTyVar env@(_, subst) tyvar
= case lookupVarEnv subst tyvar of
Just tyvar' -> (env, tyvar')
Nothing -> tidyTyVarBndr env tyvar
tidyType :: TidyEnv -> Type -> Type
tidyType env@(_, subst) ty
= go ty
where
go (TyVarTy tv) = case lookupVarEnv subst tv of
Nothing -> expand tv
Just tv' -> expand tv'
go (TyConApp tycon tys) = let args = map go tys
in args `seqList` TyConApp tycon args
go (PredTy sty) = PredTy (tidyPred env sty)
go (AppTy fun arg) = (AppTy $! (go fun)) $! (go arg)
go (FunTy fun arg) = (FunTy $! (go fun)) $! (go arg)
go (ForAllTy tv ty) = ForAllTy tvp $! (tidyType envp ty)
where
(envp, tvp) = tidyTyVarBndr env tv
expand tv | isTcTyVar tv
, FlatSkol ty <- tcTyVarDetails tv
= go ty
| otherwise
= TyVarTy tv
tidyTypes :: TidyEnv -> [Type] -> [Type]
tidyTypes env tys = map (tidyType env) tys
tidyPred :: TidyEnv -> PredType -> PredType
tidyPred env (IParam n ty) = IParam n (tidyType env ty)
tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys)
tidyPred env (EqPred ty1 ty2) = EqPred (tidyType env ty1) (tidyType env ty2)
tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
tidyOpenType env ty
= (env', tidyType env' ty)
where
env' = tidyFreeTyVars env (tyVarsOfType ty)
tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
tidyTopType :: Type -> Type
tidyTopType ty = tidyType emptyTidyEnv ty
tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
tidySkolemTyVar env tv
= ASSERT( isTcTyVar tv && (isSkolemTyVar tv || isSigTyVar tv ) )
(env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)
where
(env1, info1) = case tcTyVarDetails tv of
SkolemTv info -> (env1, SkolemTv info')
where
(env1, info') = tidy_skol_info env info
info -> (env, info)
tidy_skol_info env (GenSkol ty) = (env1, GenSkol ty1)
where
(env1, ty1) = tidyOpenType env ty
tidy_skol_info env info = (env, info)
tidyKind :: TidyEnv -> Kind -> (TidyEnv, Kind)
tidyKind env k = tidyOpenType env k
\end{code}
%************************************************************************
%* *
Predicates
%* *
%************************************************************************
\begin{code}
isImmutableTyVar :: TyVar -> Bool
isImmutableTyVar tv
| isTcTyVar tv = isSkolemTyVar tv
| otherwise = True
isTyConableTyVar, isSkolemTyVar, isExistentialTyVar,
isMetaTyVar :: TcTyVar -> Bool
isTyConableTyVar tv
= ASSERT( isTcTyVar tv)
case tcTyVarDetails tv of
MetaTv (SigTv _) _ -> False
_ -> True
isSkolemTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
SkolemTv {} -> True
FlatSkol {} -> True
MetaTv {} -> False
isExistentialTyVar tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
SkolemTv (PatSkol {}) -> True
_ -> False
isMetaTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv _ _ -> True
_ -> False
isMetaTyVarTy :: TcType -> Bool
isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
isMetaTyVarTy _ = False
isSigTyVar :: Var -> Bool
isSigTyVar tv
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
MetaTv (SigTv _) _ -> True
_ -> False
metaTvRef :: TyVar -> IORef MetaDetails
metaTvRef tv
= ASSERT2( isTcTyVar tv, ppr tv )
case tcTyVarDetails tv of
MetaTv _ ref -> ref
_ -> pprPanic "metaTvRef" (ppr tv)
isFlexi, isIndirect :: MetaDetails -> Bool
isFlexi Flexi = True
isFlexi _ = False
isIndirect (Indirect _) = True
isIndirect _ = False
isRuntimeUnkSkol :: TyVar -> Bool
isRuntimeUnkSkol x | isTcTyVar x
, SkolemTv RuntimeUnkSkol <- tcTyVarDetails x
= True
| otherwise = False
isUnkSkol :: TyVar -> Bool
isUnkSkol x | isTcTyVar x
, SkolemTv UnkSkol <- tcTyVarDetails x = True
| otherwise = False
\end{code}
%************************************************************************
%* *
\subsection{Tau, sigma and rho}
%* *
%************************************************************************
\begin{code}
mkSigmaTy :: [TyVar] -> [PredType] -> Type -> Type
mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
mkPhiTy :: [PredType] -> Type -> Type
mkPhiTy theta ty = foldr (\p r -> mkFunTy (mkPredTy p) r) ty theta
\end{code}
@isTauTy@ tests for nested foralls. It should not be called on a boxy type.
\begin{code}
isTauTy :: Type -> Bool
isTauTy ty | Just ty' <- tcView ty = isTauTy ty'
isTauTy (TyVarTy _) = True
isTauTy (TyConApp tc tys) = all isTauTy tys && isTauTyCon tc
isTauTy (AppTy a b) = isTauTy a && isTauTy b
isTauTy (FunTy a b) = isTauTy a && isTauTy b
isTauTy (PredTy _) = True
isTauTy _ = False
isTauTyCon :: TyCon -> Bool
isTauTyCon tc
| isClosedSynTyCon tc = isTauTy (snd (synTyConDefn tc))
| otherwise = True
isRigidTy :: TcType -> Bool
isRigidTy ty = all isImmutableTyVar (varSetElems (tcTyVarsOfType ty))
isRefineableTy :: TcType -> (Bool,Bool)
isRefineableTy ty = (null tc_tvs, all isImmutableTyVar tc_tvs)
where
tc_tvs = varSetElems (tcTyVarsOfType ty)
isRefineablePred :: TcPredType -> Bool
isRefineablePred pred = not (null tc_tvs) && all isImmutableTyVar tc_tvs
where
tc_tvs = varSetElems (tcTyVarsOfPred pred)
getDFunTyKey :: Type -> OccName
getDFunTyKey ty | Just ty' <- tcView ty = getDFunTyKey ty'
getDFunTyKey (TyVarTy tv) = getOccName tv
getDFunTyKey (TyConApp tc _) = getOccName tc
getDFunTyKey (AppTy fun _) = getDFunTyKey fun
getDFunTyKey (FunTy _ _) = getOccName funTyCon
getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
\end{code}
%************************************************************************
%* *
\subsection{Expanding and splitting}
%* *
%************************************************************************
These tcSplit functions are like their nonTc analogues, but
a) they do not look through newtypes
b) they do not look through PredTys
However, they are nonmonadic and do not follow through mutable type
variables. It's up to you to make sure this doesn't matter.
\begin{code}
tcSplitForAllTys :: Type -> ([TyVar], Type)
tcSplitForAllTys ty = split ty ty []
where
split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
split _ (ForAllTy tv ty) tvs
| not (isCoVar tv) = split ty ty (tv:tvs)
split orig_ty _ tvs = (reverse tvs, orig_ty)
tcIsForAllTy :: Type -> Bool
tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
tcIsForAllTy (ForAllTy tv _) = not (isCoVar tv)
tcIsForAllTy _ = False
tcSplitPredFunTy_maybe :: Type -> Maybe (PredType, Type)
tcSplitPredFunTy_maybe ty | Just ty' <- tcView ty = tcSplitPredFunTy_maybe ty'
tcSplitPredFunTy_maybe (ForAllTy tv ty)
| isCoVar tv = Just (coVarPred tv, ty)
tcSplitPredFunTy_maybe (FunTy arg res)
| Just p <- tcSplitPredTy_maybe arg = Just (p, res)
tcSplitPredFunTy_maybe _
= Nothing
tcSplitPhiTy :: Type -> (ThetaType, Type)
tcSplitPhiTy ty
= split ty []
where
split ty ts
= case tcSplitPredFunTy_maybe ty of
Just (pred, ty) -> split ty (pred:ts)
Nothing -> (reverse ts, ty)
tcSplitSigmaTy :: Type -> ([TyVar], ThetaType, Type)
tcSplitSigmaTy ty = case tcSplitForAllTys ty of
(tvs, rho) -> case tcSplitPhiTy rho of
(theta, tau) -> (tvs, theta, tau)
tcDeepSplitSigmaTy_maybe
:: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType)
tcDeepSplitSigmaTy_maybe ty
| Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty
, Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty
= Just (arg_ty:arg_tys, tvs, theta, rho)
| (tvs, theta, rho) <- tcSplitSigmaTy ty
, not (null tvs && null theta)
= Just ([], tvs, theta, rho)
| otherwise = Nothing
tcTyConAppTyCon :: Type -> TyCon
tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
Just (tc, _) -> tc
Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
tcTyConAppArgs :: Type -> [Type]
tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
Just (_, args) -> args
Nothing -> pprPanic "tcTyConAppArgs" (pprType ty)
tcSplitTyConApp :: Type -> (TyCon, [Type])
tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
Just stuff -> stuff
Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
tcSplitTyConApp_maybe ty | Just ty' <- tcView ty = tcSplitTyConApp_maybe ty'
tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
tcSplitTyConApp_maybe _ = Nothing
tcSplitFunTys :: Type -> ([Type], Type)
tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
Nothing -> ([], ty)
Just (arg,res) -> (arg:args, res')
where
(args,res') = tcSplitFunTys res
tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
tcSplitFunTy_maybe ty | Just ty' <- tcView ty = tcSplitFunTy_maybe ty'
tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
tcSplitFunTy_maybe _ = Nothing
tcSplitFunTysN
:: TcRhoType
-> Arity
-> ([TcSigmaType],
TcSigmaType)
tcSplitFunTysN ty n_args
| n_args == 0
= ([], ty)
| Just (arg,res) <- tcSplitFunTy_maybe ty
= case tcSplitFunTysN res (n_args 1) of
(args, res) -> (arg:args, res)
| otherwise
= ([], ty)
tcSplitFunTy :: Type -> (Type, Type)
tcSplitFunTy ty = expectJust "tcSplitFunTy" (tcSplitFunTy_maybe ty)
tcFunArgTy :: Type -> Type
tcFunArgTy ty = fst (tcSplitFunTy ty)
tcFunResultTy :: Type -> Type
tcFunResultTy ty = snd (tcSplitFunTy ty)
tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
tcSplitAppTy_maybe ty = repSplitAppTy_maybe ty
tcSplitAppTy :: Type -> (Type, Type)
tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
Just stuff -> stuff
Nothing -> pprPanic "tcSplitAppTy" (pprType ty)
tcSplitAppTys :: Type -> (Type, [Type])
tcSplitAppTys ty
= go ty []
where
go ty args = case tcSplitAppTy_maybe ty of
Just (ty', arg) -> go ty' (arg:args)
Nothing -> (ty,args)
tcGetTyVar_maybe :: Type -> Maybe TyVar
tcGetTyVar_maybe ty | Just ty' <- tcView ty = tcGetTyVar_maybe ty'
tcGetTyVar_maybe (TyVarTy tv) = Just tv
tcGetTyVar_maybe _ = Nothing
tcGetTyVar :: String -> Type -> TyVar
tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
tcIsTyVarTy :: Type -> Bool
tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
tcSplitDFunTy :: Type -> ([TyVar], Class, [Type])
tcSplitDFunTy ty
= case tcSplitForAllTys ty of { (tvs, rho) ->
case tcSplitDFunHead (drop_pred_tys rho) of { (clas, tys) ->
(tvs, clas, tys) }}
where
drop_pred_tys ty | Just ty' <- tcView ty = drop_pred_tys ty'
drop_pred_tys (ForAllTy tv ty) = ASSERT( isCoVar tv ) drop_pred_tys ty
drop_pred_tys (FunTy _ ty) = drop_pred_tys ty
drop_pred_tys ty = ty
tcSplitDFunHead :: Type -> (Class, [Type])
tcSplitDFunHead tau
= case tcSplitPredTy_maybe tau of
Just (ClassP clas tys) -> (clas, tys)
_ -> pprPanic "tcSplitDFunHead" (ppr tau)
tcInstHeadTyNotSynonym :: Type -> Bool
tcInstHeadTyNotSynonym ty
= case ty of
TyConApp tc _ -> not (isSynTyCon tc)
_ -> True
tcInstHeadTyAppAllTyVars :: Type -> Bool
tcInstHeadTyAppAllTyVars ty
= case ty of
TyConApp _ tys -> ok tys
FunTy arg res -> ok [arg, res]
_ -> False
where
ok tys = equalLength tvs tys && hasNoDups tvs
where
tvs = mapCatMaybes get_tv tys
get_tv (TyVarTy tv) = Just tv
get_tv _ = Nothing
\end{code}
%************************************************************************
%* *
\subsection{Predicate types}
%* *
%************************************************************************
\begin{code}
evVarPred :: EvVar -> PredType
evVarPred var
= case tcSplitPredTy_maybe (varType var) of
Just pred -> pred
Nothing -> pprPanic "evVarPred" (ppr var <+> ppr (varType var))
tcSplitPredTy_maybe :: Type -> Maybe PredType
tcSplitPredTy_maybe ty | Just ty' <- tcView ty = tcSplitPredTy_maybe ty'
tcSplitPredTy_maybe (PredTy p) = Just p
tcSplitPredTy_maybe _ = Nothing
predTyUnique :: PredType -> Unique
predTyUnique (IParam n _) = getUnique (ipNameName n)
predTyUnique (ClassP clas _) = getUnique clas
predTyUnique (EqPred a b) = pprPanic "predTyUnique" (ppr (EqPred a b))
\end{code}
\begin{code}
mkClassPred :: Class -> [Type] -> PredType
mkClassPred clas tys = ClassP clas tys
isClassPred :: PredType -> Bool
isClassPred (ClassP _ _) = True
isClassPred _ = False
isTyVarClassPred :: PredType -> Bool
isTyVarClassPred (ClassP _ tys) = all tcIsTyVarTy tys
isTyVarClassPred _ = False
getClassPredTys_maybe :: PredType -> Maybe (Class, [Type])
getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
getClassPredTys_maybe _ = Nothing
getClassPredTys :: PredType -> (Class, [Type])
getClassPredTys (ClassP clas tys) = (clas, tys)
getClassPredTys _ = panic "getClassPredTys"
mkDictTy :: Class -> [Type] -> Type
mkDictTy clas tys = mkPredTy (ClassP clas tys)
isDictLikeTy :: Type -> Bool
isDictLikeTy ty | Just ty' <- tcView ty = isDictTy ty'
isDictLikeTy (PredTy p) = isClassPred p
isDictLikeTy (TyConApp tc tys)
| isTupleTyCon tc = all isDictLikeTy tys
isDictLikeTy _ = False
\end{code}
Note [Dictionarylike types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Being "dictionary-like" means either a dictionary type or a tuple thereof.
In GHC 6.10 we build implication constraints which construct such tuples,
and if we land up with a binding
t :: (C [a], Eq [a])
t = blah
then we want to treat t as cheap under "-fdicts-cheap" for example.
(Implication constraints are normally inlined, but sadly not if the
occurrence is itself inside an INLINE function! Until we revise the
handling of implication constraints, that is.) This turned out to
be important in getting good arities in DPH code. Example:
class C a
class D a where { foo :: a -> a }
instance C a => D (Maybe a) where { foo x = x }
bar :: (C a, C b) => a -> b -> (Maybe a, Maybe b)
bar x y = (foo (Just x), foo (Just y))
Then 'bar' should jolly well have arity 4 (two dicts, two args), but
we ended up with something like
bar = __inline_me__ (\d1,d2. let t :: (D (Maybe a), D (Maybe b)) = ...
in \x,y. <blah>)
This is all a bit adhoc; eg it relies on knowing that implication
constraints build tuples.
\begin{code}
mkIPPred :: IPName Name -> Type -> PredType
mkIPPred ip ty = IParam ip ty
isIPPred :: PredType -> Bool
isIPPred (IParam _ _) = True
isIPPred _ = False
\end{code}
\begin{code}
substEqSpec :: TvSubst -> [(TyVar,Type)] -> [(TcType,TcType)]
substEqSpec subst eq_spec = [ (substTyVar subst tv, substTy subst ty)
| (tv,ty) <- eq_spec]
\end{code}
%************************************************************************
%* *
\subsection{Predicates}
%* *
%************************************************************************
isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
any foralls. E.g.
f :: (?x::Int) => Int -> Int
\begin{code}
isSigmaTy :: Type -> Bool
isSigmaTy ty | Just ty' <- tcView ty = isSigmaTy ty'
isSigmaTy (ForAllTy _ _) = True
isSigmaTy (FunTy a _) = isPredTy a
isSigmaTy _ = False
isOverloadedTy :: Type -> Bool
isOverloadedTy ty | Just ty' <- tcView ty = isOverloadedTy ty'
isOverloadedTy (ForAllTy tv ty) = isCoVar tv || isOverloadedTy ty
isOverloadedTy (FunTy a _) = isPredTy a
isOverloadedTy _ = False
isPredTy :: Type -> Bool
isPredTy ty | Just ty' <- tcView ty = isPredTy ty'
isPredTy (PredTy _) = True
isPredTy _ = False
\end{code}
\begin{code}
isFloatTy, isDoubleTy, isIntegerTy, isIntTy, isWordTy, isBoolTy,
isUnitTy, isCharTy :: Type -> Bool
isFloatTy = is_tc floatTyConKey
isDoubleTy = is_tc doubleTyConKey
isIntegerTy = is_tc integerTyConKey
isIntTy = is_tc intTyConKey
isWordTy = is_tc wordTyConKey
isBoolTy = is_tc boolTyConKey
isUnitTy = is_tc unitTyConKey
isCharTy = is_tc charTyConKey
isStringTy :: Type -> Bool
isStringTy ty
= case tcSplitTyConApp_maybe ty of
Just (tc, [arg_ty]) -> tc == listTyCon && isCharTy arg_ty
_ -> False
is_tc :: Unique -> Type -> Bool
is_tc uniq ty = case tcSplitTyConApp_maybe ty of
Just (tc, _) -> uniq == getUnique tc
Nothing -> False
\end{code}
\begin{code}
isSynFamilyTyConApp :: TcTauType -> Bool
isSynFamilyTyConApp (TyConApp tc tys) = isSynFamilyTyCon tc &&
length tys == tyConArity tc
isSynFamilyTyConApp _other = False
\end{code}
%************************************************************************
%* *
\subsection{Misc}
%* *
%************************************************************************
\begin{code}
deNoteType :: Type -> Type
deNoteType ty | Just ty' <- tcView ty = deNoteType ty'
deNoteType ty = ty
\end{code}
\begin{code}
tcTyVarsOfType :: Type -> TcTyVarSet
tcTyVarsOfType (TyVarTy tv) = if isTcTyVar tv then unitVarSet tv
else emptyVarSet
tcTyVarsOfType (TyConApp _ tys) = tcTyVarsOfTypes tys
tcTyVarsOfType (PredTy sty) = tcTyVarsOfPred sty
tcTyVarsOfType (FunTy arg res) = tcTyVarsOfType arg `unionVarSet` tcTyVarsOfType res
tcTyVarsOfType (AppTy fun arg) = tcTyVarsOfType fun `unionVarSet` tcTyVarsOfType arg
tcTyVarsOfType (ForAllTy tyvar ty) = (tcTyVarsOfType ty `delVarSet` tyvar)
`unionVarSet` tcTyVarsOfTyVar tyvar
tcTyVarsOfTyVar :: TcTyVar -> TyVarSet
tcTyVarsOfTyVar tv | isCoVar tv = tcTyVarsOfType (tyVarKind tv)
| otherwise = emptyVarSet
tcTyVarsOfTypes :: [Type] -> TyVarSet
tcTyVarsOfTypes tys = foldr (unionVarSet.tcTyVarsOfType) emptyVarSet tys
tcTyVarsOfPred :: PredType -> TyVarSet
tcTyVarsOfPred (IParam _ ty) = tcTyVarsOfType ty
tcTyVarsOfPred (ClassP _ tys) = tcTyVarsOfTypes tys
tcTyVarsOfPred (EqPred ty1 ty2) = tcTyVarsOfType ty1 `unionVarSet` tcTyVarsOfType ty2
\end{code}
Note [Silly type synonym]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
type T a = Int
What are the free tyvars of (T x)? Empty, of course!
Here's the example that Ralf Laemmel showed me:
foo :: (forall a. C u a -> C u a) -> u
mappend :: Monoid u => u -> u -> u
bar :: Monoid u => u
bar = foo (\t -> t `mappend` t)
We have to generalise at the arg to f, and we don't
want to capture the constraint (Monad (C u a)) because
it appears to mention a. Pretty silly, but it was useful to him.
exactTyVarsOfType is used by the type checker to figure out exactly
which type variables are mentioned in a type. It's also used in the
smartapp checking code
On the other hand, consider a *toplevel* definition
f = (\x -> x) :: T a -> T a
If we don't abstract over 'a' it'll get fixed to GHC.Prim.Any, and then
if we have an application like (f "x") we get a confusing error message
involving Any. So the conclusion is this: when generalising
at top level use tyVarsOfType
in nested bindings use exactTyVarsOfType
See Trac #1813 for example.
\begin{code}
exactTyVarsOfType :: TcType -> TyVarSet
exactTyVarsOfType ty
= go ty
where
go ty | Just ty' <- tcView ty = go ty'
go (TyVarTy tv) = unitVarSet tv
go (TyConApp _ tys) = exactTyVarsOfTypes tys
go (PredTy ty) = go_pred ty
go (FunTy arg res) = go arg `unionVarSet` go res
go (AppTy fun arg) = go fun `unionVarSet` go arg
go (ForAllTy tyvar ty) = delVarSet (go ty) tyvar
`unionVarSet` go_tv tyvar
go_pred (IParam _ ty) = go ty
go_pred (ClassP _ tys) = exactTyVarsOfTypes tys
go_pred (EqPred ty1 ty2) = go ty1 `unionVarSet` go ty2
go_tv tyvar | isCoVar tyvar = go (tyVarKind tyvar)
| otherwise = emptyVarSet
exactTyVarsOfTypes :: [TcType] -> TyVarSet
exactTyVarsOfTypes tys = foldr (unionVarSet . exactTyVarsOfType) emptyVarSet tys
\end{code}
Find the free tycons and classes of a type. This is used in the front
end of the compiler.
\begin{code}
tyClsNamesOfType :: Type -> NameSet
tyClsNamesOfType (TyVarTy _) = emptyNameSet
tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
tyClsNamesOfType (PredTy (IParam _ ty)) = tyClsNamesOfType ty
tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
tyClsNamesOfType (PredTy (EqPred ty1 ty2)) = tyClsNamesOfType ty1 `unionNameSets` tyClsNamesOfType ty2
tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
tyClsNamesOfType (ForAllTy _ ty) = tyClsNamesOfType ty
tyClsNamesOfTypes :: [Type] -> NameSet
tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
tyClsNamesOfDFunHead :: Type -> NameSet
tyClsNamesOfDFunHead dfun_ty
= case tcSplitSigmaTy dfun_ty of
(_, _, head_ty) -> tyClsNamesOfType head_ty
\end{code}
%************************************************************************
%* *
\subsection[TysWiredInexttype]{External types}
%* *
%************************************************************************
The compiler's foreign function interface supports the passing of a
restricted set of types as arguments and results (the restricting factor
being the )
\begin{code}
tcSplitIOType_maybe :: Type -> Maybe (TyCon, Type, CoercionI)
tcSplitIOType_maybe ty
= case tcSplitTyConApp_maybe ty of
Just (io_tycon, [io_res_ty])
| io_tycon `hasKey` ioTyConKey
-> Just (io_tycon, io_res_ty, IdCo ty)
Just (tc, tys)
| not (isRecursiveTyCon tc)
, Just (ty, co1) <- instNewTyCon_maybe tc tys
-> case tcSplitIOType_maybe ty of
Nothing -> Nothing
Just (tc, ty', co2) -> Just (tc, ty', co1 `mkTransCoI` co2)
_ -> Nothing
isFFITy :: Type -> Bool
isFFITy ty = checkRepTyCon legalFFITyCon ty
isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
isFFIArgumentTy dflags safety ty
= checkRepTyCon (legalOutgoingTyCon dflags safety) ty
isFFIExternalTy :: Type -> Bool
isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
isFFIImportResultTy :: DynFlags -> Type -> Bool
isFFIImportResultTy dflags ty
= checkRepTyCon (legalFIResultTyCon dflags) ty
isFFIExportResultTy :: Type -> Bool
isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
isFFIDynArgumentTy :: Type -> Bool
isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
isFFIDynResultTy :: Type -> Bool
isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
isFFILabelTy :: Type -> Bool
isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey]
isFFIPrimArgumentTy :: DynFlags -> Type -> Bool
isFFIPrimArgumentTy dflags ty
= checkRepTyCon (legalFIPrimArgTyCon dflags) ty
isFFIPrimResultTy :: DynFlags -> Type -> Bool
isFFIPrimResultTy dflags ty
= checkRepTyCon (legalFIPrimResultTyCon dflags) ty
isFFIDotnetTy :: DynFlags -> Type -> Bool
isFFIDotnetTy dflags ty
= checkRepTyCon (\ tc -> (legalFIResultTyCon dflags tc ||
isFFIDotnetObjTy ty || isStringTy ty)) ty
isFFIDotnetObjTy :: Type -> Bool
isFFIDotnetObjTy ty
= checkRepTyCon check_tc t_ty
where
(_, t_ty) = tcSplitForAllTys ty
check_tc tc = getName tc == objectTyConName
isFunPtrTy :: Type -> Bool
isFunPtrTy = checkRepTyConKey [funPtrTyConKey]
checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
checkRepTyCon check_tc ty
= go [] ty
where
go rec_nts ty
| Just (tc,tys) <- splitTyConApp_maybe ty
= case carefullySplitNewType_maybe rec_nts tc tys of
Just (rec_nts', ty') -> go rec_nts' ty'
Nothing -> check_tc tc
| otherwise
= False
checkRepTyConKey :: [Unique] -> Type -> Bool
checkRepTyConKey keys
= checkRepTyCon (\tc -> tyConUnique tc `elem` keys)
\end{code}
These chaps do the work; they are not exported
\begin{code}
legalFEArgTyCon :: TyCon -> Bool
legalFEArgTyCon tc
= boxedMarshalableTyCon tc
legalFIResultTyCon :: DynFlags -> TyCon -> Bool
legalFIResultTyCon dflags tc
| tc == unitTyCon = True
| otherwise = marshalableTyCon dflags tc
legalFEResultTyCon :: TyCon -> Bool
legalFEResultTyCon tc
| tc == unitTyCon = True
| otherwise = boxedMarshalableTyCon tc
legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
legalOutgoingTyCon dflags _ tc
= marshalableTyCon dflags tc
legalFFITyCon :: TyCon -> Bool
legalFFITyCon tc
= isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon
marshalableTyCon :: DynFlags -> TyCon -> Bool
marshalableTyCon dflags tc
= (xopt Opt_UnliftedFFITypes dflags
&& isUnLiftedTyCon tc
&& not (isUnboxedTupleTyCon tc)
&& case tyConPrimRep tc of
VoidRep -> False
_ -> True)
|| boxedMarshalableTyCon tc
boxedMarshalableTyCon :: TyCon -> Bool
boxedMarshalableTyCon tc
= getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
, int32TyConKey, int64TyConKey
, wordTyConKey, word8TyConKey, word16TyConKey
, word32TyConKey, word64TyConKey
, floatTyConKey, doubleTyConKey
, ptrTyConKey, funPtrTyConKey
, charTyConKey
, stablePtrTyConKey
, boolTyConKey
]
legalFIPrimArgTyCon :: DynFlags -> TyCon -> Bool
legalFIPrimArgTyCon dflags tc
= xopt Opt_UnliftedFFITypes dflags
&& isUnLiftedTyCon tc
&& not (isUnboxedTupleTyCon tc)
legalFIPrimResultTyCon :: DynFlags -> TyCon -> Bool
legalFIPrimResultTyCon dflags tc
= xopt Opt_UnliftedFFITypes dflags
&& isUnLiftedTyCon tc
&& (isUnboxedTupleTyCon tc
|| case tyConPrimRep tc of
VoidRep -> False
_ -> True)
\end{code}
Note [Marshalling VoidRep]
~~~~~~~~~~~~~~~~~~~~~~~~~~
We don't treat State# (whose PrimRep is VoidRep) as marshalable.
In turn that means you can't write
foreign import foo :: Int -> State# RealWorld
Reason: the back end falls over with panic "primRepHint:VoidRep";
and there is no compelling reason to permit it