X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcGadt.lhs;h=3761c68fada484fa600e215005bb306fbcaf7f36;hb=2423c249f5ca7785d0ec89eb33e72662da7561c1;hp=75d5c5461d8f912c2f4499a5fc5870cefe010cf6;hpb=4ea5fe11fbc339a7a1bce13cbb2a2301772b493a;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcGadt.lhs b/compiler/typecheck/TcGadt.lhs index 75d5c54..3761c68 100644 --- a/compiler/typecheck/TcGadt.lhs +++ b/compiler/typecheck/TcGadt.lhs @@ -1,4 +1,5 @@ % +% (c) The University of Glasgow 2006 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 % @@ -10,35 +11,34 @@ \begin{code} module TcGadt ( - Refinement, emptyRefinement, gadtRefine, - refineType, refineResType, + Refinement, emptyRefinement, isEmptyRefinement, + gadtRefine, + refineType, refinePred, refineResType, dataConCanMatch, tcUnifyTys, BindFlag(..) ) where -import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion ) -import Coercion ( Coercion, mkSymCoercion, mkTransCoercion, mkUnsafeCoercion, - mkLeftCoercion, mkRightCoercion, mkCoKind, coercionKindPredTy, - splitCoercionKind, decomposeCo, coercionKind ) -import TcType ( TvSubst(..), TvSubstEnv, substTy, mkTvSubst, - substTyVar, zipTopTvSubst, typeKind, - eqKind, isSubKind, repSplitAppTy_maybe, - tcView, tcGetTyVar_maybe - ) -import Type ( Type, tyVarsOfType, tyVarsOfTypes, tcEqType, mkTyVarTy ) -import TypeRep ( Type(..), PredType(..) ) -import DataCon ( DataCon, dataConUnivTyVars, dataConEqSpec ) -import Var ( CoVar, TyVar, tyVarKind, varUnique ) +#include "HsVersions.h" + +import HsSyn +import Coercion +import Type + +import TypeRep +import DataCon +import Var import VarEnv import VarSet -import ErrUtils ( Message ) -import Maybes ( MaybeErr(..), isJust ) -import Control.Monad ( foldM ) +import ErrUtils +import Maybes +import Control.Monad import Outputable -import Unique ( Unique ) -import UniqFM ( ufmToList ) +import TcType -#include "HsVersions.h" +#ifdef DEBUG +import Unique +import UniqFM +#endif \end{code} @@ -50,6 +50,8 @@ import UniqFM ( ufmToList ) \begin{code} data Refinement = Reft InScopeSet InternalReft + +type InternalReft = TyVarEnv (Coercion, Type) -- INVARIANT: a->(co,ty) then co :: (a:=:ty) -- Not necessarily idemopotent @@ -61,30 +63,44 @@ instance Outputable Refinement where emptyRefinement :: Refinement emptyRefinement = (Reft emptyInScopeSet emptyVarEnv) +isEmptyRefinement :: Refinement -> Bool +isEmptyRefinement (Reft _ env) = isEmptyVarEnv env -refineType :: Refinement -> Type -> (ExprCoFn, Type) +refineType :: Refinement -> Type -> Maybe (Coercion, Type) -- Apply the refinement to the type. -- If (refineType r ty) = (co, ty') -- Then co :: ty:=:ty' +-- Nothing => the refinement does nothing to this type refineType (Reft in_scope env) ty | not (isEmptyVarEnv env), -- Common case any (`elemVarEnv` env) (varSetElems (tyVarsOfType ty)) - = (ExprCoFn (substTy co_subst ty), substTy tv_subst ty) + = Just (substTy co_subst ty, substTy tv_subst ty) + | otherwise + = Nothing -- The type doesn't mention any refined type variables + where + tv_subst = mkTvSubst in_scope (mapVarEnv snd env) + co_subst = mkTvSubst in_scope (mapVarEnv fst env) + +refinePred :: Refinement -> PredType -> Maybe (Coercion, PredType) +refinePred (Reft in_scope env) pred + | not (isEmptyVarEnv env), -- Common case + any (`elemVarEnv` env) (varSetElems (tyVarsOfPred pred)) + = Just (mkPredTy (substPred co_subst pred), substPred tv_subst pred) | otherwise - = (idCoercion, ty) -- The type doesn't mention any refined type variables + = Nothing -- The type doesn't mention any refined type variables where tv_subst = mkTvSubst in_scope (mapVarEnv snd env) co_subst = mkTvSubst in_scope (mapVarEnv fst env) -refineResType :: Refinement -> Type -> (ExprCoFn, Type) +refineResType :: Refinement -> Type -> (HsWrapper, Type) -- Like refineType, but returns the 'sym' coercion -- If (refineResType r ty) = (co, ty') -- Then co :: ty':=:ty +-- It's convenient to return a HsWrapper here refineResType reft ty = case refineType reft ty of - (ExprCoFn co, ty1) -> (ExprCoFn (mkSymCoercion co), ty1) - (id_co, ty1) -> ASSERT( isIdCoercion id_co ) - (idCoercion, ty1) + Just (co, ty1) -> (WpCo (mkSymCoercion co), ty1) + Nothing -> (idHsWrapper, ty) \end{code} @@ -141,7 +157,7 @@ gadtRefine (Reft in_scope env1) ex_tvs co_vars -- Precondition: fvs( co_vars ) # env1 -- That is, the kinds of the co_vars are a --- fixed point of the incoming refinement +-- fixed point of the incoming refinement = ASSERT2( not $ any (`elemVarEnv` env1) (varSetElems $ tyVarsOfTypes $ map tyVarKind co_vars), ppr env1 $$ ppr co_vars $$ ppr (map tyVarKind co_vars) ) @@ -159,14 +175,16 @@ gadtRefine (Reft in_scope env1) where tv_set = mkVarSet ex_tvs in_scope' = foldr extend in_scope co_vars + + -- For each co_var, add it *and* the tyvars it mentions, to in_scope extend co_var in_scope - = extendInScopeSetSet (extendInScopeSet in_scope co_var) - (tyVarsOfType (tyVarKind co_var)) + = extendInScopeSetSet in_scope $ + extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2 where (ty1,ty2) = splitCoercionKind (tyVarKind co_var) -\end{code} +\end{code} %************************************************************************ %* * @@ -208,15 +226,13 @@ fixTvCoEnv in_scope env where fixpt = mapVarEnv step env - step (co, ty) = (co1, ty') + step (co, ty) = case refineType (Reft in_scope fixpt) ty of + Nothing -> (co, ty) + Just (co', ty') -> (mkTransCoercion co co', ty') -- Apply fixpt one step: -- Use refineType to get a substituted type, ty', and a coercion, co_fn, -- which justifies the substitution. If the coercion is not the identity -- then use transitivity with the original coercion - where - (co_fn, ty') = refineType (Reft in_scope fixpt) ty - co1 | ExprCoFn co'' <- co_fn = mkTransCoercion co co'' - | otherwise = ASSERT( isIdCoercion co_fn ) co ----------------------------- fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv @@ -226,12 +242,15 @@ fixTvSubstEnv in_scope env fixpt = mapVarEnv (substTy (mkTvSubst in_scope fixpt)) env ---------------------------- -dataConCanMatch :: DataCon -> [Type] -> Bool +dataConCanMatch :: [Type] -> DataCon -> Bool -- Returns True iff the data con can match a scrutinee of type (T tys) -- where T is the type constructor for the data con -- -- Instantiate the equations and try to unify them -dataConCanMatch con tys +dataConCanMatch tys con + | null eq_spec = True -- Common + | all isTyVarTy tys = True -- Also common + | otherwise = isJust (tcUnifyTys (\tv -> BindMe) (map (substTyVar subst . fst) eq_spec) (map snd eq_spec)) @@ -256,11 +275,7 @@ tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe %************************************************************************ \begin{code} -type InternalReft = TyVarEnv (Coercion, Type) - --- INVARIANT: a->(co,ty) then co :: (a:=:ty) --- Not necessarily idemopotent - +#ifdef DEBUG badReftElts :: InternalReft -> [(Unique, (Coercion,Type))] -- Return the BAD elements of the refinement -- Should be empty; used in asserions only @@ -273,6 +288,7 @@ badReftElts env | otherwise = False where (ty1,ty2) = coercionKind co +#endif emptyInternalReft :: InternalReft emptyInternalReft = emptyVarEnv @@ -374,11 +390,12 @@ uVar swap subst co tv1 ty -> unify subst (mkTransCoercion (mkSymCoercion co') co) ty' ty -- No, continue - Nothing -> uUnrefined subst (if swap then mkSymCoercion co else co) + Nothing -> uUnrefined swap subst co tv1 ty ty -uUnrefined :: InternalReft -- An existing substitution to extend +uUnrefined :: Bool -- Whether the input is swapped + -> InternalReft -- An existing substitution to extend -> Coercion -> TyVar -- Type variable to be unified -> Type -- with this type @@ -386,65 +403,62 @@ uUnrefined :: InternalReft -- An existing substitution to extend -> UM InternalReft -- We know that tv1 isn't refined --- PRE-CONDITION: in the call (uUnrefined r co tv1 ty2 ty2'), we know that +-- PRE-CONDITION: in the call (uUnrefined False r co tv1 ty2 ty2'), we know that -- co :: tv1:=:ty2 +-- and if the first argument is True instead, we know +-- co :: ty2:=:tv1 -uUnrefined subst co tv1 ty2 ty2' +uUnrefined swap subst co tv1 ty2 ty2' | Just ty2'' <- tcView ty2' - = uUnrefined subst co tv1 ty2 ty2'' -- Unwrap synonyms + = uUnrefined swap subst co tv1 ty2 ty2'' -- Unwrap synonyms -- This is essential, in case we have -- type Foo a = a -- and then unify a :=: Foo a -uUnrefined subst co tv1 ty2 (TyVarTy tv2) +uUnrefined swap subst co tv1 ty2 (TyVarTy tv2) | tv1 == tv2 -- Same type variable = return subst -- Check to see whether tv2 is refined | Just (co',ty') <- lookupVarEnv subst tv2 -- co' :: tv2:=:ty' - = uUnrefined subst (mkTransCoercion co co') tv1 ty' ty' + = uUnrefined False subst (mkTransCoercion (doSwap swap co) co') tv1 ty' ty' -- So both are unrefined; next, see if the kinds force the direction | eqKind k1 k2 -- Can update either; so check the bind-flags = do { b1 <- tvBindFlag tv1 ; b2 <- tvBindFlag tv2 ; case (b1,b2) of - (BindMe, _) -> bind False tv1 ty2 + (BindMe, _) -> bind swap tv1 ty2 - (AvoidMe, BindMe) -> bind True tv2 ty1 - (AvoidMe, _) -> bind False tv1 ty2 + (AvoidMe, BindMe) -> bind (not swap) tv2 ty1 + (AvoidMe, _) -> bind swap tv1 ty2 (WildCard, WildCard) -> return subst (WildCard, Skolem) -> return subst - (WildCard, _) -> bind True tv2 ty1 + (WildCard, _) -> bind (not swap) tv2 ty1 (Skolem, WildCard) -> return subst (Skolem, Skolem) -> failWith (misMatch ty1 ty2) - (Skolem, _) -> bind True tv2 ty1 + (Skolem, _) -> bind (not swap) tv2 ty1 } - | k1 `isSubKind` k2 = bindTv subst (mkSymCoercion co) tv2 ty1 -- Must update tv2 - | k2 `isSubKind` k1 = bindTv subst co tv1 ty2 -- Must update tv1 + | k1 `isSubKind` k2 = bindTv (not swap) subst co tv2 ty1 -- Must update tv2 + | k2 `isSubKind` k1 = bindTv swap subst co tv1 ty2 -- Must update tv1 | otherwise = failWith (kindMisMatch tv1 ty2) where ty1 = TyVarTy tv1 k1 = tyVarKind tv1 k2 = tyVarKind tv2 - bind swap tv ty = - ASSERT2( (coercionKindPredTy co1 `tcEqType` mkCoKind (mkTyVarTy tv) ty) - , (text "Refinement invariant failure: co = " <+> ppr co <+> ppr (coercionKindPredTy co) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty))) - return (extendVarEnv subst tv (co1,ty)) - where - co1 = if swap then mkSymCoercion co else co - -uUnrefined subst co tv1 ty2 ty2' -- ty2 is not a type variable + bind swap tv ty = extendReft swap subst tv co ty + +uUnrefined swap subst co tv1 ty2 ty2' -- ty2 is not a type variable | tv1 `elemVarSet` substTvSet subst (tyVarsOfType ty2') = failWith (occursCheck tv1 ty2) -- Occurs check | not (k2 `isSubKind` k1) = failWith (kindMisMatch tv1 ty2) -- Kind check | otherwise - = bindTv subst co tv1 ty2 -- Bind tyvar to the synonym if poss + = bindTv swap subst co tv1 ty2 -- Bind tyvar to the synonym if poss where k1 = tyVarKind tv1 k2 = typeKind ty2' @@ -459,15 +473,30 @@ substTvSet subst tvs Nothing -> unitVarSet tv Just (_,ty) -> substTvSet subst (tyVarsOfType ty) -bindTv subst co tv ty -- ty is not a type variable - = ASSERT2( (coercionKindPredTy co `tcEqType` mkCoKind (mkTyVarTy tv) ty), - (text "Refinement invariant failure: co = " <+> ppr co <+> ppr (coercionKindPredTy co) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty)) ) - do { b <- tvBindFlag tv +bindTv swap subst co tv ty -- ty is not a type variable + = do { b <- tvBindFlag tv ; case b of Skolem -> failWith (misMatch (TyVarTy tv) ty) WildCard -> return subst - other -> return (extendVarEnv subst tv (co,ty)) + other -> extendReft swap subst tv co ty } + +doSwap :: Bool -> Coercion -> Coercion +doSwap swap co = if swap then mkSymCoercion co else co + +extendReft :: Bool + -> InternalReft + -> TyVar + -> Coercion + -> Type + -> UM InternalReft +extendReft swap subst tv co ty + = ASSERT2( (coercionKindPredTy co1 `tcEqType` mkCoKind (mkTyVarTy tv) ty), + (text "Refinement invariant failure: co = " <+> ppr co1 <+> ppr (coercionKindPredTy co1) $$ text "subst = " <+> ppr tv <+> ppr (mkCoKind (mkTyVarTy tv) ty)) ) + return (extendVarEnv subst tv (co1, ty)) + where + co1 = doSwap swap co + \end{code} %************************************************************************ @@ -539,4 +568,4 @@ kindMisMatch tv1 t2 occursCheck tv ty = hang (ptext SLIT("Can't construct the infinite type")) 2 (ppr tv <+> equals <+> ppr ty) -\end{code} \ No newline at end of file +\end{code}