isDoubleTy, isFloatTy, isIntTy,
isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy,
isTauTy, tcIsTyVarTy, tcIsForAllTy,
+ allDistinctTyVars,
---------------------------------
-- Misc type manipulators
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,
--------------------------------
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
-- friends:
import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend
-import Type ( mkUTyM, unUTy ) -- Used locally
import Type ( -- Re-exports
tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
Kind, Type, SourceType(..), PredType, ThetaType,
unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
- mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
+ mkForAllTy, mkForAllTys, defaultKind, isTypeKind, isAnyTypeKind,
mkFunTy, mkFunTys, zipFunTys,
- mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
+ 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 )
isSkolemTyVar :: TcTyVar -> Bool
isSkolemTyVar tv = case mutTyVarDetails tv of
- SigTv -> True
+ SigTv -> True
+ ClsTv -> True
+ InstTv -> True
oteher -> False
isHoleTyVar :: TcTyVar -> Bool
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
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, [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)
+ -- Newtypes are opaque, so they may be split
-- However, predicates are not treated
-- as tycon applications by the type checker
tcSplitTyConApp_maybe other = Nothing
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])
(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}
+
%************************************************************************
%* *
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
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}
--------------------- 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}
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}
-- 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
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
isOverloadedTy (FunTy a b) = isPredTy a
isOverloadedTy (NoteTy n ty) = isOverloadedTy ty
-isOverloadedTy (UsageTy _ ty) = isOverloadedTy ty
isOverloadedTy _ = False
\end{code}
(tvs,theta,tau) -> (tvs,theta,mkFunTy arg tau)
hoist orig_ty (NoteTy _ ty) = hoist orig_ty ty
- hoist orig_ty (UsageTy _ 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)
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
%* *
%************************************************************************
-(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.
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 | 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
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