X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcType.lhs;h=b9ff393b608e5a6a9eb9ea9c5fbc94e02665d2bb;hb=ff818166a0a06e77becad9e28ed116f3b7f5cc8b;hp=cd4fe1447b0efc303e8939f4910217c509a2718a;hpb=a7d8f43718b167689c0a4a4c23b33a325e0239f1;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index cd4fe14..b9ff393 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -1,4 +1,4 @@ -% + % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 % \section[TcType]{Types used in the typechecker} @@ -16,22 +16,20 @@ is the principal client. \begin{code} module TcType ( -------------------------------- - -- TyThing - TyThing(..), -- instance NamedThing - - -------------------------------- -- Types TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, TcTyVar, TcTyVarSet, TcKind, -------------------------------- - -- TyVarDetails - TyVarDetails(..), isUserTyVar, isSkolemTyVar, - tyVarBindingInfo, + -- MetaDetails + Expected(..), TcRef, TcTyVarDetails(..), + MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo, + isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef, + isFlexi, isIndirect, -------------------------------- -- Builders - mkPhiTy, mkSigmaTy, + mkPhiTy, mkSigmaTy, hoistForAllTys, -------------------------------- -- Splitters @@ -40,30 +38,29 @@ module TcType ( tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs, tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitSigmaTy, - tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar, + tcGetTyVar_maybe, tcGetTyVar, --------------------------------- -- Predicates. -- Again, newtypes are opaque - tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, + tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX, isSigmaTy, isOverloadedTy, isDoubleTy, isFloatTy, isIntTy, isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isTauTy, tcIsTyVarTy, tcIsForAllTy, - allDistinctTyVars, --------------------------------- -- Misc type manipulators - deNoteType, classNamesOfTheta, + deNoteType, classesOfTheta, tyClsNamesOfType, tyClsNamesOfDFunHead, getDFunTyKey, --------------------------------- -- Predicate types getClassPredTys_maybe, getClassPredTys, - isPredTy, isClassPred, isTyVarClassPred, predHasFDs, + isClassPred, isTyVarClassPred, mkDictTy, tcSplitPredTy_maybe, - isDictTy, tcSplitDFunTy, predTyUnique, + isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique, mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, --------------------------------- @@ -77,112 +74,109 @@ module TcType ( isFFILabelTy, -- :: Type -> Bool isFFIDotnetTy, -- :: DynFlags -> Type -> Bool isFFIDotnetObjTy, -- :: Type -> Bool + isFFITy, -- :: Type -> Bool toDNType, -- :: Type -> DNType - --------------------------------- - -- Unifier and matcher - unifyTysX, unifyTyListsX, unifyExtendTysX, - matchTy, matchTys, match, - -------------------------------- -- Rexported from Type Kind, -- Stuff to do with kinds is insensitive to pre/post Tc unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds, - superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind, - isTypeKind, isAnyTypeKind, + isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, + isArgTypeKind, isSubKind, defaultKind, - Type, SourceType(..), PredType, ThetaType, + Type, PredType(..), ThetaType, mkForAllTy, mkForAllTys, mkFunTy, mkFunTys, zipFunTys, mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys, mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys, + -- Type substitutions + TvSubst(..), -- Representation visible to a few friends + TvSubstEnv, emptyTvSubst, + mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, + getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, + extendTvSubst, extendTvSubstList, isInScope, + substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr, + isUnLiftedType, -- Source types are always lifted isUnboxedTupleType, -- Ditto - isPrimitiveType, isTyVarTy, + isPrimitiveType, tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes, - tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, - typeKind, eqKind, + tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, tidySkolemTyVar, + typeKind, - tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta - ) where + tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta, -#include "HsVersions.h" + pprKind, pprParendKind, + pprType, pprParendType, pprTyThingCategory, + pprPred, pprTheta, pprThetaArrow, pprClassPred + ) where -import {-# SOURCE #-} PprType( pprType ) --- PprType imports TcType so that it can print intelligently +#include "HsVersions.h" -- friends: import TypeRep ( Type(..), TyNote(..), funTyCon ) -- friend import Type ( -- Re-exports tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, - tyVarsOfTheta, Kind, Type, SourceType(..), - PredType, ThetaType, unliftedTypeKind, + tyVarsOfTheta, Kind, PredType(..), + ThetaType, unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, + isLiftedTypeKind, isUnliftedTypeKind, mkArrowKinds, mkForAllTy, mkForAllTys, - defaultKind, isTypeKind, isAnyTypeKind, - mkFunTy, mkFunTys, zipFunTys, isTyVarTy, + defaultKind, isArgTypeKind, isOpenTypeKind, + mkFunTy, mkFunTys, zipFunTys, mkTyConApp, mkGenTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys, mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, - mkPredTys, isUnLiftedType, + mkPredTys, isUnLiftedType, isUnboxedTupleType, isPrimitiveType, splitTyConApp_maybe, tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes, tidyTyVarBndr, tidyOpenTyVar, - tidyOpenTyVars, eqKind, - hasMoreBoxityInfo, liftedBoxity, - superBoxity, typeKind, superKind, repType + tidyOpenTyVars, + isSubKind, deShadowTy, + + tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, + tcEqPred, tcCmpPred, tcEqTypeX, + + TvSubst(..), + TvSubstEnv, emptyTvSubst, + mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, + getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, + extendTvSubst, extendTvSubstList, isInScope, + substTy, substTys, substTyWith, substTheta, substTyVar, substTyVarBndr, + + typeKind, repType, + pprKind, pprParendKind, + pprType, pprParendType, pprTyThingCategory, + pprPred, pprTheta, pprThetaArrow, pprClassPred ) +import TyCon ( TyCon, isUnLiftedTyCon, tyConUnique ) import DataCon ( DataCon ) -import TyCon ( TyCon, isUnLiftedTyCon ) -import Class ( classHasFDs, Class ) -import Var ( TyVar, Id, tyVarKind, isMutTyVar, mutTyVarDetails ) -import ForeignCall ( Safety, playSafe - , DNType(..) - ) -import VarEnv +import Class ( Class ) +import Var ( TyVar, Id, isTcTyVar, mkTcTyVar, tyVarName, tyVarKind, tcTyVarDetails ) +import ForeignCall ( Safety, playSafe, DNType(..) ) import VarSet -- others: import CmdLineOpts ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt ) import Name ( Name, NamedThing(..), mkInternalName, getSrcLoc ) -import OccName ( OccName, mkDictOcc ) import NameSet +import VarEnv ( TidyEnv ) +import OccName ( OccName, mkDictOcc ) import PrelNames -- Lots (e.g. in isFFIArgumentTy) -import TysWiredIn ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon, - charTyCon, listTyCon ) +import TysWiredIn ( unitTyCon, charTyCon, listTyCon ) import BasicTypes ( IPName(..), ipNameName ) -import Unique ( Unique, Uniquable(..) ) -import SrcLoc ( SrcLoc ) -import Util ( cmpList, thenCmp, equalLength, snocView ) +import SrcLoc ( SrcLoc, SrcSpan ) +import Util ( snocView ) import Maybes ( maybeToBool, expectJust ) import Outputable -\end{code} - - -%************************************************************************ -%* * - TyThing -%* * -%************************************************************************ - -\begin{code} -data TyThing = AnId Id - | ADataCon DataCon - | ATyCon TyCon - | AClass Class - -instance NamedThing TyThing where - getName (AnId id) = getName id - getName (ATyCon tc) = getName tc - getName (AClass cl) = getName cl - getName (ADataCon dc) = getName dc +import DATA_IOREF \end{code} @@ -221,17 +215,7 @@ tau ::= tyvar -- In all cases, a (saturated) type synonym application is legal, -- provided it expands to the required form. - \begin{code} -type SigmaType = Type -type RhoType = Type -type TauType = Type -\end{code} - -\begin{code} -type TcTyVar = TyVar -- Might be a mutable tyvar -type TcTyVarSet = TyVarSet - type TcType = Type -- A TcType can have mutable type variables -- Invariant on ForAllTy in TcTypes: -- forall a. T @@ -243,7 +227,12 @@ type TcThetaType = ThetaType type TcSigmaType = TcType type TcRhoType = TcType type TcTauType = TcType -type TcKind = TcType +type TcKind = Kind +type TcTyVarSet = TyVarSet + +type TcRef a = IORef a +data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference + | Check ty -- The type to check during type checking \end{code} @@ -258,53 +247,143 @@ checking. It's attached to mutable type variables only. It's knot-tied back to Var.lhs. There is no reason in principle why Var.lhs shouldn't actually have the definition, but it "belongs" here. +Note [Signature skolems] +~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this + + x :: [a] + y :: b + (x,y,z) = ([y,z], z, head x) + +Here, x and y have type sigs, which go into the environment. We used to +instantiate their types with skolem constants, and push those types into +the RHS, so we'd typecheck the RHS with type + ( [a*], b*, c ) +where a*, b* are skolem constants, and c is an ordinary meta type varible. + +The trouble is that the occurrences of z in the RHS force a* and b* to +be the *same*, so we can't make them into skolem constants that don't unify +with each other. Alas. + +On the other hand, we *must* use skolems for signature type variables, +becuase GADT type refinement refines skolems only. + +One solution woudl be insist that in the above defn the programmer uses +the same type variable in both type signatures. But that takes explanation. + +The alternative (currently implemented) is to have a special kind of skolem +constant, SigSkokTv, which can unify with other SigSkolTvs. + + \begin{code} -data TyVarDetails - = SigTv -- Introduced when instantiating a type signature, - -- prior to checking that the defn of a fn does - -- have the expected type. Should not be instantiated. - -- - -- f :: forall a. a -> a - -- f = e - -- When checking e, with expected type (a->a), we - -- should not instantiate a - - | ClsTv -- Scoped type variable introduced by a class decl - -- class C a where ... - - | InstTv -- Ditto, but instance decl - - | PatSigTv -- Scoped type variable, introduced by a pattern - -- type signature - -- \ x::a -> e - - | VanillaTv -- Everything else - -isUserTyVar :: TcTyVar -> Bool -- Avoid unifying these if possible -isUserTyVar tv = case mutTyVarDetails tv of - VanillaTv -> False - other -> True - -isSkolemTyVar :: TcTyVar -> Bool -isSkolemTyVar tv = case mutTyVarDetails tv of - SigTv -> True - ClsTv -> True - InstTv -> True - oteher -> False - -tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars -tyVarBindingInfo tv - | isMutTyVar tv - = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv), - ptext SLIT("at") <+> ppr (getSrcLoc tv)] - | otherwise - = empty +type TcTyVar = TyVar -- Used only during type inference + +-- A TyVarDetails is inside a TyVar +data TcTyVarDetails + = MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type + | SkolemTv SkolemInfo -- A skolem constant + | SigSkolTv Name (IORef MetaDetails) -- Ditto, but from a type signature; + -- see Note [Signature skolems] + -- The MetaDetails, if filled in, will + -- always be another SigSkolTv + +data SkolemInfo + = SigSkol Name -- Bound at a type signature + | ClsSkol Class -- Bound at a class decl + | InstSkol Id -- Bound at an instance decl + | PatSkol DataCon -- An existential type variable bound by a pattern for + SrcSpan -- a data constructor with an existential type. E.g. + -- data T = forall a. Eq a => MkT a + -- f (MkT x) = ... + -- The pattern MkT x will allocate an existential type + -- variable for 'a'. + | ArrowSkol SrcSpan -- An arrow form (see TcArrows) + + | GenSkol [TcTyVar] -- Bound when doing a subsumption check for + TcType -- (forall tvs. ty) + SrcSpan + +data MetaDetails + = Flexi -- Flexi type variables unify to become + -- Indirects. + + | Indirect TcType -- Type indirections, treated as wobbly + -- for the purpose of GADT unification. + +tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar) +-- Tidy the type inside a GenSkol, preparatory to printing it +tidySkolemTyVar env tv + = ASSERT( isSkolemTyVar tv ) + (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1) where - details SigTv = ptext SLIT("type signature") - details ClsTv = ptext SLIT("class declaration") - details InstTv = ptext SLIT("instance declaration") - details PatSigTv = ptext SLIT("pattern type signature") - details VanillaTv = ptext SLIT("//vanilla//") -- Ditto + (env1, info1) = case tcTyVarDetails tv of + SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc)) + where + (env1, tvs1) = tidyOpenTyVars env tvs + (env2, ty1) = tidyOpenType env1 ty + info -> (env, info) + +pprTcTyVar :: TcTyVar -> SDoc +-- Print tyvar with info about its binding +pprTcTyVar tv + = quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv) + where + ppr_details (MetaTv _) = ptext SLIT("is a meta type variable") + ppr_details (SigSkolTv id _) = ptext SLIT("is bound by") <+> pprSkolInfo (SigSkol id) + ppr_details (SkolemTv info) = ptext SLIT("is bound by") <+> pprSkolInfo info + +pprSkolInfo :: SkolemInfo -> SDoc +pprSkolInfo (SigSkol id) = ptext SLIT("the type signature for") <+> quotes (ppr id) +pprSkolInfo (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls) +pprSkolInfo (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df) +pprSkolInfo (ArrowSkol loc) = ptext SLIT("the arrow form at") <+> ppr loc +pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc), + nest 2 (ptext SLIT("at") <+> ppr loc)] +pprSkolInfo (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type") + <+> quotes (ppr (mkForAllTys tvs ty)), + nest 2 (ptext SLIT("at") <+> ppr loc)] + +instance Outputable MetaDetails where + ppr Flexi = ptext SLIT("Flexi") + ppr (Indirect ty) = ptext SLIT("Indirect") <+> ppr ty + +isImmutableTyVar, isSkolemTyVar, isExistentialTyVar, isMetaTyVar :: TyVar -> Bool +isImmutableTyVar tv + | isTcTyVar tv = isSkolemTyVar tv + | otherwise = True + +isSkolemTyVar tv + = ASSERT( isTcTyVar tv ) + case tcTyVarDetails tv of + SkolemTv _ -> True + SigSkolTv _ _ -> True + MetaTv _ -> False + +isExistentialTyVar tv -- Existential type variable, bound by a pattern + = ASSERT( isTcTyVar tv ) + case tcTyVarDetails tv of + SkolemTv (PatSkol _ _) -> True + other -> False + +isMetaTyVar tv + = ASSERT( isTcTyVar tv ) + case tcTyVarDetails tv of + MetaTv _ -> True + other -> False + +metaTvRef :: TyVar -> IORef MetaDetails +metaTvRef tv + = ASSERT( isTcTyVar tv ) + case tcTyVarDetails tv of + MetaTv ref -> ref + other -> pprPanic "metaTvRef" (ppr tv) + +isFlexi, isIndirect :: MetaDetails -> Bool +isFlexi Flexi = True +isFlexi other = False + +isIndirect (Indirect _) = True +isIndirect other = False \end{code} @@ -317,11 +396,10 @@ tyVarBindingInfo tv \begin{code} mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau) -mkPhiTy :: [SourceType] -> Type -> Type +mkPhiTy :: [PredType] -> Type -> Type mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta \end{code} - @isTauTy@ tests for nested for-alls. \begin{code} @@ -330,7 +408,7 @@ 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 (SourceTy p) = True -- Don't look through source types +isTauTy (PredTy p) = True -- Don't look through source types isTauTy (NoteTy _ ty) = isTauTy ty isTauTy other = False \end{code} @@ -338,15 +416,14 @@ isTauTy other = False \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 (SourceTy (NType tc _)) = getOccName tc -- Newtypes are quite reasonable -getDFunTyKey ty = pprPanic "getDFunTyKey" (pprType ty) --- SourceTy shouldn't happen +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 ty = pprPanic "getDFunTyKey" (pprType ty) +-- PredTy shouldn't happen \end{code} @@ -401,10 +478,9 @@ tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of Nothing -> pprPanic "tcSplitTyConApp" (pprType ty) tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type]) -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) +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 -- Newtypes are opaque, so they may be split -- However, predicates are not treated -- as tycon applications by the type checker @@ -427,16 +503,13 @@ tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res } tcSplitAppTy_maybe :: Type -> Maybe (Type, Type) -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 (SourceTy (NType tc tys)) = tc_split_app tc tys --- Don't forget that newtype! -tcSplitAppTy_maybe (TyConApp tc tys) = tc_split_app tc tys -tcSplitAppTy_maybe other = Nothing - -tc_split_app tc tys = case snocView tys of - Just (tys',ty') -> Just (TyConApp tc tys', ty') - Nothing -> Nothing +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 (TyConApp tc tys) = case snocView tys of + Just (tys', ty') -> Just (TyConApp tc tys', ty') + Nothing -> Nothing +tcSplitAppTy_maybe other = Nothing tcSplitAppTy ty = case tcSplitAppTy_maybe ty of Just stuff -> stuff @@ -460,57 +533,20 @@ tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty) tcIsTyVarTy :: Type -> Bool tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe 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 stripped off. - -\begin{code} -tcSplitMethodTy :: Type -> (PredType, Type) -tcSplitMethodTy ty = split ty - where - split (FunTy arg res) = case tcSplitPredTy_maybe arg of - Just p -> (p, res) - Nothing -> panic "splitMethodTy" - split (NoteTy n ty) = split ty - split _ = panic "splitMethodTy" -tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type]) +tcSplitDFunTy :: Type -> ([TyVar], [PredType], Class, [Type]) -- Split the type of a dictionary function tcSplitDFunTy ty - = case tcSplitSigmaTy ty of { (tvs, theta, tau) -> - case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) -> + = case tcSplitSigmaTy ty of { (tvs, theta, tau) -> + case tcSplitDFunHead tau of { (clas, tys) -> (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 +tcSplitDFunHead :: Type -> (Class, [Type]) +tcSplitDFunHead tau + = case tcSplitPredTy_maybe tau of + Just (ClassP clas tys) -> (clas, tys) +\end{code} -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} %************************************************************************ @@ -519,36 +555,18 @@ allDistinctTyVars (ty:tys) acc %* * %************************************************************************ -"Predicates" are particular source types, namelyClassP or IParams - \begin{code} -isPred :: SourceType -> Bool -isPred (ClassP _ _) = True -isPred (IParam _ _) = True -isPred (NType _ _) = False - -isPredTy :: Type -> Bool -isPredTy (NoteTy _ 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 (SourceTy p) | isPred p = Just p -tcSplitPredTy_maybe other = Nothing +tcSplitPredTy_maybe (NoteTy _ ty) = tcSplitPredTy_maybe ty +tcSplitPredTy_maybe (PredTy p) = Just p +tcSplitPredTy_maybe other = Nothing predTyUnique :: PredType -> Unique predTyUnique (IParam n _) = getUnique (ipNameName n) predTyUnique (ClassP clas tys) = getUnique clas -predHasFDs :: PredType -> Bool --- True if the predicate has functional depenencies; --- I.e. should participate in improvement -predHasFDs (IParam _ _) = True -predHasFDs (ClassP cls _) = classHasFDs cls - -mkPredName :: Unique -> SrcLoc -> SourceType -> Name +mkPredName :: Unique -> SrcLoc -> PredType -> Name 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} @@ -559,14 +577,14 @@ mkPredName uniq loc (IParam ip ty) = mkInternalName uniq (getOccName (ipNameNa \begin{code} mkClassPred clas tys = ClassP clas tys -isClassPred :: SourceType -> Bool +isClassPred :: PredType -> Bool isClassPred (ClassP clas tys) = True isClassPred other = False isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys isTyVarClassPred other = False -getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type]) +getClassPredTys_maybe :: PredType -> Maybe (Class, [Type]) getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys) getClassPredTys_maybe _ = Nothing @@ -577,7 +595,7 @@ mkDictTy :: Class -> [Type] -> Type mkDictTy clas tys = mkPredTy (ClassP clas tys) isDictTy :: Type -> Bool -isDictTy (SourceTy p) = isClassPred p +isDictTy (PredTy p) = isClassPred p isDictTy (NoteTy _ ty) = isDictTy ty isDictTy other = False \end{code} @@ -585,7 +603,7 @@ isDictTy other = False --------------------- Implicit parameters --------------------------------- \begin{code} -isIPPred :: SourceType -> Bool +isIPPred :: PredType -> Bool isIPPred (IParam _ _) = True isIPPred other = False @@ -609,101 +627,6 @@ isLinearPred other = False %************************************************************************ %* * -\subsection{Comparison} -%* * -%************************************************************************ - -Comparison, taking note of newtypes, predicates, etc, -But ignoring usage types - -\begin{code} -tcEqType :: Type -> Type -> Bool -tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False } - -tcEqTypes :: [Type] -> [Type] -> Bool -tcEqTypes ty1 ty2 = case ty1 `tcCmpTypes` ty2 of { EQ -> True; other -> False } - -tcEqPred :: PredType -> PredType -> Bool -tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False } - -------------- -tcCmpType :: Type -> Type -> Ordering -tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2 - -tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2 - -tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2 -------------- -cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2 - -------------- -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 - - -- Look through NoteTy -cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2 -cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2 - - -- 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 (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2 -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 - - -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy -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 (SourceTy _) t2 = GT - -cmpTy env _ _ = LT -\end{code} - -\begin{code} -cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering -cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2) - -- Compare types as well as names for implicit parameters - -- This comparison is used exclusively (I think) for the - -- finite map built in TcSimplify -cmpSourceTy env (IParam _ _) sty = LT - -cmpSourceTy env (ClassP _ _) (IParam _ _) = GT -cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2) -cmpSourceTy env (ClassP _ _) (NType _ _) = LT - -cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2) -cmpSourceTy env (NType _ _) sty = GT -\end{code} - -PredTypes are used as a FM key in TcSimplify, -so we take the easy path and make them an instance of Ord - -\begin{code} -instance Eq SourceType where { (==) = tcEqPred } -instance Ord SourceType where { compare = tcCmpPred } -\end{code} - - -%************************************************************************ -%* * \subsection{Predicates} %* * %************************************************************************ @@ -724,6 +647,12 @@ isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty isOverloadedTy (FunTy a b) = isPredTy a isOverloadedTy (NoteTy n ty) = isOverloadedTy ty isOverloadedTy _ = False + +isPredTy :: Type -> Bool -- Belongs in TcType because it does + -- not look through newtypes, or predtypes (of course) +isPredTy (NoteTy _ ty) = isPredTy ty +isPredTy (PredTy sty) = True +isPredTy _ = False \end{code} \begin{code} @@ -743,6 +672,79 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of \end{code} + + +%************************************************************************ +%* * + Hoisting for-alls +%* * +%************************************************************************ + +hoistForAllTys is used for user-written type signatures only +We want to 'look through' type synonyms when doing this +so it's better done on the Type than the HsType + +It moves 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 + +Also: it eliminates duplicate constraints. These can show up +when hoisting constraints, notably implicit parameters. + +It tries hard to retain type synonyms if hoisting does not break one +up. Not only does this improve error messages, but there's a tricky +interaction with Haskell 98. H98 requires no unsaturated type +synonyms, which is checked by checkValidType. This runs after +hoisting, so we don't want hoisting to remove the SynNotes! (We can't +run validity checking before hoisting because in mutually-recursive +type definitions we postpone validity checking until after the knot is +tied.) + +\begin{code} +hoistForAllTys :: Type -> Type +hoistForAllTys ty + = go (deShadowTy ty) + -- Running over ty with an empty substitution gives it the + -- no-shadowing property. This is important. For example: + -- type Foo r = forall a. a -> r + -- foo :: Foo (Foo ()) + -- Here the hoisting should give + -- foo :: forall a a1. a -> a1 -> () + -- + -- What about type vars that are lexically in scope in the envt? + -- We simply rely on them having a different unique to any + -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars + -- out of the envt, which is boring and (I think) not necessary. + + where + go (TyVarTy tv) = TyVarTy tv + go (TyConApp tc tys) = TyConApp tc (map go tys) + go (PredTy pred) = PredTy pred -- No nested foralls + go (NoteTy (SynNote ty1) ty2) = NoteTy (SynNote (go ty1)) (go ty2) + go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard the free tyvar note + go (FunTy arg res) = mk_fun_ty (go arg) (go res) + go (AppTy fun arg) = AppTy (go fun) (go arg) + go (ForAllTy tv ty) = ForAllTy tv (go ty) + + -- mk_fun_ty does all the work. + -- It's building t1 -> t2: + -- if t2 is a for-all type, push t1 inside it + -- if t2 is (pred -> t3), check for duplicates + mk_fun_ty ty1 ty2 + | not (isSigmaTy ty2) -- No forall's, or context => + = FunTy ty1 ty2 + | PredTy p1 <- ty1 -- ty1 is a predicate + = if p1 `elem` theta then -- so check for duplicates + ty2 + else + mkSigmaTy tvs (p1:theta) tau + | otherwise + = mkSigmaTy tvs theta (FunTy ty1 tau) + where + (tvs, theta, tau) = tcSplitSigmaTy ty2 +\end{code} + + %************************************************************************ %* * \subsection{Misc} @@ -751,19 +753,18 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of \begin{code} deNoteType :: Type -> Type - -- Remove synonyms, but not source types + -- Remove synonyms, but not predicate types deNoteType ty@(TyVarTy tyvar) = ty deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys) -deNoteType (SourceTy p) = SourceTy (deNoteSourceType p) +deNoteType (PredTy p) = PredTy (deNotePredType 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) -deNoteSourceType :: SourceType -> SourceType -deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys) -deNoteSourceType (IParam n ty) = IParam n (deNoteType ty) -deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys) +deNotePredType :: PredType -> PredType +deNotePredType (ClassP c tys) = ClassP c (map deNoteType tys) +deNotePredType (IParam n ty) = IParam n (deNoteType ty) \end{code} Find the free tycons and classes of a type. This is used in the front @@ -775,9 +776,8 @@ 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 (PredTy (IParam n ty)) = tyClsNamesOfType ty +tyClsNamesOfType (PredTy (ClassP cl tys)) = unitNameSet (getName cl) `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 @@ -795,9 +795,9 @@ tyClsNamesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of (tvs,_,head_ty) -> tyClsNamesOfType head_ty -classNamesOfTheta :: ThetaType -> [Name] +classesOfTheta :: ThetaType -> [Class] -- Looks just for ClassP things; maybe it should check -classNamesOfTheta preds = [ getName c | ClassP c _ <- preds ] +classesOfTheta preds = [ c | ClassP c _ <- preds ] \end{code} @@ -812,6 +812,10 @@ restricted set of types as arguments and results (the restricting factor being the ) \begin{code} +isFFITy :: Type -> Bool +-- True for any TyCon that can possibly be an arg or result of an FFI call +isFFITy ty = checkRepTyCon legalFFITyCon ty + isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool -- Checks for valid argument type for a 'foreign import' isFFIArgumentTy dflags safety ty @@ -831,17 +835,17 @@ isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty isFFIDynArgumentTy :: Type -> Bool -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr, -- or a newtype of either. -isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon) +isFFIDynArgumentTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey] isFFIDynResultTy :: Type -> Bool -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr, -- or a newtype of either. -isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon) +isFFIDynResultTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey] isFFILabelTy :: Type -> Bool -- The type of a foreign label must be Ptr, FunPtr, Addr, -- or a newtype of either. -isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon) +isFFILabelTy = checkRepTyConKey [ptrTyConKey, funPtrTyConKey, addrTyConKey] isFFIDotnetTy :: DynFlags -> Type -> Bool isFFIDotnetTy dflags ty @@ -903,10 +907,17 @@ toDNType ty checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool -- Look through newtypes -- Non-recursive ones are transparent to splitTyConApp, - -- but recursive ones aren't + -- but recursive ones aren't. Manuel had: + -- newtype T = MkT (Ptr T) + -- and wanted it to work... checkRepTyCon check_tc ty | Just (tc,_) <- splitTyConApp_maybe (repType ty) = check_tc tc | otherwise = False + +checkRepTyConKey :: [Unique] -> Type -> Bool +-- Like checkRepTyCon, but just looks at the TyCon key +checkRepTyConKey keys + = checkRepTyCon (\tc -> tyConUnique tc `elem` keys) \end{code} ---------------------------------------------- @@ -946,6 +957,11 @@ legalOutgoingTyCon dflags safety tc | otherwise = marshalableTyCon dflags tc +legalFFITyCon :: TyCon -> Bool +-- True for any TyCon that can possibly be an arg or result of an FFI call +legalFFITyCon tc + = isUnLiftedTyCon tc || boxedMarshalableTyCon tc || tc == unitTyCon + marshalableTyCon dflags tc = (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc) || boxedMarshalableTyCon tc @@ -969,252 +985,3 @@ isByteArrayLikeTyCon tc = \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 - - -- Predicates -uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst - | n1 == n2 = uTysX t1 t2 k subst -uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst - | c1 == c2 = uTyListsX tys1 tys2 k subst -uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst - | tc1 == tc2 = uTyListsX tys1 tys2 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 && equalLength tys1 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 tcSplitAppTy_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 tcSplitAppTy_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 - - -- 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 `eqKind` tyVarKind tv1 - && occur_check_ok ty2 - -> -- No kind mismatch nor occur check - 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 ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv - -matchTys tmpls tys1 tys2 = match_list 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 :: 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 (TyVarTy v) ty tmpls k senv - | v `elemVarSet` tmpls - = -- v is a template variable - case lookupSubstEnv senv v of - 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 - - | otherwise - = -- v is not a template variable; ty had better match - -- Can't use (==) because types differ - case tcGetTyVar_maybe ty of - Just v' | v == v' -> k senv -- Success - other -> Nothing -- Failure - -- This tcGetTyVar_maybe is *required* because it must strip Notes. - -- 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. - - -- Predicates -match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv - | n1 == n2 = match t1 t2 tmpls k senv -match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv - | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv -match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv - | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv - - -- Functions; just check the two parts -match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv - = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv - -match (AppTy fun1 arg1) ty2 tmpls k senv - = case tcSplitAppTy_maybe ty2 of - Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv - Nothing -> Nothing -- Fail - -match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv - | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv - --- Newtypes are opaque; other source types should not happen -match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv - | tc1 == tc2 = match_list_exactly tys1 tys2 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 (NoteTy n1 ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv -match ty1 (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv - --- Catch-all fails -match _ _ _ _ _ = Nothing - -match_list_exactly tys1 tys2 tmpls k senv - = match_list tys1 tys2 tmpls k' senv - where - k' (senv', tys2') | null tys2' = k senv' -- Succeed - | otherwise = Nothing -- Fail - -match_list [] tys2 tmpls k senv = k (senv, tys2) -match_list (ty1:tys1) [] tmpls k senv = Nothing -- Not enough arg tys => failure -match_list (ty1:tys1) (ty2:tys2) tmpls k senv - = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv -\end{code}