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