Separate the language flags from the other DynFlag's

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

diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs
index d509692..022796e 100644 (file)
--- a/compiler/typecheck/TcPat.lhs
+++ b/compiler/typecheck/TcPat.lhs
@@ -6,14 +6,7 @@
 TcPat: Typechecking patterns
 
 \begin{code}
 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"
               addDataConStupidTheta, badFieldCon, polyPatSig ) where
 
 #include "HsVersions.h"

@@ -32,25 +25,24 @@ import TcSimplify
 import TcEnv
 import TcMType
 import TcType
 import TcEnv
 import TcMType
 import TcType

+import VarEnv

 import VarSet
 import TcUnify
 import TcHsType
 import TysWiredIn
 import VarSet
 import TcUnify
 import TcHsType
 import TysWiredIn

-import Type

 import Coercion
 import StaticFlags
 import TyCon
 import DataCon
 import Coercion
 import StaticFlags
 import TyCon
 import DataCon

-import DynFlags

 import PrelNames
 import BasicTypes hiding (SuccessFlag(..))
 import PrelNames
 import BasicTypes hiding (SuccessFlag(..))

+import DynFlags

 import SrcLoc
 import ErrUtils
 import Util
 import SrcLoc
 import ErrUtils
 import Util

-import Maybes

 import Outputable
 import FastString
 import Outputable
 import FastString

-import Monad
+import Control.Monad

 \end{code}
 
 
 \end{code}
 
 

@@ -77,11 +69,12 @@ tcLetPat sig_fn pat pat_ty thing_inside
        ; return (pat', res) }
 
 -----------------
        ; 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,
 
 -- This is the externally-callable wrapper function
 -- Typecheck the patterns, extend the environment to bind the variables,

@@ -94,18 +87,20 @@ tcLamPats :: [LPat Name]            -- Patterns,
 --   3. Check the body
 --   4. Check that no existentials escape
 
 --   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
 
                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) }
 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) }

@@ -122,7 +117,7 @@ tc_lam_pats ctxt pat_ty_prs res_ty thing_inside
        ; (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))
        ; (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 res_ty
+                                    then nonRigidResult ctxt res_ty

                                     else thing_inside res_ty }
 
        ; let tys = map snd pat_ty_prs
                                     else thing_inside res_ty }
 
        ; let tys = map snd pat_ty_prs

@@ -144,7 +139,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).
 
 --     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
   = return ()  -- Short cut for case when there are no existentials
 
 tcCheckExistentialPat pats ex_tvs pat_tys body_ty

@@ -159,14 +154,16 @@ data PatState = PS {
   }
 
 data PatCtxt 
   }
 
 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
 
   | 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 :: PatState -> UserTypeCtxt
 patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt

-patSigCtxt other                       = LamPatSigCtxt
+patSigCtxt _                            = LamPatSigCtxt

 \end{code}
 
 
 \end{code}
 
 

@@ -182,7 +179,7 @@ tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
 tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
   | Just mono_ty <- lookup_sig bndr_name
   = do { mono_name <- newLocalName bndr_name
 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
+       ; _ <- boxyUnify mono_ty pat_ty

        ; return (Id.mkLocalId mono_name mono_ty) }
 
   | otherwise
        ; return (Id.mkLocalId mono_name mono_ty) }
 
   | otherwise

@@ -214,8 +211,13 @@ bindInstsOfPatId id thing_inside
        ; return (res, binds) }
 
 -------------------
        ; return (res, binds) }
 
 -------------------

+unBoxPatBndrType :: BoxyType -> Name -> TcM TcType

 unBoxPatBndrType  ty name = unBoxArgType ty (ptext (sLit "The variable") <+> quotes (ppr name))
 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"))
 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
 unBoxViewPatType  ty pat  = unBoxArgType ty (ptext (sLit "The view pattern") <+> ppr pat)
 
 unBoxArgType :: BoxyType -> SDoc -> TcM TcType

@@ -234,7 +236,7 @@ unBoxArgType ty pp_this
                return ty'
          else do       -- OpenTypeKind, so constrain it
        { ty2 <- newFlexiTyVarTy argTypeKind
                return ty'
          else do       -- OpenTypeKind, so constrain it
        { ty2 <- newFlexiTyVarTy argTypeKind

-       ; unifyType ty' ty2
+       ; _ <- unifyType ty' ty2

        ; return ty' }}
   where
     msg = pp_this <+> ptext (sLit "cannot be bound to an unboxed tuple")
        ; return ty' }}
   where
     msg = pp_this <+> ptext (sLit "cannot be bound to an unboxed tuple")

@@ -361,12 +363,15 @@ tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
        -- getLIE/extendLIEs: see Note [Hopping the LIE in lazy patterns]
 
        -- Check no existentials
        -- 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
 
        -- Check that the pattern has a lifted type
        ; pat_tv <- newBoxyTyVar liftedTypeKind

-       ; boxyUnify pat_ty (mkTyVarTy pat_tv)
+       ; _ <- boxyUnify pat_ty (mkTyVarTy pat_tv)

 
        ; return (LazyPat pat', [], res) }
 
 
        ; return (LazyPat pat', [], res) }
 

@@ -422,12 +427,19 @@ 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
 -- 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
        ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
                              tc_lpat pat inner_ty pstate thing_inside

-       ; return (SigPatOut pat' inner_ty, tvs, res) }
+        ; return (SigPatOut pat' inner_ty, tvs, res) }

 
 

-tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
+-- Use this when we add pattern coercions back in
+--       return (mkCoPatCoI (mkSymCoI coi) (SigPatOut pat' inner_ty) pat_ty
+--                 , tvs, res) }
+
+tc_pat _ pat@(TypePat _) _ _

   = failWithTc (badTypePat pat)
 
 ------------------------
   = failWithTc (badTypePat pat)
 
 ------------------------

@@ -474,7 +486,7 @@ tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
 
 ------------------------
 -- Data constructors
 
 ------------------------
 -- 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 }
   = do { data_con <- tcLookupDataCon con_name
        ; let tycon = dataConTyCon data_con
        ; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }

@@ -486,7 +498,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
        ; 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
                        -- pattern coercions have to
                        -- be of kind: pat_ty ~ lit_ty
                        -- hence, sym coi

@@ -495,7 +506,7 @@ tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
 
 ------------------------
 -- Overloaded patterns: n, and n+k
 
 ------------------------
 -- 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)
   = do { let orig = LiteralOrigin over_lit
        ; lit'    <- tcOverloadedLit orig over_lit pat_ty
        ; eq'     <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)

@@ -508,7 +519,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) }
 
        ; 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
   = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
        ; let pat_ty' = idType bndr_id
              orig    = LiteralOrigin lit

@@ -566,7 +577,7 @@ the split arguments for the representation tycon :R123Map as {Int, c, w}
 
 In other words, boxySplitTyConAppWithFamily implicitly takes the coercion 
 
 
 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
 
 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

@@ -592,7 +603,7 @@ to express the local scope of GADT refinements.
 
 \begin{code}
 --     Running example:
 
 \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 
 --      with scrutinee of type (T ty)
 
 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon 

@@ -609,21 +620,19 @@ 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 
          -- 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
         ; 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
 
          -- Add the stupid theta

-       ; addDataConStupidTheta data_con ctxt_res_tys
+       ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys

 
        ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs  
                      -- Get location from monad, not from ex_tvs
 
        ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs  
                      -- Get location from monad, not from ex_tvs

@@ -647,8 +656,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
 
          else do   -- The general case, with existential, and local equality 
                     -- constraints

-       { checkTc (case pat_ctxt pstate of { ProcPat -> False; other -> True })
+       { checkTc (notProcPat (pat_ctxt pstate))

                  (existentialProcPat data_con)
                  (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,
 
           -- Need to test for rigidity if *any* constraints in theta as class
           -- constraints may have superclass equality constraints.  However,

@@ -656,7 +666,7 @@ 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
           -- 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.
         ; let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec]
              theta'   = substTheta tenv (eq_preds ++ full_theta)
           --   constraints.
         ; let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec]
              theta'   = substTheta tenv (eq_preds ++ full_theta)

@@ -666,8 +676,14 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
              pstate' | no_equalities = pstate
                      | otherwise     = pstate { pat_eqs = True }
 
              pstate' | no_equalities = pstate
                      | otherwise     = pstate { pat_eqs = True }
 

-       ; unless no_equalities (checkTc (isRigidTy pat_ty)
-                                        (nonRigidMatch data_con))
+        ; 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
 
        ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
                tcConArgs data_con arg_tys' arg_pats pstate' thing_inside

@@ -689,12 +705,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
     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) -> 
        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)
             ; (_, 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:" <+>
             }
       where
         traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>

@@ -706,8 +736,8 @@ 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.
     --
     -- 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
       | Just co_con <- tyConFamilyCoercion_maybe tycon 
 --      , not (isNewTyCon tycon)       -- newtypes are explicitly unwrapped by
                                     -- the desugarer

@@ -716,11 +746,10 @@ tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
           --    wants a located pattern.
       = CoPat (WpCast $ mkTyConApp co_con args)       -- co fam ty to repr ty
              (pat {pat_ty = mkTyConApp tycon args})    -- representation type
           --    wants a located pattern.
       = 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
 
       | otherwise
       = pat
 

-

 tcConArgs :: DataCon -> [TcSigmaType]
          -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
 
 tcConArgs :: DataCon -> [TcSigmaType]
          -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
 

@@ -745,9 +774,6 @@ tcConArgs data_con arg_tys (InfixCon p1 p2) pstate thing_inside
   where
     con_arity  = dataConSourceArity data_con
 
   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) }
 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) }

@@ -803,7 +829,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
        -- 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}
 
     inst_theta = substTheta tenv stupid_theta
 \end{code}
 

@@ -848,63 +876,37 @@ tcOverloadedLit :: InstOrigin
                 -> HsOverLit Name
                 -> BoxyRhoType
                 -> TcM (HsOverLit TcId)
                 -> 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
        -- 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
                -- 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
 
   | 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")
                lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit, 
                                    tci_ty = res_tau, tci_loc = loc}
   = do         { loc <- getInstLoc orig
        ; res_tau <- zapToMonotype res_ty
        ; new_uniq <- newUnique
        ; 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
        ; extendLIE lit_inst

-       ; return (HsVar (instToId lit_inst)) }
+       ; return (lit { ol_witness = witness, ol_type = res_ty }) }

 \end{code}
 
 
 \end{code}
 
 

@@ -985,13 +987,16 @@ patCtxt pat           = Just (hang (ptext (sLit "In the pattern:"))
 
 -----------------------------------------------
 
 
 -----------------------------------------------
 

+existentialExplode :: LPat Name -> SDoc

 existentialExplode pat
   = hang (vcat [text "My brain just exploded.",
 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)
 
                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
 sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env 
   = do { pat_tys' <- mapM zonkTcType pat_tys
        ; body_ty' <- zonkTcType body_ty

@@ -1022,6 +1027,11 @@ polyPatSig sig_ty
   = hang (ptext (sLit "Illegal polymorphic type signature in pattern:"))
        2 (ppr sig_ty)
 
   = hang (ptext (sLit "Illegal polymorphic type signature in pattern:"))
        2 (ppr sig_ty)
 

+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
 badTypePat pat = ptext (sLit "Illegal type pattern") <+> ppr pat
 
 existentialProcPat :: DataCon -> SDoc

@@ -1029,23 +1039,42 @@ 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 $
   = 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))
 
        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"))
+lazyUnliftedPatErr :: OutputableBndr name => Pat name -> TcM ()
+lazyUnliftedPatErr pat
+  = failWithTc $
+    hang (ptext (sLit "A lazy (~) pattern cannot contain unlifted types"))
+       2 (ppr pat)

 
 

-nonRigidResult res_ty
+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'))
   = 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"))
+                        2 (ptext (sLit "Solution: add a type signature for")
+                                 <+> what ctxt )

        ; failWithTcM (env1, msg) }
        ; failWithTcM (env1, msg) }

-
-inaccessibleAlt msg
-  = hang (ptext (sLit "Inaccessible case alternative:")) 2 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}
 \end{code}