From 1166c7d62f3fa9acd2084c90df6585cbbf868ceb Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Fri, 13 Oct 2006 11:58:01 +0000 Subject: [PATCH] Change type of TcGadt.refineType, plus consequences --- compiler/basicTypes/MkId.lhs | 12 ++++++------ compiler/typecheck/TcEnv.lhs | 12 +++++++----- compiler/typecheck/TcGadt.lhs | 22 ++++++++++------------ compiler/typecheck/TcPat.lhs | 9 +++++++-- 4 files changed, 30 insertions(+), 25 deletions(-) diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs index fd4e3e2..88d889a 100644 --- a/compiler/basicTypes/MkId.lhs +++ b/compiler/basicTypes/MkId.lhs @@ -592,14 +592,14 @@ mkRecordSelId tycon field_label -- T1 b' (c : [b]=[b']) (x:Maybe b') -- -> x `cast` Maybe (sym (right c)) - Succeeded refinement = gadtRefine emptyRefinement ex_tvs co_tvs - (co_fn, res_ty) = refineType refinement (idType the_arg_id) + -- Generate the refinement for b'=b, -- and apply to (Maybe b'), to get (Maybe b) - - rhs = case co_fn of - WpCo co -> Cast (Var the_arg_id) co - id_co -> ASSERT(isIdHsWrapper id_co) Var the_arg_id + Succeeded refinement = gadtRefine emptyRefinement ex_tvs co_tvs + the_arg_id_ty = idType the_arg_id + (rhs, res_ty) = case refineType refinement the_arg_id_ty of + Just (co, res_ty) -> (Cast (Var the_arg_id) co, res_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 diff --git a/compiler/typecheck/TcEnv.lhs b/compiler/typecheck/TcEnv.lhs index c638c04..2e3b80b 100644 --- a/compiler/typecheck/TcEnv.lhs +++ b/compiler/typecheck/TcEnv.lhs @@ -405,11 +405,13 @@ refineEnvironment reft thing_inside ; setLclEnv (env {tcl_env = le'}) thing_inside } where refine elt@(ATcId { tct_co = Just co, tct_type = ty }) - = let (co', ty') = refineType reft ty - in elt { tct_co = Just (co' <.> co), tct_type = ty' } - refine (ATyVar tv ty) = ATyVar tv (snd (refineType reft ty)) - -- Ignore the coercion that refineType returns - refine elt = elt + | Just (co', ty') <- refineType reft ty + = elt { tct_co = Just (WpCo co' <.> co), tct_type = ty' } + refine (ATyVar tv ty) + | Just (_, ty') <- refineType reft ty + = ATyVar tv ty' -- Ignore the coercion that refineType returns + + refine elt = elt -- Common case \end{code} %************************************************************************ diff --git a/compiler/typecheck/TcGadt.lhs b/compiler/typecheck/TcGadt.lhs index 4e71827..4129df5 100644 --- a/compiler/typecheck/TcGadt.lhs +++ b/compiler/typecheck/TcGadt.lhs @@ -21,7 +21,6 @@ module TcGadt ( import HsSyn import Coercion -import Type import TypeRep import DataCon import Var @@ -60,16 +59,17 @@ emptyRefinement :: Refinement emptyRefinement = (Reft emptyInScopeSet emptyVarEnv) -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) @@ -78,11 +78,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} @@ -206,15 +206,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 diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs index e1a1f24..c9b5d6e 100644 --- a/compiler/typecheck/TcPat.lhs +++ b/compiler/typecheck/TcPat.lhs @@ -279,7 +279,9 @@ tc_lpat :: LPat Name tc_lpat (L span pat) pat_ty pstate thing_inside = setSrcSpan span $ maybeAddErrCtxt (patCtxt pat) $ - do { let (coercion, pat_ty') = refineType (pat_reft pstate) pat_ty + do { let mb_reft = refineType (pat_reft pstate) pat_ty + pat_ty' = case mb_reft of { Just (_, ty') -> ty'; Nothing -> pat_ty } + -- Make sure the result type reflects the current refinement -- We must do this here, so that it correctly ``sees'' all -- the refinements to the left. Example: @@ -289,7 +291,10 @@ tc_lpat (L span pat) pat_ty pstate thing_inside -- pattern had better see it. ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside - ; return (mkCoPat coercion (L span pat') pat_ty, tvs, res) } + ; let final_pat = case mb_reft of + Nothing -> pat' + Just (co,_) -> CoPat (WpCo co) pat' pat_ty + ; return (L span final_pat, tvs, res) } -------------------- tc_pat :: PatState -- 1.7.10.4