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, predMentionsIPs, inheritablePred, isIPPred, mkPredName,
+ mkClassPred, inheritablePred, isIPPred, mkPredName,
---------------------------------
-- Foreign import and export
isPrimitiveType,
tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
- tidyTyVar, tidyTyVars,
+ tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
typeKind, eqKind, eqUsage,
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
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,
isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
splitNewType_maybe, splitTyConApp_maybe,
tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
- tidyTyVar, tidyTyVars, eqKind, eqUsage,
+ tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
)
-import TyCon ( TyCon, isPrimTyCon, tyConArity, isNewTyCon, isUnLiftedTyCon )
-import Class ( classTyCon, classHasFDs, Class )
-import Var ( TyVar, tyVarKind )
+import TyCon ( TyCon, isUnLiftedTyCon )
+import Class ( classHasFDs, Class )
+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 PrelNames -- Lots (e.g. in isFFIArgumentTy)
import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
-import Unique ( Unique, Uniquable(..), mkTupleTyConUnique )
+import BasicTypes ( ipNameName )
+import Unique ( Unique, Uniquable(..) )
import SrcLoc ( SrcLoc )
-import Util ( cmpList, thenCmp )
+import Util ( cmpList, thenCmp, equalLength )
import Maybes ( maybeToBool, expectJust )
-import BasicTypes ( Boxity(..) )
import Outputable
\end{code}
%************************************************************************
%* *
-\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
isPred :: SourceType -> Bool
isPred (ClassP _ _) = True
isPred (IParam _ _) = True
-isPred (NType _ __) = False
+isPred (NType _ _) = False
isPredTy :: Type -> Bool
isPredTy (NoteTy _ ty) = isPredTy ty
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}
-- 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}
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 }
\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 (UsageTy _ ty) = isSigmaTy ty
+isSigmaTy _ = False
isOverloadedTy :: Type -> Bool
isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
isIntTy = is_tc intTyConKey
isAddrTy = is_tc addrTyConKey
isBoolTy = is_tc boolTyConKey
-isUnitTy = is_tc (mkTupleTyConUnique Boxed 0)
+isUnitTy = is_tc unitTyConKey
is_tc :: Unique -> Type -> Bool
-- Newtypes are opaque to this
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
-- Type constructors must match
uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
- | (con1 == con2 && length tys1 == length tys2)
+ | (con1 == con2 && equalLength tys1 tys2)
= uTyListsX tys1 tys2 k subst
-- Applications need a bit of care!
projects / ghc-hetmet.git / blobdiff