Commit 1166c7d6 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com
Browse files

Change type of TcGadt.refineType, plus consequences

parent 5ad61e14
......@@ -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
......
......@@ -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}
%************************************************************************
......
......@@ -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
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment