module TcType (
--------------------------------
-- Types
- TauType, RhoType, SigmaType,
+ TcType, TcSigmaType, TcPhiType, TcTauType, TcPredType, TcThetaType,
+ TcTyVar, TcTyVarSet, TcKind,
+
+ --------------------------------
+ -- TyVarDetails
+ TyVarDetails(..), isUserTyVar, isSkolemTyVar, isHoleTyVar,
+ tyVarBindingInfo,
--------------------------------
-- Builders
---------------------------------
-- Predicates.
-- Again, newtypes are opaque
- tcEqType, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
- isQualifiedTy, isOverloadedTy,
+ tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
+ isSigmaTy, isOverloadedTy,
isDoubleTy, isFloatTy, isIntTy,
isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy,
isTauTy, tcIsTyVarTy, tcIsForAllTy,
isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
mkDictTy, tcSplitPredTy_maybe, predTyUnique,
isDictTy, tcSplitDFunTy, predTyUnique,
- mkClassPred, inheritablePred, isIPPred, mkPredName,
+ mkClassPred, inheritablePred, isIPPred, mkPredName,
---------------------------------
-- Foreign import and export
-- friends:
import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
-import Type ( mkUTyM, unUTy ) -- Used locally
import Type ( -- Re-exports
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
- Kind, Type, TauType, SourceType(..), PredType, ThetaType,
+ Kind, Type, SourceType(..), PredType, ThetaType,
unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
mkFunTy, mkFunTys, zipFunTys,
)
import TyCon ( TyCon, isUnLiftedTyCon )
import Class ( classHasFDs, Class )
-import Var ( TyVar, tyVarKind )
+import Var ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
import ForeignCall ( Safety, playSafe )
import VarEnv
import VarSet
-- others:
import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
-import Name ( Name, NamedThing(..), mkLocalName )
+import Name ( Name, NamedThing(..), mkLocalName, getSrcLoc )
import OccName ( OccName, mkDictOcc )
import NameSet
import PrelNames -- Lots (e.g. in isFFIArgumentTy)
import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
+import BasicTypes ( ipNameName )
import Unique ( Unique, Uniquable(..) )
import SrcLoc ( SrcLoc )
import Util ( cmpList, thenCmp, equalLength )
%************************************************************************
%* *
-\subsection{Tau, sigma and rho}
+\subsection{Types}
%* *
%************************************************************************
+The type checker divides the generic Type world into the
+following more structured beasts:
+
+sigma ::= forall tyvars. theta => phi
+ -- A sigma type is a qualified type
+ --
+ -- Note that even if 'tyvars' is empty, theta
+ -- may not be: e.g. (?x::Int) => Int
+
+ -- Note that 'sigma' is in prenex form:
+ -- all the foralls are at the front.
+ -- A 'phi' type has no foralls to the right of
+ -- an arrow
+
+phi ::= sigma -> phi
+ | tau
+
+-- A 'tau' type has no quantification anywhere
+-- Note that the args of a type constructor must be taus
+tau ::= tyvar
+ | tycon tau_1 .. tau_n
+ | tau_1 tau_2
+ | tau_1 -> tau_2
+
+-- In all cases, a (saturated) type synonym application is legal,
+-- provided it expands to the required form.
+
+
\begin{code}
-type SigmaType = Type
-type RhoType = Type
+type SigmaType = Type
+type PhiType = Type
+type TauType = Type
+\end{code}
+
+\begin{code}
+type TcTyVar = TyVar -- Might be a mutable tyvar
+type TcTyVarSet = TyVarSet
+
+type TcType = Type -- A TcType can have mutable type variables
+ -- Invariant on ForAllTy in TcTypes:
+ -- forall a. T
+ -- a cannot occur inside a MutTyVar in T; that is,
+ -- T is "flattened" before quantifying over a
+
+type TcPredType = PredType
+type TcThetaType = ThetaType
+type TcSigmaType = TcType
+type TcPhiType = TcType
+type TcTauType = TcType
+type TcKind = TcType
+\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 knot-tied back to Var.lhs. There is no reason in principle
+why Var.lhs shouldn't actually have the definition, but it "belongs" here.
+
+\begin{code}
+data TyVarDetails
+ = HoleTv -- Used *only* by the type checker when passing in a type
+ -- variable that should be side-effected to the result type.
+ -- Always has kind openTypeKind.
+ -- Never appears in types
+
+ | SigTv -- Introduced when instantiating a type signature,
+ -- prior to checking that the defn of a fn does
+ -- have the expected type. Should not be instantiated.
+ --
+ -- f :: forall a. a -> a
+ -- f = e
+ -- When checking e, with expected type (a->a), we
+ -- should not instantiate a
+
+ | ClsTv -- Scoped type variable introduced by a class decl
+ -- class C a where ...
+
+ | InstTv -- Ditto, but instance decl
+
+ | PatSigTv -- Scoped type variable, introduced by a pattern
+ -- type signature
+ -- \ x::a -> e
+
+ | VanillaTv -- Everything else
+
+isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible
+isUserTyVar tv = case mutTyVarDetails tv of
+ VanillaTv -> False
+ other -> True
+
+isSkolemTyVar :: TcTyVar -> Bool
+isSkolemTyVar tv = case mutTyVarDetails tv of
+ SigTv -> True
+ oteher -> False
+
+isHoleTyVar :: TcTyVar -> Bool
+-- NB: the hole might be filled in by now, and this
+-- function does not check for that
+isHoleTyVar tv = ASSERT( isMutTyVar tv )
+ case mutTyVarDetails tv of
+ HoleTv -> True
+ other -> False
+
+tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
+tyVarBindingInfo tv
+ | isMutTyVar tv
+ = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
+ ptext SLIT("at") <+> ppr (getSrcLoc tv)]
+ | otherwise
+ = empty
+ where
+ details SigTv = ptext SLIT("type signature")
+ details ClsTv = ptext SLIT("class declaration")
+ details InstTv = ptext SLIT("instance declaration")
+ details PatSigTv = ptext SLIT("pattern type signature")
+ details HoleTv = ptext SLIT("//hole//") -- Should not happen
+ details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection{Tau, sigma and rho}
+%* *
+%************************************************************************
+
+\begin{code}
mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
mkRhoTy :: [SourceType] -> Type -> Type
-mkRhoTy theta ty = UASSERT2( not (isUTy ty), pprType ty )
- foldr (\p r -> FunTy (mkUTyM (mkPredTy p)) (mkUTyM r)) ty theta
-
+mkRhoTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
\end{code}
isTauTy (FunTy a b) = isTauTy a && isTauTy b
isTauTy (SourceTy p) = True -- Don't look through source types
isTauTy (NoteTy _ ty) = isTauTy ty
-isTauTy (UsageTy _ ty) = isTauTy ty
isTauTy other = False
\end{code}
getDFunTyKey (NoteTy _ t) = getDFunTyKey t
getDFunTyKey (FunTy arg _) = getOccName funTyCon
getDFunTyKey (ForAllTy _ t) = getDFunTyKey t
-getDFunTyKey (UsageTy _ t) = getDFunTyKey t
getDFunTyKey (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable
getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty)
-- SourceTy shouldn't happen
where
split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
split orig_ty (NoteTy n ty) tvs = split orig_ty ty tvs
- split orig_ty (UsageTy _ ty) tvs = split orig_ty ty tvs
split orig_ty t tvs = (reverse tvs, orig_ty)
tcIsForAllTy (ForAllTy tv ty) = True
tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
-tcIsForAllTy (UsageTy n ty) = tcIsForAllTy ty
tcIsForAllTy t = False
tcSplitRhoTy :: Type -> ([PredType], Type)
Just p -> split res res (p:ts)
Nothing -> (reverse ts, orig_ty)
split orig_ty (NoteTy n ty) ts = split orig_ty ty ts
- split orig_ty (UsageTy _ ty) ts = split orig_ty ty ts
split orig_ty ty ts = (reverse ts, orig_ty)
tcSplitSigmaTy ty = case tcSplitForAllTys ty of
tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
-- Newtypes are opaque, so they may be split
tcSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
-tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [unUTy arg,unUTy res])
+tcSplitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [arg,res])
tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
-tcSplitTyConApp_maybe (UsageTy _ ty) = tcSplitTyConApp_maybe ty
tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
-- However, predicates are not treated
-- as tycon applications by the type checker
tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
tcSplitFunTy_maybe (FunTy arg res) = Just (arg, res)
tcSplitFunTy_maybe (NoteTy n ty) = tcSplitFunTy_maybe ty
-tcSplitFunTy_maybe (UsageTy _ ty) = tcSplitFunTy_maybe ty
tcSplitFunTy_maybe other = Nothing
tcFunArgTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
-tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2)
+tcSplitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [ty1], ty2)
tcSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
tcSplitAppTy_maybe (NoteTy n ty) = tcSplitAppTy_maybe ty
-tcSplitAppTy_maybe (UsageTy _ ty) = tcSplitAppTy_maybe ty
tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
--- Don't forget that newtype!
tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys
tcGetTyVar_maybe :: Type -> Maybe TyVar
tcGetTyVar_maybe (TyVarTy tv) = Just tv
tcGetTyVar_maybe (NoteTy _ t) = tcGetTyVar_maybe t
-tcGetTyVar_maybe ty@(UsageTy _ _) = pprPanic "tcGetTyVar_maybe: UTy:" (pprType ty)
tcGetTyVar_maybe other = Nothing
tcGetTyVar :: String -> Type -> TyVar
Just p -> (p, res)
Nothing -> panic "splitMethodTy"
split (NoteTy n ty) = split ty
- split (UsageTy _ ty) = split ty
split _ = panic "splitMethodTy"
tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
isPred :: SourceType -> Bool
isPred (ClassP _ _) = True
isPred (IParam _ _) = True
-isPred (NType _ __) = False
+isPred (NType _ _) = False
isPredTy :: Type -> Bool
isPredTy (NoteTy _ ty) = isPredTy ty
-isPredTy (UsageTy _ ty) = isPredTy ty
isPredTy (SourceTy sty) = isPred sty
isPredTy _ = False
tcSplitPredTy_maybe :: Type -> Maybe PredType
-- Returns Just for predicates only
tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty
-tcSplitPredTy_maybe (UsageTy _ ty) = tcSplitPredTy_maybe ty
tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
tcSplitPredTy_maybe other = Nothing
predTyUnique :: PredType -> Unique
-predTyUnique (IParam n _) = getUnique n
+predTyUnique (IParam n _) = getUnique (ipNameName n)
predTyUnique (ClassP clas tys) = getUnique clas
predHasFDs :: PredType -> Bool
mkPredName :: Unique -> SrcLoc -> SourceType -> Name
mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
-mkPredName uniq loc (IParam name ty) = name
+mkPredName uniq loc (IParam ip ty) = mkLocalName uniq (getOccName (ipNameName ip)) loc
\end{code}
--------------------- Dictionary types ---------------------------------
\begin{code}
-mkClassPred clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
- ClassP clas tys
+mkClassPred clas tys = ClassP clas tys
isClassPred :: SourceType -> Bool
isClassPred (ClassP clas tys) = True
getClassPredTys (ClassP clas tys) = (clas, tys)
mkDictTy :: Class -> [Type] -> Type
-mkDictTy clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
- mkPredTy (ClassP clas tys)
+mkDictTy clas tys = mkPredTy (ClassP clas tys)
isDictTy :: Type -> Bool
isDictTy (SourceTy p) = isClassPred p
isDictTy (NoteTy _ ty) = isDictTy ty
-isDictTy (UsageTy _ ty) = isDictTy ty
isDictTy other = False
\end{code}
tcEqType :: Type -> Type -> Bool
tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
+tcEqTypes :: [Type] -> [Type] -> Bool
+tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False }
+
tcEqPred :: PredType -> PredType -> Bool
tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
-- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
-- we in effect substitute tv2 for tv1 in t1 before continuing
- -- Look through NoteTy and UsageTy
+ -- Look through NoteTy
cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
-cmpTy env (UsageTy _ ty1) ty2 = cmpTy env ty1 ty2
-cmpTy env ty1 (UsageTy _ ty2) = cmpTy env ty1 ty2
-- Deal with equal constructors
cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
\begin{code}
cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
-cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
+cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
-- Compare types as well as names for implicit parameters
-- This comparison is used exclusively (I think) for the
-- finite map built in TcSimplify
%* *
%************************************************************************
-isQualifiedTy returns true of any qualified type. It doesn't *necessarily* have
+isSigmaTy returns true of any qualified type. It doesn't *necessarily* have
any foralls. E.g.
f :: (?x::Int) => Int -> Int
\begin{code}
-isQualifiedTy :: Type -> Bool
-isQualifiedTy (ForAllTy tyvar ty) = True
-isQualifiedTy (FunTy a b) = isPredTy a
-isQualifiedTy (NoteTy n ty) = isQualifiedTy ty
-isQualifiedTy (UsageTy _ ty) = isQualifiedTy ty
-isQualifiedTy _ = False
+isSigmaTy :: Type -> Bool
+isSigmaTy (ForAllTy tyvar ty) = True
+isSigmaTy (FunTy a b) = isPredTy a
+isSigmaTy (NoteTy n ty) = isSigmaTy ty
+isSigmaTy _ = False
isOverloadedTy :: Type -> Bool
isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
isOverloadedTy (FunTy a b) = isPredTy a
isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
-isOverloadedTy (UsageTy _ ty) = isOverloadedTy ty
isOverloadedTy _ = False
\end{code}
\begin{code}
hoistForAllTys :: Type -> Type
- -- Move all the foralls to the top
- -- e.g. T -> forall a. a ==> forall a. T -> a
- -- Careful: LOSES USAGE ANNOTATIONS!
+-- Used for user-written type signatures only
+-- Move all the foralls and constraints to the top
+-- e.g. T -> forall a. a ==> forall a. T -> a
+-- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
+--
+-- We want to 'look through' type synonyms when doing this
+-- so it's better done on the Type than the HsType
+
hoistForAllTys ty
- = case hoist ty of { (tvs, body) -> mkForAllTys tvs body }
+ = case hoist ty ty of
+ (tvs, theta, body) -> mkForAllTys tvs (mkFunTys theta body)
where
- hoist :: Type -> ([TyVar], Type)
- hoist ty = case tcSplitFunTys ty of { (args, res) ->
- case tcSplitForAllTys res of {
- ([], body) -> ([], ty) ;
- (tvs1, body1) -> case hoist body1 of { (tvs2,body2) ->
- (tvs1 ++ tvs2, mkFunTys args body2)
- }}}
+ hoist orig_ty (ForAllTy tv ty) = case hoist ty ty of
+ (tvs,theta,tau) -> (tv:tvs,theta,tau)
+ hoist orig_ty (FunTy arg res)
+ | isPredTy arg = case hoist res res of
+ (tvs,theta,tau) -> (tvs,arg:theta,tau)
+ | otherwise = case hoist res res of
+ (tvs,theta,tau) -> (tvs,theta,mkFunTy arg tau)
+
+ hoist orig_ty (NoteTy _ ty) = hoist orig_ty ty
+ hoist orig_ty ty = ([], [], orig_ty)
\end{code}
deNoteType (AppTy fun arg) = AppTy (deNoteType fun) (deNoteType arg)
deNoteType (FunTy fun arg) = FunTy (deNoteType fun) (deNoteType arg)
deNoteType (ForAllTy tv ty) = ForAllTy tv (deNoteType ty)
-deNoteType (UsageTy u ty) = UsageTy u (deNoteType ty)
deNoteSourceType :: SourceType -> SourceType
-deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
-deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
-deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
+deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
+deNoteSourceType (IParam n ty) = IParam n (deNoteType ty)
+deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
\end{code}
Find the free names of a type, including the type constructors and classes it mentions
namesOfType (FunTy arg res) = namesOfType arg `unionNameSets` namesOfType res
namesOfType (AppTy fun arg) = namesOfType fun `unionNameSets` namesOfType arg
namesOfType (ForAllTy tyvar ty) = namesOfType ty `delFromNameSet` getName tyvar
-namesOfType (UsageTy u ty) = namesOfType u `unionNameSets` namesOfType ty
namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
#endif
- -- Ignore usages
-uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
-uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
-
-- Anything else fails
uTysX ty1 ty2 k subst = Nothing
| typeKind ty2 `eqKind` tyVarKind tv1
&& occur_check_ok ty2
-> -- No kind mismatch nor occur check
- UASSERT( not (isUTy ty2) )
k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
| otherwise -> Nothing -- Fail if kind mis-match or occur check
| v `elemVarSet` tmpls
= -- v is a template variable
case lookupSubstEnv senv v of
- Nothing -> UASSERT( not (isUTy ty) )
- k (extendSubstEnv senv v (DoneTy ty))
+ Nothing -> k (extendSubstEnv senv v (DoneTy ty))
Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
| otherwise -> Nothing -- Fails
match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
| tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
-match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
-match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
-
-- With type synonyms, we have to be careful for the exact
-- same reasons as in the unifier. Please see the
-- considerable commentary there before changing anything
projects / ghc-hetmet.git / blobdiff