diff options
Diffstat (limited to 'ghc/compiler/types')
| -rw-r--r-- | ghc/compiler/types/FunDeps.lhs | 9 | ||||
| -rw-r--r-- | ghc/compiler/types/Generics.lhs | 20 | ||||
| -rw-r--r-- | ghc/compiler/types/InstEnv.lhs | 14 | ||||
| -rw-r--r-- | ghc/compiler/types/PprType.lhs | 92 | ||||
| -rw-r--r-- | ghc/compiler/types/TyCon.lhs | 32 | ||||
| -rw-r--r-- | ghc/compiler/types/Type.lhs | 632 | ||||
| -rw-r--r-- | ghc/compiler/types/TypeRep.lhs | 72 | ||||
| -rw-r--r-- | ghc/compiler/types/Unify.lhs | 303 |
8 files changed, 294 insertions, 880 deletions
diff --git a/ghc/compiler/types/FunDeps.lhs b/ghc/compiler/types/FunDeps.lhs index efbd8d6492..4854e0ca8a 100644 --- a/ghc/compiler/types/FunDeps.lhs +++ b/ghc/compiler/types/FunDeps.lhs @@ -15,9 +15,11 @@ module FunDeps ( import Name ( getSrcLoc ) import Var ( Id, TyVar ) import Class ( Class, FunDep, classTvsFds ) -import Type ( Type, ThetaType, PredType(..), predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred ) import Subst ( mkSubst, emptyInScopeSet, substTy ) -import Unify ( unifyTyListsX, unifyExtendTysX ) +import TcType ( Type, ThetaType, SourceType(..), PredType, + predTyUnique, mkClassPred, tyVarsOfTypes, tyVarsOfPred, + unifyTyListsX, unifyExtendTysX, tcEqType + ) import VarSet import VarEnv import Outputable @@ -211,7 +213,8 @@ checkGroup :: InstEnv Id -> [(PredType,SDoc)] -> [(Equation, SDoc)] checkGroup inst_env (p1@(IParam _ ty, _) : ips) = -- For implicit parameters, all the types must match - [((emptyVarSet, ty, ty'), mkEqnMsg p1 p2) | p2@(IParam _ ty', _) <- ips, ty /= ty'] + [ ((emptyVarSet, ty, ty'), mkEqnMsg p1 p2) + | p2@(IParam _ ty', _) <- ips, not (ty `tcEqType` ty')] checkGroup inst_env clss@((ClassP cls _, _) : _) = -- For classes life is more complicated diff --git a/ghc/compiler/types/Generics.lhs b/ghc/compiler/types/Generics.lhs index 537be155d4..b14ad1bba2 100644 --- a/ghc/compiler/types/Generics.lhs +++ b/ghc/compiler/types/Generics.lhs @@ -10,9 +10,9 @@ import HsSyn ( HsExpr(..), InPat(..), mkSimpleMatch ) import Type ( Type, isUnLiftedType, applyTys, tyVarsOfType, tyVarsOfTypes, mkTyVarTys, mkForAllTys, mkTyConApp, mkFunTy, isTyVarTy, getTyVar_maybe, - splitSigmaTy, splitTyConApp_maybe, funTyCon + funTyCon ) - +import TcType ( tcSplitTyConApp_maybe, tcSplitSigmaTy, tcSplitSigmaTy ) import DataCon ( DataCon, dataConOrigArgTys, dataConWrapId, dataConId, isExistentialDataCon ) import TyCon ( TyCon, tyConTyVars, tyConDataConsIfAvailable, @@ -187,7 +187,7 @@ validGenericInstanceType :: Type -> Bool -- f {| a + Int |} validGenericInstanceType inst_ty - = case splitTyConApp_maybe inst_ty of + = case tcSplitTyConApp_maybe inst_ty of Just (tycon, tys) -> all isTyVarTy tys && tycon `elem` genericTyCons Nothing -> False @@ -202,12 +202,12 @@ validGenericMethodType :: Type -> Bool validGenericMethodType ty = valid tau where - (local_tvs, _, tau) = splitSigmaTy ty + (local_tvs, _, tau) = tcSplitSigmaTy ty valid ty | isTyVarTy ty = True | no_tyvars_in_ty = True - | otherwise = case splitTyConApp_maybe ty of + | otherwise = case tcSplitTyConApp_maybe ty of Just (tc,tys) -> valid_tycon tc && all valid tys Nothing -> False where @@ -266,7 +266,7 @@ mkTyConGenInfo tycon [from_name, to_name] (from_fn, to_fn, rep_ty) | isNewTyCon tycon - = ( mkLams tyvars $ Lam x $ Note (Coerce newrep_ty tycon_ty) (Var x), + = ( mkLams tyvars $ Lam x $ Var x, Var (dataConWrapId the_datacon), newrep_ty ) @@ -281,7 +281,7 @@ mkTyConGenInfo tycon [from_name, to_name] ---------------------- -- Newtypes only [the_datacon] = datacons - newrep_ty = applyTys (expectJust "mkGenTyConInfo" (newTyConRep tycon)) tyvar_tys + (_, newrep_ty) = newTyConRep tycon ---------------------- -- Non-newtypes only @@ -463,11 +463,11 @@ mkGenericRhs sel_id tyvar tycon -- Takes out the ForAll and the Class restrictions -- in front of the type of the method. - (_,_,op_ty) = splitSigmaTy (idType sel_id) + (_,_,op_ty) = tcSplitSigmaTy (idType sel_id) -- Do it again! This deals with the case where the method type -- is polymorphic -- see notes above - (local_tvs,_,final_ty) = splitSigmaTy op_ty + (local_tvs,_,final_ty) = tcSplitSigmaTy op_ty -- Now we probably have a tycon in front -- of us, quite probably a FunTyCon. @@ -488,7 +488,7 @@ generate_bimap env@(tv,ep,local_tvs) ty Just tv1 | tv == tv1 -> ep -- The class tyvar | otherwise -> ASSERT( tv1 `elem` local_tvs) -- One of the polymorphic tyvars of the method idEP - Nothing -> bimapApp env (splitTyConApp_maybe ty) + Nothing -> bimapApp env (tcSplitTyConApp_maybe ty) ------------------- bimapApp :: EPEnv -> Maybe (TyCon, [Type]) -> EP RenamedHsExpr diff --git a/ghc/compiler/types/InstEnv.lhs b/ghc/compiler/types/InstEnv.lhs index a3bb8d4746..d660fc6b72 100644 --- a/ghc/compiler/types/InstEnv.lhs +++ b/ghc/compiler/types/InstEnv.lhs @@ -22,14 +22,14 @@ import VarSet import VarEnv import Maybes ( MaybeErr(..), returnMaB, failMaB, thenMaB, maybeToBool ) import Name ( getSrcLoc ) -import Type ( Type, tyConAppTyCon, mkTyVarTy, - splitDFunTy, tyVarsOfTypes +import TcType ( Type, tcTyConAppTyCon, mkTyVarTy, + tcSplitDFunTy, tyVarsOfTypes, + matchTys, unifyTyListsX, allDistinctTyVars ) import PprType ( pprClassPred ) import FunDeps ( checkClsFD ) import TyCon ( TyCon ) import Outputable -import Unify ( matchTys, unifyTyListsX, allDistinctTyVars ) import UniqFM ( UniqFM, lookupWithDefaultUFM, addToUFM, emptyUFM, eltsUFM ) import Id ( idType ) import ErrUtils ( Message ) @@ -52,8 +52,8 @@ simpleDFunClassTyCon :: DFunId -> (Class, TyCon) simpleDFunClassTyCon dfun = (clas, tycon) where - (_,_,clas,[ty]) = splitDFunTy (idType dfun) - tycon = tyConAppTyCon ty + (_,_,clas,[ty]) = tcSplitDFunTy (idType dfun) + tycon = tcTyConAppTyCon ty pprInstEnv :: InstEnv -> SDoc pprInstEnv env @@ -319,7 +319,7 @@ addToInstEnv dflags (inst_env, errs) dfun_id where cls_inst_env = classInstEnv inst_env clas - (ins_tvs, _, clas, ins_tys) = splitDFunTy (idType dfun_id) + (ins_tvs, _, clas, ins_tys) = tcSplitDFunTy (idType dfun_id) bad_fundeps = badFunDeps cls_inst_env clas ins_tv_set ins_tys fundep_err = fundepErr dfun_id (head bad_fundeps) @@ -427,5 +427,5 @@ addInstErr what dfun1 dfun2 where ppr_dfun dfun = ppr (getSrcLoc dfun) <> colon <+> pprClassPred clas tys where - (_,_,clas,tys) = splitDFunTy (idType dfun) + (_,_,clas,tys) = tcSplitDFunTy (idType dfun) \end{code} diff --git a/ghc/compiler/types/PprType.lhs b/ghc/compiler/types/PprType.lhs index 36ebf46564..6c663034c0 100644 --- a/ghc/compiler/types/PprType.lhs +++ b/ghc/compiler/types/PprType.lhs @@ -19,12 +19,11 @@ module PprType( -- friends: -- (PprType can see all the representations it's trying to print) import TypeRep ( Type(..), TyNote(..), Kind, liftedTypeKind ) -- friend -import Type ( PredType(..), ThetaType, - splitPredTy_maybe, - splitForAllTys, splitSigmaTy, splitRhoTy, - isPredTy, isDictTy, splitTyConApp_maybe, splitFunTy_maybe, - predRepTy, isUTyVar - ) +import Type ( SourceType(..), isUTyVar, eqKind ) +import TcType ( ThetaType, PredType, tcSplitPredTy_maybe, + tcSplitSigmaTy, isPredTy, isDictTy, + tcSplitTyConApp_maybe, tcSplitFunTy_maybe + ) import Var ( TyVar, tyVarKind ) import Class ( Class ) import TyCon ( TyCon, isPrimTyCon, isTupleTyCon, tupleTyConBoxity, @@ -115,51 +114,36 @@ ppr_ty ctxt_prec (TyVarTy tyvar) ppr_ty ctxt_prec ty@(TyConApp tycon tys) -- KIND CASE; it's of the form (Type x) - | tycon `hasKey` typeConKey && n_tys == 1 + | tycon `hasKey` typeConKey, + [ty] <- tys = -- For kinds, print (Type x) as just x if x is a -- type constructor (must be Boxed, Unboxed, AnyBox) -- Otherwise print as (Type x) - case ty1 of + case ty of TyConApp bx [] -> ppr (getOccName bx) -- Always unqualified other -> maybeParen ctxt_prec tYCON_PREC - (sep [ppr tycon, nest 4 tys_w_spaces]) + (ppr tycon <+> ppr_ty tYCON_PREC ty) -- USAGE CASE - | (tycon `hasKey` usOnceTyConKey || tycon `hasKey` usManyTyConKey) && n_tys == 0 + | (tycon `hasKey` usOnceTyConKey || tycon `hasKey` usManyTyConKey), + null tys = -- For usages (! and .), always print bare OccName, without pkg/mod/uniq ppr (getOccName (tyConName tycon)) -- TUPLE CASE (boxed and unboxed) - | isTupleTyCon tycon - && length tys == tyConArity tycon -- no magic if partially applied - = tupleParens (tupleTyConBoxity tycon) tys_w_commas + | isTupleTyCon tycon, + length tys == tyConArity tycon -- No magic if partially applied + = tupleParens (tupleTyConBoxity tycon) + (sep (punctuate comma (map (ppr_ty tOP_PREC) tys))) -- LIST CASE - | tycon `hasKey` listTyConKey && n_tys == 1 - = brackets (ppr_ty tOP_PREC ty1) - - -- DICTIONARY CASE, prints {C a} - -- This means that instance decls come out looking right in interfaces - -- and that in turn means they get "gated" correctly when being slurped in - | maybeToBool maybe_pred - = braces (pprPred pred) - - -- NO-ARGUMENT CASE (=> no parens) - | null tys - = ppr tycon + | tycon `hasKey` listTyConKey, + [ty] <- tys + = brackets (ppr_ty tOP_PREC ty) -- GENERAL CASE | otherwise - = maybeParen ctxt_prec tYCON_PREC (sep [ppr tycon, nest 4 tys_w_spaces]) - - where - n_tys = length tys - (ty1:_) = tys - Just pred = maybe_pred - maybe_pred = splitPredTy_maybe ty -- Checks class and arity - tys_w_commas = sep (punctuate comma (map (ppr_ty tOP_PREC) tys)) - tys_w_spaces = sep (map (ppr_ty tYCON_PREC) tys) - + = ppr_tc_app ctxt_prec tycon tys ppr_ty ctxt_prec ty@(ForAllTy _ _) @@ -170,10 +154,9 @@ ppr_ty ctxt_prec ty@(ForAllTy _ _) ppr_ty tOP_PREC tau ] where - (tyvars, rho) = splitForAllTys ty - (theta, tau) = splitRhoTy rho + (tyvars, theta, tau) = tcSplitSigmaTy ty - pp_tyvars sty = hsep (map pprTyVarBndr some_tyvars) + pp_tyvars sty = sep (map pprTyVarBndr some_tyvars) where some_tyvars | userStyle sty && not opt_PprStyle_RawTypes = filter (not . isUTyVar) tyvars -- hide uvars from user @@ -210,7 +193,14 @@ ppr_ty ctxt_prec (NoteTy (SynNote ty) expansion) ppr_ty ctxt_prec (NoteTy (FTVNote _) ty) = ppr_ty ctxt_prec ty -ppr_ty ctxt_prec (PredTy p) = braces (pprPred p) +ppr_ty ctxt_prec (SourceTy (NType tc tys)) + = ppr_tc_app ctxt_prec tc tys + +ppr_ty ctxt_prec (SourceTy pred) = braces (pprPred pred) + +ppr_tc_app ctxt_prec tc [] = ppr tc +ppr_tc_app ctxt_prec tc tys = maybeParen ctxt_prec tYCON_PREC + (sep [ppr tc, nest 4 (sep (map (ppr_ty tYCON_PREC) tys))]) \end{code} @@ -227,7 +217,7 @@ and when in debug mode. pprTyVarBndr :: TyVar -> SDoc pprTyVarBndr tyvar = getPprStyle $ \ sty -> - if (ifaceStyle sty && kind /= liftedTypeKind) || debugStyle sty then + if (ifaceStyle sty && not (kind `eqKind` liftedTypeKind)) || debugStyle sty then hsep [ppr tyvar, dcolon, pprParendKind kind] -- See comments with ppDcolon in PprCore.lhs else @@ -252,20 +242,24 @@ description for profiling. getTyDescription :: Type -> String getTyDescription ty - = case (splitSigmaTy ty) of { (_, _, tau_ty) -> + = case (tcSplitSigmaTy ty) of { (_, _, tau_ty) -> case tau_ty of - TyVarTy _ -> "*" - AppTy fun _ -> getTyDescription fun - FunTy _ res -> '-' : '>' : fun_result res - TyConApp tycon _ -> getOccString tycon + TyVarTy _ -> "*" + AppTy fun _ -> getTyDescription fun + FunTy _ res -> '-' : '>' : fun_result res + TyConApp tycon _ -> getOccString tycon NoteTy (FTVNote _) ty -> getTyDescription ty NoteTy (SynNote ty1) _ -> getTyDescription ty1 - PredTy p -> getTyDescription (predRepTy p) - ForAllTy _ ty -> getTyDescription ty + SourceTy sty -> getSourceTyDescription sty + ForAllTy _ ty -> getTyDescription ty } where fun_result (FunTy _ res) = '>' : fun_result res fun_result other = getTyDescription other + +getSourceTyDescription (ClassP cl tys) = getOccString cl +getSourceTyDescription (NType tc tys) = getOccString tc +getSourceTyDescription (IParam id ty) = getOccString id \end{code} @@ -294,8 +288,8 @@ showTypeCategory ty = if isDictTy ty then '+' else - case splitTyConApp_maybe ty of - Nothing -> if maybeToBool (splitFunTy_maybe ty) + case tcSplitTyConApp_maybe ty of + Nothing -> if maybeToBool (tcSplitFunTy_maybe ty) then '>' else '.' diff --git a/ghc/compiler/types/TyCon.lhs b/ghc/compiler/types/TyCon.lhs index 4fc0348773..faa3b3fcfd 100644 --- a/ghc/compiler/types/TyCon.lhs +++ b/ghc/compiler/types/TyCon.lhs @@ -182,15 +182,17 @@ type ArgVrcs = [(Bool,Bool)] -- Tyvar variance info: [(occPos,occNeg)] data AlgTyConFlavour = DataTyCon -- Data type + | EnumTyCon -- Special sort of enumeration type + | NewTyCon Type -- Newtype, with its *ultimate* representation type -- By 'ultimate' I mean that the rep type is not itself -- a newtype or type synonym. - -- The rep type has explicit for-alls for the tyvars of - -- the TyCon. Thus: + -- The rep type has free type variables the tyConTyVars + -- Thus: -- newtype T a = MkT [(a,Int)] - -- The rep type is forall a. [(a,Int)] + -- The rep type is [(a,Int)] -- -- The rep type isn't entirely simple: -- for a recursive newtype we pick () as the rep type @@ -267,7 +269,7 @@ mkAlgTyCon name kind tyvars theta argvrcs cons ncons sels flavour rec genInfo = gen_info } -mkClassTyCon name kind tyvars argvrcs con clas flavour +mkClassTyCon name kind tyvars argvrcs con clas flavour rec = AlgTyCon { tyConName = name, tyConUnique = nameUnique name, @@ -281,7 +283,7 @@ mkClassTyCon name kind tyvars argvrcs con clas flavour noOfDataCons = 1, algTyConClass = Just clas, algTyConFlavour = flavour, - algTyConRec = NonRecursive, + algTyConRec = rec, genInfo = Nothing } @@ -365,18 +367,26 @@ isAlgTyCon (AlgTyCon {}) = True isAlgTyCon (TupleTyCon {}) = True isAlgTyCon other = False --- isDataTyCon returns False for @newtype@ and for unboxed tuples -isDataTyCon (AlgTyCon {algTyConFlavour = new_or_data}) = case new_or_data of - NewTyCon _ -> False - other -> True +-- isDataTyCon returns True for data types that are represented by +-- heap-allocated constructors. +-- These are srcutinised by Core-level @case@ expressions, and they +-- get info tables allocated for them. +-- True for all @data@ types +-- False for newtypes +-- unboxed tuples +isDataTyCon (AlgTyCon {algTyConFlavour = new_or_data, algTyConRec = is_rec}) + = case new_or_data of + NewTyCon _ -> False + other -> True + isDataTyCon (TupleTyCon {tyConBoxed = boxity}) = isBoxed boxity isDataTyCon other = False isNewTyCon (AlgTyCon {algTyConFlavour = NewTyCon _}) = True isNewTyCon other = False -newTyConRep (AlgTyCon {algTyConFlavour = NewTyCon rep}) = Just rep -newTyConRep other = Nothing +newTyConRep :: TyCon -> ([TyVar], Type) +newTyConRep (AlgTyCon {tyConTyVars = tvs, algTyConFlavour = NewTyCon rep}) = (tvs, rep) -- A "product" tycon -- has *one* constructor, diff --git a/ghc/compiler/types/Type.lhs b/ghc/compiler/types/Type.lhs index 2b1a149f94..b782b198e3 100644 --- a/ghc/compiler/types/Type.lhs +++ b/ghc/compiler/types/Type.lhs @@ -6,7 +6,7 @@ \begin{code} module Type ( -- re-exports from TypeRep: - Type, + Type, PredType, TauType, ThetaType, Kind, TyVarSubst, superKind, superBoxity, -- KX and BX respectively @@ -30,46 +30,36 @@ module Type ( mkAppTy, mkAppTys, splitAppTy, splitAppTys, splitAppTy_maybe, - mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe, splitFunTys, splitFunTysN, + mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe, splitFunTys, funResultTy, funArgTy, zipFunTys, mkTyConApp, mkTyConTy, tyConAppTyCon, tyConAppArgs, splitTyConApp_maybe, splitTyConApp, - splitAlgTyConApp_maybe, splitAlgTyConApp, mkUTy, splitUTy, splitUTy_maybe, isUTy, uaUTy, unUTy, liftUTy, mkUTyM, isUsageKind, isUsage, isUTyVar, - mkSynTy, deNoteType, + mkSynTy, - repType, splitRepFunTys, splitNewType_maybe, typePrimRep, + repType, splitRepFunTys, typePrimRep, mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, - applyTy, applyTys, hoistForAllTys, isForAllTy, + applyTy, applyTys, isForAllTy, - -- Predicates and the like - PredType(..), getClassPredTys_maybe, getClassPredTys, - isPredTy, isClassPred, isTyVarClassPred, predHasFDs, - mkDictTy, mkPredTy, mkPredTys, splitPredTy_maybe, predTyUnique, - splitDictTy, splitDictTy_maybe, isDictTy, predRepTy, splitDFunTy, - mkClassPred, predMentionsIPs, inheritablePred, isIPPred, mkPredName, + -- Source types + SourceType(..), sourceTypeRep, - -- Tau, Rho, Sigma - TauType, RhoType, SigmaType, ThetaType, - isTauTy, mkRhoTy, splitRhoTy, splitMethodTy, - mkSigmaTy, isSigmaTy, splitSigmaTy, - getDFunTyKey, + -- Newtypes + mkNewTyConApp, -- Lifting and boxity - isUnLiftedType, isUnboxedTupleType, isAlgType, - isDataType, isNewType, isPrimitiveType, + isUnLiftedType, isUnboxedTupleType, isAlgType, -- Free variables tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta, - namesOfType, usageAnnOfType, typeKind, addFreeTyVars, - namesOfDFunHead, + usageAnnOfType, typeKind, addFreeTyVars, -- Tidying up for printing tidyType, tidyTypes, @@ -77,6 +67,9 @@ module Type ( tidyTyVar, tidyTyVars, tidyFreeTyVars, tidyTopType, tidyPred, + -- Comparison + eqType, eqKind, eqUsage, + -- Seq seqType, seqTypes @@ -103,11 +96,11 @@ import VarSet import OccName ( mkDictOcc ) import Name ( Name, NamedThing(..), OccName, mkLocalName, tidyOccName ) import NameSet -import Class ( classTyCon, classHasFDs, Class ) -import TyCon ( TyCon, +import Class ( classTyCon ) +import TyCon ( TyCon, isRecursiveTyCon, isUnboxedTupleTyCon, isUnLiftedTyCon, - isFunTyCon, isDataTyCon, isNewTyCon, newTyConRep, - isAlgTyCon, isSynTyCon, tyConArity, + isFunTyCon, isNewTyCon, newTyConRep, + isAlgTyCon, isSynTyCon, tyConArity, tyConTyVars, tyConKind, tyConDataCons, getSynTyConDefn, tyConPrimRep, isPrimTyCon ) @@ -132,13 +125,13 @@ import UniqSet ( sizeUniqSet ) -- Should come via VarSet \begin{code} hasMoreBoxityInfo :: Kind -> Kind -> Bool hasMoreBoxityInfo k1 k2 - | k2 == openTypeKind = True - | otherwise = k1 == k2 + | k2 `eqKind` openTypeKind = True + | otherwise = k1 `eqType` k2 defaultKind :: Kind -> Kind -- Used when generalising: default kind '?' to '*' -defaultKind kind | kind == openTypeKind = liftedTypeKind - | otherwise = kind +defaultKind kind | kind `eqKind` openTypeKind = liftedTypeKind + | otherwise = kind \end{code} @@ -160,25 +153,25 @@ mkTyVarTys :: [TyVar] -> [Type] mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy getTyVar :: String -> Type -> TyVar -getTyVar msg (TyVarTy tv) = tv -getTyVar msg (PredTy p) = getTyVar msg (predRepTy p) -getTyVar msg (NoteTy _ t) = getTyVar msg t +getTyVar msg (TyVarTy tv) = tv +getTyVar msg (SourceTy p) = getTyVar msg (sourceTypeRep p) +getTyVar msg (NoteTy _ t) = getTyVar msg t getTyVar msg ty@(UsageTy _ _) = pprPanic "getTyVar: UTy:" (text msg $$ pprType ty) -getTyVar msg other = panic ("getTyVar: " ++ msg) +getTyVar msg other = panic ("getTyVar: " ++ msg) getTyVar_maybe :: Type -> Maybe TyVar -getTyVar_maybe (TyVarTy tv) = Just tv -getTyVar_maybe (NoteTy _ t) = getTyVar_maybe t -getTyVar_maybe (PredTy p) = getTyVar_maybe (predRepTy p) +getTyVar_maybe (TyVarTy tv) = Just tv +getTyVar_maybe (NoteTy _ t) = getTyVar_maybe t +getTyVar_maybe (SourceTy p) = getTyVar_maybe (sourceTypeRep p) getTyVar_maybe ty@(UsageTy _ _) = pprPanic "getTyVar_maybe: UTy:" (pprType ty) -getTyVar_maybe other = Nothing +getTyVar_maybe other = Nothing isTyVarTy :: Type -> Bool -isTyVarTy (TyVarTy tv) = True -isTyVarTy (NoteTy _ ty) = isTyVarTy ty -isTyVarTy (PredTy p) = isTyVarTy (predRepTy p) +isTyVarTy (TyVarTy tv) = True +isTyVarTy (NoteTy _ ty) = isTyVarTy ty +isTyVarTy (SourceTy p) = isTyVarTy (sourceTypeRep p) isTyVarTy ty@(UsageTy _ _) = pprPanic "isTyVarTy: UTy:" (pprType ty) -isTyVarTy other = False +isTyVarTy other = False \end{code} @@ -191,7 +184,7 @@ invariant: use it. \begin{code} mkAppTy orig_ty1 orig_ty2 - = ASSERT( not (isPredTy orig_ty1) ) -- Predicates are of kind * + = ASSERT( not (isSourceTy orig_ty1) ) -- Source types are of kind * UASSERT2( not (isUTy orig_ty2), pprType orig_ty1 <+> pprType orig_ty2 ) -- argument must be unannotated mk_app orig_ty1 @@ -209,7 +202,7 @@ mkAppTys orig_ty1 [] = orig_ty1 -- returns to (Ratio Integer), which has needlessly lost -- the Rational part. mkAppTys orig_ty1 orig_tys2 - = ASSERT( not (isPredTy orig_ty1) ) -- Predicates are of kind * + = ASSERT( not (isSourceTy orig_ty1) ) -- Source types are of kind * UASSERT2( not (any isUTy orig_tys2), pprType orig_ty1 <+> fsep (map pprType orig_tys2) ) -- arguments must be unannotated mk_app orig_ty1 @@ -223,7 +216,7 @@ splitAppTy_maybe :: Type -> Maybe (Type, Type) splitAppTy_maybe (FunTy ty1 ty2) = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2) splitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2) splitAppTy_maybe (NoteTy _ ty) = splitAppTy_maybe ty -splitAppTy_maybe (PredTy p) = splitAppTy_maybe (predRepTy p) +splitAppTy_maybe (SourceTy p) = splitAppTy_maybe (sourceTypeRep p) splitAppTy_maybe (TyConApp tc []) = Nothing splitAppTy_maybe (TyConApp tc tys) = split tys [] where @@ -243,7 +236,7 @@ splitAppTys ty = split ty ty [] where split orig_ty (AppTy ty arg) args = split ty ty (arg:args) split orig_ty (NoteTy _ ty) args = split orig_ty ty args - split orig_ty (PredTy p) args = split orig_ty (predRepTy p) args + split orig_ty (SourceTy p) args = split orig_ty (sourceTypeRep p) args split orig_ty (FunTy ty1 ty2) args = ASSERT( null args ) (TyConApp funTyCon [], [unUTy ty1,unUTy ty2]) split orig_ty (TyConApp tc tc_args) args = (TyConApp tc [], tc_args ++ args) @@ -268,13 +261,13 @@ mkFunTys tys ty = UASSERT2( all isUTy (ty:tys), fsep (map pprType (tys++[ty])) ) splitFunTy :: Type -> (Type, Type) splitFunTy (FunTy arg res) = (arg, res) splitFunTy (NoteTy _ ty) = splitFunTy ty -splitFunTy (PredTy p) = splitFunTy (predRepTy p) +splitFunTy (SourceTy p) = splitFunTy (sourceTypeRep p) splitFunTy ty@(UsageTy _ _) = pprPanic "splitFunTy: UTy:" (pprType ty) splitFunTy_maybe :: Type -> Maybe (Type, Type) splitFunTy_maybe (FunTy arg res) = Just (arg, res) splitFunTy_maybe (NoteTy _ ty) = splitFunTy_maybe ty -splitFunTy_maybe (PredTy p) = splitFunTy_maybe (predRepTy p) +splitFunTy_maybe (SourceTy p) = splitFunTy_maybe (sourceTypeRep p) splitFunTy_maybe ty@(UsageTy _ _) = pprPanic "splitFunTy_maybe: UTy:" (pprType ty) splitFunTy_maybe other = Nothing @@ -283,41 +276,31 @@ splitFunTys ty = split [] ty ty where split args orig_ty (FunTy arg res) = split (arg:args) res res split args orig_ty (NoteTy _ ty) = split args orig_ty ty - split args orig_ty (PredTy p) = split args orig_ty (predRepTy p) + split args orig_ty (SourceTy p) = split args orig_ty (sourceTypeRep p) split args orig_ty (UsageTy _ _) = pprPanic "splitFunTys: UTy:" (pprType orig_ty) split args orig_ty ty = (reverse args, orig_ty) -splitFunTysN :: String -> Int -> Type -> ([Type], Type) -splitFunTysN msg orig_n orig_ty = split orig_n [] orig_ty orig_ty - where - split 0 args syn_ty ty = (reverse args, syn_ty) - split n args syn_ty (FunTy arg res) = split (n-1) (arg:args) res res - split n args syn_ty (NoteTy _ ty) = split n args syn_ty ty - split n args syn_ty (PredTy p) = split n args syn_ty (predRepTy p) - split n args syn_ty (UsageTy _ _) = pprPanic "splitFunTysN: UTy:" (pprType orig_ty) - split n args syn_ty ty = pprPanic ("splitFunTysN: " ++ msg) (int orig_n <+> pprType orig_ty) - zipFunTys :: Outputable a => [a] -> Type -> ([(a,Type)], Type) zipFunTys orig_xs orig_ty = split [] orig_xs orig_ty orig_ty where split acc [] nty ty = (reverse acc, nty) split acc (x:xs) nty (FunTy arg res) = split ((x,arg):acc) xs res res split acc xs nty (NoteTy _ ty) = split acc xs nty ty - split acc xs nty (PredTy p) = split acc xs nty (predRepTy p) + split acc xs nty (SourceTy p) = split acc xs nty (sourceTypeRep p) split acc xs nty (UsageTy _ _) = pprPanic "zipFunTys: UTy:" (ppr orig_xs <+> pprType orig_ty) split acc (x:xs) nty ty = pprPanic "zipFunTys" (ppr orig_xs <+> pprType orig_ty) funResultTy :: Type -> Type funResultTy (FunTy arg res) = res funResultTy (NoteTy _ ty) = funResultTy ty -funResultTy (PredTy p) = funResultTy (predRepTy p) +funResultTy (SourceTy p) = funResultTy (sourceTypeRep p) funResultTy (UsageTy _ ty) = funResultTy ty funResultTy ty = pprPanic "funResultTy" (pprType ty) funArgTy :: Type -> Type funArgTy (FunTy arg res) = arg funArgTy (NoteTy _ ty) = funArgTy ty -funArgTy (PredTy p) = funArgTy (predRepTy p) +funArgTy (SourceTy p) = funArgTy (sourceTypeRep p) funArgTy (UsageTy _ ty) = funArgTy ty funArgTy ty = pprPanic "funArgTy" (pprType ty) \end{code} @@ -326,13 +309,19 @@ funArgTy ty = pprPanic "funArgTy" (pprType ty) --------------------------------------------------------------------- TyConApp ~~~~~~~~ +@mkTyConApp@ is a key function, because it builds a TyConApp, FunTy or SourceTy, +as apppropriate. \begin{code} mkTyConApp :: TyCon -> [Type] -> Type mkTyConApp tycon tys - | isFunTyCon tycon && length tys == 2 - = case tys of - (ty1:ty2:_) -> FunTy (mkUTyM ty1) (mkUTyM ty2) + | isFunTyCon tycon, [ty1,ty2] <- tys + = FunTy (mkUTyM ty1) (mkUTyM ty2) + + | isNewTyCon tycon, -- A saturated newtype application; + not (isRecursiveTyCon tycon), -- Not recursive (we don't use SourceTypes for them) + length tys == tyConArity tycon -- use the SourceType form + = SourceTy (NType tycon tys) | otherwise = ASSERT(not (isSynTyCon tycon)) @@ -348,14 +337,10 @@ mkTyConTy tycon = ASSERT( not (isSynTyCon tycon) ) -- including functions are returned as Just .. tyConAppTyCon :: Type -> TyCon -tyConAppTyCon ty = case splitTyConApp_maybe ty of - Just (tc,_) -> tc - Nothing -> pprPanic "tyConAppTyCon" (pprType ty) +tyConAppTyCon ty = fst (splitTyConApp ty) tyConAppArgs :: Type -> [Type] -tyConAppArgs ty = case splitTyConApp_maybe ty of - Just (_,args) -> args - Nothing -> pprPanic "tyConAppArgs" (pprType ty) +tyConAppArgs ty = snd (splitTyConApp ty) splitTyConApp :: Type -> (TyCon, [Type]) splitTyConApp ty = case splitTyConApp_maybe ty of @@ -366,34 +351,9 @@ splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type]) splitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys) splitTyConApp_maybe (FunTy arg res) = Just (funTyCon, [unUTy arg,unUTy res]) splitTyConApp_maybe (NoteTy _ ty) = splitTyConApp_maybe ty -splitTyConApp_maybe (PredTy p) = splitTyConApp_maybe (predRepTy p) +splitTyConApp_maybe (SourceTy p) = splitTyConApp_maybe (sourceTypeRep p) splitTyConApp_maybe (UsageTy _ ty) = splitTyConApp_maybe ty splitTyConApp_maybe other = Nothing - --- splitAlgTyConApp_maybe looks for --- *saturated* applications of *algebraic* data types --- "Algebraic" => newtype, data type, or dictionary (not function types) --- We return the constructors too, so there had better be some. - -splitAlgTyConApp_maybe :: Type -> Maybe (TyCon, [Type], [DataCon]) -splitAlgTyConApp_maybe (TyConApp tc tys) - | isAlgTyCon tc && - tyConArity tc == length tys = Just (tc, tys, tyConDataCons tc) -splitAlgTyConApp_maybe (NoteTy _ ty) = splitAlgTyConApp_maybe ty -splitAlgTyConApp_maybe (PredTy p) = splitAlgTyConApp_maybe (predRepTy p) -splitAlgTyConApp_maybe (UsageTy _ ty)= splitAlgTyConApp_maybe ty -splitAlgTyConApp_maybe other = Nothing - -splitAlgTyConApp :: Type -> (TyCon, [Type], [DataCon]) - -- Here the "algebraic" property is an *assertion* -splitAlgTyConApp (TyConApp tc tys) = ASSERT( isAlgTyCon tc && tyConArity tc == length tys ) - (tc, tys, tyConDataCons tc) -splitAlgTyConApp (NoteTy _ ty) = splitAlgTyConApp ty -splitAlgTyConApp (PredTy p) = splitAlgTyConApp (predRepTy p) -splitAlgTyConApp (UsageTy _ ty) = splitAlgTyConApp ty -#ifdef DEBUG -splitAlgTyConApp ty = pprPanic "splitAlgTyConApp" (pprType ty) -#endif \end{code} @@ -409,21 +369,6 @@ mkSynTy syn_tycon tys (substTy (mkTyVarSubst tyvars tys) body) where (tyvars, body) = getSynTyConDefn syn_tycon - -deNoteType :: Type -> Type - -- Remove synonyms, but not Preds -deNoteType ty@(TyVarTy tyvar) = ty -deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys) -deNoteType (PredTy p) = PredTy (deNotePred p) -deNoteType (NoteTy _ ty) = deNoteType ty -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) - -deNotePred :: PredType -> PredType -deNotePred (ClassP c tys) = ClassP c (map deNoteType tys) -deNotePred (IParam n ty) = IParam n (deNoteType ty) \end{code} Notes on type synonyms @@ -446,22 +391,18 @@ interfaces. Notably this plays a role in tcTySigs in TcBinds.lhs. repType looks through (a) for-alls, and - (b) newtypes - (c) synonyms - (d) predicates - (e) usage annotations -It's useful in the back end where we're not -interested in newtypes anymore. + (b) synonyms + (c) predicates + (d) usage annotations +It's useful in the back end. \begin{code} repType :: Type -> Type repType (ForAllTy _ ty) = repType ty repType (NoteTy _ ty) = repType ty -repType (PredTy p) = repType (predRepTy p) +repType (SourceTy p) = repType (sourceTypeRep p) repType (UsageTy _ ty) = repType ty -repType ty = case splitNewType_maybe ty of - Just ty' -> repType ty' -- Still re-apply repType in case of for-all - Nothing -> ty +repType ty = ty splitRepFunTys :: Type -> ([Type], Type) -- Like splitFunTys, but looks through newtypes and for-alls @@ -476,20 +417,6 @@ typePrimRep ty = case repType ty of FunTy _ _ -> PtrRep AppTy _ _ -> PtrRep -- ?? TyVarTy _ -> PtrRep - -splitNewType_maybe :: Type -> Maybe Type --- Find the representation of a newtype, if it is one --- Looks through multiple levels of newtype, but does not look through for-alls -splitNewType_maybe (NoteTy _ ty) = splitNewType_maybe ty -splitNewType_maybe (PredTy p) = splitNewType_maybe (predRepTy p) -splitNewType_maybe (UsageTy _ ty) = splitNewType_maybe ty -splitNewType_maybe (TyConApp tc tys) = case newTyConRep tc of - Just rep_ty -> ASSERT( length tys == tyConArity tc ) - -- The assert should hold because repType should - -- only be applied to *types* (of kind *) - Just (applyTys rep_ty tys) - Nothing -> Nothing -splitNewType_maybe other = Nothing \end{code} @@ -522,7 +449,7 @@ splitForAllTy_maybe :: Type -> Maybe (TyVar, Type) splitForAllTy_maybe ty = splitFAT_m ty where splitFAT_m (NoteTy _ ty) = splitFAT_m ty - splitFAT_m (PredTy p) = splitFAT_m (predRepTy p) + splitFAT_m (SourceTy p) = splitFAT_m (sourceTypeRep p) splitFAT_m (ForAllTy tyvar ty) = Just(tyvar, ty) splitFAT_m (UsageTy _ ty) = splitFAT_m ty splitFAT_m _ = Nothing @@ -532,7 +459,7 @@ splitForAllTys ty = split ty ty [] where split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs) split orig_ty (NoteTy _ ty) tvs = split orig_ty ty tvs - split orig_ty (PredTy p) tvs = split orig_ty (predRepTy p) tvs + split orig_ty (SourceTy p) tvs = split orig_ty (sourceTypeRep p) tvs split orig_ty (UsageTy _ ty) tvs = split orig_ty ty tvs split orig_ty t tvs = (reverse tvs, orig_ty) \end{code} @@ -543,7 +470,7 @@ Applying a for-all to its arguments. Lift usage annotation as required. \begin{code} applyTy :: Type -> Type -> Type -applyTy (PredTy p) arg = applyTy (predRepTy p) arg +applyTy (SourceTy p) arg = applyTy (sourceTypeRep p) arg applyTy (NoteTy _ fun) arg = applyTy fun arg applyTy (ForAllTy tv ty) arg = UASSERT2( not (isUTy arg), ptext SLIT("applyTy") @@ -564,7 +491,7 @@ applyTys fun_ty arg_tys split fun_ty [] = (Nothing, [], fun_ty) split (NoteTy _ fun_ty) args = split fun_ty args - split (PredTy p) args = split (predRepTy p) args + split (SourceTy p) args = split (sourceTypeRep p) args split (ForAllTy tv fun_ty) (arg:args) = case split fun_ty args of (mu, tvs, ty) -> (mu, tv:tvs, ty) split (UsageTy u ty) args = case split ty args of @@ -574,23 +501,6 @@ applyTys fun_ty arg_tys split other_ty args = panic "applyTys" \end{code} -\begin{code} -hoistForAllTys :: Type -> Type - -- Move all the foralls to the top - -- e.g. T -> forall a. a ==> forall a. T -> a - -- Careful: LOSES USAGE ANNOTATIONS! -hoistForAllTys ty - = case hoist ty of { (tvs, body) -> mkForAllTys tvs body } - where - hoist :: Type -> ([TyVar], Type) - hoist ty = case splitFunTys ty of { (args, res) -> - case splitForAllTys res of { - ([], body) -> ([], ty) ; - (tvs1, body1) -> case hoist body1 of { (tvs2,body2) -> - (tvs1 ++ tvs2, mkFunTys args body2) - }}} -\end{code} - --------------------------------------------------------------------- UsageTy @@ -601,7 +511,8 @@ Constructing and taking apart usage types. \begin{code} mkUTy :: Type -> Type -> Type mkUTy u ty - = ASSERT2( typeKind u == usageTypeKind, ptext SLIT("mkUTy:") <+> pprType u <+> pprType ty ) + = ASSERT2( typeKind u `eqKind` usageTypeKind, + ptext SLIT("mkUTy:") <+> pprType u <+> pprType ty ) UASSERT2( not (isUTy ty), ptext SLIT("mkUTy:") <+> pprType u <+> pprType ty ) -- if u == usMany then ty else : ToDo? KSW 2000-10 #ifdef DO_USAGES @@ -657,8 +568,8 @@ mkUTyM ty = mkUTy usMany ty \begin{code} isUsageKind :: Kind -> Bool isUsageKind k - = ASSERT( typeKind k == superKind ) - k == usageTypeKind + = ASSERT( typeKind k `eqKind` superKind ) + k `eqKind` usageTypeKind isUsage :: Type -> Bool isUsage ty @@ -672,215 +583,36 @@ isUTyVar v %************************************************************************ %* * -\subsection{Predicates} +\subsection{Source types} %* * %************************************************************************ -"Dictionary" types are just ordinary data types, but you can -tell from the type constructor whether it's a dictionary or not. +A "source type" is a type that is a separate type as far as the type checker is +concerned, but which has low-level representation as far as the back end is concerned. -\begin{code} -mkClassPred clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) ) - ClassP clas tys - -isClassPred (ClassP clas tys) = True -isClassPred other = False - -isIPPred (IParam _ _) = True -isIPPred other = False - -isTyVarClassPred (ClassP clas tys) = all isTyVarTy tys -isTyVarClassPred other = False - -getClassPredTys_maybe :: PredType -> Maybe (Class, [Type]) -getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys) -getClassPredTys_maybe _ = Nothing - -getClassPredTys :: PredType -> (Class, [Type]) -getClassPredTys (ClassP clas tys) = (clas, tys) - -inheritablePred :: 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 4 with ?v = 9) --- The point is that g's type must be quantifed over ?v: --- 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 - -predMentionsIPs :: PredType -> NameSet -> Bool -predMentionsIPs (IParam n _) ns = n `elemNameSet` ns -predMentionsIPs other ns = False - -predHasFDs :: PredType -> Bool --- True if the predicate has functional depenencies; --- I.e. should participate in improvement -predHasFDs (IParam _ _) = True -predHasFDs (ClassP cls _) = classHasFDs cls - -mkDictTy :: Class -> [Type] -> Type -mkDictTy clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) ) - mkPredTy (ClassP clas tys) - -mkPredTy :: PredType -> Type -mkPredTy pred = PredTy pred - -mkPredTys :: ThetaType -> [Type] -mkPredTys preds = map PredTy preds - -predTyUnique :: PredType -> Unique -predTyUnique (IParam n _) = getUnique n -predTyUnique (ClassP clas tys) = getUnique clas - -predRepTy :: PredType -> Type --- Convert a predicate to its "representation type"; --- the type of evidence for that predicate, which is actually passed at runtime -predRepTy (ClassP clas tys) = TyConApp (classTyCon clas) tys -predRepTy (IParam n ty) = ty - -isPredTy :: Type -> Bool -isPredTy (NoteTy _ ty) = isPredTy ty -isPredTy (PredTy _) = True -isPredTy (UsageTy _ ty)= isPredTy ty -isPredTy _ = False - -isDictTy :: Type -> Bool -isDictTy (NoteTy _ ty) = isDictTy ty -isDictTy (PredTy (ClassP _ _)) = True -isDictTy (UsageTy _ ty) = isDictTy ty -isDictTy other = False - -splitPredTy_maybe :: Type -> Maybe PredType -splitPredTy_maybe (NoteTy _ ty) = splitPredTy_maybe ty -splitPredTy_maybe (PredTy p) = Just p -splitPredTy_maybe (UsageTy _ ty)= splitPredTy_maybe ty -splitPredTy_maybe other = Nothing - -splitDictTy :: Type -> (Class, [Type]) -splitDictTy (NoteTy _ ty) = splitDictTy ty -splitDictTy (PredTy (ClassP clas tys)) = (clas, tys) - -splitDictTy_maybe :: Type -> Maybe (Class, [Type]) -splitDictTy_maybe (NoteTy _ ty) = splitDictTy_maybe ty -splitDictTy_maybe (PredTy (ClassP clas tys)) = Just (clas, tys) -splitDictTy_maybe other = Nothing - -splitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type]) --- Split the type of a dictionary function -splitDFunTy ty - = case splitSigmaTy ty of { (tvs, theta, tau) -> - case splitDictTy tau of { (clas, tys) -> - (tvs, theta, clas, tys) }} - -namesOfDFunHead :: 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 splitSigmaTy dfun_ty of - (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty) - (map getName tvs) - -mkPredName :: Unique -> SrcLoc -> PredType -> Name -mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc -mkPredName uniq loc (IParam name ty) = name -\end{code} +Source types are always lifted. -%************************************************************************ -%* * -\subsection{Tau, sigma and rho} -%* * -%************************************************************************ - -@isTauTy@ tests for nested for-alls. - -\begin{code} -isTauTy :: Type -> Bool -isTauTy (TyVarTy v) = True -isTauTy (TyConApp _ tys) = all isTauTy tys -isTauTy (AppTy a b) = isTauTy a && isTauTy b -isTauTy (FunTy a b) = isTauTy a && isTauTy b -isTauTy (PredTy p) = isTauTy (predRepTy p) -isTauTy (NoteTy _ ty) = isTauTy ty -isTauTy (UsageTy _ ty) = isTauTy ty -isTauTy other = False -\end{code} - -\begin{code} -mkRhoTy :: [PredType] -> Type -> Type -mkRhoTy theta ty = UASSERT2( not (isUTy ty), pprType ty ) - foldr (\p r -> FunTy (mkUTyM (mkPredTy p)) (mkUTyM r)) ty theta - -splitRhoTy :: Type -> ([PredType], Type) -splitRhoTy ty = split ty ty [] - where - split orig_ty (FunTy arg res) ts = case splitPredTy_maybe arg of - Just p -> split res res (p:ts) - Nothing -> (reverse ts, orig_ty) - split orig_ty (NoteTy _ 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) -\end{code} - -The type of a method for class C is always of the form: - Forall a1..an. C a1..an => sig_ty -where sig_ty is the type given by the method's signature, and thus in general -is a ForallTy. At the point that splitMethodTy is called, it is expected -that the outer Forall has already been stripped off. splitMethodTy then -returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or -Usages stripped off. +The key function is sourceTypeRep which gives the representation of a source type: \begin{code} -splitMethodTy :: Type -> (PredType, Type) -splitMethodTy ty = split ty - where - split (FunTy arg res) = case splitPredTy_maybe arg of - Just p -> (p, res) - Nothing -> panic "splitMethodTy" - split (NoteTy _ ty) = split ty - split (UsageTy _ ty) = split ty - split _ = panic "splitMethodTy" -\end{code} - - -isSigmaType returns true of any qualified type. It doesn't *necessarily* have -any foralls. E.g. - f :: (?x::Int) => Int -> Int - -\begin{code} -mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau) - -isSigmaTy :: Type -> Bool -isSigmaTy (ForAllTy tyvar ty) = True -isSigmaTy (FunTy a b) = isPredTy a -isSigmaTy (NoteTy _ ty) = isSigmaTy ty -isSigmaTy (UsageTy _ ty) = isSigmaTy ty -isSigmaTy _ = False - -splitSigmaTy :: Type -> ([TyVar], [PredType], Type) -splitSigmaTy ty = - (tyvars, theta, tau) - where - (tyvars,rho) = splitForAllTys ty - (theta,tau) = splitRhoTy rho -\end{code} - -\begin{code} -getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to - -- construct a dictionary function name -getDFunTyKey (TyVarTy tv) = getOccName tv -getDFunTyKey (TyConApp tc _) = getOccName tc -getDFunTyKey (AppTy fun _) = getDFunTyKey fun -getDFunTyKey (NoteTy _ t) = getDFunTyKey t -getDFunTyKey (FunTy arg _) = getOccName funTyCon -getDFunTyKey (ForAllTy _ t) = getDFunTyKey t -getDFunTyKey (UsageTy _ t) = getDFunTyKey t --- PredTy shouldn't happen +sourceTypeRep :: SourceType -> Type +-- Convert a predicate to its "representation type"; +-- the type of evidence for that predicate, which is actually passed at runtime +sourceTypeRep (IParam n ty) = ty +sourceTypeRep (ClassP clas tys) = mkTyConApp (classTyCon clas) tys + -- Note the mkTyConApp; the classTyCon might be a newtype! +sourceTypeRep (NType tc tys) = case newTyConRep tc of + (tvs, rep_ty) -> substTy (mkTyVarSubst tvs tys) rep_ty + -- ToDo: Consider caching this substitution in a NType + +mkNewTyConApp :: TyCon -> [Type] -> SourceType +mkNewTyConApp tc tys = NType tc tys -- Here is where we might cache the substitution + +isSourceTy :: Type -> Bool +isSourceTy (NoteTy _ ty) = isSourceTy ty +isSourceTy (UsageTy _ ty) = isSourceTy ty +isSourceTy (SourceTy sty) = True +isSourceTy _ = False \end{code} @@ -899,7 +631,7 @@ typeKind :: Type -> Kind typeKind (TyVarTy tyvar) = tyVarKind tyvar typeKind (TyConApp tycon tys) = foldr (\_ k -> funResultTy k) (tyConKind tycon) tys typeKind (NoteTy _ ty) = typeKind ty -typeKind (PredTy _) = liftedTypeKind -- Predicates are always +typeKind (SourceTy _) = liftedTypeKind -- Predicates are always -- represented by lifted types typeKind (AppTy fun arg) = funResultTy (typeKind fun) @@ -931,7 +663,7 @@ tyVarsOfType (TyVarTy tv) = unitVarSet tv tyVarsOfType (TyConApp tycon tys) = tyVarsOfTypes tys tyVarsOfType (NoteTy (FTVNote tvs) ty2) = tvs tyVarsOfType (NoteTy (SynNote ty1) ty2) = tyVarsOfType ty1 -tyVarsOfType (PredTy p) = tyVarsOfPred p +tyVarsOfType (SourceTy sty) = tyVarsOfSourceType sty tyVarsOfType (FunTy arg res) = tyVarsOfType arg `unionVarSet` tyVarsOfType res tyVarsOfType (AppTy fun arg) = tyVarsOfType fun `unionVarSet` tyVarsOfType arg tyVarsOfType (ForAllTy tyvar ty) = tyVarsOfType ty `minusVarSet` unitVarSet tyvar @@ -941,31 +673,20 @@ tyVarsOfTypes :: [Type] -> TyVarSet tyVarsOfTypes tys = foldr (unionVarSet.tyVarsOfType) emptyVarSet tys tyVarsOfPred :: PredType -> TyVarSet -tyVarsOfPred (ClassP clas tys) = tyVarsOfTypes tys -tyVarsOfPred (IParam n ty) = tyVarsOfType ty +tyVarsOfPred = tyVarsOfSourceType -- Just a subtype + +tyVarsOfSourceType :: SourceType -> TyVarSet +tyVarsOfSourceType (IParam n ty) = tyVarsOfType ty +tyVarsOfSourceType (ClassP clas tys) = tyVarsOfTypes tys +tyVarsOfSourceType (NType tc tys) = tyVarsOfTypes tys tyVarsOfTheta :: ThetaType -> TyVarSet -tyVarsOfTheta = foldr (unionVarSet . tyVarsOfPred) emptyVarSet +tyVarsOfTheta = foldr (unionVarSet . tyVarsOfSourceType) emptyVarSet -- Add a Note with the free tyvars to the top of the type addFreeTyVars :: Type -> Type addFreeTyVars ty@(NoteTy (FTVNote _) _) = ty addFreeTyVars ty = NoteTy (FTVNote (tyVarsOfType ty)) ty - --- Find the free names of a type, including the type constructors and classes it mentions -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 (PredTy p) = namesOfType (predRepTy p) -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 \end{code} Usage annotations of a type @@ -983,7 +704,7 @@ usageAnnOfType ty goT (TyConApp tc tys) = concatMap goT tys goT (FunTy sty1 sty2) = goS sty1 ++ goS sty2 goT (ForAllTy mv ty) = goT ty - goT (PredTy p) = goT (predRepTy p) + goT (SourceTy p) = goT (sourceTypeRep p) goT ty@(UsageTy _ _) = pprPanic "usageAnnOfType: unexpected usage:" (pprType ty) goT (NoteTy note ty) = goT ty @@ -1045,7 +766,7 @@ tidyType env@(tidy_env, subst) ty go (TyConApp tycon tys) = let args = map go tys in args `seqList` TyConApp tycon args go (NoteTy note ty) = (NoteTy SAPPLY (go_note note)) SAPPLY (go ty) - go (PredTy p) = PredTy (tidyPred env p) + go (SourceTy sty) = SourceTy (tidySourceType env sty) go (AppTy fun arg) = (AppTy SAPPLY (go fun)) SAPPLY (go arg) go (FunTy fun arg) = (FunTy SAPPLY (go fun)) SAPPLY (go arg) go (ForAllTy tv ty) = ForAllTy tvp SAPPLY (tidyType envp ty) @@ -1058,9 +779,13 @@ tidyType env@(tidy_env, subst) ty tidyTypes env tys = map (tidyType env) tys -tidyPred :: TidyEnv -> PredType -> PredType -tidyPred env (ClassP clas tys) = ClassP clas (tidyTypes env tys) -tidyPred env (IParam n ty) = IParam n (tidyType env ty) +tidyPred :: TidyEnv -> SourceType -> SourceType +tidyPred = tidySourceType + +tidySourceType :: TidyEnv -> SourceType -> SourceType +tidySourceType env (IParam n ty) = IParam n (tidyType env ty) +tidySourceType env (ClassP clas tys) = ClassP clas (tidyTypes env tys) +tidySourceType env (NType tc tys) = NType tc (tidyTypes env tys) \end{code} @@ -1101,7 +826,8 @@ isUnLiftedType (ForAllTy tv ty) = isUnLiftedType ty isUnLiftedType (NoteTy _ ty) = isUnLiftedType ty isUnLiftedType (TyConApp tc _) = isUnLiftedTyCon tc isUnLiftedType (UsageTy _ ty) = isUnLiftedType ty -isUnLiftedType other = False +isUnLiftedType (SourceTy _) = False -- All source types are lifted +isUnLiftedType other = False isUnboxedTupleType :: Type -> Bool isUnboxedTupleType ty = case splitTyConApp_maybe ty of @@ -1114,28 +840,6 @@ isAlgType ty = case splitTyConApp_maybe ty of Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc ) isAlgTyCon tc other -> False - --- Should only be applied to *types*; hence the assert -isDataType :: Type -> Bool -isDataType ty = case splitTyConApp_maybe ty of - Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc ) - isDataTyCon tc - other -> False - -isNewType :: Type -> Bool -isNewType ty = case splitTyConApp_maybe ty of - Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc ) - isNewTyCon tc - other -> False - -isPrimitiveType :: Type -> Bool --- Returns types that are opaque to Haskell. --- Most of these are unlifted, but now that we interact with .NET, we --- may have primtive (foreign-imported) types that are lifted -isPrimitiveType ty = case splitTyConApp_maybe ty of - Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc ) - isPrimTyCon tc - other -> False \end{code} @@ -1151,7 +855,7 @@ seqType (TyVarTy tv) = tv `seq` () seqType (AppTy t1 t2) = seqType t1 `seq` seqType t2 seqType (FunTy t1 t2) = seqType t1 `seq` seqType t2 seqType (NoteTy note t2) = seqNote note `seq` seqType t2 -seqType (PredTy p) = seqPred p +seqType (SourceTy p) = seqPred p seqType (TyConApp tc tys) = tc `seq` seqTypes tys seqType (ForAllTy tv ty) = tv `seq` seqType ty seqType (UsageTy u ty) = seqType u `seq` seqType ty @@ -1164,9 +868,10 @@ seqNote :: TyNote -> () seqNote (SynNote ty) = seqType ty seqNote (FTVNote set) = sizeUniqSet set `seq` () -seqPred :: PredType -> () -seqPred (ClassP c tys) = c `seq` seqTypes tys -seqPred (IParam n ty) = n `seq` seqType ty +seqPred :: SourceType -> () +seqPred (ClassP c tys) = c `seq` seqTypes tys +seqPred (NType tc tys) = tc `seq` seqTypes tys +seqPred (IParam n ty) = n `seq` seqType ty \end{code} @@ -1176,78 +881,37 @@ seqPred (IParam n ty) = n `seq` seqType ty %* * %************************************************************************ +Comparison; don't use instances so that we know where it happens. +Look through newtypes but not usage types. \begin{code} -instance Eq Type where - ty1 == ty2 = case ty1 `compare` ty2 of { EQ -> True; other -> False } - -instance Ord Type where - compare ty1 ty2 = cmpTy emptyVarEnv ty1 ty2 - -cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering - -- The "env" maps type variables in ty1 to type variables in ty2 - -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2) - -- we in effect substitute tv2 for tv1 in t1 before continuing - - -- Get rid of NoteTy -cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2 -cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2 - - -- Get rid of PredTy -cmpTy env (PredTy p1) (PredTy p2) = cmpPred env p1 p2 -cmpTy env (PredTy p1) ty2 = cmpTy env (predRepTy p1) ty2 -cmpTy env ty1 (PredTy p2) = cmpTy env ty1 (predRepTy p2) - - -- Deal with equal constructors -cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of - Just tv1a -> tv1a `compare` tv2 - Nothing -> tv1 `compare` tv2 - -cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2 -cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2 -cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2) -cmpTy env (ForAllTy tv1 t1) (ForAllTy tv2 t2) = cmpTy (extendVarEnv env tv1 tv2) t1 t2 -cmpTy env (UsageTy u1 t1) (UsageTy u2 t2) = cmpTy env u1 u2 `thenCmp` cmpTy env t1 t2 - - -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < UsageTy -cmpTy env (AppTy _ _) (TyVarTy _) = GT - -cmpTy env (FunTy _ _) (TyVarTy _) = GT -cmpTy env (FunTy _ _) (AppTy _ _) = GT - -cmpTy env (TyConApp _ _) (TyVarTy _) = GT -cmpTy env (TyConApp _ _) (AppTy _ _) = GT -cmpTy env (TyConApp _ _) (FunTy _ _) = GT - -cmpTy env (ForAllTy _ _) (TyVarTy _) = GT -cmpTy env (ForAllTy _ _) (AppTy _ _) = GT -cmpTy env (ForAllTy _ _) (FunTy _ _) = GT -cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT - -cmpTy env (UsageTy _ _) other = GT - -cmpTy env _ _ = LT - - -cmpTys env [] [] = EQ -cmpTys env (t:ts) [] = GT -cmpTys env [] (t:ts) = LT -cmpTys env (t1:t1s) (t2:t2s) = cmpTy env t1 t2 `thenCmp` cmpTys env t1s t2s +eqType t1 t2 = eq_ty emptyVarEnv t1 t2 +eqKind = eqType -- No worries about looking +eqUsage = eqType -- through source types for these two + +-- Look through Notes +eq_ty env (NoteTy _ t1) t2 = eq_ty env t1 t2 +eq_ty env t1 (NoteTy _ t2) = eq_ty env t1 t2 + +-- Look through SourceTy. This is where the looping danger comes from +eq_ty env (SourceTy sty1) t2 = eq_ty env (sourceTypeRep sty1) t2 +eq_ty env t1 (SourceTy sty2) = eq_ty env t1 (sourceTypeRep sty2) + +-- The rest is plain sailing +eq_ty env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of + Just tv1a -> tv1a == tv2 + Nothing -> tv1 == tv2 +eq_ty env (ForAllTy tv1 t1) (ForAllTy tv2 t2) + | tv1 == tv2 = eq_ty env t1 t2 + | otherwise = eq_ty (extendVarEnv env tv1 tv2) t1 t2 +eq_ty env (AppTy s1 t1) (AppTy s2 t2) = (eq_ty env s1 s2) && (eq_ty env t1 t2) +eq_ty env (FunTy s1 t1) (FunTy s2 t2) = (eq_ty env s1 s2) && (eq_ty env t1 t2) +eq_ty env (UsageTy _ t1) (UsageTy _ t2) = eq_ty env t1 t2 +eq_ty env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 == tc2) && (eq_tys env tys1 tys2) +eq_ty env t1 t2 = False + +eq_tys env [] [] = True +eq_tys env (t1:tys1) (t2:tys2) = (eq_ty env t1 t2) && (eq_tys env tys2 tys2) +eq_tys env tys1 tys2 = False \end{code} -\begin{code} -instance Eq PredType where - p1 == p2 = case p1 `compare` p2 of { EQ -> True; other -> False } - -instance Ord PredType where - compare p1 p2 = cmpPred emptyVarEnv p1 p2 - -cmpPred :: TyVarEnv TyVar -> PredType -> PredType -> Ordering -cmpPred 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 -cmpPred env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2) -cmpPred env (IParam _ _) (ClassP _ _) = LT -cmpPred env (ClassP _ _) (IParam _ _) = GT -\end{code} diff --git a/ghc/compiler/types/TypeRep.lhs b/ghc/compiler/types/TypeRep.lhs index d48bcaca92..a00b86f628 100644 --- a/ghc/compiler/types/TypeRep.lhs +++ b/ghc/compiler/types/TypeRep.lhs @@ -5,9 +5,9 @@ \begin{code} module TypeRep ( - Type(..), TyNote(..), PredType(..), -- Representation visible to friends + Type(..), TyNote(..), SourceType(..), -- Representation visible to friends - Kind, ThetaType, RhoType, TauType, SigmaType, -- Synonyms + Kind, TauType, PredType, ThetaType, -- Synonyms TyVarSubst, superKind, superBoxity, -- KX and BX respectively @@ -92,6 +92,36 @@ ByteArray# Yes Yes No No ( a, b ) No Yes Yes Yes [a] No Yes Yes Yes + + + ---------------------- + A note about newtypes + ---------------------- + +Consider + newtype N = MkN Int + +Then we want N to be represented as an Int, and that's what we arrange. +The front end of the compiler [TcType.lhs] treats N as opaque, +the back end treats it as transparent [Type.lhs]. + +There's a bit of a problem with recursive newtypes + newtype P = MkP P + newtype Q = MkQ (Q->Q) + +Here the 'implicit expansion' we get from treating P and Q as transparent +would give rise to infinite types, which in turn makes eqType diverge. +Similarly splitForAllTys and splitFunTys can get into a loop. + +Solution: for recursive newtypes use a coerce, and treat the newtype +and its representation as distinct right through the compiler. That's +what you get if you use recursive newtypes. (They are rare, so who +cares if they are a tiny bit less efficient.) + +The TyCon still says "I'm a newtype", but we do not represent the +newtype application as a SourceType; instead as a TyConApp. + + %************************************************************************ %* * \subsection{The data type} @@ -102,6 +132,7 @@ ByteArray# Yes Yes No No \begin{code} type SuperKind = Type type Kind = Type +type TauType = Type type TyVarSubst = TyVarEnv Type @@ -125,8 +156,8 @@ data Type TyVar Type - | PredTy -- A Haskell predicate - PredType + | SourceTy -- A high level source type + SourceType -- ...can be expanded to a representation type... | UsageTy -- A usage-annotated type Type -- - Annotation of kind $ (i.e., usage annotation) @@ -137,13 +168,11 @@ data Type Type -- The expanded version data TyNote - = SynNote Type -- The unexpanded version of the type synonym; always a TyConApp - | FTVNote TyVarSet -- The free type variables of the noted expression + = FTVNote TyVarSet -- The free type variables of the noted expression -type ThetaType = [PredType] -type RhoType = Type -type TauType = Type -type SigmaType = Type + | SynNote Type -- Used for type synonyms + -- The Type is always a TyConApp, and is the un-expanded form. + -- The type to which the note is attached is the expanded form. \end{code} INVARIANT: UsageTys are optional, but may *only* appear immediately @@ -152,7 +181,19 @@ to be annotated (such as the type of an Id). NoteTys are transparent for the purposes of this rule. ------------------------------------- - Predicates + Source types + +A type of the form + SourceTy sty +represents a value whose type is the Haskell source type sty. +It can be expanded into its representation, but: + + * The type checker must treat it as opaque + * The rest of the compiler treats it as transparent + +There are two main uses + a) Haskell predicates + b) newtypes Consider these examples: f :: (Eq a) => a -> Int @@ -163,8 +204,13 @@ Here the "Eq a" and "?x :: Int -> Int" and "r\l" are all called *predicates* Predicates are represented inside GHC by PredType: \begin{code} -data PredType = ClassP Class [Type] - | IParam Name Type +data SourceType = ClassP Class [Type] -- Class predicate + | IParam Name Type -- Implicit parameter + | NType TyCon [Type] -- A *saturated*, *non-recursive* newtype application + -- [See notes at top about newtypes] + +type PredType = SourceType -- A subtype for predicates +type ThetaType = [PredType] \end{code} (We don't support TREX records yet, but the setup is designed diff --git a/ghc/compiler/types/Unify.lhs b/ghc/compiler/types/Unify.lhs deleted file mode 100644 index b284a6f3a7..0000000000 --- a/ghc/compiler/types/Unify.lhs +++ /dev/null @@ -1,303 +0,0 @@ -% -% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 -% -\section{Unify} - -This module contains a unifier and a matcher, both of which -use an explicit substitution - -\begin{code} -module Unify ( unifyTysX, unifyTyListsX, unifyExtendTysX, - allDistinctTyVars, - match, matchTy, matchTys, - ) where - -#include "HsVersions.h" - -import TypeRep ( Type(..) ) -- friend -import Type ( typeKind, tyVarsOfType, splitAppTy_maybe, getTyVar_maybe, - splitUTy, isUTy, deNoteType - ) - -import PprType () -- Instances - -- This import isn't strictly necessary, but it makes sure that - -- PprType is below Unify in the hierarchy, which in turn makes - -- fewer modules boot-import PprType - -import Var ( tyVarKind ) -import VarSet -import VarEnv ( TyVarSubstEnv, emptySubstEnv, lookupSubstEnv, extendSubstEnv, - SubstResult(..) - ) - -import Outputable -\end{code} - -%************************************************************************ -%* * -\subsection{Unification with an explicit substitution} -%* * -%************************************************************************ - -(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 getTyVar_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. - -\begin{code} -type MySubst - = (TyVarSet, -- Set of template tyvars - TyVarSubstEnv) -- Not necessarily idempotent - -unifyTysX :: TyVarSet -- Template tyvars - -> Type - -> Type - -> Maybe TyVarSubstEnv -unifyTysX tmpl_tyvars ty1 ty2 - = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv) - -unifyExtendTysX :: TyVarSet -- Template tyvars - -> TyVarSubstEnv -- Substitution to start with - -> Type - -> Type - -> Maybe TyVarSubstEnv -- Extended substitution -unifyExtendTysX tmpl_tyvars subst ty1 ty2 - = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst) - -unifyTyListsX :: TyVarSet -> [Type] -> [Type] - -> Maybe TyVarSubstEnv -unifyTyListsX tmpl_tyvars tys1 tys2 - = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv) - - -uTysX :: Type - -> Type - -> (MySubst -> Maybe result) - -> MySubst - -> Maybe result - -uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst -uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst - - -- Variables; go for uVar -uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst - | tyvar1 == tyvar2 - = k subst -uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_) - | tyvar1 `elemVarSet` tmpls - = uVarX tyvar1 ty2 k subst -uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_) - | tyvar2 `elemVarSet` tmpls - = uVarX tyvar2 ty1 k subst - - -- Functions; just check the two parts -uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst - = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst - - -- Type constructors must match -uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst - | (con1 == con2 && length tys1 == length tys2) - = uTyListsX tys1 tys2 k subst - - -- Applications need a bit of care! - -- They can match FunTy and TyConApp, so use splitAppTy_maybe - -- NB: we've already dealt with type variables and Notes, - -- so if one type is an App the other one jolly well better be too -uTysX (AppTy s1 t1) ty2 k subst - = case splitAppTy_maybe ty2 of - Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst - Nothing -> Nothing -- Fail - -uTysX ty1 (AppTy s2 t2) k subst - = case splitAppTy_maybe ty1 of - Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst - Nothing -> Nothing -- Fail - - -- Not expecting for-alls in unification -#ifdef DEBUG -uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)" -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 - - -uTyListsX [] [] k subst = k subst -uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst -uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths -\end{code} - -\begin{code} --- Invariant: tv1 is a unifiable variable -uVarX tv1 ty2 k subst@(tmpls, env) - = case lookupSubstEnv env tv1 of - Just (DoneTy ty1) -> -- Already bound - uTysX ty1 ty2 k subst - - Nothing -- Not already bound - | typeKind ty2 == 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 - where - occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty)) - occur_check_ok_tv tv | tv1 == tv = False - | otherwise = case lookupSubstEnv env tv of - Nothing -> True - Just (DoneTy ty) -> occur_check_ok ty -\end{code} - - - -%************************************************************************ -%* * -\subsection{Matching on types} -%* * -%************************************************************************ - -Matching is a {\em unidirectional} process, matching a type against a -template (which is just a type with type variables in it). The -matcher assumes that there are no repeated type variables in the -template, so that it simply returns a mapping of type variables to -types. It also fails on nested foralls. - -@matchTys@ matches corresponding elements of a list of templates and -types. It and @matchTy@ both ignore usage annotations, unlike the -main function @match@. - -\begin{code} -matchTy :: TyVarSet -- Template tyvars - -> Type -- Template - -> Type -- Proposed instance of template - -> Maybe TyVarSubstEnv -- Matching substitution - - -matchTys :: TyVarSet -- Template tyvars - -> [Type] -- Templates - -> [Type] -- Proposed instance of template - -> Maybe (TyVarSubstEnv, -- Matching substitution - [Type]) -- Left over instance types - -matchTy tmpls ty1 ty2 = match False ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv - -matchTys tmpls tys1 tys2 = match_list False tys1 tys2 tmpls - (\ (senv,tys) -> Just (senv,tys)) - emptySubstEnv -\end{code} - -@match@ is the main function. It takes a flag indicating whether -usage annotations are to be respected. - -\begin{code} -match :: Bool -- Respect usages? - -> Type -> Type -- Current match pair - -> TyVarSet -- Template vars - -> (TyVarSubstEnv -> Maybe result) -- Continuation - -> TyVarSubstEnv -- Current subst - -> Maybe result - --- When matching against a type variable, see if the variable --- has already been bound. If so, check that what it's bound to --- is the same as ty; if not, bind it and carry on. - -match uflag (TyVarTy v) ty tmpls k senv - | v `elemVarSet` tmpls - = -- v is a template variable - case lookupSubstEnv senv v of - Nothing -> UASSERT( not (isUTy ty) ) - k (extendSubstEnv senv v (DoneTy ty)) - Just (DoneTy ty') | ty' == ty -> k senv -- Succeeds - | otherwise -> Nothing -- Fails - - | otherwise - = -- v is not a template variable; ty had better match - -- Can't use (==) because types differ - case deNoteType ty of - TyVarTy v' | v == v' -> k senv -- Success - other -> Nothing -- Failure - -- This deNoteType is *required* and cost me much pain. I guess - -- the reason the Note-stripping case is *last* rather than first - -- is to preserve type synonyms etc., so I'm not moving it to the - -- top; but this means that (without the deNotetype) a type - -- variable may not match the pattern (TyVarTy v') as one would - -- expect, due to an intervening Note. KSW 2000-06. - -match uflag (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv - = match uflag arg1 arg2 tmpls (match uflag res1 res2 tmpls k) senv - -match uflag (AppTy fun1 arg1) ty2 tmpls k senv - = case splitAppTy_maybe ty2 of - Just (fun2,arg2) -> match uflag fun1 fun2 tmpls (match uflag arg1 arg2 tmpls k) senv - Nothing -> Nothing -- Fail - -match uflag (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv - | tc1 == tc2 - = match_list uflag tys1 tys2 tmpls k' senv - where - k' (senv', tys2') | null tys2' = k senv' -- Succeed - | otherwise = Nothing -- Fail - -match False (UsageTy _ ty1) ty2 tmpls k senv = match False ty1 ty2 tmpls k senv -match False ty1 (UsageTy _ ty2) tmpls k senv = match False ty1 ty2 tmpls k senv - -match True (UsageTy u1 ty1) (UsageTy u2 ty2) tmpls k senv - = match True u1 u2 tmpls (match True ty1 ty2 tmpls k) senv -match True ty1@(UsageTy _ _) ty2 tmpls k senv - = case splitUTy ty2 of { (u,ty2') -> match True ty1 ty2' tmpls k senv } -match True ty1 ty2@(UsageTy _ _) tmpls k senv - = case splitUTy ty1 of { (u,ty1') -> match True 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 - -- here! (WDP 95/05) -match uflag (NoteTy _ ty1) ty2 tmpls k senv = match uflag ty1 ty2 tmpls k senv -match uflag ty1 (NoteTy _ ty2) tmpls k senv = match uflag ty1 ty2 tmpls k senv - --- Catch-all fails -match _ _ _ _ _ _ = Nothing - -match_list uflag [] tys2 tmpls k senv = k (senv, tys2) -match_list uflag (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure -match_list uflag (ty1:tys1) (ty2:tys2) tmpls k senv - = match uflag ty1 ty2 tmpls (match_list uflag tys1 tys2 tmpls k) senv -\end{code} - - |