Retain simplifications of implication constraints

[ghc-hetmet.git] / compiler / typecheck / TcPat.lhs

diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs
index 6cb177e..a5d4209 100644 (file)
--- a/compiler/typecheck/TcPat.lhs
+++ b/compiler/typecheck/TcPat.lhs
@@ -132,7 +132,7 @@ tcCheckExistentialPat pats [] pat_tys body_ty
   = return ()  -- Short cut for case when there are no existentials
 
 tcCheckExistentialPat pats ex_tvs pat_tys body_ty
-  = addErrCtxtM (sigPatCtxt (collectPatsBinders pats) ex_tvs pat_tys body_ty)  $
+  = addErrCtxtM (sigPatCtxt pats ex_tvs pat_tys body_ty)       $
     checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
 
 data PatState = PS {
@@ -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
@@ -526,14 +531,14 @@ tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
         -> HsConDetails Name (LPat Name) -> (PatState -> TcM a)
         -> TcM (Pat TcId, [TcTyVar], a)
 tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
-  = do { span <- getSrcSpanM   -- Span for the whole pattern
-       ; let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys) = dataConFullSig data_con
-             skol_info = PatSkol data_con span
+  = do { let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys) = dataConFullSig data_con
+             skol_info = PatSkol data_con
              origin    = SigOrigin skol_info
 
          -- Instantiate the constructor type variables [a->ty]
        ; ctxt_res_tys <- boxySplitTyConAppWithFamily tycon pat_ty
-       ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs
+       ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs  -- Get location from monad,
+                                                       -- not from ex_tvs
        ; let tenv     = zipTopTvSubst (univ_tvs ++ ex_tvs)
                                      (ctxt_res_tys ++ mkTyVarTys ex_tvs')
              eq_spec' = substEqSpec tenv eq_spec
@@ -548,7 +553,8 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
 
        ; loc <- getInstLoc origin
        ; dicts <- newDictBndrs loc theta'
-       ; dict_binds <- tcSimplifyCheck doc ex_tvs' dicts lie_req
+       ; dict_binds <- tcSimplifyCheckPat loc co_vars (pat_reft pstate') 
+                                          ex_tvs' dicts lie_req
 
        ; addDataConStupidTheta data_con ctxt_res_tys
 
@@ -562,8 +568,6 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
             ex_tvs' ++ inner_tvs, res)
        }
   where
-    doc = ptext SLIT("existential context for") <+> quotes (ppr data_con)
-
     -- Split against the family tycon if the pattern constructor belongs to a
     -- representation tycon.
     --
@@ -800,7 +804,8 @@ newLitInst orig lit res_ty  -- Make a LitInst
        ; res_tau <- zapToMonotype res_ty
        ; new_uniq <- newUnique
        ; let   lit_nm   = mkSystemVarName new_uniq FSLIT("lit")
-               lit_inst = LitInst lit_nm lit res_tau loc
+               lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit, 
+                                   tci_ty = res_tau, tci_loc = loc}
        ; extendLIE lit_inst
        ; return (HsVar (instToId lit_inst)) }
 \end{code}
@@ -889,7 +894,7 @@ existentialExplode pat
                text "In the binding group for"])
        4 (ppr pat)
 
-sigPatCtxt bound_ids bound_tvs pat_tys body_ty tidy_env 
+sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env 
   = do { pat_tys' <- mapM zonkTcType pat_tys
        ; body_ty' <- zonkTcType body_ty
        ; let (env1,  tidy_tys)    = tidyOpenTypes tidy_env (map idType show_ids)
@@ -899,9 +904,11 @@ sigPatCtxt bound_ids bound_tvs pat_tys body_ty tidy_env
                 sep [ptext SLIT("When checking an existential match that binds"),
                      nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
                      ptext SLIT("The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
-                     ptext SLIT("The body has type:") <+> ppr tidy_body_ty
+                     ptext SLIT("The body has type:") <+> ppr tidy_body_ty,
+                     ppr pats
                ]) }
   where
+    bound_ids = collectPatsBinders pats
     show_ids = filter is_interesting bound_ids
     is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs