New syntax for GADT-style record declarations, and associated refactoring
[ghc-hetmet.git] / compiler / typecheck / TcPat.lhs
index 61ee938..bef5ec7 100644 (file)
@@ -6,14 +6,7 @@
 TcPat: Typechecking patterns
 
 \begin{code}
-{-# 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,
+module TcPat ( tcLetPat, tcPat, tcPats, tcOverloadedLit,
               addDataConStupidTheta, badFieldCon, polyPatSig ) where
 
 #include "HsVersions.h"
@@ -32,6 +25,7 @@ import TcSimplify
 import TcEnv
 import TcMType
 import TcType
+import VarEnv
 import VarSet
 import TcUnify
 import TcHsType
@@ -41,9 +35,9 @@ import Coercion
 import StaticFlags
 import TyCon
 import DataCon
-import DynFlags
 import PrelNames
 import BasicTypes hiding (SuccessFlag(..))
+import DynFlags        ( DynFlag( Opt_GADTs ) )
 import SrcLoc
 import ErrUtils
 import Util
@@ -77,11 +71,12 @@ tcLetPat sig_fn pat pat_ty thing_inside
        ; return (pat', res) }
 
 -----------------
-tcLamPats :: [LPat Name]               -- Patterns,
-         -> [BoxySigmaType]            --   and their types
-         -> BoxyRhoType                -- Result type,
-         -> (BoxyRhoType -> TcM a)     --   and the checker for the body
-         -> TcM ([LPat TcId], a)
+tcPats :: HsMatchContext Name
+       -> [LPat Name]           -- Patterns,
+       -> [BoxySigmaType]       --   and their types
+       -> BoxyRhoType           -- Result type,
+       -> (BoxyRhoType -> TcM a) --   and the checker for the body
+       -> TcM ([LPat TcId], a)
 
 -- This is the externally-callable wrapper function
 -- Typecheck the patterns, extend the environment to bind the variables,
@@ -94,18 +89,20 @@ tcLamPats :: [LPat Name]            -- Patterns,
 --   3. Check the body
 --   4. Check that no existentials escape
 
-tcLamPats pats tys res_ty thing_inside
-  = tc_lam_pats LamPat (zipEqual "tcLamPats" pats tys)
+tcPats ctxt pats tys res_ty thing_inside
+  = tc_lam_pats (APat ctxt) (zipEqual "tcLamPats" pats tys)
                res_ty thing_inside
 
-tcLamPat :: LPat Name -> BoxySigmaType 
-        -> BoxyRhoType             -- Result type
-        -> (BoxyRhoType -> TcM a)  -- Checker for body, given its result type
-        -> TcM (LPat TcId, a)
-
-tcProcPat = tc_lam_pat ProcPat
-tcLamPat  = tc_lam_pat LamPat
+tcPat :: HsMatchContext Name
+      -> LPat Name -> BoxySigmaType 
+      -> BoxyRhoType             -- Result type
+      -> (BoxyRhoType -> TcM a)  -- Checker for body, given
+                                 -- its result type
+      -> TcM (LPat TcId, a)
+tcPat ctxt = tc_lam_pat (APat ctxt)
 
+tc_lam_pat :: PatCtxt -> LPat Name -> BoxySigmaType -> BoxyRhoType
+           -> (BoxyRhoType -> TcM a) -> TcM (LPat TcId, a)
 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) }
@@ -119,10 +116,11 @@ tc_lam_pats :: PatCtxt
 tc_lam_pats ctxt pat_ty_prs res_ty thing_inside 
   =  do        { let init_state = PS { pat_ctxt = ctxt, pat_eqs = False }
 
-       ; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
-                                 if (pat_eqs pstate' && (not $ isRigidTy res_ty))
-                                    then failWithTc (nonRigidResult res_ty)
-                                    else thing_inside res_ty
+       ; (pats', ex_tvs, res) <- do { traceTc (text "tc_lam_pats" <+> (ppr pat_ty_prs $$ ppr res_ty)) 
+                                 ; tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
+                                   if (pat_eqs pstate' && (not $ isRigidTy res_ty))
+                                    then nonRigidResult ctxt res_ty
+                                    else thing_inside res_ty }
 
        ; let tys = map snd pat_ty_prs
        ; tcCheckExistentialPat pats' ex_tvs tys res_ty
@@ -143,7 +141,7 @@ tcCheckExistentialPat :: [LPat TcId]                -- Patterns (just for error message)
 --     f (C g) x = g x
 -- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).
 
-tcCheckExistentialPat pats [] pat_tys body_ty
+tcCheckExistentialPat _ [] _ _
   = return ()  -- Short cut for case when there are no existentials
 
 tcCheckExistentialPat pats ex_tvs pat_tys body_ty
@@ -152,19 +150,22 @@ tcCheckExistentialPat pats ex_tvs pat_tys body_ty
 
 data PatState = PS {
        pat_ctxt :: PatCtxt,
-       pat_eqs  :: Bool        -- <=> there are GADT equational constraints 
-                               --     for refinement 
+       pat_eqs  :: Bool        -- <=> there are any equational constraints 
+                               -- Used at the end to say whether the result
+                               -- type must be rigid
   }
 
 data PatCtxt 
-  = LamPat 
-  | ProcPat                            -- The pattern in (proc pat -> ...)
-                                       --      see Note [Arrows and patterns]
+  = APat (HsMatchContext Name)
   | LetPat (Name -> Maybe TcRhoType)   -- Used for let(rec) bindings
 
+notProcPat :: PatCtxt -> Bool
+notProcPat (APat ProcExpr) = False
+notProcPat _              = True
+
 patSigCtxt :: PatState -> UserTypeCtxt
 patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
-patSigCtxt other                       = LamPatSigCtxt
+patSigCtxt _                            = LamPatSigCtxt
 \end{code}
 
 
@@ -212,9 +213,14 @@ bindInstsOfPatId id thing_inside
        ; return (res, binds) }
 
 -------------------
-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)
+unBoxPatBndrType :: BoxyType -> Name -> TcM TcType
+unBoxPatBndrType  ty name = unBoxArgType ty (ptext (sLit "The variable") <+> quotes (ppr name))
+
+unBoxWildCardType :: BoxyType -> TcM TcType
+unBoxWildCardType ty      = unBoxArgType ty (ptext (sLit "A wild-card pattern"))
+
+unBoxViewPatType :: BoxyType -> Pat Name -> TcM TcType
+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; 
@@ -235,7 +241,7 @@ unBoxArgType ty pp_this
        ; unifyType ty' ty2
        ; return ty' }}
   where
-    msg = pp_this <+> ptext SLIT("cannot be bound to an unboxed tuple")
+    msg = pp_this <+> ptext (sLit "cannot be bound to an unboxed tuple")
 \end{code}
 
 
@@ -359,8 +365,11 @@ tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
        -- getLIE/extendLIEs: see Note [Hopping the LIE in lazy patterns]
 
        -- Check no existentials
-       ; if (null pat_tvs) then return ()
-         else lazyPatErr lpat pat_tvs
+       ; unless (null pat_tvs) $ lazyPatErr lpat pat_tvs
+
+       -- Check there are no unlifted types under the lazy pattern
+       ; when (any (isUnLiftedType . idType) $ collectPatBinders pat') $
+               lazyUnliftedPatErr lpat
 
        -- Check that the pattern has a lifted type
        ; pat_tv <- newBoxyTyVar liftedTypeKind
@@ -420,12 +429,15 @@ tc_pat pstate (orig@(ViewPat expr pat _)) overall_pat_ty thing_inside
 -- Type signatures in patterns
 -- See Note [Pattern coercions] below
 tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
-  = do { (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
+  = do { (inner_ty, tv_binds, coi) <- tcPatSig (patSigCtxt pstate) sig_ty 
+                                                                    pat_ty
+        ; unless (isIdentityCoI coi) $ 
+            failWithTc (badSigPat pat_ty)
        ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
                              tc_lpat pat inner_ty pstate thing_inside
        ; return (SigPatOut pat' inner_ty, tvs, res) }
 
-tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
+tc_pat _ pat@(TypePat _) _ _
   = failWithTc (badTypePat pat)
 
 ------------------------
@@ -472,7 +484,7 @@ tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
 
 ------------------------
 -- Data constructors
-tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
+tc_pat pstate (ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
   = do { data_con <- tcLookupDataCon con_name
        ; let tycon = dataConTyCon data_con
        ; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }
@@ -484,7 +496,6 @@ tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
        ; coi <- boxyUnify lit_ty pat_ty
                        -- coi is of kind: lit_ty ~ pat_ty
        ; res <- thing_inside pstate
-       ; span <- getSrcSpanM
                        -- pattern coercions have to
                        -- be of kind: pat_ty ~ lit_ty
                        -- hence, sym coi
@@ -493,7 +504,7 @@ tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
 
 ------------------------
 -- Overloaded patterns: n, and n+k
-tc_pat pstate pat@(NPat over_lit mb_neg eq) pat_ty thing_inside
+tc_pat pstate (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)
@@ -506,7 +517,7 @@ tc_pat pstate pat@(NPat over_lit mb_neg eq) pat_ty thing_inside
        ; res <- thing_inside pstate
        ; return (NPat lit' mb_neg' eq', [], res) }
 
-tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
+tc_pat pstate (NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
   = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
        ; let pat_ty' = idType bndr_id
              orig    = LiteralOrigin lit
@@ -564,7 +575,7 @@ 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}
+  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
@@ -590,7 +601,7 @@ to express the local scope of GADT refinements.
 
 \begin{code}
 --     Running example:
--- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
+-- MkT :: forall a b c. (a~[b]) => b -> c -> T a
 --      with scrutinee of type (T ty)
 
 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon 
@@ -607,18 +618,16 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
          -- Instantiate the constructor type variables [a->ty]
          -- This may involve doing a family-instance coercion, and building a
          -- wrapper 
-       ; (ctxt_res_tys, coi) <- boxySplitTyConAppWithFamily tycon pat_ty
+       ; (ctxt_res_tys, coi, unwrap_ty) <- 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
+                  uwScrut = unwrapFamInstScrutinee tycon ctxt_res_tys
+                                                   unwrap_ty res_pat
 
          -- Add the stupid theta
        ; addDataConStupidTheta data_con ctxt_res_tys
@@ -645,13 +654,9 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
 
          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 })
+       { checkTc (notProcPat (pat_ctxt pstate))
                  (existentialProcPat data_con)
+                 -- See Note [Arrows and patterns]
 
           -- Need to test for rigidity if *any* constraints in theta as class
           -- constraints may have superclass equality constraints.  However,
@@ -659,13 +664,27 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
           -- 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 
+          --   if we explicitly or implicitly (by a GADT def) have equality 
           --   constraints.
-        ; unless (all (not . isEqPred) theta') $
-            checkTc (isRigidTy pat_ty) (nonRigidMatch data_con)
+        ; 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'
+             no_equalities = not (any isEqPred theta')
+             pstate' | no_equalities = pstate
+                     | otherwise     = pstate { pat_eqs = True }
+
+        ; gadts_on <- doptM Opt_GADTs
+       ; checkTc (no_equalities || gadts_on)
+                 (ptext (sLit "A pattern match on a GADT requires -XGADTs"))
+                 -- Trac #2905 decided that a *pattern-match* of a GADT
+                 -- should require the GADT language flag
+
+       ; unless no_equalities $ checkTc (isRigidTy pat_ty) $
+                                 nonRigidMatch (pat_ctxt pstate) 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'
@@ -684,12 +703,26 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
     boxySplitTyConAppWithFamily tycon pat_ty =
       traceTc traceMsg >>
       case tyConFamInst_maybe tycon of
-        Nothing                   -> boxySplitTyConApp tycon pat_ty
+        Nothing                   -> 
+          do { (scrutinee_arg_tys, coi1) <- boxySplitTyConApp tycon pat_ty
+             ; return (scrutinee_arg_tys, coi1, pat_ty)
+             }
        Just (fam_tycon, instTys) -> 
-         do { (scrutinee_arg_tys, coi) <- boxySplitTyConApp fam_tycon pat_ty
+         do { (scrutinee_arg_tys, coi1) <- boxySplitTyConApp fam_tycon pat_ty
             ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
-            ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
-            ; return (freshTvs, coi)
+             ; let instTys' = substTys subst instTys
+            ; cois <- boxyUnifyList instTys' scrutinee_arg_tys
+             ; let coi = if isIdentityCoI coi1
+                         then  -- pat_ty was splittable
+                               -- => boxyUnifyList had real work to do
+                           mkTyConAppCoI fam_tycon instTys' cois
+                         else  -- pat_ty was not splittable
+                               -- => scrutinee_arg_tys are fresh tvs and
+                               --    boxyUnifyList just instantiated those
+                           coi1
+            ; return (freshTvs, coi, mkTyConApp fam_tycon instTys')
+                                      -- this is /= pat_ty 
+                                      -- iff cois is non-trivial
             }
       where
         traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
@@ -701,21 +734,20 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
     -- 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
+    unwrapFamInstScrutinee :: TyCon -> [Type] -> Type -> Pat Id -> Pat Id
+    unwrapFamInstScrutinee tycon args unwrap_ty 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
+      = CoPat (WpCast $ mkTyConApp co_con args)       -- co fam ty to repr ty
              (pat {pat_ty = mkTyConApp tycon args})    -- representation type
-             pat_ty                                    -- family inst type
+             unwrap_ty                                 -- family inst type
       | otherwise
       = pat
 
-
 tcConArgs :: DataCon -> [TcSigmaType]
          -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
 
@@ -740,9 +772,6 @@ tcConArgs data_con arg_tys (InfixCon p1 p2) pstate thing_inside
   where
     con_arity  = dataConSourceArity data_con
 
-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 (HsRecFields rpats' dd), tvs, res) }
@@ -798,7 +827,9 @@ addDataConStupidTheta data_con inst_tys
        -- 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
+    tenv = mkTopTvSubst (dataConUnivTyVars data_con `zip` inst_tys)
+        -- NB: inst_tys can be longer than the univ tyvars
+        --     because the constructor might have existentials
     inst_theta = substTheta tenv stupid_theta
 \end{code}
 
@@ -843,63 +874,37 @@ tcOverloadedLit :: InstOrigin
                 -> HsOverLit Name
                 -> BoxyRhoType
                 -> TcM (HsOverLit TcId)
-tcOverloadedLit orig lit@(HsIntegral i fi _) res_ty
-  | not (fi `isHsVar` fromIntegerName) -- Do not generate a LitInst for rebindable syntax.  
+tcOverloadedLit orig lit@(OverLit { ol_val = val, ol_rebindable = rebindable
+                                 , ol_witness = meth_name }) res_ty
+  | rebindable
+       -- Do not generate a LitInst for rebindable syntax.  
        -- Reason: If we do, tcSimplify will call lookupInst, which
        --         will call tcSyntaxName, which does unification, 
        --         which tcSimplify doesn't like
        -- 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))) res_ty) }
-
-  | Just expr <- shortCutIntLit i res_ty 
-  = return (HsIntegral i expr res_ty)
-
-  | otherwise
-  = do         { expr <- newLitInst orig lit res_ty
-       ; return (HsIntegral i expr 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)
+  = do { hs_lit <- mkOverLit val
+       ; let lit_ty = hsLitType hs_lit
+       ; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
                -- Overloaded literals must have liftedTypeKind, because
                -- 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))) res_ty) }
+       ; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
+       ; return (lit { ol_witness = witness, ol_type = res_ty }) }
 
-  | Just expr <- shortCutFracLit r res_ty 
-  = return (HsFractional r expr res_ty)
+  | Just expr <- shortCutLit val res_ty 
+  = return (lit { ol_witness = expr, ol_type = 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 (HsIsString s expr res_ty) }
-
-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")
+       ; let   lit_nm   = mkSystemVarName new_uniq (fsLit "lit")
                lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit, 
                                    tci_ty = res_tau, tci_loc = loc}
+               witness = HsVar (instToId lit_inst)
        ; extendLIE lit_inst
-       ; return (HsVar (instToId lit_inst)) }
+       ; return (lit { ol_witness = witness, ol_type = res_ty }) }
 \end{code}
 
 
@@ -975,18 +980,21 @@ patCtxt :: Pat Name -> Maybe Message      -- Not all patterns are worth pushing a con
 patCtxt (VarPat _)  = Nothing
 patCtxt (ParPat _)  = Nothing
 patCtxt (AsPat _ _) = Nothing
-patCtxt pat        = Just (hang (ptext SLIT("In the pattern:")) 
+patCtxt pat        = Just (hang (ptext (sLit "In the pattern:")) 
                               4 (ppr pat))
 
 -----------------------------------------------
 
+existentialExplode :: LPat Name -> SDoc
 existentialExplode pat
   = hang (vcat [text "My brain just exploded.",
-               text "I can't handle pattern bindings for existentially-quantified constructors.",
+               text "I can't handle pattern bindings for existential or GADT data constructors.",
                text "Instead, use a case-expression, or do-notation, to unpack the constructor.",
                text "In the binding group for"])
        4 (ppr pat)
 
+sigPatCtxt :: [LPat Var] -> [Var] -> [TcType] -> TcType -> TidyEnv
+           -> TcM (TidyEnv, SDoc)
 sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env 
   = do { pat_tys' <- mapM zonkTcType pat_tys
        ; body_ty' <- zonkTcType body_ty
@@ -994,10 +1002,10 @@ sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env
              (env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys'
              (env3, tidy_body_ty) = tidyOpenType  env2 body_ty'
        ; return (env3,
-                sep [ptext SLIT("When checking an existential match that binds"),
+                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 pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
+                     ptext (sLit "The body has type:") <+> ppr tidy_body_ty
                ]) }
   where
     bound_ids = collectPatsBinders pats
@@ -1009,34 +1017,62 @@ sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env
 
 badFieldCon :: DataCon -> Name -> SDoc
 badFieldCon con field
-  = hsep [ptext SLIT("Constructor") <+> quotes (ppr con),
-         ptext SLIT("does not have field"), quotes (ppr field)]
+  = hsep [ptext (sLit "Constructor") <+> quotes (ppr con),
+         ptext (sLit "does not have field"), quotes (ppr field)]
 
 polyPatSig :: TcType -> SDoc
 polyPatSig sig_ty
-  = hang (ptext SLIT("Illegal polymorphic type signature in pattern:"))
+  = hang (ptext (sLit "Illegal polymorphic type signature in pattern:"))
        2 (ppr sig_ty)
 
-badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
+badSigPat :: TcType -> SDoc
+badSigPat pat_ty = ptext (sLit "Pattern signature must exactly match:") <+> 
+                   ppr pat_ty
+
+badTypePat :: Pat Name -> SDoc
+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"))
+  = 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
+lazyPatErr :: Pat name -> [TcTyVar] -> TcM ()
+lazyPatErr _ tvs
   = failWithTc $
-    hang (ptext SLIT("A lazy (~) pattern cannot bind existential type variables"))
+    hang (ptext (sLit "A lazy (~) pattern cannot match existential or GADT data constructors"))
        2 (vcat (map pprSkolTvBinding tvs))
 
-nonRigidMatch con
-  =  hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con))
-       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"))
+lazyUnliftedPatErr :: OutputableBndr name => Pat name -> TcM ()
+lazyUnliftedPatErr pat
+  = failWithTc $
+    hang (ptext (sLit "A lazy (~) pattern cannot contain unlifted types"))
+       2 (ppr pat)
 
-inaccessibleAlt msg
-  = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
+nonRigidMatch :: PatCtxt -> DataCon -> SDoc
+nonRigidMatch ctxt con
+  =  hang (ptext (sLit "GADT pattern match in non-rigid context for") <+> quotes (ppr con))
+       2 (ptext (sLit "Probable solution: add a type signature for") <+> what ctxt)
+  where
+     what (APat (FunRhs f _)) = quotes (ppr f)
+     what (APat CaseAlt)      = ptext (sLit "the scrutinee of the case expression")
+     what (APat LambdaExpr )  = ptext (sLit "the lambda expression")
+     what (APat (StmtCtxt _)) = ptext (sLit "the right hand side of a do/comprehension binding")
+     what _other             = ptext (sLit "something")
+
+nonRigidResult :: PatCtxt -> Type -> TcM a
+nonRigidResult ctxt res_ty
+  = do { env0 <- tcInitTidyEnv
+       ; let (env1, res_ty') = tidyOpenType env0 res_ty
+             msg = hang (ptext (sLit "GADT pattern match with non-rigid result type")
+                               <+> quotes (ppr res_ty'))
+                        2 (ptext (sLit "Solution: add a type signature for")
+                                 <+> what ctxt )
+       ; failWithTcM (env1, msg) }
+  where
+     what (APat (FunRhs f _)) = quotes (ppr f)
+     what (APat CaseAlt)      = ptext (sLit "the entire case expression")
+     what (APat LambdaExpr)   = ptext (sLit "the lambda exression")
+     what (APat (StmtCtxt _)) = ptext (sLit "the entire do/comprehension expression")
+     what _other              = ptext (sLit "something")
 \end{code}