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