Type checking for type synonym families
[ghc-hetmet.git] / compiler / typecheck / TcPat.lhs
index 33b7630..8b2fac2 100644 (file)
@@ -1,60 +1,47 @@
 %
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
-\section[TcPat]{Typechecking patterns}
+
+TcPat: Typechecking patterns
 
 \begin{code}
 module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcOverloadedLit,
-              badFieldCon, polyPatSig ) where
+              addDataConStupidTheta, badFieldCon, polyPatSig ) where
 
 #include "HsVersions.h"
 
 import {-# SOURCE #-}  TcExpr( tcSyntaxOp )
-import HsSyn           ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), HsExpr(..),
-                         mkCoPat, idCoercion,
-                         LHsBinds, emptyLHsBinds, isEmptyLHsBinds, 
-                         collectPatsBinders, nlHsLit )
-import TcHsSyn         ( TcId, hsLitType )
+
+import HsSyn
+import TcHsSyn
 import TcRnMonad
-import Inst            ( InstOrigin(..), shortCutFracLit, shortCutIntLit, 
-                         newDicts, instToId, tcInstStupidTheta, isHsVar
-                       )
-import Id              ( Id, idType, mkLocalId )
-import CoreFVs         ( idFreeTyVars )
-import Name            ( Name, mkSystemVarName )
-import TcSimplify      ( tcSimplifyCheck, bindInstsOfLocalFuns )
-import TcEnv           ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
-                         tcLookupClass, tcLookupDataCon, refineEnvironment,
-                         tcLookupField, tcMetaTy )
-import TcMType                 ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars, 
-+                        newCoVars, zonkTcType )
-import TcType          ( TcType, TcTyVar, TcSigmaType, TcRhoType, BoxyType,
-                         SkolemInfo(PatSkol), 
-                         BoxySigmaType, BoxyRhoType, argTypeKind, typeKind,
-                         pprSkolTvBinding, isRigidTy, tcTyVarsOfTypes, 
-                         zipTopTvSubst, isArgTypeKind, isUnboxedTupleType,
-                         mkTyVarTys, mkClassPred, isOverloadedTy, substEqSpec,
-                         mkFunTy, mkFunTys, tidyOpenType, tidyOpenTypes )
-import VarSet          ( elemVarSet )
-import {- Kind parts of -} 
-       Type            ( liftedTypeKind )
-import TcUnify         ( boxySplitTyConApp, boxySplitListTy, unBox,
-                         zapToMonotype, boxyUnify, checkSigTyVarsWrt,
-                         unifyType )
-import TcHsType                ( UserTypeCtxt(..), tcPatSig )
-import TysWiredIn      ( boolTy, parrTyCon, tupleTyCon )
-import Type            ( substTys, substTheta )
-import StaticFlags     ( opt_IrrefutableTuples )
-import TyCon           ( TyCon, FieldLabel )
-import DataCon         ( DataCon, dataConTyCon, dataConFullSig, dataConName,
-                         dataConFieldLabels, dataConSourceArity )
-import PrelNames       ( integralClassName, fromIntegerName, integerTyConName, 
-                         fromRationalName, rationalTyConName )
-import BasicTypes      ( isBoxed )
-import SrcLoc          ( Located(..), SrcSpan, noLoc )
-import ErrUtils                ( Message )
-import Util            ( zipEqual )
-import Maybes          ( MaybeErr(..) )
+import Inst
+import Id
+import Var
+import CoreFVs
+import Name
+import TcSimplify
+import TcEnv
+import TcMType
+import TcType
+import VarSet
+import TcUnify
+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
+import ErrUtils
+import Util
+import Maybes
 import Outputable
 import FastString
 \end{code}
@@ -73,7 +60,8 @@ tcLetPat :: (Name -> Maybe TcRhoType)
         -> 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
@@ -118,11 +106,13 @@ tc_lam_pats :: [(LPat Name,BoxySigmaType)]
                    -> ((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 }
+  =  do        { let init_state = PS { pat_ctxt = LamPat, 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
@@ -147,12 +137,14 @@ 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 {
        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 
@@ -184,18 +176,18 @@ tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty
                --      f t = case t of { MkT g -> ... }
                -- Here, the 'g' must get type (forall a. a->a) from the
                -- MkT context
-       ; return (mkLocalId bndr_name pat_ty') }
+       ; 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
        ; boxyUnify mono_ty pat_ty
-       ; return (mkLocalId mono_name mono_ty) }
+       ; return (Id.mkLocalId mono_name mono_ty) }
 
   | otherwise
   = do { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
        ; mono_name <- newLocalName bndr_name
-       ; return (mkLocalId mono_name pat_ty') }
+       ; return (Id.mkLocalId mono_name pat_ty') }
 
 
 -------------------
@@ -224,7 +216,7 @@ unBoxArgType ty pp_this
        -- but they improve error messages, and allocate fewer tyvars
        ; if isUnboxedTupleType ty' then
                failWithTc msg
-         else if isArgTypeKind (typeKind ty') then
+         else if isSubArgTypeKind (typeKind ty') then
                return ty'
          else do       -- OpenTypeKind, so constrain it
        { ty2 <- newFlexiTyVarTy argTypeKind
@@ -243,7 +235,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.
@@ -294,7 +286,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:
@@ -304,7 +298,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
@@ -342,11 +339,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
@@ -428,9 +440,15 @@ 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 (wrapPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty, [], res) }
 
 ------------------------
 -- Overloaded patterns: n, and n+k
@@ -460,13 +478,12 @@ tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
        -- The Report says that n+k patterns must be in Integral
        -- We may not want this when using re-mappable syntax, though (ToDo?)
        ; icls <- tcLookupClass integralClassName
-       ; dicts <- newDicts orig [mkClassPred icls [pat_ty']]   
-       ; extendLIEs dicts
+       ; instStupidTheta orig [mkClassPred icls [pat_ty']]     
     
        ; 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}
 
 
@@ -477,6 +494,61 @@ tc_pat _ _other_pat _ _ = panic "tc_pat"   -- DictPat, ConPatOut, SigPatOut, VarP
 %*                                                                     *
 %************************************************************************
 
+[Pattern matching indexed data types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the following declarations:
+
+  data family Map k :: * -> *
+  data instance Map (a, b) v = MapPair (Map a (Pair b v))
+
+and a case expression
+
+  case x :: Map (Int, c) w of MapPair m -> ...
+
+As explained by [Wrappers for data instance tycons] in MkIds.lhs, the
+worker/wrapper types for MapPair are
+
+  $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
+  $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
+
+So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
+:R123Map, which means the straight use of boxySplitTyConApp would give a type
+error.  Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
+boxySplitTyConApp with the family tycon Map instead, which gives us the family
+type list {(Int, c), w}.  To get the correct split for :R123Map, we need to
+unify the family type list {(Int, c), w} with the instance types {(a, b), v}
+(provided by tyConFamInst_maybe together with the family tycon).  This
+unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
+the split arguments for the representation tycon :R123Map as {Int, c, w}
+
+In other words, boxySplitTyConAppWithFamily implicitly takes the coercion 
+
+  Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}
+
+moving between representation and family type into account.  To produce type
+correct Core, this coercion needs to be used to case the type of the scrutinee
+from the family to the representation type.  This is achieved by
+unwrapFamInstScrutinee using a CoPat around the result pattern.
+
+Now it might appear seem as if we could have used the existing GADT type
+refinement infrastructure of refineAlt and friends instead of the explicit
+unification and CoPat generation.  However, that would be wrong.  Why?  The
+whole point of GADT refinement is that the refinement is local to the case
+alternative.  In contrast, the substitution generated by the unification of
+the family type list and instance types needs to be propagated to the outside.
+Imagine that in the above example, the type of the scrutinee would have been
+(Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
+substitution [x -> (a, b), v -> w].  In contrast to GADT matching, the
+instantiation of x with (a, b) must be global; ie, it must be valid in *all*
+alternatives of the case expression, whereas in the GADT case it might vary
+between alternatives.
+
+In fact, if we have a data instance declaration defining a GADT, eq_spec will
+be non-empty and we will get a mixture of global instantiations and local
+refinement from a single match.  This neatly reflects that, as soon as we
+have constrained the type of the scrutinee to the required type index, all
+further type refinement is local to the alternative.
+
 \begin{code}
 --     Running example:
 -- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
@@ -484,44 +556,85 @@ tc_pat _ _other_pat _ _ = panic "tc_pat"  -- DictPat, ConPatOut, SigPatOut, VarP
 
 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 { 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, eq_theta, dict_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 <- boxySplitTyConApp tycon pat_ty
-       ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs
+       ; 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')
+                                      (ctxt_res_tys ++ mkTyVarTys ex_tvs')
              eq_spec' = substEqSpec tenv eq_spec
-             theta'   = substTheta  tenv theta
+             theta'   = substTheta  tenv (eq_theta ++ dict_theta)
              arg_tys' = substTys    tenv arg_tys
 
        ; co_vars <- newCoVars eq_spec' -- Make coercion variables
-       ; pstate' <- refineAlt data_con pstate ex_tvs co_vars pat_ty
-
+       ; pstate' <- refineAlt data_con pstate ex_tvs' co_vars pat_ty
+       
        ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
                tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
 
-       ; dicts <- newDicts (SigOrigin skol_info) theta'
-       ; dict_binds <- tcSimplifyCheck doc ex_tvs' dicts lie_req
-
-       ; tcInstStupidTheta data_con ctxt_res_tys
-
-       ; return (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) 
+       ; 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)
        }
   where
-    doc = ptext SLIT("existential context for") <+> quotes (ppr data_con)
+    -- 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
+            ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
+            ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
+            ; return freshTvs
+            }
+      where
+        traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
+                        ppr tycon <+> ppr pat_ty
+                      , text "  family instance:" <+> 
+                        ppr (tyConFamInst_maybe tycon)
+                       ]
+
+    -- Wraps the pattern (which must be a ConPatOut pattern) in a coercion
+    -- pattern if the tycon is an instance of a family.
+    --
+    unwrapFamInstScrutinee :: TyCon -> [Type] -> Pat Id -> Pat Id
+    unwrapFamInstScrutinee tycon args pat
+      | Just co_con <- tyConFamilyCoercion_maybe tycon 
+--      , not (isNewTyCon tycon)       -- newtypes are explicitly unwrapped by
+                                    -- the desugarer
+          -- NB: We can use CoPat directly, rather than mkCoPat, as we know the
+          --    coercion is not the identity; mkCoPat is inconvenient as it
+          --    wants a located pattern.
+      = CoPat (WpCo $ mkTyConApp co_con args)       -- co fam ty to repr ty
+             (pat {pat_ty = mkTyConApp tycon args})    -- representation type
+             pat_ty                                    -- family inst type
+      | otherwise
+      = pat
+
 
 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
@@ -543,15 +656,18 @@ tcConArgs data_con [arg_ty1,arg_ty2] (InfixCon p1 p2) pstate thing_inside
   where
     con_arity  = dataConSourceArity data_con
 
-tcConArgs data_con arg_tys (RecCon rpats) 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 (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
-    tc_field :: Checker (Located Name, LPat Name) (Located TcId, LPat TcId)
-    tc_field (field_lbl, pat) pstate thing_inside
+    tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
+    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 ((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
@@ -589,6 +705,22 @@ tcConArg (arg_pat, arg_ty) pstate thing_inside
        --     refinements from peer argument patterns to the left
 \end{code}
 
+\begin{code}
+addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
+-- Instantiate the "stupid theta" of the data con, and throw 
+-- the constraints into the constraint set
+addDataConStupidTheta data_con inst_tys
+  | null stupid_theta = return ()
+  | otherwise        = instStupidTheta origin inst_theta
+  where
+    origin = OccurrenceOf (dataConName data_con)
+       -- The origin should always report "occurrence of C"
+       -- even when C occurs in a pattern
+    stupid_theta = dataConStupidTheta data_con
+    tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
+    inst_theta = substTheta tenv stupid_theta
+\end{code}
+
 
 %************************************************************************
 %*                                                                     *
@@ -605,11 +737,15 @@ 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)
+  = do { opt_gadt <- doptM Opt_GADTs   -- No type-refinement unless GADTs are on
+       ; if (not opt_gadt) then return pstate
+         else 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:
@@ -624,17 +760,20 @@ 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
                    
-                   trace_msg = text "refineAlt:match" <+> ppr con <+> ppr reft
-       }
+                   trace_msg = text "refineAlt:match" <+> 
+                               vcat [ ppr con <+> ppr ex_tvs,
+                                      ppr [(v, tyVarKind v) | v <- co_vars],
+                                      ppr reft]
+       } } }
 \end{code}
 
 
@@ -688,13 +827,27 @@ tcOverloadedLit orig lit@(HsFractional r fr) res_ty
   = do         { expr <- newLitInst orig lit res_ty
        ; return (HsFractional r expr) }
 
+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)))) }
+
+  | Just expr <- shortCutStringLit s res_ty 
+  = return (HsIsString s expr)
+
+  | otherwise
+  = do         { expr <- newLitInst orig lit res_ty
+       ; return (HsIsString s expr) }
+
 newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
 newLitInst orig lit res_ty     -- Make a LitInst
   = do         { loc <- getInstLoc orig
        ; 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}
@@ -780,10 +933,11 @@ 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)
 
-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)
@@ -796,8 +950,9 @@ sigPatCtxt bound_ids bound_tvs pat_tys body_ty tidy_env
                      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
@@ -816,13 +971,23 @@ badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
 
 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"))
 
+nonRigidResult res_ty
+  =  hang (ptext SLIT("GADT pattern match with non-rigid result type") <+> quotes (ppr res_ty))
+       2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))
+
 inaccessibleAlt msg
   = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
 \end{code}
+
+\begin{code}
+wrapPatCoI :: CoercionI -> Pat a -> TcType -> Pat a
+wrapPatCoI IdCo     pat ty = pat
+wrapPatCoI (ACo co) pat ty = CoPat (WpCo co) pat ty
+\end{code}