X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcType.lhs;h=b1161048817a229f81abaa553cd6e7643e1175ce;hb=0a7b8d872ebf93a1bfc8f87a8a60cce0097ecfc2;hp=7f4e0df433b3233743549a18ceaa4a21c678d135;hpb=9e93335020e64a811dbbb223e1727c76933a93ae;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index 7f4e0df..b116104 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -17,7 +17,13 @@ is the principal client. module TcType ( -------------------------------- -- Types - TauType, RhoType, SigmaType, + TcType, TcSigmaType, TcPhiType, TcTauType, TcPredType, TcThetaType, + TcTyVar, TcTyVarSet, TcKind, + + -------------------------------- + -- TyVarDetails + TyVarDetails(..), isUserTyVar, isSkolemTyVar, isHoleTyVar, + tyVarBindingInfo, -------------------------------- -- Builders @@ -35,8 +41,8 @@ module TcType ( --------------------------------- -- 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, @@ -53,7 +59,7 @@ module TcType ( isPredTy, isClassPred, isTyVarClassPred, predHasFDs, mkDictTy, tcSplitPredTy_maybe, predTyUnique, isDictTy, tcSplitDFunTy, predTyUnique, - mkClassPred, predMentionsIPs, inheritablePred, isIPPred, mkPredName, + mkClassPred, inheritablePred, isIPPred, mkPredName, --------------------------------- -- Foreign import and export @@ -106,7 +112,7 @@ 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, @@ -120,18 +126,19 @@ import Type ( -- Re-exports ) 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 ) @@ -142,14 +149,143 @@ import Outputable %************************************************************************ %* * -\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 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} -type SigmaType = Type -type RhoType = Type +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 @@ -343,7 +479,7 @@ tcSplitDFunTy ty isPred :: SourceType -> Bool isPred (ClassP _ _) = True isPred (IParam _ _) = True -isPred (NType _ __) = False +isPred (NType _ _) = False isPredTy :: Type -> Bool isPredTy (NoteTy _ ty) = isPredTy ty @@ -359,7 +495,7 @@ 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 @@ -370,7 +506,7 @@ predHasFDs (ClassP cls _) = classHasFDs cls 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} @@ -423,10 +559,6 @@ inheritablePred :: PredType -> Bool -- which can be free in g's rhs, and shared by both calls to g inheritablePred (ClassP _ _) = True inheritablePred other = False - -predMentionsIPs :: SourceType -> NameSet -> Bool -predMentionsIPs (IParam n _) ns = n `elemNameSet` ns -predMentionsIPs other ns = False \end{code} @@ -443,6 +575,9 @@ But ignoring usage types 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 } @@ -501,7 +636,7 @@ cmpTy env _ _ = LT \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 @@ -530,17 +665,17 @@ instance Ord SourceType where { compare = tcCmpPred } %* * %************************************************************************ -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 (UsageTy _ ty) = isSigmaTy ty +isSigmaTy _ = False isOverloadedTy :: Type -> Bool isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty @@ -605,9 +740,9 @@ 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