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