compiler/typecheck/TcPat.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   4 %
   5
   6 TcPat: Typechecking patterns
   7
   8 \begin{code}
   9 {-# OPTIONS -w #-}
  10 -- The above warning supression flag is a temporary kludge.
  11 -- While working on this module you are encouraged to remove it and fix
  12 -- any warnings in the module. See
  13 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
  14 -- for details
  15
  16 module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcProcPat, tcOverloadedLit,
  17                addDataConStupidTheta, badFieldCon, polyPatSig ) where
  18
  19 #include "HsVersions.h"
  20
  21 import {-# SOURCE #-}   TcExpr( tcSyntaxOp, tcInferRho)
  22
  23 import HsSyn
  24 import TcHsSyn
  25 import TcRnMonad
  26 import Inst
  27 import Id
  28 import Var
  29 import CoreFVs
  30 import Name
  31 import TcSimplify
  32 import TcEnv
  33 import TcMType
  34 import TcType
  35 import VarSet
  36 import TcUnify
  37 import TcHsType
  38 import TysWiredIn
  39 import TcGadt
  40 import Type
  41 import Coercion
  42 import StaticFlags
  43 import TyCon
  44 import DataCon
  45 import DynFlags
  46 import PrelNames
  47 import BasicTypes hiding (SuccessFlag(..))
  48 import SrcLoc
  49 import ErrUtils
  50 import Util
  51 import Maybes
  52 import Outputable
  53 import FastString
  54 \end{code}
  55
  56
  57 %************************************************************************
  58 %*                                                                      *
  59                 External interface
  60 %*                                                                      *
  61 %************************************************************************
  62
  63 \begin{code}
  64 tcLetPat :: (Name -> Maybe TcRhoType)
  65          -> LPat Name -> BoxySigmaType
  66          -> TcM a
  67          -> TcM (LPat TcId, a)
  68 tcLetPat sig_fn pat pat_ty thing_inside
  69   = do  { let init_state = PS { pat_ctxt = LetPat sig_fn,
  70                                 pat_reft = emptyRefinement,
  71                                 pat_eqs  = False }
  72         ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state (\ _ -> thing_inside)
  73
  74         -- Don't know how to deal with pattern-bound existentials yet
  75         ; checkTc (null ex_tvs) (existentialExplode pat)
  76
  77         ; return (pat', res) }
  78
  79 -----------------
  80 tcLamPats :: [LPat Name]                                -- Patterns,
  81           -> [BoxySigmaType]                            --   and their types
  82           -> BoxyRhoType                                -- Result type,
  83           -> ((Refinement, BoxyRhoType) -> TcM a)       --   and the checker for the body
  84           -> TcM ([LPat TcId], a)
  85
  86 -- This is the externally-callable wrapper function
  87 -- Typecheck the patterns, extend the environment to bind the variables,
  88 -- do the thing inside, use any existentially-bound dictionaries to
  89 -- discharge parts of the returning LIE, and deal with pattern type
  90 -- signatures
  91
  92 --   1. Initialise the PatState
  93 --   2. Check the patterns
  94 --   3. Apply the refinement to the environment and result type
  95 --   4. Check the body
  96 --   5. Check that no existentials escape
  97
  98 tcLamPats pats tys res_ty thing_inside
  99   = tc_lam_pats LamPat (zipEqual "tcLamPats" pats tys)
 100                 (emptyRefinement, res_ty) thing_inside
 101
 102 tcLamPat :: LPat Name -> BoxySigmaType
 103          -> (Refinement,BoxyRhoType)            -- Result type
 104          -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type
 105          -> TcM (LPat TcId, a)
 106
 107 tcProcPat = tc_lam_pat ProcPat
 108 tcLamPat  = tc_lam_pat LamPat
 109
 110 tc_lam_pat ctxt pat pat_ty res_ty thing_inside
 111   = do  { ([pat'],thing) <- tc_lam_pats ctxt [(pat, pat_ty)] res_ty thing_inside
 112         ; return (pat', thing) }
 113
 114 -----------------
 115 tc_lam_pats :: PatCtxt
 116             -> [(LPat Name,BoxySigmaType)]
 117             -> (Refinement,BoxyRhoType)                 -- Result type
 118             -> ((Refinement,BoxyRhoType) -> TcM a)      -- Checker for body, given its result type
 119             -> TcM ([LPat TcId], a)
 120 tc_lam_pats ctxt pat_ty_prs (reft, res_ty) thing_inside
 121   =  do { let init_state = PS { pat_ctxt = ctxt, pat_reft = reft, pat_eqs = False }
 122
 123         ; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
 124                                   refineEnvironment (pat_reft pstate') (pat_eqs pstate') $
 125                                   if (pat_eqs pstate' && (not $ isRigidTy res_ty))
 126                                      then failWithTc (nonRigidResult res_ty)
 127                                      else thing_inside (pat_reft pstate', res_ty)
 128
 129         ; let tys = map snd pat_ty_prs
 130         ; tcCheckExistentialPat pats' ex_tvs tys res_ty
 131
 132         ; returnM (pats', res) }
 133
 134
 135 -----------------
 136 tcCheckExistentialPat :: [LPat TcId]            -- Patterns (just for error message)
 137                       -> [TcTyVar]              -- Existentially quantified tyvars bound by pattern
 138                       -> [BoxySigmaType]        -- Types of the patterns
 139                       -> BoxyRhoType            -- Type of the body of the match
 140                                                 -- Tyvars in either of these must not escape
 141                       -> TcM ()
 142 -- NB: we *must* pass "pats_tys" not just "body_ty" to tcCheckExistentialPat
 143 -- For example, we must reject this program:
 144 --      data C = forall a. C (a -> Int)
 145 --      f (C g) x = g x
 146 -- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).
 147
 148 tcCheckExistentialPat pats [] pat_tys body_ty
 149   = return ()   -- Short cut for case when there are no existentials
 150
 151 tcCheckExistentialPat pats ex_tvs pat_tys body_ty
 152   = addErrCtxtM (sigPatCtxt pats ex_tvs pat_tys body_ty)        $
 153     checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
 154
 155 data PatState = PS {
 156         pat_ctxt :: PatCtxt,
 157         pat_reft :: Refinement, -- Binds rigid TcTyVars to their refinements
 158         pat_eqs  :: Bool        -- <=> there are GADT equational constraints
 159                                 --     for refinement
 160   }
 161
 162 data PatCtxt
 163   = LamPat
 164   | ProcPat                             -- The pattern in (proc pat -> ...)
 165                                         --      see Note [Arrows and patterns]
 166   | LetPat (Name -> Maybe TcRhoType)    -- Used for let(rec) bindings
 167
 168 patSigCtxt :: PatState -> UserTypeCtxt
 169 patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
 170 patSigCtxt other                        = LamPatSigCtxt
 171 \end{code}
 172
 173
 174
 175 %************************************************************************
 176 %*                                                                      *
 177                 Binders
 178 %*                                                                      *
 179 %************************************************************************
 180
 181 \begin{code}
 182 tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
 183 tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
 184   | Just mono_ty <- lookup_sig bndr_name
 185   = do  { mono_name <- newLocalName bndr_name
 186         ; boxyUnify mono_ty pat_ty
 187         ; return (Id.mkLocalId mono_name mono_ty) }
 188
 189   | otherwise
 190   = do  { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
 191         ; mono_name <- newLocalName bndr_name
 192         ; return (Id.mkLocalId mono_name pat_ty') }
 193
 194 tcPatBndr (PS { pat_ctxt = _lam_or_proc }) bndr_name pat_ty
 195   = do  { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
 196                 -- We have an undecorated binder, so we do rule ABS1,
 197                 -- by unboxing the boxy type, forcing any un-filled-in
 198                 -- boxes to become monotypes
 199                 -- NB that pat_ty' can still be a polytype:
 200                 --      data T = MkT (forall a. a->a)
 201                 --      f t = case t of { MkT g -> ... }
 202                 -- Here, the 'g' must get type (forall a. a->a) from the
 203                 -- MkT context
 204         ; return (Id.mkLocalId bndr_name pat_ty') }
 205
 206
 207 -------------------
 208 bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId)
 209 bindInstsOfPatId id thing_inside
 210   | not (isOverloadedTy (idType id))
 211   = do { res <- thing_inside; return (res, emptyLHsBinds) }
 212   | otherwise
 213   = do  { (res, lie) <- getLIE thing_inside
 214         ; binds <- bindInstsOfLocalFuns lie [id]
 215         ; return (res, binds) }
 216
 217 -------------------
 218 unBoxPatBndrType  ty name = unBoxArgType ty (ptext SLIT("The variable") <+> quotes (ppr name))
 219 unBoxWildCardType ty      = unBoxArgType ty (ptext SLIT("A wild-card pattern"))
 220 unBoxViewPatType  ty pat  = unBoxArgType ty (ptext SLIT("The view pattern") <+> ppr pat)
 221
 222 unBoxArgType :: BoxyType -> SDoc -> TcM TcType
 223 -- In addition to calling unbox, unBoxArgType ensures that the type is of ArgTypeKind;
 224 -- that is, it can't be an unboxed tuple.  For example,
 225 --      case (f x) of r -> ...
 226 -- should fail if 'f' returns an unboxed tuple.
 227 unBoxArgType ty pp_this
 228   = do  { ty' <- unBox ty       -- Returns a zonked type
 229
 230         -- Neither conditional is strictly necesssary (the unify alone will do)
 231         -- but they improve error messages, and allocate fewer tyvars
 232         ; if isUnboxedTupleType ty' then
 233                 failWithTc msg
 234           else if isSubArgTypeKind (typeKind ty') then
 235                 return ty'
 236           else do       -- OpenTypeKind, so constrain it
 237         { ty2 <- newFlexiTyVarTy argTypeKind
 238         ; unifyType ty' ty2
 239         ; return ty' }}
 240   where
 241     msg = pp_this <+> ptext SLIT("cannot be bound to an unboxed tuple")
 242 \end{code}
 243
 244
 245 %************************************************************************
 246 %*                                                                      *
 247                 The main worker functions
 248 %*                                                                      *
 249 %************************************************************************
 250
 251 Note [Nesting]
 252 ~~~~~~~~~~~~~~
 253 tcPat takes a "thing inside" over which the pattern scopes.  This is partly
 254 so that tcPat can extend the environment for the thing_inside, but also
 255 so that constraints arising in the thing_inside can be discharged by the
 256 pattern.
 257
 258 This does not work so well for the ErrCtxt carried by the monad: we don't
 259 want the error-context for the pattern to scope over the RHS.
 260 Hence the getErrCtxt/setErrCtxt stuff in tc_lpats.
 261
 262 \begin{code}
 263 --------------------
 264 type Checker inp out =  forall r.
 265                           inp
 266                        -> PatState
 267                        -> (PatState -> TcM r)
 268                        -> TcM (out, [TcTyVar], r)
 269
 270 tcMultiple :: Checker inp out -> Checker [inp] [out]
 271 tcMultiple tc_pat args pstate thing_inside
 272   = do  { err_ctxt <- getErrCtxt
 273         ; let loop pstate []
 274                 = do { res <- thing_inside pstate
 275                      ; return ([], [], res) }
 276
 277               loop pstate (arg:args)
 278                 = do { (p', p_tvs, (ps', ps_tvs, res))
 279                                 <- tc_pat arg pstate $ \ pstate' ->
 280                                    setErrCtxt err_ctxt $
 281                                    loop pstate' args
 282                 -- setErrCtxt: restore context before doing the next pattern
 283                 -- See note [Nesting] above
 284
 285                      ; return (p':ps', p_tvs ++ ps_tvs, res) }
 286
 287         ; loop pstate args }
 288
 289 --------------------
 290 tc_lpat_pr :: (LPat Name, BoxySigmaType)
 291            -> PatState
 292            -> (PatState -> TcM a)
 293            -> TcM (LPat TcId, [TcTyVar], a)
 294 tc_lpat_pr (pat, ty) = tc_lpat pat ty
 295
 296 tc_lpat :: LPat Name
 297         -> BoxySigmaType
 298         -> PatState
 299         -> (PatState -> TcM a)
 300         -> TcM (LPat TcId, [TcTyVar], a)
 301 tc_lpat (L span pat) pat_ty pstate thing_inside
 302   = setSrcSpan span               $
 303     maybeAddErrCtxt (patCtxt pat) $
 304     do  { let mb_reft = refineType (pat_reft pstate) pat_ty
 305               pat_ty' = case mb_reft of { Just (_, ty') -> ty'; Nothing -> pat_ty }
 306
 307                 -- Make sure the result type reflects the current refinement
 308                 -- We must do this here, so that it correctly ``sees'' all
 309                 -- the refinements to the left.  Example:
 310                 -- Suppose C :: forall a. T a -> a -> Foo
 311                 -- Pattern      C a p1 True
 312                 -- So p1 might refine 'a' to True, and the True
 313                 -- pattern had better see it.
 314
 315         ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
 316         ; let final_pat = case mb_reft of
 317                                 Nothing     -> pat'
 318                                 Just (co,_) -> CoPat (WpCo co) pat' pat_ty
 319         ; return (L span final_pat, tvs, res) }
 320
 321 --------------------
 322 tc_pat  :: PatState
 323         -> Pat Name
 324         -> BoxySigmaType        -- Fully refined result type
 325         -> (PatState -> TcM a)  -- Thing inside
 326         -> TcM (Pat TcId,       -- Translated pattern
 327                 [TcTyVar],      -- Existential binders
 328                 a)              -- Result of thing inside
 329
 330 tc_pat pstate (VarPat name) pat_ty thing_inside
 331   = do  { id <- tcPatBndr pstate name pat_ty
 332         ; (res, binds) <- bindInstsOfPatId id $
 333                           tcExtendIdEnv1 name id $
 334                           (traceTc (text "binding" <+> ppr name <+> ppr (idType id))
 335                            >> thing_inside pstate)
 336         ; let pat' | isEmptyLHsBinds binds = VarPat id
 337                    | otherwise             = VarPatOut id binds
 338         ; return (pat', [], res) }
 339
 340 tc_pat pstate (ParPat pat) pat_ty thing_inside
 341   = do  { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
 342         ; return (ParPat pat', tvs, res) }
 343
 344 tc_pat pstate (BangPat pat) pat_ty thing_inside
 345   = do  { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
 346         ; return (BangPat pat', tvs, res) }
 347
 348 -- There's a wrinkle with irrefutable patterns, namely that we
 349 -- must not propagate type refinement from them.  For example
 350 --      data T a where { T1 :: Int -> T Int; ... }
 351 --      f :: T a -> Int -> a
 352 --      f ~(T1 i) y = y
 353 -- It's obviously not sound to refine a to Int in the right
 354 -- hand side, because the arugment might not match T1 at all!
 355 --
 356 -- Nor should a lazy pattern bind any existential type variables
 357 -- because they won't be in scope when we do the desugaring
 358 --
 359 -- Note [Hopping the LIE in lazy patterns]
 360 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 361 -- In a lazy pattern, we must *not* discharge constraints from the RHS
 362 -- from dictionaries bound in the pattern.  E.g.
 363 --      f ~(C x) = 3
 364 -- We can't discharge the Num constraint from dictionaries bound by
 365 -- the pattern C!
 366 --
 367 -- So we have to make the constraints from thing_inside "hop around"
 368 -- the pattern.  Hence the getLLE and extendLIEs later.
 369
 370 tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
 371   = do  { (pat', pat_tvs, (res,lie))
 372                 <- tc_lpat pat pat_ty pstate $ \ _ ->
 373                    getLIE (thing_inside pstate)
 374                 -- Ignore refined pstate', revert to pstate
 375         ; extendLIEs lie
 376         -- getLIE/extendLIEs: see Note [Hopping the LIE in lazy patterns]
 377
 378         -- Check no existentials
 379         ; if (null pat_tvs) then return ()
 380           else lazyPatErr lpat pat_tvs
 381
 382         -- Check that the pattern has a lifted type
 383         ; pat_tv <- newBoxyTyVar liftedTypeKind
 384         ; boxyUnify pat_ty (mkTyVarTy pat_tv)
 385
 386         ; return (LazyPat pat', [], res) }
 387
 388 tc_pat pstate (WildPat _) pat_ty thing_inside
 389   = do  { pat_ty' <- unBoxWildCardType pat_ty   -- Make sure it's filled in with monotypes
 390         ; res <- thing_inside pstate
 391         ; return (WildPat pat_ty', [], res) }
 392
 393 tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
 394   = do  { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
 395         ; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
 396                               tc_lpat pat (idType bndr_id) pstate thing_inside
 397             -- NB: if we do inference on:
 398             --          \ (y@(x::forall a. a->a)) = e
 399             -- we'll fail.  The as-pattern infers a monotype for 'y', which then
 400             -- fails to unify with the polymorphic type for 'x'.  This could
 401             -- perhaps be fixed, but only with a bit more work.
 402             --
 403             -- If you fix it, don't forget the bindInstsOfPatIds!
 404         ; return (AsPat (L nm_loc bndr_id) pat', tvs, res) }
 405
 406 tc_pat pstate (orig@(ViewPat expr pat _)) overall_pat_ty thing_inside
 407   = do  { -- morally, expr must have type
 408          -- `forall a1...aN. OPT' -> B`
 409          -- where overall_pat_ty is an instance of OPT'.
 410          -- Here, we infer a rho type for it,
 411          -- which replaces the leading foralls and constraints
 412          -- with fresh unification variables.
 413          (expr',expr'_inferred) <- tcInferRho expr
 414          -- next, we check that expr is coercible to `overall_pat_ty -> pat_ty`
 415        ; let expr'_expected = \ pat_ty -> (mkFunTy overall_pat_ty pat_ty)
 416          -- tcSubExp: expected first, offered second
 417          -- returns coercion
 418          --
 419          -- NOTE: this forces pat_ty to be a monotype (because we use a unification
 420          -- variable to find it).  this means that in an example like
 421          -- (view -> f)    where view :: _ -> forall b. b
 422          -- we will only be able to use view at one instantation in the
 423          -- rest of the view
 424         ; (expr_coerc, pat_ty) <- tcInfer (\ pat_ty -> tcSubExp (expr'_expected pat_ty) expr'_inferred)
 425          -- pattern must have pat_ty
 426        ; (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
 427          -- this should get zonked later on, but we unBox it here
 428          -- so that we do the same checks as above
 429         ; annotation_ty <- unBoxViewPatType overall_pat_ty orig
 430         ; return (ViewPat (mkLHsWrap expr_coerc expr') pat' annotation_ty, tvs, res) }
 431
 432 -- Type signatures in patterns
 433 -- See Note [Pattern coercions] below
 434 tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
 435   = do  { (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
 436         ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
 437                               tc_lpat pat inner_ty pstate thing_inside
 438         ; return (SigPatOut pat' inner_ty, tvs, res) }
 439
 440 tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
 441   = failWithTc (badTypePat pat)
 442
 443 ------------------------
 444 -- Lists, tuples, arrays
 445 tc_pat pstate (ListPat pats _) pat_ty thing_inside
 446   = do  { (elt_ty, coi) <- boxySplitListTy pat_ty
 447         ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
 448                                                 pats pstate thing_inside
 449         ; return (mkCoPatCoI coi (ListPat pats' elt_ty) pat_ty, pats_tvs, res) }
 450
 451 tc_pat pstate (PArrPat pats _) pat_ty thing_inside
 452   = do  { (elt_ty, coi) <- boxySplitPArrTy pat_ty
 453         ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
 454                                                 pats pstate thing_inside
 455         ; ifM (null pats) (zapToMonotype pat_ty)  -- c.f. ExplicitPArr in TcExpr
 456         ; return (mkCoPatCoI coi (PArrPat pats' elt_ty) pat_ty, pats_tvs, res) }
 457
 458 tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
 459   = do  { let tc = tupleTyCon boxity (length pats)
 460         ; (arg_tys, coi) <- boxySplitTyConApp tc pat_ty
 461         ; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys)
 462                                                pstate thing_inside
 463
 464         -- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
 465         -- so that we can experiment with lazy tuple-matching.
 466         -- This is a pretty odd place to make the switch, but
 467         -- it was easy to do.
 468         ; let pat_ty'          = mkTyConApp tc arg_tys
 469                                      -- pat_ty /= pat_ty iff coi /= IdCo
 470               unmangled_result = TuplePat pats' boxity pat_ty'
 471               possibly_mangled_result
 472                 | opt_IrrefutableTuples &&
 473                   isBoxed boxity            = LazyPat (noLoc unmangled_result)
 474                 | otherwise                 = unmangled_result
 475
 476         ; ASSERT( length arg_tys == length pats )      -- Syntactically enforced
 477           return (mkCoPatCoI coi possibly_mangled_result pat_ty, pats_tvs, res)
 478         }
 479
 480 ------------------------
 481 -- Data constructors
 482 tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
 483   = do  { data_con <- tcLookupDataCon con_name
 484         ; let tycon = dataConTyCon data_con
 485         ; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }
 486
 487 ------------------------
 488 -- Literal patterns
 489 tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
 490   = do  { let lit_ty = hsLitType simple_lit
 491         ; coi <- boxyUnify lit_ty pat_ty
 492                         -- coi is of kind: lit_ty ~ pat_ty
 493         ; res <- thing_inside pstate
 494         ; span <- getSrcSpanM
 495                         -- pattern coercions have to
 496                         -- be of kind: pat_ty ~ lit_ty
 497                         -- hence, sym coi
 498         ; returnM (mkCoPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty,
 499                    [], res) }
 500
 501 ------------------------
 502 -- Overloaded patterns: n, and n+k
 503 tc_pat pstate pat@(NPat over_lit mb_neg eq) pat_ty thing_inside
 504   = do  { let orig = LiteralOrigin over_lit
 505         ; lit'    <- tcOverloadedLit orig over_lit pat_ty
 506         ; eq'     <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
 507         ; mb_neg' <- case mb_neg of
 508                         Nothing  -> return Nothing      -- Positive literal
 509                         Just neg ->     -- Negative literal
 510                                         -- The 'negate' is re-mappable syntax
 511                             do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
 512                                ; return (Just neg') }
 513         ; res <- thing_inside pstate
 514         ; returnM (NPat lit' mb_neg' eq', [], res) }
 515
 516 tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
 517   = do  { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
 518         ; let pat_ty' = idType bndr_id
 519               orig    = LiteralOrigin lit
 520         ; lit' <- tcOverloadedLit orig lit pat_ty'
 521
 522         -- The '>=' and '-' parts are re-mappable syntax
 523         ; ge'    <- tcSyntaxOp orig ge    (mkFunTys [pat_ty', pat_ty'] boolTy)
 524         ; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty')
 525
 526         -- The Report says that n+k patterns must be in Integral
 527         -- We may not want this when using re-mappable syntax, though (ToDo?)
 528         ; icls <- tcLookupClass integralClassName
 529         ; instStupidTheta orig [mkClassPred icls [pat_ty']]
 530
 531         ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
 532         ; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
 533
 534 tc_pat _ _other_pat _ _ = panic "tc_pat"        -- ConPatOut, SigPatOut, VarPatOut
 535 \end{code}
 536
 537
 538 %************************************************************************
 539 %*                                                                      *
 540         Most of the work for constructors is here
 541         (the rest is in the ConPatIn case of tc_pat)
 542 %*                                                                      *
 543 %************************************************************************
 544
 545 [Pattern matching indexed data types]
 546 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 547 Consider the following declarations:
 548
 549   data family Map k :: * -> *
 550   data instance Map (a, b) v = MapPair (Map a (Pair b v))
 551
 552 and a case expression
 553
 554   case x :: Map (Int, c) w of MapPair m -> ...
 555
 556 As explained by [Wrappers for data instance tycons] in MkIds.lhs, the
 557 worker/wrapper types for MapPair are
 558
 559   $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
 560   $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
 561
 562 So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
 563 :R123Map, which means the straight use of boxySplitTyConApp would give a type
 564 error.  Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
 565 boxySplitTyConApp with the family tycon Map instead, which gives us the family
 566 type list {(Int, c), w}.  To get the correct split for :R123Map, we need to
 567 unify the family type list {(Int, c), w} with the instance types {(a, b), v}
 568 (provided by tyConFamInst_maybe together with the family tycon).  This
 569 unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
 570 the split arguments for the representation tycon :R123Map as {Int, c, w}
 571
 572 In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
 573
 574   Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}
 575
 576 moving between representation and family type into account.  To produce type
 577 correct Core, this coercion needs to be used to case the type of the scrutinee
 578 from the family to the representation type.  This is achieved by
 579 unwrapFamInstScrutinee using a CoPat around the result pattern.
 580
 581 Now it might appear seem as if we could have used the existing GADT type
 582 refinement infrastructure of refineAlt and friends instead of the explicit
 583 unification and CoPat generation.  However, that would be wrong.  Why?  The
 584 whole point of GADT refinement is that the refinement is local to the case
 585 alternative.  In contrast, the substitution generated by the unification of
 586 the family type list and instance types needs to be propagated to the outside.
 587 Imagine that in the above example, the type of the scrutinee would have been
 588 (Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
 589 substitution [x -> (a, b), v -> w].  In contrast to GADT matching, the
 590 instantiation of x with (a, b) must be global; ie, it must be valid in *all*
 591 alternatives of the case expression, whereas in the GADT case it might vary
 592 between alternatives.
 593
 594 In fact, if we have a data instance declaration defining a GADT, eq_spec will
 595 be non-empty and we will get a mixture of global instantiations and local
 596 refinement from a single match.  This neatly reflects that, as soon as we
 597 have constrained the type of the scrutinee to the required type index, all
 598 further type refinement is local to the alternative.
 599
 600 \begin{code}
 601 --      Running example:
 602 -- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
 603 --       with scrutinee of type (T ty)
 604
 605 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
 606          -> BoxySigmaType       -- Type of the pattern
 607          -> HsConPatDetails Name -> (PatState -> TcM a)
 608          -> TcM (Pat TcId, [TcTyVar], a)
 609 tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
 610   = do  { let (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _) = dataConFullSig data_con
 611               skol_info  = PatSkol data_con
 612               origin     = SigOrigin skol_info
 613               full_theta = eq_theta ++ dict_theta
 614
 615           -- Instantiate the constructor type variables [a->ty]
 616           -- This may involve doing a family-instance coercion, and building a wrapper
 617         ; (ctxt_res_tys, coi) <- boxySplitTyConAppWithFamily tycon pat_ty
 618         ; let pat_ty' = mkTyConApp tycon ctxt_res_tys
 619                                      -- pat_ty /= pat_ty iff coi /= IdCo
 620               wrap_res_pat res_pat
 621                 = mkCoPatCoI coi (unwrapFamInstScrutinee tycon ctxt_res_tys res_pat) pat_ty
 622
 623           -- Add the stupid theta
 624         ; addDataConStupidTheta data_con ctxt_res_tys
 625
 626         ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs  -- Get location from monad,
 627                                                         -- not from ex_tvs
 628         ; let tenv     = zipTopTvSubst (univ_tvs ++ ex_tvs)
 629                                        (ctxt_res_tys ++ mkTyVarTys ex_tvs')
 630               arg_tys' = substTys tenv arg_tys
 631
 632         ; if null ex_tvs && null eq_spec && null full_theta
 633           then do {     -- The common case; no class bindings etc (see Note [Arrows and patterns])
 634                     (arg_pats', inner_tvs, res) <- tcConArgs data_con arg_tys'
 635                                                                arg_pats pstate thing_inside
 636                   ; let res_pat = ConPatOut { pat_con = L con_span data_con,
 637                                               pat_tvs = [], pat_dicts = [], pat_binds = emptyLHsBinds,
 638                                               pat_args = arg_pats', pat_ty = pat_ty' }
 639
 640                     ; return (wrap_res_pat res_pat, inner_tvs, res) }
 641
 642           else do       -- The general case, with existential, and local equality constraints
 643         { let eq_spec' = substEqSpec tenv eq_spec
 644               theta'   = substTheta  tenv full_theta
 645               ctxt     = pat_ctxt pstate
 646         ; checkTc (case ctxt of { ProcPat -> False; other -> True })
 647                   (existentialProcPat data_con)
 648         ; co_vars <- newCoVars eq_spec' -- Make coercion variables
 649         ; traceTc (text "tcConPat: refineAlt")
 650         ; pstate' <- refineAlt data_con pstate ex_tvs' co_vars pat_ty
 651         ; traceTc (text "tcConPat: refineAlt done!")
 652
 653         ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
 654                 tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
 655
 656         ; loc <- getInstLoc origin
 657         ; dicts <- newDictBndrs loc theta'
 658         ; dict_binds <- tcSimplifyCheckPat loc co_vars (pat_reft pstate')
 659                            ex_tvs' dicts lie_req
 660
 661         ; let res_pat = ConPatOut { pat_con = L con_span data_con,
 662                                     pat_tvs = ex_tvs' ++ co_vars,
 663                                     pat_dicts = map instToVar dicts,
 664                                     pat_binds = dict_binds,
 665                                     pat_args = arg_pats', pat_ty = pat_ty' }
 666         ; return (wrap_res_pat res_pat, ex_tvs' ++ inner_tvs, res)
 667         } }
 668   where
 669     -- Split against the family tycon if the pattern constructor
 670     -- belongs to a family instance tycon.
 671     boxySplitTyConAppWithFamily tycon pat_ty =
 672       traceTc traceMsg >>
 673       case tyConFamInst_maybe tycon of
 674         Nothing                   -> boxySplitTyConApp tycon pat_ty
 675         Just (fam_tycon, instTys) ->
 676           do { (scrutinee_arg_tys, coi) <- boxySplitTyConApp fam_tycon pat_ty
 677              ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
 678              ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
 679              ; return (freshTvs, coi)
 680              }
 681       where
 682         traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
 683                          ppr tycon <+> ppr pat_ty
 684                        , text "  family instance:" <+>
 685                          ppr (tyConFamInst_maybe tycon)
 686                        ]
 687
 688     -- Wraps the pattern (which must be a ConPatOut pattern) in a coercion
 689     -- pattern if the tycon is an instance of a family.
 690     --
 691     unwrapFamInstScrutinee :: TyCon -> [Type] -> Pat Id -> Pat Id
 692     unwrapFamInstScrutinee tycon args pat
 693       | Just co_con <- tyConFamilyCoercion_maybe tycon
 694 --      , not (isNewTyCon tycon)       -- newtypes are explicitly unwrapped by
 695                                      -- the desugarer
 696           -- NB: We can use CoPat directly, rather than mkCoPat, as we know the
 697           --     coercion is not the identity; mkCoPat is inconvenient as it
 698           --     wants a located pattern.
 699       = CoPat (WpCo $ mkTyConApp co_con args)       -- co fam ty to repr ty
 700               (pat {pat_ty = mkTyConApp tycon args})    -- representation type
 701               pat_ty                                    -- family inst type
 702       | otherwise
 703       = pat
 704
 705
 706 tcConArgs :: DataCon -> [TcSigmaType]
 707           -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
 708
 709 tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
 710   = do  { checkTc (con_arity == no_of_args)     -- Check correct arity
 711                   (arityErr "Constructor" data_con con_arity no_of_args)
 712         ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
 713         ; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys
 714                                               pstate thing_inside
 715         ; return (PrefixCon arg_pats', tvs, res) }
 716   where
 717     con_arity  = dataConSourceArity data_con
 718     no_of_args = length arg_pats
 719
 720 tcConArgs data_con arg_tys (InfixCon p1 p2) pstate thing_inside
 721   = do  { checkTc (con_arity == 2)      -- Check correct arity
 722                   (arityErr "Constructor" data_con con_arity 2)
 723         ; let [arg_ty1,arg_ty2] = arg_tys       -- This can't fail after the arity check
 724         ; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
 725                                               pstate thing_inside
 726         ; return (InfixCon p1' p2', tvs, res) }
 727   where
 728     con_arity  = dataConSourceArity data_con
 729
 730 tcConArgs data_con other_args (InfixCon p1 p2) pstate thing_inside
 731   = pprPanic "tcConArgs" (ppr data_con) -- InfixCon always has two arguments
 732
 733 tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
 734   = do  { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
 735         ; return (RecCon (HsRecFields rpats' dd), tvs, res) }
 736   where
 737     tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
 738     tc_field (HsRecField field_lbl pat pun) pstate thing_inside
 739       = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
 740            ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
 741            ; return (HsRecField sel_id pat' pun, tvs, res) }
 742
 743     find_field_ty :: FieldLabel -> TcM (Id, TcType)
 744     find_field_ty field_lbl
 745         = case [ty | (f,ty) <- field_tys, f == field_lbl] of
 746
 747                 -- No matching field; chances are this field label comes from some
 748                 -- other record type (or maybe none).  As well as reporting an
 749                 -- error we still want to typecheck the pattern, principally to
 750                 -- make sure that all the variables it binds are put into the
 751                 -- environment, else the type checker crashes later:
 752                 --      f (R { foo = (a,b) }) = a+b
 753                 -- If foo isn't one of R's fields, we don't want to crash when
 754                 -- typechecking the "a+b".
 755            [] -> do { addErrTc (badFieldCon data_con field_lbl)
 756                     ; bogus_ty <- newFlexiTyVarTy liftedTypeKind
 757                     ; return (error "Bogus selector Id", bogus_ty) }
 758
 759                 -- The normal case, when the field comes from the right constructor
 760            (pat_ty : extras) ->
 761                 ASSERT( null extras )
 762                 do { sel_id <- tcLookupField field_lbl
 763                    ; return (sel_id, pat_ty) }
 764
 765     field_tys :: [(FieldLabel, TcType)]
 766     field_tys = zip (dataConFieldLabels data_con) arg_tys
 767         -- Don't use zipEqual! If the constructor isn't really a record, then
 768         -- dataConFieldLabels will be empty (and each field in the pattern
 769         -- will generate an error below).
 770
 771 tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id)
 772 tcConArg (arg_pat, arg_ty) pstate thing_inside
 773   = tc_lpat arg_pat arg_ty pstate thing_inside
 774         -- NB: the tc_lpat will refine pat_ty if necessary
 775         --     based on the current pstate, which may include
 776         --     refinements from peer argument patterns to the left
 777 \end{code}
 778
 779 \begin{code}
 780 addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
 781 -- Instantiate the "stupid theta" of the data con, and throw
 782 -- the constraints into the constraint set
 783 addDataConStupidTheta data_con inst_tys
 784   | null stupid_theta = return ()
 785   | otherwise         = instStupidTheta origin inst_theta
 786   where
 787     origin = OccurrenceOf (dataConName data_con)
 788         -- The origin should always report "occurrence of C"
 789         -- even when C occurs in a pattern
 790     stupid_theta = dataConStupidTheta data_con
 791     tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
 792     inst_theta = substTheta tenv stupid_theta
 793 \end{code}
 794
 795 Note [Arrows and patterns]
 796 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 797 (Oct 07) Arrow noation has the odd property that it involves "holes in the scope".
 798 For example:
 799   expr :: Arrow a => a () Int
 800   expr = proc (y,z) -> do
 801           x <- term -< y
 802           expr' -< x
 803
 804 Here the 'proc (y,z)' binding scopes over the arrow tails but not the
 805 arrow body (e.g 'term').  As things stand (bogusly) all the
 806 constraints from the proc body are gathered together, so constraints
 807 from 'term' will be seen by the tcPat for (y,z).  But we must *not*
 808 bind constraints from 'term' here, becuase the desugarer will not make
 809 these bindings scope over 'term'.
 810
 811 The Right Thing is not to confuse these constraints together. But for
 812 now the Easy Thing is to ensure that we do not have existential or
 813 GADT constraints in a 'proc', and to short-cut the constraint
 814 simplification for such vanilla patterns so that it binds no
 815 constraints. Hence the 'fast path' in tcConPat; but it's also a good
 816 plan for ordinary vanilla patterns to bypass the constraint
 817 simplification step.
 818
 819
 820 %************************************************************************
 821 %*                                                                      *
 822                 Type refinement
 823 %*                                                                      *
 824 %************************************************************************
 825
 826 \begin{code}
 827 refineAlt :: DataCon            -- For tracing only
 828           -> PatState
 829           -> [TcTyVar]          -- Existentials
 830           -> [CoVar]            -- Equational constraints
 831           -> BoxySigmaType      -- Pattern type
 832           -> TcM PatState
 833
 834 refineAlt con pstate ex_tvs [] pat_ty
 835   | null $ dataConEqTheta con
 836   = return pstate       -- Common case: no equational constraints
 837
 838 refineAlt con pstate ex_tvs co_vars pat_ty
 839   = do  { opt_gadt <- doptM Opt_GADTs   -- No type-refinement unless GADTs are on
 840         ; if (not opt_gadt) then return pstate
 841           else do
 842
 843         { checkTc (isRigidTy pat_ty) (nonRigidMatch con)
 844         -- We are matching against a GADT constructor with non-trivial
 845         -- constraints, but pattern type is wobbly.  For now we fail.
 846         -- We can make sense of this, however:
 847         -- Suppose MkT :: forall a b. (a:=:[b]) => b -> T a
 848         --      (\x -> case x of { MkT v -> v })
 849         -- We can infer that x must have type T [c], for some wobbly 'c'
 850         -- and translate to
 851         --      (\(x::T [c]) -> case x of
 852         --                        MkT b (g::([c]:=:[b])) (v::b) -> v `cast` sym g
 853         -- To implement this, we'd first instantiate the equational
 854         -- constraints with *wobbly* type variables for the existentials;
 855         -- then unify these constraints to make pat_ty the right shape;
 856         -- then proceed exactly as in the rigid case
 857
 858                 -- In the rigid case, we perform type refinement
 859         ; case gadtRefine (pat_reft pstate) ex_tvs co_vars of {
 860             Failed msg     -> failWithTc (inaccessibleAlt msg) ;
 861             Succeeded reft -> do { traceTc trace_msg
 862                                  ; return (pstate { pat_reft = reft, pat_eqs = (pat_eqs pstate || not (null $ dataConEqTheta con)) }) }
 863                     -- DO NOT refine the envt right away, because we
 864                     -- might be inside a lazy pattern.  Instead, refine pstate
 865                 where
 866
 867                     trace_msg = text "refineAlt:match" <+>
 868                                 vcat [ ppr con <+> ppr ex_tvs,
 869                                        ppr [(v, tyVarKind v) | v <- co_vars],
 870                                        ppr reft]
 871         } } }
 872 \end{code}
 873
 874
 875 %************************************************************************
 876 %*                                                                      *
 877                 Overloaded literals
 878 %*                                                                      *
 879 %************************************************************************
 880
 881 In tcOverloadedLit we convert directly to an Int or Integer if we
 882 know that's what we want.  This may save some time, by not
 883 temporarily generating overloaded literals, but it won't catch all
 884 cases (the rest are caught in lookupInst).
 885
 886 \begin{code}
 887 tcOverloadedLit :: InstOrigin
 888                  -> HsOverLit Name
 889                  -> BoxyRhoType
 890                  -> TcM (HsOverLit TcId)
 891 tcOverloadedLit orig lit@(HsIntegral i fi _) res_ty
 892   | not (fi `isHsVar` fromIntegerName)  -- Do not generate a LitInst for rebindable syntax.
 893         -- Reason: If we do, tcSimplify will call lookupInst, which
 894         --         will call tcSyntaxName, which does unification,
 895         --         which tcSimplify doesn't like
 896         -- ToDo: noLoc sadness
 897   = do  { integer_ty <- tcMetaTy integerTyConName
 898         ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty)
 899         ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty))) res_ty) }
 900
 901   | Just expr <- shortCutIntLit i res_ty
 902   = return (HsIntegral i expr res_ty)
 903
 904   | otherwise
 905   = do  { expr <- newLitInst orig lit res_ty
 906         ; return (HsIntegral i expr res_ty) }
 907
 908 tcOverloadedLit orig lit@(HsFractional r fr _) res_ty
 909   | not (fr `isHsVar` fromRationalName) -- c.f. HsIntegral case
 910   = do  { rat_ty <- tcMetaTy rationalTyConName
 911         ; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty res_ty)
 912                 -- Overloaded literals must have liftedTypeKind, because
 913                 -- we're instantiating an overloaded function here,
 914                 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
 915                 -- However this'll be picked up by tcSyntaxOp if necessary
 916         ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty))) res_ty) }
 917
 918   | Just expr <- shortCutFracLit r res_ty
 919   = return (HsFractional r expr res_ty)
 920
 921   | otherwise
 922   = do  { expr <- newLitInst orig lit res_ty
 923         ; return (HsFractional r expr res_ty) }
 924
 925 tcOverloadedLit orig lit@(HsIsString s fr _) res_ty
 926   | not (fr `isHsVar` fromStringName)   -- c.f. HsIntegral case
 927   = do  { str_ty <- tcMetaTy stringTyConName
 928         ; fr' <- tcSyntaxOp orig fr (mkFunTy str_ty res_ty)
 929         ; return (HsIsString s (HsApp (noLoc fr') (nlHsLit (HsString s))) res_ty) }
 930
 931   | Just expr <- shortCutStringLit s res_ty
 932   = return (HsIsString s expr res_ty)
 933
 934   | otherwise
 935   = do  { expr <- newLitInst orig lit res_ty
 936         ; return (HsIsString s expr res_ty) }
 937
 938 newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
 939 newLitInst orig lit res_ty      -- Make a LitInst
 940   = do  { loc <- getInstLoc orig
 941         ; res_tau <- zapToMonotype res_ty
 942         ; new_uniq <- newUnique
 943         ; let   lit_nm   = mkSystemVarName new_uniq FSLIT("lit")
 944                 lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit,
 945                                     tci_ty = res_tau, tci_loc = loc}
 946         ; extendLIE lit_inst
 947         ; return (HsVar (instToId lit_inst)) }
 948 \end{code}
 949
 950
 951 %************************************************************************
 952 %*                                                                      *
 953                 Note [Pattern coercions]
 954 %*                                                                      *
 955 %************************************************************************
 956
 957 In principle, these program would be reasonable:
 958
 959         f :: (forall a. a->a) -> Int
 960         f (x :: Int->Int) = x 3
 961
 962         g :: (forall a. [a]) -> Bool
 963         g [] = True
 964
 965 In both cases, the function type signature restricts what arguments can be passed
 966 in a call (to polymorphic ones).  The pattern type signature then instantiates this
 967 type.  For example, in the first case,  (forall a. a->a) <= Int -> Int, and we
 968 generate the translated term
 969         f = \x' :: (forall a. a->a).  let x = x' Int in x 3
 970
 971 From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
 972 And it requires a significant amount of code to implement, becuase we need to decorate
 973 the translated pattern with coercion functions (generated from the subsumption check
 974 by tcSub).
 975
 976 So for now I'm just insisting on type *equality* in patterns.  No subsumption.
 977
 978 Old notes about desugaring, at a time when pattern coercions were handled:
 979
 980 A SigPat is a type coercion and must be handled one at at time.  We can't
 981 combine them unless the type of the pattern inside is identical, and we don't
 982 bother to check for that.  For example:
 983
 984         data T = T1 Int | T2 Bool
 985         f :: (forall a. a -> a) -> T -> t
 986         f (g::Int->Int)   (T1 i) = T1 (g i)
 987         f (g::Bool->Bool) (T2 b) = T2 (g b)
 988
 989 We desugar this as follows:
 990
 991         f = \ g::(forall a. a->a) t::T ->
 992             let gi = g Int
 993             in case t of { T1 i -> T1 (gi i)
 994                            other ->
 995             let gb = g Bool
 996             in case t of { T2 b -> T2 (gb b)
 997                            other -> fail }}
 998
 999 Note that we do not treat the first column of patterns as a
1000 column of variables, because the coerced variables (gi, gb)
1001 would be of different types.  So we get rather grotty code.
1002 But I don't think this is a common case, and if it was we could
1003 doubtless improve it.
1004
1005 Meanwhile, the strategy is:
1006         * treat each SigPat coercion (always non-identity coercions)
1007                 as a separate block
1008         * deal with the stuff inside, and then wrap a binding round
1009                 the result to bind the new variable (gi, gb, etc)
1010
1011
1012 %************************************************************************
1013 %*                                                                      *
1014 \subsection{Errors and contexts}
1015 %*                                                                      *
1016 %************************************************************************
1017
1018 \begin{code}
1019 patCtxt :: Pat Name -> Maybe Message    -- Not all patterns are worth pushing a context
1020 patCtxt (VarPat _)  = Nothing
1021 patCtxt (ParPat _)  = Nothing
1022 patCtxt (AsPat _ _) = Nothing
1023 patCtxt pat         = Just (hang (ptext SLIT("In the pattern:"))
1024                                4 (ppr pat))
1025
1026 -----------------------------------------------
1027
1028 existentialExplode pat
1029   = hang (vcat [text "My brain just exploded.",
1030                 text "I can't handle pattern bindings for existentially-quantified constructors.",
1031                 text "Instead, use a case-expression, or do-notation, to unpack the constructor.",
1032                 text "In the binding group for"])
1033         4 (ppr pat)
1034
1035 sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env
1036   = do  { pat_tys' <- mapM zonkTcType pat_tys
1037         ; body_ty' <- zonkTcType body_ty
1038         ; let (env1,  tidy_tys)    = tidyOpenTypes tidy_env (map idType show_ids)
1039               (env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys'
1040               (env3, tidy_body_ty) = tidyOpenType  env2 body_ty'
1041         ; return (env3,
1042                  sep [ptext SLIT("When checking an existential match that binds"),
1043                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
1044                       ptext SLIT("The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
1045                       ptext SLIT("The body has type:") <+> ppr tidy_body_ty
1046                 ]) }
1047   where
1048     bound_ids = collectPatsBinders pats
1049     show_ids = filter is_interesting bound_ids
1050     is_interesting id = any (`elemVarSet` varTypeTyVars id) bound_tvs
1051
1052     ppr_id id ty = ppr id <+> dcolon <+> ppr ty
1053         -- Don't zonk the types so we get the separate, un-unified versions
1054
1055 badFieldCon :: DataCon -> Name -> SDoc
1056 badFieldCon con field
1057   = hsep [ptext SLIT("Constructor") <+> quotes (ppr con),
1058           ptext SLIT("does not have field"), quotes (ppr field)]
1059
1060 polyPatSig :: TcType -> SDoc
1061 polyPatSig sig_ty
1062   = hang (ptext SLIT("Illegal polymorphic type signature in pattern:"))
1063        2 (ppr sig_ty)
1064
1065 badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
1066
1067 existentialProcPat :: DataCon -> SDoc
1068 existentialProcPat con
1069   = hang (ptext SLIT("Illegal constructor") <+> quotes (ppr con) <+> ptext SLIT("in a 'proc' pattern"))
1070        2 (ptext SLIT("Proc patterns cannot use existentials or GADTs"))
1071
1072 lazyPatErr pat tvs
1073   = failWithTc $
1074     hang (ptext SLIT("A lazy (~) pattern cannot bind existential type variables"))
1075        2 (vcat (map pprSkolTvBinding tvs))
1076
1077 nonRigidMatch con
1078   =  hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con))
1079         2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))
1080
1081 nonRigidResult res_ty
1082   =  hang (ptext SLIT("GADT pattern match with non-rigid result type") <+> quotes (ppr res_ty))
1083         2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))
1084
1085 inaccessibleAlt msg
1086   = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
1087 \end{code}