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,
tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
isSigmaTy, isOverloadedTy,
isDoubleTy, isFloatTy, isIntTy,
- isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy,
+ isIntegerTy, isAddrTy, isBoolTy, isUnitTy,
isTauTy, tcIsTyVarTy, tcIsForAllTy,
+ allDistinctTyVars,
---------------------------------
-- Misc type manipulators
- hoistForAllTys, deNoteType,
- namesOfType, namesOfDFunHead,
+ deNoteType, classNamesOfTheta,
+ tyClsNamesOfType, tyClsNamesOfDFunHead,
getDFunTyKey,
---------------------------------
-- Predicate types
- PredType, getClassPredTys_maybe, getClassPredTys,
+ getClassPredTys_maybe, getClassPredTys,
isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
- mkDictTy, tcSplitPredTy_maybe, predTyUnique,
+ mkDictTy, tcSplitPredTy_maybe,
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,
--------------------------------
Kind, -- Stuff to do with kinds is insensitive to pre/post Tc
unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
- isTypeKind,
+ isTypeKind, isAnyTypeKind,
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,
import {-# SOURCE #-} PprType( pprType )
+-- PprType imports TcType so that it can print intelligently
-- friends:
import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
Kind, Type, SourceType(..), PredType, ThetaType,
unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
- mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
- mkFunTy, mkFunTys, zipFunTys,
- mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+ mkForAllTy, mkForAllTys, defaultKind, isTypeKind, isAnyTypeKind,
+ 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}
isFloatTy = is_tc floatTyConKey
isDoubleTy = is_tc doubleTyConKey
-isForeignPtrTy = is_tc foreignPtrTyConKey
isIntegerTy = is_tc integerTyConKey
isIntTy = is_tc intTyConKey
isAddrTy = is_tc addrTyConKey
%************************************************************************
\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
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
-This is used in the front end of the compiler
+Find the free tycons and classes of a type. This is used in the front
+end of the compiler.
\begin{code}
-namesOfType :: Type -> NameSet
-namesOfType (TyVarTy tv) = unitNameSet (getName tv)
-namesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
-namesOfType (NoteTy (SynNote ty1) ty2) = namesOfType ty1
-namesOfType (NoteTy other_note ty2) = namesOfType ty2
-namesOfType (SourceTy (IParam n ty)) = namesOfType ty
-namesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
-namesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
-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
-
-namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
-
-namesOfDFunHead :: Type -> NameSet
+tyClsNamesOfType :: Type -> NameSet
+tyClsNamesOfType (TyVarTy tv) = emptyNameSet
+tyClsNamesOfType (TyConApp tycon tys) = unitNameSet (getName tycon) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (NoteTy (SynNote ty1) ty2) = tyClsNamesOfType ty1
+tyClsNamesOfType (NoteTy other_note ty2) = tyClsNamesOfType ty2
+tyClsNamesOfType (SourceTy (IParam n ty)) = tyClsNamesOfType ty
+tyClsNamesOfType (SourceTy (ClassP cl tys)) = unitNameSet (getName cl) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (SourceTy (NType tc tys)) = unitNameSet (getName tc) `unionNameSets` tyClsNamesOfTypes tys
+tyClsNamesOfType (FunTy arg res) = tyClsNamesOfType arg `unionNameSets` tyClsNamesOfType res
+tyClsNamesOfType (AppTy fun arg) = tyClsNamesOfType fun `unionNameSets` tyClsNamesOfType arg
+tyClsNamesOfType (ForAllTy tyvar ty) = tyClsNamesOfType ty
+
+tyClsNamesOfTypes tys = foldr (unionNameSets . tyClsNamesOfType) emptyNameSet tys
+
+tyClsNamesOfDFunHead :: Type -> NameSet
-- Find the free type constructors and classes
-- of the head of the dfun instance type
-- The 'dfun_head_type' is because of
-- instance Foo a => Baz T where ...
-- The decl is an orphan if Baz and T are both not locally defined,
-- even if Foo *is* locally defined
-namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
- (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
- (map getName tvs)
+tyClsNamesOfDFunHead dfun_ty
+ = case tcSplitSigmaTy dfun_ty of
+ (tvs,_,head_ty) -> tyClsNamesOfType head_ty
+
+classNamesOfTheta :: ThetaType -> [Name]
+-- Looks just for ClassP things; maybe it should check
+classNamesOfTheta preds = [ getName c | ClassP c _ <- preds ]
\end{code}
-- bytearrays from a _ccall_ / foreign declaration
-- (or be passed them as arguments in foreign exported functions).
legalFEArgTyCon tc
- | getUnique tc `elem` [ foreignObjTyConKey, foreignPtrTyConKey,
- byteArrayTyConKey, mutableByteArrayTyConKey ]
+ | getUnique tc `elem` [ byteArrayTyConKey, mutableByteArrayTyConKey ]
= False
-- It's also illegal to make foreign exports that take unboxed
-- arguments. The RTS API currently can't invoke such things. --SDM 7/2000
legalFIResultTyCon :: DynFlags -> TyCon -> Bool
legalFIResultTyCon dflags tc
| getUnique tc `elem`
- [ foreignObjTyConKey, foreignPtrTyConKey,
- byteArrayTyConKey, mutableByteArrayTyConKey ] = False
+ [ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
| tc == unitTyCon = True
| otherwise = marshalableTyCon dflags tc
legalFEResultTyCon :: TyCon -> Bool
legalFEResultTyCon tc
| getUnique tc `elem`
- [ foreignObjTyConKey, foreignPtrTyConKey,
- byteArrayTyConKey, mutableByteArrayTyConKey ] = False
+ [ byteArrayTyConKey, mutableByteArrayTyConKey ] = False
| tc == unitTyCon = True
| otherwise = boxedMarshalableTyCon tc
, word32TyConKey, word64TyConKey
, floatTyConKey, doubleTyConKey
, addrTyConKey, ptrTyConKey, funPtrTyConKey
- , charTyConKey, foreignObjTyConKey
- , foreignPtrTyConKey
+ , charTyConKey
, stablePtrTyConKey
, byteArrayTyConKey, mutableByteArrayTyConKey
, boolTyConKey
%* *
%************************************************************************
-(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.
| v `elemVarSet` tmpls
= -- v is a template variable
case lookupSubstEnv senv v of
- Nothing -> k (extendSubstEnv senv v (DoneTy ty))
+ Nothing | typeKind ty `eqKind` tyVarKind v
+ -- We do a kind check, just as in the uVarX above
+ -- The kind check is needed to avoid bogus matches
+ -- of (a b) with (c d), where the kinds don't match
+ -- An occur check isn't needed when matching.
+ -> k (extendSubstEnv senv v (DoneTy ty))
+
+ | otherwise -> Nothing -- Fails
+
Just (DoneTy ty') | ty' `tcEqType` ty -> k senv -- Succeeds
| otherwise -> Nothing -- Fails
projects / ghc-hetmet.git / blobdiff