X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcGadt.lhs;h=3761c68fada484fa600e215005bb306fbcaf7f36;hb=2423c249f5ca7785d0ec89eb33e72662da7561c1;hp=4e71827d01b394463fccb11fb25ac9bd9570c529;hpb=ab22f4e6456820c1b5169d75f5975a94e61f54ce;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcGadt.lhs b/compiler/typecheck/TcGadt.lhs index 4e71827..3761c68 100644 --- a/compiler/typecheck/TcGadt.lhs +++ b/compiler/typecheck/TcGadt.lhs @@ -11,8 +11,9 @@ \begin{code} module TcGadt ( - Refinement, emptyRefinement, gadtRefine, - refineType, refineResType, + Refinement, emptyRefinement, isEmptyRefinement, + gadtRefine, + refineType, refinePred, refineResType, dataConCanMatch, tcUnifyTys, BindFlag(..) ) where @@ -22,6 +23,7 @@ module TcGadt ( import HsSyn import Coercion import Type + import TypeRep import DataCon import Var @@ -31,11 +33,11 @@ import ErrUtils import Maybes import Control.Monad import Outputable +import TcType #ifdef DEBUG import Unique import UniqFM -import TcType #endif \end{code} @@ -48,6 +50,8 @@ import TcType \begin{code} data Refinement = Reft InScopeSet InternalReft + +type InternalReft = TyVarEnv (Coercion, Type) -- INVARIANT: a->(co,ty) then co :: (a:=:ty) -- Not necessarily idemopotent @@ -59,17 +63,31 @@ instance Outputable Refinement where emptyRefinement :: Refinement emptyRefinement = (Reft emptyInScopeSet emptyVarEnv) +isEmptyRefinement :: Refinement -> Bool +isEmptyRefinement (Reft _ env) = isEmptyVarEnv env -refineType :: Refinement -> Type -> (HsWrapper, 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)) - = (WpCo (substTy co_subst ty), substTy tv_subst ty) + = Just (substTy co_subst ty, substTy tv_subst ty) | otherwise - = (idHsWrapper, 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) + +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 + = 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) @@ -78,11 +96,11 @@ 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 - (WpCo co, ty1) -> (WpCo (mkSymCoercion co), ty1) - (id_co, ty1) -> ASSERT( isIdHsWrapper id_co ) - (idHsWrapper, ty1) + Just (co, ty1) -> (WpCo (mkSymCoercion co), ty1) + Nothing -> (idHsWrapper, ty) \end{code} @@ -139,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) ) @@ -157,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} %************************************************************************ %* * @@ -206,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 | WpCo co'' <- co_fn = mkTransCoercion co co'' - | otherwise = ASSERT( isIdHsWrapper co_fn ) co ----------------------------- fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv @@ -224,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)) @@ -254,11 +275,6 @@ 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