module TcType (
--------------------------------
-- Types
- TcType, TcSigmaType, TcPhiType, TcTauType, TcPredType, TcThetaType,
+ TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
TcTyVar, TcTyVarSet, TcKind,
--------------------------------
--------------------------------
-- Builders
- mkRhoTy, mkSigmaTy,
+ mkPhiTy, mkSigmaTy,
--------------------------------
-- Splitters
-- These are important because they do not look through newtypes
- tcSplitForAllTys, tcSplitRhoTy,
+ tcSplitForAllTys, tcSplitPhiTy,
tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
tcSplitAppTy_maybe, tcSplitAppTy, tcSplitSigmaTy,
isDoubleTy, isFloatTy, isIntTy,
isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy,
isTauTy, tcIsTyVarTy, tcIsForAllTy,
+ allDistinctTyVars,
---------------------------------
-- Misc type manipulators
- hoistForAllTys, deNoteType,
+ deNoteType,
namesOfType, namesOfDFunHead,
getDFunTyKey,
isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
mkDictTy, tcSplitPredTy_maybe, predTyUnique,
isDictTy, tcSplitDFunTy, predTyUnique,
- mkClassPred, inheritablePred, isIPPred, mkPredName,
+ mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName,
---------------------------------
-- Foreign import and export
---------------------------------
-- Unifier and matcher
unifyTysX, unifyTyListsX, unifyExtendTysX,
- allDistinctTyVars,
matchTy, matchTys, match,
--------------------------------
Type, SourceType(..), PredType, ThetaType,
mkForAllTy, mkForAllTys,
mkFunTy, mkFunTys, zipFunTys,
- mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+ mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
isUnLiftedType, -- Source types are always lifted
isUnboxedTupleType, -- Ditto
- isPrimitiveType,
+ isPrimitiveType, isTyVarTy,
tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
Kind, Type, SourceType(..), PredType, ThetaType,
unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
mkForAllTy, mkForAllTys, defaultKind, isTypeKind, isAnyTypeKind,
- mkFunTy, mkFunTys, zipFunTys,
- mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+ mkFunTy, mkFunTys, zipFunTys, isTyVarTy,
+ mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
splitNewType_maybe, splitTyConApp_maybe,
-- others:
import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
-import Name ( Name, NamedThing(..), mkLocalName, getSrcLoc )
+import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc )
import OccName ( OccName, mkDictOcc )
import NameSet
import PrelNames -- Lots (e.g. in isFFIArgumentTy)
import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
-import BasicTypes ( ipNameName )
+import BasicTypes ( IPName(..), ipNameName )
import Unique ( Unique, Uniquable(..) )
import SrcLoc ( SrcLoc )
import Util ( cmpList, thenCmp, equalLength )
The type checker divides the generic Type world into the
following more structured beasts:
-sigma ::= forall tyvars. theta => phi
+sigma ::= forall tyvars. phi
-- A sigma type is a qualified type
--
-- Note that even if 'tyvars' is empty, theta
-- A 'phi' type has no foralls to the right of
-- an arrow
-phi ::= sigma -> phi
+phi :: theta => rho
+
+rho ::= sigma -> rho
| tau
-- A 'tau' type has no quantification anywhere
\begin{code}
type SigmaType = Type
-type PhiType = Type
+type RhoType = Type
type TauType = Type
\end{code}
type TcPredType = PredType
type TcThetaType = ThetaType
type TcSigmaType = TcType
-type TcPhiType = TcType
+type TcRhoType = TcType
type TcTauType = TcType
type TcKind = TcType
\end{code}
isSkolemTyVar :: TcTyVar -> Bool
isSkolemTyVar tv = case mutTyVarDetails tv of
- SigTv -> True
+ SigTv -> True
+ ClsTv -> True
+ InstTv -> True
oteher -> False
isHoleTyVar :: TcTyVar -> Bool
%************************************************************************
\begin{code}
-mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
+mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau)
-mkRhoTy :: [SourceType] -> Type -> Type
-mkRhoTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
+mkPhiTy :: [SourceType] -> Type -> Type
+mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta
\end{code}
tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty
tcIsForAllTy t = False
-tcSplitRhoTy :: Type -> ([PredType], Type)
-tcSplitRhoTy ty = split ty ty []
+tcSplitPhiTy :: Type -> ([PredType], Type)
+tcSplitPhiTy ty = split ty ty []
where
split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
Just p -> split res res (p:ts)
split orig_ty ty ts = (reverse ts, orig_ty)
tcSplitSigmaTy ty = case tcSplitForAllTys ty of
- (tvs, rho) -> case tcSplitRhoTy rho of
+ (tvs, rho) -> case tcSplitPhiTy rho of
(theta, tau) -> (tvs, theta, tau)
tcTyConAppTyCon :: Type -> TyCon
Nothing -> pprPanic "tcSplitTyConApp" (pprType ty)
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, [arg,res])
tcSplitTyConApp_maybe (NoteTy n ty) = tcSplitTyConApp_maybe ty
tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
+ -- Newtypes are opaque, so they may be split
-- However, predicates are not treated
-- as tycon applications by the type checker
tcSplitTyConApp_maybe other = Nothing
(tvs, theta, clas, tys) }}
\end{code}
+(allDistinctTyVars tys tvs) = True
+ iff
+all the types tys are type variables,
+distinct from each other and from tvs.
+
+This is useful when checking that unification hasn't unified signature
+type variables. For example, if the type sig is
+ f :: forall a b. a -> b -> b
+we want to check that 'a' and 'b' havn't
+ (a) been unified with a non-tyvar type
+ (b) been unified with each other (all distinct)
+ (c) been unified with a variable free in the environment
+
+\begin{code}
+allDistinctTyVars :: [Type] -> TyVarSet -> Bool
+
+allDistinctTyVars [] acc
+ = True
+allDistinctTyVars (ty:tys) acc
+ = case tcGetTyVar_maybe ty of
+ Nothing -> False -- (a)
+ Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
+ | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
+\end{code}
+
%************************************************************************
%* *
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 ip ty) = mkLocalName uniq (getOccName (ipNameName ip)) loc
+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}
isIPPred (IParam _ _) = True
isIPPred other = False
-inheritablePred :: PredType -> Bool
+isInheritablePred :: PredType -> Bool
-- Can be inherited by a context. For example, consider
-- f x = let g y = (?v, y+x)
-- in (g 3 with ?v = 8,
-- g :: (?v :: a) => a -> a
-- 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
-inheritablePred (ClassP _ _) = True
-inheritablePred other = False
+isInheritablePred (ClassP _ _) = True
+isInheritablePred other = False
+
+isLinearPred :: TcPredType -> Bool
+isLinearPred (IParam (Linear n) _) = True
+isLinearPred other = False
\end{code}
%************************************************************************
\begin{code}
-hoistForAllTys :: Type -> Type
--- 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 ty of
- (tvs, theta, body) -> mkForAllTys tvs (mkFunTys theta body)
- where
- 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}
-
-
-\begin{code}
deNoteType :: Type -> Type
-- Remove synonyms, but not source types
deNoteType ty@(TyVarTy tyvar) = ty
%* *
%************************************************************************
-(allDistinctTyVars tys tvs) = True
- iff
-all the types tys are type variables,
-distinct from each other and from tvs.
-
-This is useful when checking that unification hasn't unified signature
-type variables. For example, if the type sig is
- f :: forall a b. a -> b -> b
-we want to check that 'a' and 'b' havn't
- (a) been unified with a non-tyvar type
- (b) been unified with each other (all distinct)
- (c) been unified with a variable free in the environment
-
-\begin{code}
-allDistinctTyVars :: [Type] -> TyVarSet -> Bool
-
-allDistinctTyVars [] acc
- = True
-allDistinctTyVars (ty:tys) acc
- = case tcGetTyVar_maybe ty of
- Nothing -> False -- (a)
- Just tv | tv `elemVarSet` acc -> False -- (b) or (c)
- | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv)
-\end{code}
-
-
-%************************************************************************
-%* *
-\subsection{Unification with an explicit substitution}
-%* *
-%************************************************************************
-
Unify types with an explicit substitution and no monad.
Ignore usage annotations.