Add quasi-quotation, courtesy of Geoffrey Mainland
[ghc-hetmet.git] / compiler / typecheck / TcPat.lhs
index a5d4209..5815688 100644 (file)
@@ -6,12 +6,19 @@
 TcPat: Typechecking patterns
 
 \begin{code}
-module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcOverloadedLit,
+{-# 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 TcPat ( tcLetPat, tcLamPat, tcLamPats, tcProcPat, tcOverloadedLit,
               addDataConStupidTheta, badFieldCon, polyPatSig ) where
 
 #include "HsVersions.h"
 
-import {-# SOURCE #-}  TcExpr( tcSyntaxOp )
+import {-# SOURCE #-}  TcExpr( tcSyntaxOp, tcInferRho)
 
 import HsSyn
 import TcHsSyn
@@ -31,9 +38,11 @@ import TcHsType
 import TysWiredIn
 import TcGadt
 import Type
+import Coercion
 import StaticFlags
 import TyCon
 import DataCon
+import DynFlags
 import PrelNames
 import BasicTypes hiding (SuccessFlag(..))
 import SrcLoc
@@ -42,6 +51,7 @@ import Util
 import Maybes
 import Outputable
 import FastString
+import Monad
 \end{code}
 
 
@@ -54,11 +64,12 @@ import FastString
 \begin{code}
 tcLetPat :: (Name -> Maybe TcRhoType)
         -> LPat Name -> BoxySigmaType 
-        -> TcM a
+        -> TcM a
         -> TcM (LPat TcId, a)
 tcLetPat sig_fn pat pat_ty thing_inside
   = do { let init_state = PS { pat_ctxt = LetPat sig_fn, 
-                               pat_reft = emptyRefinement }
+                               pat_reft = emptyRefinement,
+                               pat_eqs  = False }
        ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state (\ _ -> thing_inside)
 
        -- Don't know how to deal with pattern-bound existentials yet
@@ -86,28 +97,35 @@ tcLamPats :: [LPat Name]                            -- Patterns,
 --   5. Check that no existentials escape
 
 tcLamPats pats tys res_ty thing_inside
-  = tc_lam_pats (zipEqual "tcLamPats" pats tys)
+  = tc_lam_pats LamPat (zipEqual "tcLamPats" pats tys)
                (emptyRefinement, res_ty) thing_inside
 
 tcLamPat :: LPat Name -> BoxySigmaType 
         -> (Refinement,BoxyRhoType)            -- Result type
         -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type
         -> TcM (LPat TcId, a)
-tcLamPat pat pat_ty res_ty thing_inside
-  = do { ([pat'],thing) <- tc_lam_pats [(pat, pat_ty)] res_ty thing_inside
+
+tcProcPat = tc_lam_pat ProcPat
+tcLamPat  = tc_lam_pat LamPat
+
+tc_lam_pat ctxt pat pat_ty res_ty thing_inside
+  = do { ([pat'],thing) <- tc_lam_pats ctxt [(pat, pat_ty)] res_ty thing_inside
        ; return (pat', thing) }
 
 -----------------
-tc_lam_pats :: [(LPat Name,BoxySigmaType)]
+tc_lam_pats :: PatCtxt
+           -> [(LPat Name,BoxySigmaType)]
                    -> (Refinement,BoxyRhoType)                 -- Result type
                    -> ((Refinement,BoxyRhoType) -> TcM a)      -- Checker for body, given its result type
                    -> TcM ([LPat TcId], a)
-tc_lam_pats pat_ty_prs (reft, res_ty) thing_inside 
-  =  do        { let init_state = PS { pat_ctxt = LamPat, pat_reft = reft }
+tc_lam_pats ctxt pat_ty_prs (reft, res_ty) thing_inside 
+  =  do        { let init_state = PS { pat_ctxt = ctxt, pat_reft = reft, pat_eqs = False }
 
        ; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
-                                 refineEnvironment (pat_reft pstate') $
-                                 thing_inside (pat_reft pstate', res_ty)
+                                 refineEnvironment (pat_reft pstate') (pat_eqs pstate') $
+                                 if (pat_eqs pstate' && (not $ isRigidTy res_ty))
+                                    then failWithTc (nonRigidResult res_ty)
+                                    else thing_inside (pat_reft pstate', res_ty)
 
        ; let tys = map snd pat_ty_prs
        ; tcCheckExistentialPat pats' ex_tvs tys res_ty
@@ -137,11 +155,15 @@ tcCheckExistentialPat pats ex_tvs pat_tys body_ty
 
 data PatState = PS {
        pat_ctxt :: PatCtxt,
-       pat_reft :: Refinement  -- Binds rigid TcTyVars to their refinements
+       pat_reft :: Refinement, -- Binds rigid TcTyVars to their refinements
+       pat_eqs  :: Bool        -- <=> there are GADT equational constraints 
+                               --     for refinement 
   }
 
 data PatCtxt 
   = LamPat 
+  | ProcPat                            -- The pattern in (proc pat -> ...)
+                                       --      see Note [Arrows and patterns]
   | LetPat (Name -> Maybe TcRhoType)   -- Used for let(rec) bindings
 
 patSigCtxt :: PatState -> UserTypeCtxt
@@ -159,18 +181,6 @@ patSigCtxt other                   = LamPatSigCtxt
 
 \begin{code}
 tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
-tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty
-  = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
-               -- We have an undecorated binder, so we do rule ABS1,
-               -- by unboxing the boxy type, forcing any un-filled-in
-               -- boxes to become monotypes
-               -- NB that pat_ty' can still be a polytype:
-               --      data T = MkT (forall a. a->a)
-               --      f t = case t of { MkT g -> ... }
-               -- Here, the 'g' must get type (forall a. a->a) from the
-               -- MkT context
-       ; return (Id.mkLocalId bndr_name pat_ty') }
-
 tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
   | Just mono_ty <- lookup_sig bndr_name
   = do { mono_name <- newLocalName bndr_name
@@ -182,6 +192,18 @@ tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
        ; mono_name <- newLocalName bndr_name
        ; return (Id.mkLocalId mono_name pat_ty') }
 
+tcPatBndr (PS { pat_ctxt = _lam_or_proc }) bndr_name pat_ty
+  = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
+               -- We have an undecorated binder, so we do rule ABS1,
+               -- by unboxing the boxy type, forcing any un-filled-in
+               -- boxes to become monotypes
+               -- NB that pat_ty' can still be a polytype:
+               --      data T = MkT (forall a. a->a)
+               --      f t = case t of { MkT g -> ... }
+               -- Here, the 'g' must get type (forall a. a->a) from the
+               -- MkT context
+       ; return (Id.mkLocalId bndr_name pat_ty') }
+
 
 -------------------
 bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId)
@@ -196,6 +218,7 @@ bindInstsOfPatId id thing_inside
 -------------------
 unBoxPatBndrType  ty name = unBoxArgType ty (ptext SLIT("The variable") <+> quotes (ppr name))
 unBoxWildCardType ty      = unBoxArgType ty (ptext SLIT("A wild-card pattern"))
+unBoxViewPatType  ty pat  = unBoxArgType ty (ptext SLIT("The view pattern") <+> ppr pat)
 
 unBoxArgType :: BoxyType -> SDoc -> TcM TcType
 -- In addition to calling unbox, unBoxArgType ensures that the type is of ArgTypeKind; 
@@ -228,7 +251,7 @@ unBoxArgType ty pp_this
 
 Note [Nesting]
 ~~~~~~~~~~~~~~
-tcPat takes a "thing inside" over which the patter scopes.  This is partly
+tcPat takes a "thing inside" over which the pattern scopes.  This is partly
 so that tcPat can extend the environment for the thing_inside, but also 
 so that constraints arising in the thing_inside can be discharged by the
 pattern.
@@ -298,11 +321,12 @@ tc_lpat (L span pat) pat_ty pstate thing_inside
 
 --------------------
 tc_pat :: PatState
-       -> Pat Name -> BoxySigmaType    -- Fully refined result type
-       -> (PatState -> TcM a)  -- Thing inside
-       -> TcM (Pat TcId,       -- Translated pattern
-               [TcTyVar],      -- Existential binders
-               a)              -- Result of thing inside
+        -> Pat Name 
+        -> BoxySigmaType       -- Fully refined result type
+        -> (PatState -> TcM a) -- Thing inside
+        -> TcM (Pat TcId,      -- Translated pattern
+                [TcTyVar],     -- Existential binders
+                a)             -- Result of thing inside
 
 tc_pat pstate (VarPat name) pat_ty thing_inside
   = do { id <- tcPatBndr pstate name pat_ty
@@ -332,11 +356,26 @@ tc_pat pstate (BangPat pat) pat_ty thing_inside
 --
 -- Nor should a lazy pattern bind any existential type variables
 -- because they won't be in scope when we do the desugaring
+--
+-- Note [Hopping the LIE in lazy patterns]
+-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- In a lazy pattern, we must *not* discharge constraints from the RHS
+-- from dictionaries bound in the pattern.  E.g.
+--     f ~(C x) = 3
+-- We can't discharge the Num constraint from dictionaries bound by
+-- the pattern C!  
+--
+-- So we have to make the constraints from thing_inside "hop around" 
+-- the pattern.  Hence the getLLE and extendLIEs later.
+
 tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
-  = do { (pat', pat_tvs, res) <- tc_lpat pat pat_ty pstate $ \ _ ->
-                                 thing_inside pstate
-                                       -- Ignore refined pstate',
-                                       -- revert to pstate
+  = do { (pat', pat_tvs, (res,lie)) 
+               <- tc_lpat pat pat_ty pstate $ \ _ ->
+                  getLIE (thing_inside pstate)
+               -- Ignore refined pstate', revert to pstate
+       ; extendLIEs lie
+       -- getLIE/extendLIEs: see Note [Hopping the LIE in lazy patterns]
+
        -- Check no existentials
        ; if (null pat_tvs) then return ()
          else lazyPatErr lpat pat_tvs
@@ -347,6 +386,9 @@ tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
 
        ; return (LazyPat pat', [], res) }
 
+tc_pat _ p@(QuasiQuotePat _) _ _
+  = pprPanic "Should never see QuasiQuotePat in type checker" (ppr p)
+
 tc_pat pstate (WildPat _) pat_ty thing_inside
   = do { pat_ty' <- unBoxWildCardType pat_ty   -- Make sure it's filled in with monotypes
        ; res <- thing_inside pstate
@@ -365,6 +407,34 @@ tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
            -- If you fix it, don't forget the bindInstsOfPatIds!
        ; return (AsPat (L nm_loc bndr_id) pat', tvs, res) }
 
+tc_pat pstate (orig@(ViewPat expr pat _)) overall_pat_ty thing_inside 
+  = do { -- morally, expr must have type
+         -- `forall a1...aN. OPT' -> B` 
+         -- where overall_pat_ty is an instance of OPT'.
+         -- Here, we infer a rho type for it,
+         -- which replaces the leading foralls and constraints
+         -- with fresh unification variables.
+         (expr',expr'_inferred) <- tcInferRho expr
+         -- next, we check that expr is coercible to `overall_pat_ty -> pat_ty`
+       ; let expr'_expected = \ pat_ty -> (mkFunTy overall_pat_ty pat_ty)
+         -- tcSubExp: expected first, offered second
+         -- returns coercion
+         -- 
+         -- NOTE: this forces pat_ty to be a monotype (because we use a unification 
+         -- variable to find it).  this means that in an example like
+         -- (view -> f)    where view :: _ -> forall b. b
+         -- we will only be able to use view at one instantation in the
+         -- rest of the view
+       ; (expr_coerc, pat_ty) <- tcInfer $ \ pat_ty -> 
+               tcSubExp ViewPatOrigin (expr'_expected pat_ty) expr'_inferred
+
+         -- pattern must have pat_ty
+       ; (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
+         -- this should get zonked later on, but we unBox it here
+         -- so that we do the same checks as above
+       ; annotation_ty <- unBoxViewPatType overall_pat_ty orig        
+       ; return (ViewPat (mkLHsWrap expr_coerc expr') pat' annotation_ty, tvs, res) }
+
 -- Type signatures in patterns
 -- See Note [Pattern coercions] below
 tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
@@ -379,20 +449,26 @@ tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
 ------------------------
 -- Lists, tuples, arrays
 tc_pat pstate (ListPat pats _) pat_ty thing_inside
-  = do { elt_ty <- boxySplitListTy pat_ty
+  = do { (elt_ty, coi) <- boxySplitListTy pat_ty
+        ; let scoi = mkSymCoI coi
        ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
                                                pats pstate thing_inside
-       ; return (ListPat pats' elt_ty, pats_tvs, res) }
+       ; return (mkCoPatCoI scoi (ListPat pats' elt_ty) pat_ty, pats_tvs, res) 
+        }
 
 tc_pat pstate (PArrPat pats _) pat_ty thing_inside
-  = do { [elt_ty] <- boxySplitTyConApp parrTyCon pat_ty
+  = do { (elt_ty, coi) <- boxySplitPArrTy pat_ty
+        ; let scoi = mkSymCoI coi
        ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
                                                pats pstate thing_inside 
-       ; ifM (null pats) (zapToMonotype pat_ty)        -- c.f. ExplicitPArr in TcExpr
-       ; return (PArrPat pats' elt_ty, pats_tvs, res) }
+       ; ifM (null pats) (zapToMonotype pat_ty)  -- c.f. ExplicitPArr in TcExpr
+       ; return (mkCoPatCoI scoi (PArrPat pats' elt_ty) pat_ty, pats_tvs, res)
+        }
 
 tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
-  = do { arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty
+  = do { let tc = tupleTyCon boxity (length pats)
+        ; (arg_tys, coi) <- boxySplitTyConApp tc pat_ty
+        ; let scoi = mkSymCoI coi
        ; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys)
                                               pstate thing_inside
 
@@ -400,13 +476,17 @@ tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
        -- so that we can experiment with lazy tuple-matching.
        -- This is a pretty odd place to make the switch, but
        -- it was easy to do.
-       ; let unmangled_result = TuplePat pats' boxity pat_ty
+       ; let pat_ty'          = mkTyConApp tc arg_tys
+                                     -- pat_ty /= pat_ty iff coi /= IdCo
+              unmangled_result = TuplePat pats' boxity pat_ty'
              possibly_mangled_result
-               | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result)
-               | otherwise                               = unmangled_result
+               | opt_IrrefutableTuples && 
+                  isBoxed boxity            = LazyPat (noLoc unmangled_result)
+               | otherwise                 = unmangled_result
 
-       ; ASSERT( length arg_tys == length pats )       -- Syntactically enforced
-         return (possibly_mangled_result, pats_tvs, res) }
+       ; ASSERT( length arg_tys == length pats )      -- Syntactically enforced
+         return (mkCoPatCoI scoi possibly_mangled_result pat_ty, pats_tvs, res)
+        }
 
 ------------------------
 -- Data constructors
@@ -418,13 +498,20 @@ tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_insi
 ------------------------
 -- Literal patterns
 tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
-  = do { boxyUnify (hsLitType simple_lit) pat_ty
+  = do { let lit_ty = hsLitType simple_lit
+       ; coi <- boxyUnify lit_ty pat_ty
+                       -- coi is of kind: lit_ty ~ pat_ty
        ; res <- thing_inside pstate
-       ; returnM (LitPat simple_lit, [], res) }
+       ; span <- getSrcSpanM
+                       -- pattern coercions have to
+                       -- be of kind: pat_ty ~ lit_ty
+                       -- hence, sym coi
+       ; returnM (mkCoPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty, 
+                   [], res) }
 
 ------------------------
 -- Overloaded patterns: n, and n+k
-tc_pat pstate pat@(NPat over_lit mb_neg eq _) pat_ty thing_inside
+tc_pat pstate pat@(NPat over_lit mb_neg eq) pat_ty thing_inside
   = do { let orig = LiteralOrigin over_lit
        ; lit'    <- tcOverloadedLit orig over_lit pat_ty
        ; eq'     <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
@@ -435,7 +522,7 @@ tc_pat pstate pat@(NPat over_lit mb_neg eq _) pat_ty thing_inside
                            do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
                               ; return (Just neg') }
        ; res <- thing_inside pstate
-       ; returnM (NPat lit' mb_neg' eq' pat_ty, [], res) }
+       ; returnM (NPat lit' mb_neg' eq', [], res) }
 
 tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
   = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
@@ -455,7 +542,7 @@ tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
        ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
        ; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
 
-tc_pat _ _other_pat _ _ = panic "tc_pat"       -- DictPat, ConPatOut, SigPatOut, VarPatOut
+tc_pat _ _other_pat _ _ = panic "tc_pat"       -- ConPatOut, SigPatOut, VarPatOut
 \end{code}
 
 
@@ -528,58 +615,102 @@ further type refinement is local to the alternative.
 
 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon 
         -> BoxySigmaType       -- Type of the pattern
-        -> HsConDetails Name (LPat Name) -> (PatState -> TcM a)
+        -> HsConPatDetails Name -> (PatState -> TcM a)
         -> TcM (Pat TcId, [TcTyVar], a)
 tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
-  = do { let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys) = dataConFullSig data_con
-             skol_info = PatSkol data_con
-             origin    = SigOrigin skol_info
+  = do { let (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _)
+                = dataConFullSig data_con
+             skol_info  = PatSkol data_con
+             origin     = SigOrigin skol_info
+             full_theta = eq_theta ++ dict_theta
 
          -- Instantiate the constructor type variables [a->ty]
-       ; ctxt_res_tys <- boxySplitTyConAppWithFamily tycon pat_ty
-       ; 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
-             theta'   = substTheta  tenv theta
-             arg_tys' = substTys    tenv arg_tys
+         -- This may involve doing a family-instance coercion, and building a
+         -- wrapper 
+       ; (ctxt_res_tys, coi) <- boxySplitTyConAppWithFamily tycon pat_ty
+        ; let sym_coi = mkSymCoI coi  -- boxy split coercion oriented wrongly
+             pat_ty' = mkTyConApp tycon ctxt_res_tys
+                                      -- pat_ty' /= pat_ty iff coi /= IdCo
+              
+              wrap_res_pat res_pat = mkCoPatCoI sym_coi uwScrut pat_ty
+                where
+                  uwScrut = unwrapFamInstScrutinee tycon ctxt_res_tys res_pat
+
+        ; traceTc $ case sym_coi of
+                      IdCo -> text "sym_coi:IdCo" 
+                      ACo co -> text "sym_coi: ACoI" <+> ppr co
+
+         -- Add the stupid theta
+       ; addDataConStupidTheta data_con ctxt_res_tys
+
+       ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs  
+                     -- Get location from monad, not from ex_tvs
 
-       ; co_vars <- newCoVars eq_spec' -- Make coercion variables
-       ; pstate' <- refineAlt data_con pstate ex_tvs' co_vars pat_ty
+       ; let tenv     = zipTopTvSubst (univ_tvs ++ ex_tvs)
+                                      (ctxt_res_tys ++ mkTyVarTys ex_tvs')
+             arg_tys' = substTys tenv arg_tys
+
+       ; if null ex_tvs && null eq_spec && null full_theta
+         then do { -- The common case; no class bindings etc 
+                    -- (see Note [Arrows and patterns])
+                   (arg_pats', inner_tvs, res) <- tcConArgs data_con arg_tys' 
+                                                   arg_pats pstate thing_inside
+                 ; let res_pat = ConPatOut { pat_con = L con_span data_con, 
+                                             pat_tvs = [], pat_dicts = [], 
+                                              pat_binds = emptyLHsBinds,
+                                             pat_args = arg_pats', 
+                                              pat_ty = pat_ty' }
+
+                   ; return (wrap_res_pat res_pat, inner_tvs, res) }
+
+         else do   -- The general case, with existential, and local equality 
+                    -- constraints
+       { let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec]
+             theta'   = substTheta tenv (eq_preds ++ full_theta)
+                           -- order is *important* as we generate the list of
+                           -- dictionary binders from theta'
+             ctxt     = pat_ctxt pstate
+       ; checkTc (case ctxt of { ProcPat -> False; other -> True })
+                 (existentialProcPat data_con)
+
+          -- Need to test for rigidity if *any* constraints in theta as class
+          -- constraints may have superclass equality constraints.  However,
+          -- we don't want to check for rigidity if we got here only because
+          -- ex_tvs was non-null.
+--        ; unless (null theta') $
+          -- FIXME: AT THE MOMENT WE CHEAT!  We only perform the rigidity test
+          --   if we explicit or implicit (by a GADT def) have equality 
+          --   constraints.
+        ; unless (all (not . isEqPred) theta') $
+            checkTc (isRigidTy pat_ty) (nonRigidMatch data_con)
 
        ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
-               tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
+               tcConArgs data_con arg_tys' arg_pats pstate thing_inside
 
        ; loc <- getInstLoc origin
        ; dicts <- newDictBndrs loc theta'
-       ; dict_binds <- tcSimplifyCheckPat loc co_vars (pat_reft pstate') 
-                                          ex_tvs' dicts lie_req
-
-       ; addDataConStupidTheta data_con ctxt_res_tys
-
-       ; return
-           (unwrapFamInstScrutinee tycon ctxt_res_tys $
-              ConPatOut { pat_con = L con_span data_con, 
-                          pat_tvs = ex_tvs' ++ co_vars,
-                          pat_dicts = map instToId dicts, 
-                          pat_binds = dict_binds,
-                          pat_args = arg_pats', pat_ty = pat_ty },
-            ex_tvs' ++ inner_tvs, res)
-       }
+       ; dict_binds <- tcSimplifyCheckPat loc [] emptyRefinement
+                          ex_tvs' dicts lie_req
+
+        ; let res_pat = ConPatOut { pat_con = L con_span data_con, 
+                                   pat_tvs = ex_tvs',
+                                   pat_dicts = map instToVar dicts, 
+                                   pat_binds = dict_binds,
+                                   pat_args = arg_pats', pat_ty = pat_ty' }
+       ; return (wrap_res_pat res_pat, ex_tvs' ++ inner_tvs, res)
+       } }
   where
-    -- Split against the family tycon if the pattern constructor belongs to a
-    -- representation tycon.
-    --
+    -- Split against the family tycon if the pattern constructor 
+    -- belongs to a family instance tycon.
     boxySplitTyConAppWithFamily tycon pat_ty =
       traceTc traceMsg >>
       case tyConFamInst_maybe tycon of
         Nothing                   -> boxySplitTyConApp tycon pat_ty
        Just (fam_tycon, instTys) -> 
-         do { scrutinee_arg_tys <- boxySplitTyConApp fam_tycon pat_ty
+         do { (scrutinee_arg_tys, coi) <- boxySplitTyConApp fam_tycon pat_ty
             ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
             ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
-            ; return freshTvs
+            ; return (freshTvs, coi)
             }
       where
         traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
@@ -607,8 +738,7 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
 
 
 tcConArgs :: DataCon -> [TcSigmaType]
-         -> Checker (HsConDetails Name (LPat Name)) 
-                    (HsConDetails Id (LPat Id))
+         -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
 
 tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
   = do { checkTc (con_arity == no_of_args)     -- Check correct arity
@@ -621,9 +751,10 @@ tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
     con_arity  = dataConSourceArity data_con
     no_of_args = length arg_pats
 
-tcConArgs data_con [arg_ty1,arg_ty2] (InfixCon p1 p2) pstate thing_inside
+tcConArgs data_con arg_tys (InfixCon p1 p2) pstate thing_inside
   = do { checkTc (con_arity == 2)      -- Check correct arity
                  (arityErr "Constructor" data_con con_arity 2)
+       ; let [arg_ty1,arg_ty2] = arg_tys       -- This can't fail after the arity check
        ; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
                                              pstate thing_inside
        ; return (InfixCon p1' p2', tvs, res) }
@@ -633,16 +764,15 @@ tcConArgs data_con [arg_ty1,arg_ty2] (InfixCon p1 p2) pstate thing_inside
 tcConArgs data_con other_args (InfixCon p1 p2) pstate thing_inside
   = pprPanic "tcConArgs" (ppr data_con)        -- InfixCon always has two arguments
 
-tcConArgs data_con arg_tys (RecCon rpats) pstate thing_inside
+tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
   = do { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
-       ; return (RecCon rpats', tvs, res) }
+       ; return (RecCon (HsRecFields rpats' dd), tvs, res) }
   where
-    -- doc comments are typechecked to Nothing here
     tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
-    tc_field (HsRecField field_lbl pat _) pstate thing_inside
+    tc_field (HsRecField field_lbl pat pun) pstate thing_inside
       = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
           ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
-          ; return (mkRecField sel_id pat', tvs, res) }
+          ; return (HsRecField sel_id pat' pun, tvs, res) }
 
     find_field_ty :: FieldLabel -> TcM (Id, TcType)
     find_field_ty field_lbl
@@ -696,6 +826,30 @@ addDataConStupidTheta data_con inst_tys
     inst_theta = substTheta tenv stupid_theta
 \end{code}
 
+Note [Arrows and patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+(Oct 07) Arrow noation has the odd property that it involves "holes in the scope". 
+For example:
+  expr :: Arrow a => a () Int
+  expr = proc (y,z) -> do
+          x <- term -< y
+          expr' -< x
+
+Here the 'proc (y,z)' binding scopes over the arrow tails but not the
+arrow body (e.g 'term').  As things stand (bogusly) all the
+constraints from the proc body are gathered together, so constraints
+from 'term' will be seen by the tcPat for (y,z).  But we must *not*
+bind constraints from 'term' here, becuase the desugarer will not make
+these bindings scope over 'term'.
+
+The Right Thing is not to confuse these constraints together. But for
+now the Easy Thing is to ensure that we do not have existential or
+GADT constraints in a 'proc', and to short-cut the constraint
+simplification for such vanilla patterns so that it binds no
+constraints. Hence the 'fast path' in tcConPat; but it's also a good
+plan for ordinary vanilla patterns to bypass the constraint
+simplification step.
+
 
 %************************************************************************
 %*                                                                     *
@@ -712,11 +866,12 @@ refineAlt :: DataCon              -- For tracing only
          -> TcM PatState
 
 refineAlt con pstate ex_tvs [] pat_ty
+  | null $ dataConEqTheta con
   = return pstate      -- Common case: no equational constraints
 
 refineAlt con pstate ex_tvs co_vars pat_ty
-  | not (isRigidTy pat_ty)
-  = failWithTc (nonRigidMatch con)
+  = -- See Note [Flags and equational constraints]
+    do { checkTc (isRigidTy pat_ty) (nonRigidMatch con)
        -- We are matching against a GADT constructor with non-trivial
        -- constraints, but pattern type is wobbly.  For now we fail.
        -- We can make sense of this, however:
@@ -731,11 +886,11 @@ refineAlt con pstate ex_tvs co_vars pat_ty
        -- then unify these constraints to make pat_ty the right shape;
        -- then proceed exactly as in the rigid case
 
-  | otherwise  -- In the rigid case, we perform type refinement
-  = case gadtRefine (pat_reft pstate) ex_tvs co_vars of {
+               -- In the rigid case, we perform type refinement
+       ; case gadtRefine (pat_reft pstate) ex_tvs co_vars of {
            Failed msg     -> failWithTc (inaccessibleAlt msg) ;
            Succeeded reft -> do { traceTc trace_msg
-                                ; return (pstate { pat_reft = reft }) }
+                                ; return (pstate { pat_reft = reft, pat_eqs = (pat_eqs pstate || not (null $ dataConEqTheta con)) }) }
                    -- DO NOT refine the envt right away, because we 
                    -- might be inside a lazy pattern.  Instead, refine pstate
                where
@@ -744,9 +899,20 @@ refineAlt con pstate ex_tvs co_vars pat_ty
                                vcat [ ppr con <+> ppr ex_tvs,
                                       ppr [(v, tyVarKind v) | v <- co_vars],
                                       ppr reft]
-       }
+       } }
 \end{code}
 
+Note [Flags and equational constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If there are equational constraints, we take account of them
+regardless of flag settings; -XGADTs etc applies only to the
+*definition* of a data type.
+
+An alternative would be also to reject a program that *used*
+constructors with equational constraints.  But want we should avoid at
+all costs is simply to *ignore* the constraints, since that gives
+incomprehensible errors (Trac #2004).
+
 
 %************************************************************************
 %*                                                                     *
@@ -764,7 +930,7 @@ tcOverloadedLit :: InstOrigin
                 -> HsOverLit Name
                 -> BoxyRhoType
                 -> TcM (HsOverLit TcId)
-tcOverloadedLit orig lit@(HsIntegral i fi) res_ty
+tcOverloadedLit orig lit@(HsIntegral i fi _) res_ty
   | not (fi `isHsVar` fromIntegerName) -- Do not generate a LitInst for rebindable syntax.  
        -- Reason: If we do, tcSimplify will call lookupInst, which
        --         will call tcSyntaxName, which does unification, 
@@ -772,16 +938,16 @@ tcOverloadedLit orig lit@(HsIntegral i fi) res_ty
        -- ToDo: noLoc sadness
   = do { integer_ty <- tcMetaTy integerTyConName
        ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty)
-       ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty)))) }
+       ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty))) res_ty) }
 
   | Just expr <- shortCutIntLit i res_ty 
-  = return (HsIntegral i expr)
+  = return (HsIntegral i expr res_ty)
 
   | otherwise
   = do         { expr <- newLitInst orig lit res_ty
-       ; return (HsIntegral i expr) }
+       ; return (HsIntegral i expr res_ty) }
 
-tcOverloadedLit orig lit@(HsFractional r fr) res_ty
+tcOverloadedLit orig lit@(HsFractional r fr _) res_ty
   | not (fr `isHsVar` fromRationalName)        -- c.f. HsIntegral case
   = do { rat_ty <- tcMetaTy rationalTyConName
        ; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty res_ty)
@@ -789,14 +955,27 @@ tcOverloadedLit orig lit@(HsFractional r fr) res_ty
                -- we're instantiating an overloaded function here,
                -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
                -- However this'll be picked up by tcSyntaxOp if necessary
-       ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty)))) }
+       ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty))) res_ty) }
 
   | Just expr <- shortCutFracLit r res_ty 
-  = return (HsFractional r expr)
+  = return (HsFractional r expr res_ty)
+
+  | otherwise
+  = do         { expr <- newLitInst orig lit res_ty
+       ; return (HsFractional r expr res_ty) }
+
+tcOverloadedLit orig lit@(HsIsString s fr _) res_ty
+  | not (fr `isHsVar` fromStringName)  -- c.f. HsIntegral case
+  = do { str_ty <- tcMetaTy stringTyConName
+       ; fr' <- tcSyntaxOp orig fr (mkFunTy str_ty res_ty)
+       ; return (HsIsString s (HsApp (noLoc fr') (nlHsLit (HsString s))) res_ty) }
+
+  | Just expr <- shortCutStringLit s res_ty 
+  = return (HsIsString s expr res_ty)
 
   | otherwise
   = do         { expr <- newLitInst orig lit res_ty
-       ; return (HsFractional r expr) }
+       ; return (HsIsString s expr res_ty) }
 
 newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
 newLitInst orig lit res_ty     -- Make a LitInst
@@ -891,6 +1070,7 @@ patCtxt pat            = Just (hang (ptext SLIT("In the pattern:"))
 existentialExplode pat
   = hang (vcat [text "My brain just exploded.",
                text "I can't handle pattern bindings for existentially-quantified constructors.",
+               text "Instead, use a case-expression, or do-notation, to unpack the constructor.",
                text "In the binding group for"])
        4 (ppr pat)
 
@@ -904,13 +1084,12 @@ sigPatCtxt pats 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,
-                     ppr pats
+                     ptext SLIT("The body has type:") <+> ppr tidy_body_ty
                ]) }
   where
     bound_ids = collectPatsBinders pats
     show_ids = filter is_interesting bound_ids
-    is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
+    is_interesting id = any (`elemVarSet` varTypeTyVars id) bound_tvs
 
     ppr_id id ty = ppr id <+> dcolon <+> ppr ty
        -- Don't zonk the types so we get the separate, un-unified versions
@@ -923,18 +1102,27 @@ badFieldCon con field
 polyPatSig :: TcType -> SDoc
 polyPatSig sig_ty
   = hang (ptext SLIT("Illegal polymorphic type signature in pattern:"))
-        4 (ppr sig_ty)
+       2 (ppr sig_ty)
 
 badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
 
+existentialProcPat :: DataCon -> SDoc
+existentialProcPat con
+  = hang (ptext SLIT("Illegal constructor") <+> quotes (ppr con) <+> ptext SLIT("in a 'proc' pattern"))
+       2 (ptext SLIT("Proc patterns cannot use existentials or GADTs"))
+
 lazyPatErr pat tvs
   = failWithTc $
-    hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
+    hang (ptext SLIT("A lazy (~) pattern cannot bind existential type variables"))
        2 (vcat (map pprSkolTvBinding tvs))
 
 nonRigidMatch con
   =  hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con))
-       2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))
+       2 (ptext SLIT("Solution: add a type signature"))
+
+nonRigidResult res_ty
+  =  hang (ptext SLIT("GADT pattern match with non-rigid result type") <+> quotes (ppr res_ty))
+       2 (ptext SLIT("Solution: add a type signature"))
 
 inaccessibleAlt msg
   = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg