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