From bf1bf9fb07f1607aa66e7490b2df1ac1b62dd2d0 Mon Sep 17 00:00:00 2001 From: Manuel M T Chakravarty Date: Mon, 3 Mar 2008 06:33:47 +0000 Subject: [PATCH] Remove GADT refinements, part 4 - MkId.mkRecordSelId only used a special case of refineGadt, which doesn't need full unification. That special case is now implemented as TcGadt.matchRefine and TcGadt.refineGadt can finally go. --- compiler/basicTypes/MkId.lhs | 26 ++++--- compiler/typecheck/TcGadt.lhs | 164 ++++++++++++++--------------------------- 2 files changed, 69 insertions(+), 121 deletions(-) diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs index 7d472b1..4f30291 100644 --- a/compiler/basicTypes/MkId.lhs +++ b/compiler/basicTypes/MkId.lhs @@ -594,8 +594,8 @@ mkRecordSelId tycon field_label -- Allocate Ids. We do it a funny way round because field_dict_tys is -- almost always empty. Also note that we use max_dict_tys -- rather than n_dict_tys, because the latter gives an infinite loop: - -- n_dict tys depends on the_alts, which depens on arg_ids, which depends - -- on arity, which depends on n_dict tys. Sigh! Mega sigh! + -- n_dict tys depends on the_alts, which depens on arg_ids, which + -- depends on arity, which depends on n_dict tys. Sigh! Mega sigh! stupid_dict_ids = mkTemplateLocalsNum 1 stupid_dict_tys max_stupid_dicts = length (tyConStupidTheta tycon) field_dict_base = max_stupid_dicts + 1 @@ -638,13 +638,15 @@ mkRecordSelId tycon field_label -- foo :: forall a. T -> a -> a -- foo = /\a. \t:T. case t of { MkT f -> f a } - mk_alt data_con - = ASSERT2( data_ty `tcEqType` field_ty, ppr data_con $$ ppr data_ty $$ ppr field_ty ) + mk_alt data_con + = ASSERT2( data_ty `tcEqType` field_ty, + ppr data_con $$ ppr data_ty $$ ppr field_ty ) mkReboxingAlt rebox_uniqs data_con (ex_tvs ++ co_tvs ++ arg_vs) rhs where -- get pattern binders with types appropriately instantiated arg_uniqs = map mkBuiltinUnique [arg_base..] - (ex_tvs, co_tvs, arg_vs) = dataConOrigInstPat arg_uniqs data_con scrut_ty_args + (ex_tvs, co_tvs, arg_vs) = dataConOrigInstPat arg_uniqs data_con + scrut_ty_args rebox_base = arg_base + length ex_tvs + length co_tvs + length arg_vs rebox_uniqs = map mkBuiltinUnique [rebox_base..] @@ -658,14 +660,16 @@ mkRecordSelId tycon field_label -- Generate the refinement for b'=b, -- and apply to (Maybe b'), to get (Maybe b) - Succeeded refinement = gadtRefine emptyRefinement ex_tvs co_tvs - the_arg_id_ty = idType the_arg_id - (rhs, data_ty) = case refineType refinement the_arg_id_ty of - Just (co, data_ty) -> (Cast (Var the_arg_id) co, data_ty) - Nothing -> (Var the_arg_id, the_arg_id_ty) + reft = matchRefine co_tvs + the_arg_id_ty = idType the_arg_id + (rhs, data_ty) = + case refineType reft the_arg_id_ty of + Just (co, data_ty) -> (Cast (Var the_arg_id) co, data_ty) + Nothing -> (Var the_arg_id, the_arg_id_ty) field_vs = filter (not . isPredTy . idType) arg_vs - the_arg_id = assoc "mkRecordSelId:mk_alt" (field_lbls `zip` field_vs) field_label + the_arg_id = assoc "mkRecordSelId:mk_alt" + (field_lbls `zip` field_vs) field_label field_lbls = dataConFieldLabels data_con error_expr = mkRuntimeErrorApp rEC_SEL_ERROR_ID field_ty full_msg diff --git a/compiler/typecheck/TcGadt.lhs b/compiler/typecheck/TcGadt.lhs index e45d6bd..fd82201 100644 --- a/compiler/typecheck/TcGadt.lhs +++ b/compiler/typecheck/TcGadt.lhs @@ -10,16 +10,9 @@ %************************************************************************ \begin{code} -{-# OPTIONS -w #-} --- The above warning supression flag is a temporary kludge. --- While working on this module you are encouraged to remove it and fix --- any warnings in the module. See --- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings --- for details - module TcGadt ( Refinement, emptyRefinement, isEmptyRefinement, - gadtRefine, + matchRefine, refineType, refinePred, refineResType, tcUnifyTys, BindFlag(..) ) where @@ -39,7 +32,6 @@ import Maybes import Control.Monad import Outputable import TcType -import Unique import UniqFM import FastString \end{code} @@ -59,7 +51,7 @@ type InternalReft = TyVarEnv (Coercion, Type) -- Not necessarily idemopotent instance Outputable Refinement where - ppr (Reft in_scope env) + ppr (Reft _in_scope env) = ptext SLIT("Refinement") <+> braces (ppr env) @@ -109,86 +101,73 @@ refineResType reft ty %************************************************************************ %* * - 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 in_scope $ + = 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) + + 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} + %************************************************************************ %* * Unification @@ -221,23 +200,6 @@ 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) = 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 - ------------------------------ -- XXX Can we do this more nicely, by exploiting laziness? -- Or avoid needing it in the first place? fixTvSubstEnv :: InScopeSet -> TvSubstEnv -> TvSubstEnv @@ -248,11 +210,6 @@ fixTvSubstEnv in_scope env = f env then e else f e' ----------------------------- -tryToBind :: TyVarSet -> TyVar -> BindFlag -tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe - | otherwise = AvoidMe - \end{code} @@ -263,19 +220,6 @@ tryToBind tv_set tv | tv `elemVarSet` tv_set = BindMe %************************************************************************ \begin{code} -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 - emptyInternalReft :: InternalReft emptyInternalReft = emptyVarEnv -- 1.7.10.4