Change type of TcGadt.refineType, plus consequences

diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs
index fd4e3e2..88d889a 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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