-
+%
+% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%
\section[TcType]{Types used in the typechecker}
newtypes, and predicates are meaningful.
* look through usage types
-The "tc" prefix is for "typechechecker", because the type checker
+The "tc" prefix is for "TypeChecker", because the type checker
is the principal client.
\begin{code}
---------------------------------
-- Misc type manipulators
- deNoteType, classesOfTheta,
+ deNoteType,
tyClsNamesOfType, tyClsNamesOfDFunHead,
getDFunTyKey,
isClassPred, isTyVarClassPred, isEqPred,
mkDictTy, tcSplitPredTy_maybe,
isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique,
- mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
- dataConsStupidTheta, isRefineableTy,
+ mkClassPred, isInheritablePred, isIPPred,
+ dataConsStupidTheta, isRefineableTy, isRefineablePred,
---------------------------------
-- Foreign import and export
--------------------------------
-- Rexported from Type
Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
- unliftedTypeKind, liftedTypeKind, unboxedTypeKind, argTypeKind,
+ unliftedTypeKind, liftedTypeKind, argTypeKind,
openTypeKind, mkArrowKind, mkArrowKinds,
isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind,
isSubArgTypeKind, isSubKind, defaultKind,
#include "HsVersions.h"
-- friends:
-import TypeRep ( Type(..), funTyCon, Kind ) -- friend
-
-import Type ( -- Re-exports
- tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
- tyVarsOfTheta, Kind, PredType(..), KindVar,
- ThetaType, isUnliftedTypeKind, unliftedTypeKind,
--- ??? unboxedTypeKind,
- argTypeKind,
- liftedTypeKind, openTypeKind, mkArrowKind,
- tySuperKind, isLiftedTypeKind,
- mkArrowKinds, mkForAllTy, mkForAllTys,
- defaultKind, isSubArgTypeKind, isSubOpenTypeKind,
- mkFunTy, mkFunTys, zipFunTys,
- mkTyConApp, mkAppTy,
- mkAppTys, applyTy, applyTys,
- mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy,
- mkPredTys, isUnLiftedType,
- isUnboxedTupleType, isPrimitiveType,
- splitTyConApp_maybe,
- tidyTopType, tidyType, tidyPred, tidyTypes,
- tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
- tidyTyVarBndr, tidyOpenTyVar,
- tidyOpenTyVars, tidyKind,
- isSubKind, tcView,
-
- tcEqType, tcEqTypes, tcCmpType, tcCmpTypes,
- tcEqPred, tcCmpPred, tcEqTypeX, eqKind,
-
- TvSubst(..),
- TvSubstEnv, emptyTvSubst, mkTvSubst, zipTyEnv,
- mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst,
- getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope,
- extendTvSubst, extendTvSubstList, isInScope, notElemTvSubst,
- substTy, substTys, substTyWith, substTheta,
- substTyVar, substTyVarBndr, substPred, lookupTyVar,
-
- typeKind, repType, coreView, repSplitAppTy_maybe,
- pprKind, pprParendKind,
- pprType, pprParendType, pprTyThingCategory,
- pprPred, pprTheta, pprThetaArrow, pprClassPred
- )
-import TyCon ( TyCon, isUnLiftedTyCon, isSynTyCon, synTyConDefn, tyConUnique )
-import DataCon ( DataCon, dataConStupidTheta, dataConResTys )
-import Class ( Class )
-import Var ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails )
-import ForeignCall ( Safety, DNType(..) )
-import Unify ( tcMatchTys )
+import TypeRep
+import DataCon
+import Class
+import Var
+import ForeignCall
+import Unify
import VarSet
+import Type
+import TyCon
-- others:
-import DynFlags ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
-import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc, mkSystemName )
+import DynFlags
+import CoreSyn
+import Name
import NameSet
-import VarEnv ( TidyEnv )
-import OccName ( OccName, mkDictOcc, mkOccName, tvName )
-import PrelNames -- Lots (e.g. in isFFIArgumentTy)
-import TysWiredIn ( unitTyCon, charTyCon, listTyCon )
-import BasicTypes ( IPName(..), Arity, ipNameName )
-import SrcLoc ( SrcLoc, SrcSpan )
-import Util ( snocView, equalLength )
-import Maybes ( maybeToBool, expectJust, mapCatMaybes )
-import ListSetOps ( hasNoDups )
-import List ( nubBy )
+import VarEnv
+import OccName
+import PrelNames
+import TysWiredIn
+import BasicTypes
+import Util
+import Maybes
+import ListSetOps
import Outputable
-import DATA_IOREF
+
+import Data.List
+import Data.IORef
\end{code}
-- For a BoxTv, this type must be non-boxy
-- For a TauTv, this type must be a tau-type
+-- Generally speaking, SkolemInfo should not contain location info
+-- that is contained in the Name of the tyvar with this SkolemInfo
data SkolemInfo
= SigSkol UserTypeCtxt -- A skolem that is created by instantiating
-- a programmer-supplied type signature
-- The rest are for non-scoped skolems
| ClsSkol Class -- Bound at a class decl
- | InstSkol Id -- Bound at an instance decl
+ | InstSkol -- Bound at an instance decl
+ | FamInstSkol -- Bound at a family instance decl
| PatSkol DataCon -- An existential type variable bound by a pattern for
- SrcSpan -- a data constructor with an existential type. E.g.
+ -- a data constructor with an existential type. E.g.
-- data T = forall a. Eq a => MkT a
-- f (MkT x) = ...
-- The pattern MkT x will allocate an existential type
-- variable for 'a'.
- | ArrowSkol SrcSpan -- An arrow form (see TcArrows)
+ | ArrowSkol -- An arrow form (see TcArrows)
+ | RuleSkol RuleName -- The LHS of a RULE
| GenSkol [TcTyVar] -- Bound when doing a subsumption check for
TcType -- (forall tvs. ty)
- SrcSpan
| UnkSkol -- Unhelpful info (until I improve it)
-------------------------------------
-- UserTypeCtxt describes the places where a
-- programmer-written type signature can occur
+-- Like SkolemInfo, no location info
data UserTypeCtxt
= FunSigCtxt Name -- Function type signature
-- Also used for types in SPECIALISE pragmas
| ResSigCtxt -- Result type sig
-- f x :: t = ....
| ForSigCtxt Name -- Foreign inport or export signature
- | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
| DefaultDeclCtxt -- Types in a default declaration
| SpecInstCtxt -- SPECIALISE instance pragma
kindVarRef :: KindVar -> IORef MetaDetails
kindVarRef tc =
+ ASSERT ( isTcTyVar tc )
case tcTyVarDetails tc of
MetaTv TauTv ref -> ref
other -> pprPanic "kindVarRef" (ppr tc)
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 (RuleSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
pprUserTypeCtxt DefaultDeclCtxt = ptext SLIT("a type in a `default' declaration")
pprUserTypeCtxt SpecInstCtxt = ptext SLIT("a SPECIALISE instance pragma")
(env1, info') = tidy_skol_info env info
info -> (env, info)
- tidy_skol_info env (GenSkol tvs ty loc) = (env2, GenSkol tvs1 ty1 loc)
+ tidy_skol_info env (GenSkol tvs ty) = (env2, GenSkol tvs1 ty1)
where
(env1, tvs1) = tidyOpenTyVars env tvs
(env2, ty1) = tidyOpenType env1 ty
-- Print info about the binding of a skolem tyvar,
-- or nothing if we don't have anything useful to say
pprSkolTvBinding tv
- = ppr_details (tcTyVarDetails tv)
+ = ASSERT ( isTcTyVar tv )
+ ppr_details (tcTyVarDetails tv)
where
ppr_details (MetaTv TauTv _) = quotes (ppr tv) <+> ptext SLIT("is a meta type variable")
ppr_details (MetaTv BoxTv _) = quotes (ppr tv) <+> ptext SLIT("is a boxy type variable")
ppr_details (MetaTv (SigTv info) _) = ppr_skol info
ppr_details (SkolemTv info) = ppr_skol info
- ppr_skol UnkSkol = empty -- Unhelpful; omit
- ppr_skol (SigSkol ctxt) = sep [quotes (ppr tv) <+> ptext SLIT("is bound by") <+> pprUserTypeCtxt ctxt,
- nest 2 (ptext SLIT("at") <+> ppr (getSrcLoc tv))]
- ppr_skol info = quotes (ppr tv) <+> pprSkolInfo info
+ ppr_skol UnkSkol = empty -- Unhelpful; omit
+ ppr_skol info = quotes (ppr tv) <+> ptext SLIT("is bound by")
+ <+> sep [pprSkolInfo info, nest 2 (ptext SLIT("at") <+> ppr (getSrcLoc tv))]
pprSkolInfo :: SkolemInfo -> SDoc
-pprSkolInfo (SigSkol ctxt) = ptext SLIT("is bound by") <+> pprUserTypeCtxt ctxt
-pprSkolInfo (ClsSkol cls) = ptext SLIT("is bound by the class declaration for") <+> quotes (ppr cls)
-pprSkolInfo (InstSkol df) = ptext SLIT("is bound by the instance declaration at") <+> ppr (getSrcLoc df)
-pprSkolInfo (ArrowSkol loc) = ptext SLIT("is bound by the arrow form at") <+> ppr loc
-pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("is bound by the pattern for") <+> quotes (ppr dc),
- nest 2 (ptext SLIT("at") <+> ppr loc)]
-pprSkolInfo (GenSkol tvs ty loc) = sep [sep [ptext SLIT("is bound by the polymorphic type"),
- nest 2 (quotes (ppr (mkForAllTys tvs ty)))],
- nest 2 (ptext SLIT("at") <+> ppr loc)]
--- UnkSkol, SigSkol
+pprSkolInfo (SigSkol ctxt) = pprUserTypeCtxt ctxt
+pprSkolInfo (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
+pprSkolInfo InstSkol = ptext SLIT("the instance declaration")
+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("the constructor") <+> quotes (ppr dc)]
+pprSkolInfo (GenSkol tvs ty) = sep [ptext SLIT("the polymorphic type"),
+ nest 2 (quotes (ppr (mkForAllTys tvs ty)))]
+
+-- UnkSkol
-- For type variables the others are dealt with by pprSkolTvBinding.
-- For Insts, these cases should not happen
pprSkolInfo UnkSkol = panic "UnkSkol"
isExistentialTyVar tv -- Existential type variable, bound by a pattern
= ASSERT( isTcTyVar tv )
case tcTyVarDetails tv of
- SkolemTv (PatSkol _ _) -> True
- other -> False
+ SkolemTv (PatSkol {}) -> True
+ other -> False
isMetaTyVar tv
= ASSERT2( isTcTyVar tv, ppr tv )
mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
mkPhiTy :: [PredType] -> Type -> Type
-mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
+mkPhiTy theta ty = foldr (\p r -> mkFunTy (mkPredTy p) r) ty theta
\end{code}
@isTauTy@ tests for nested for-alls. It should not be called on a boxy type.
isTauTyCon :: TyCon -> Bool
-- Returns False for type synonyms whose expansion is a polytype
-isTauTyCon tc | isSynTyCon tc = isTauTy (snd (synTyConDefn tc))
- | otherwise = True
+isTauTyCon tc
+ | isSynTyCon tc && not (isOpenTyCon tc) = isTauTy (snd (synTyConDefn tc))
+ | otherwise = True
---------------
isBoxyTy :: TcType -> Bool
isRigidTy :: TcType -> Bool
-- A type is rigid if it has no meta type variables in it
-isRigidTy ty = all isSkolemTyVar (varSetElems (tcTyVarsOfType ty))
+isRigidTy ty = all isImmutableTyVar (varSetElems (tcTyVarsOfType ty))
isRefineableTy :: TcType -> Bool
-- A type should have type refinements applied to it if it has
-- free type variables, and they are all rigid
-isRefineableTy ty = not (null tc_tvs) && all isSkolemTyVar tc_tvs
+isRefineableTy ty = not (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 -- Get some string from a type, to be used to
-- construct a dictionary function name
tcSplitForAllTys ty = split ty ty []
where
split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
- split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
- split orig_ty t tvs = (reverse tvs, orig_ty)
+ split orig_ty (ForAllTy tv ty) tvs
+ | not (isCoVar tv) = split ty ty (tv:tvs)
+ split orig_ty t tvs = (reverse tvs, orig_ty)
tcIsForAllTy ty | Just ty' <- tcView ty = tcIsForAllTy ty'
-tcIsForAllTy (ForAllTy tv ty) = True
+tcIsForAllTy (ForAllTy tv ty) = not (isCoVar tv)
tcIsForAllTy t = False
tcSplitPhiTy :: Type -> (ThetaType, Type)
tcSplitPhiTy ty = split ty ty []
where
split orig_ty ty tvs | Just ty' <- tcView ty = split orig_ty ty' tvs
+
+ split orig_ty (ForAllTy tv ty) ts
+ | isCoVar tv = split ty ty (eq_pred:ts)
+ where
+ PredTy eq_pred = tyVarKind tv
split orig_ty (FunTy arg res) ts
| Just p <- tcSplitPredTy_maybe arg = split res res (p:ts)
split orig_ty ty ts = (reverse ts, orig_ty)
-----------------------
tcTyConAppTyCon :: Type -> TyCon
-tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
+tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
+ Just (tc, _) -> tc
+ Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
tcTyConAppArgs :: Type -> [Type]
-tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
+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
predTyUnique :: PredType -> Unique
predTyUnique (IParam n _) = getUnique (ipNameName n)
predTyUnique (ClassP clas tys) = getUnique clas
-
-mkPredName :: Unique -> SrcLoc -> PredType -> Name
-mkPredName uniq loc (ClassP cls tys) = mkInternalName uniq (mkDictOcc (getOccName cls)) loc
-mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameName ip)) loc
\end{code}
getClassPredTys (ClassP clas tys) = (clas, tys)
getClassPredTys other = panic "getClassPredTys"
-isEqPred :: PredType -> Bool
-isEqPred (EqPred {}) = True
-isEqPred _ = False
-
mkDictTy :: Class -> [Type] -> Type
mkDictTy clas tys = mkPredTy (ClassP clas tys)
-- but it doesn't need to be quantified over the Num a dictionary
-- which can be free in g's rhs, and shared by both calls to g
isInheritablePred (ClassP _ _) = True
-isInheritablePred other = False
-
-isLinearPred :: TcPredType -> Bool
-isLinearPred (IParam (Linear n) _) = True
-isLinearPred other = False
+isInheritablePred (EqPred _ _) = True
+isInheritablePred other = False
\end{code}
--------------------- Equality predicates ---------------------------------
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
+tcTyVarsOfType (ForAllTy tyvar ty) = (tcTyVarsOfType ty `delVarSet` tyvar)
+ `unionVarSet` tcTyVarsOfTyVar tyvar
-- We do sometimes quantify over skolem TcTyVars
+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 (IParam _ ty) = tcTyVarsOfType ty
+tcTyVarsOfPred (ClassP _ tys) = tcTyVarsOfTypes tys
+tcTyVarsOfPred (EqPred ty1 ty2) = tcTyVarsOfType ty1 `unionVarSet` tcTyVarsOfType ty2
\end{code}
Note [Silly type synonym]
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 (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
tyClsNamesOfType (NoteTy _ ty2) = tyClsNamesOfType ty2
tyClsNamesOfType (PredTy (IParam n 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 tyvar ty) = tyClsNamesOfType ty
tyClsNamesOfDFunHead dfun_ty
= case tcSplitSigmaTy dfun_ty of
(tvs,_,head_ty) -> tyClsNamesOfType head_ty
-
-classesOfTheta :: ThetaType -> [Class]
--- Looks just for ClassP things; maybe it should check
-classesOfTheta preds = [ c | ClassP c _ <- preds ]
\end{code}
projects / ghc-hetmet.git / blobdiff