X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcGadt.lhs;h=fd82201b763ca2fd00a65da9f463eaa8f3ab8e67;hb=bf1bf9fb07f1607aa66e7490b2df1ac1b62dd2d0;hp=4e71827d01b394463fccb11fb25ac9bd9570c529;hpb=ab22f4e6456820c1b5169d75f5975a94e61f54ce;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcGadt.lhs b/compiler/typecheck/TcGadt.lhs index 4e71827..fd82201 100644 --- a/compiler/typecheck/TcGadt.lhs +++ b/compiler/typecheck/TcGadt.lhs @@ -11,9 +11,9 @@ \begin{code} module TcGadt ( - Refinement, emptyRefinement, gadtRefine, - refineType, refineResType, - dataConCanMatch, + Refinement, emptyRefinement, isEmptyRefinement, + matchRefine, + refineType, refinePred, refineResType, tcUnifyTys, BindFlag(..) ) where @@ -22,8 +22,8 @@ module TcGadt ( import HsSyn import Coercion import Type + import TypeRep -import DataCon import Var import VarEnv import VarSet @@ -31,12 +31,9 @@ import ErrUtils import Maybes import Control.Monad import Outputable - -#ifdef DEBUG -import Unique -import UniqFM import TcType -#endif +import UniqFM +import FastString \end{code} @@ -48,28 +45,44 @@ 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 instance Outputable Refinement where - ppr (Reft in_scope env) + ppr (Reft _in_scope env) = ptext SLIT("Refinement") <+> braces (ppr env) 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 + = 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 - = (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) @@ -78,93 +91,82 @@ 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} %************************************************************************ %* * - Generating a type refinement + Simple generation of a type refinement %* * %************************************************************************ \begin{code} -gadtRefine :: Refinement - -> [TyVar] -- Bind these by preference - -> [CoVar] - -> MaybeErr Message Refinement +matchRefine :: [CoVar] -> Refinement \end{code} -(gadtRefine cvs) takes a list of coercion variables, and returns a -list of coercions, obtained by unifying the types equated by the -incoming coercions. The returned coercions all have kinds of form -(a:=:ty), where a is a rigid type variable. - -Example: - gadtRefine [c :: (a,Int):=:(Bool,b)] - = [ right (left c) :: a:=:Bool, - sym (right c) :: b:=:Int ] - -That is, given evidence 'c' that (a,Int)=(Bool,b), it returns derived -evidence in easy-to-use form. In particular, given any e::ty, we know -that: - e `cast` ty[right (left c)/a, sym (right c)/b] - :: ty [Bool/a, Int/b] - -Two refinements: - -- It can fail, if the coercion is unsatisfiable. - -- It's biased, by being given a set of type variables to bind - when there is a choice. Example: - MkT :: forall a. a -> T [a] - f :: forall b. T [b] -> b - f x = let v = case x of { MkT y -> y } - in ... - Here we want to bind [a->b], not the other way round, because - in this example the return type is wobbly, and we want the - program to typecheck - - --- E.g. (a, Bool, right (left c)) --- INVARIANT: in the triple (tv, ty, co), we have (co :: tv:=:ty) --- The result is idempotent: the +Given a list of coercions, where for each coercion c::(ty1~ty2), the type ty2 +is a specialisation of ty1, produce a type refinement that maps the variables +of ty1 to the corresponding sub-terms of ty2 using appropriate coercions; eg, + + matchRefine (co :: [(a, b)] ~ [(c, Maybe d)]) + = { right (left (right co)) :: a ~ c + , right (right co) :: b ~ Maybe d + } + +Precondition: The rhs types must indeed be a specialisation of the lhs types; + i.e., some free variables of the lhs are replaced with either distinct free + variables or proper type terms to obtain the rhs. (We don't perform full + unification or type matching here!) + +NB: matchRefine does *not* expand the type synonyms. \begin{code} -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 - - = ASSERT2( not $ any (`elemVarEnv` env1) (varSetElems $ tyVarsOfTypes $ map tyVarKind co_vars), - ppr env1 $$ ppr co_vars $$ ppr (map tyVarKind co_vars) ) - initUM (tryToBind tv_set) $ - do { -- Run the unifier, starting with an empty env - ; env2 <- foldM do_one emptyInternalReft co_vars - - -- Find the fixed point of the resulting - -- non-idempotent substitution - ; let tmp_env = env1 `plusVarEnv` env2 - out_env = fixTvCoEnv in_scope' tmp_env - ; WARN( not (null (badReftElts tmp_env)), ppr (badReftElts tmp_env) $$ ppr tmp_env ) - WARN( not (null (badReftElts out_env)), ppr (badReftElts out_env) $$ ppr out_env ) - return (Reft in_scope' out_env) } +matchRefine co_vars + = Reft in_scope (foldr plusVarEnv emptyVarEnv (map refineOne co_vars)) where - tv_set = mkVarSet ex_tvs - in_scope' = foldr extend in_scope co_vars + in_scope = foldr extend emptyInScopeSet 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)) - - do_one reft co_var = unify reft (TyVarTy co_var) ty1 ty2 - where - (ty1,ty2) = splitCoercionKind (tyVarKind co_var) -\end{code} + = extendInScopeSetSet in_scope $ + extendVarSet (tyVarsOfType (tyVarKind co_var)) co_var + + refineOne co_var = refine (TyVarTy co_var) ty1 ty2 + where + (ty1, ty2) = splitCoercionKind (tyVarKind co_var) + + refine co (TyVarTy tv) ty = unitVarEnv tv (co, ty) + refine co (TyConApp _ tys) (TyConApp _ tys') = refineArgs co tys tys' + refine co (NoteTy _ ty) ty' = refine co ty ty' + refine co ty (NoteTy _ ty') = refine co ty ty' + refine _ (PredTy _) (PredTy _) = + error "TcGadt.matchRefine: PredTy" + refine co (FunTy arg res) (FunTy arg' res') = + refine (mkRightCoercion (mkLeftCoercion co)) arg arg' + `plusVarEnv` + refine (mkRightCoercion co) res res' + refine co (AppTy fun arg) (AppTy fun' arg') = + refine (mkLeftCoercion co) fun fun' + `plusVarEnv` + refine (mkRightCoercion co) arg arg' + refine co (ForAllTy tv ty) (ForAllTy _tv ty') = + refine (mkForAllCoercion tv co) ty ty' `delVarEnv` tv + refine _ _ _ = error "RcGadt.matchRefine: mismatch" + + refineArgs :: Coercion -> [Type] -> [Type] -> InternalReft + refineArgs co tys tys' = + fst $ foldr refineArg (emptyVarEnv, id) (zip tys tys') + where + refineArg (ty, ty') (reft, coWrapper) + = (refine (mkRightCoercion (coWrapper co)) ty ty' `plusVarEnv` reft, + mkLeftCoercion . coWrapper) +\end{code} + %************************************************************************ %* * @@ -198,51 +200,15 @@ tcUnifyTys bind_fn tys1 tys2 ---------------------------- -fixTvCoEnv :: InScopeSet -> InternalReft -> InternalReft - -- Find the fixed point of a Refinement - -- (assuming it has no loops!) -fixTvCoEnv in_scope env - = fixpt - where - fixpt = mapVarEnv step env - - step (co, ty) = (co1, 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 - ------------------------------ +-- XXX Can we do this more nicely, by exploiting laziness? +-- Or avoid needing it in the first place? fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv -fixTvSubstEnv in_scope env - = fixpt +fixTvSubstEnv in_scope env = f env where - fixpt = mapVarEnv (substTy (mkTvSubst in_scope fixpt)) env - ----------------------------- -dataConCanMatch :: DataCon -> [Type] -> 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 - = isJust (tcUnifyTys (\tv -> BindMe) - (map (substTyVar subst . fst) eq_spec) - (map snd eq_spec)) - where - dc_tvs = dataConUnivTyVars con - eq_spec = dataConEqSpec con - subst = zipTopTvSubst dc_tvs tys - ----------------------------- -tryToBind :: TyVarSet -> TyVar -> BindFlag -tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe - | otherwise = AvoidMe - + f e = let e' = mapUFM (substTy (mkTvSubst in_scope e)) e + in if and $ eltsUFM $ intersectUFM_C tcEqType e e' + then e + else f e' \end{code} @@ -254,26 +220,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 --- Should be empty; used in asserions only -badReftElts env - = filter (not . ok) (ufmToList env) - where - ok :: (Unique, (Coercion, Type)) -> Bool - ok (u, (co, ty)) | Just tv <- tcGetTyVar_maybe ty1 - = varUnique tv == u && ty `tcEqType` ty2 - | otherwise = False - where - (ty1,ty2) = coercionKind co -#endif - emptyInternalReft :: InternalReft emptyInternalReft = emptyVarEnv