compiler/typecheck/TcPat.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   4 %
   5
   6 TcPat: Typechecking patterns
   7
   8 \begin{code}
   9 {-# OPTIONS -w #-}
  10 -- The above warning supression flag is a temporary kludge.
  11 -- While working on this module you are encouraged to remove it and fix
  12 -- any warnings in the module. See
  13 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
  14 -- for details
  15
  16 module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcProcPat, tcOverloadedLit,
  17                addDataConStupidTheta, badFieldCon, polyPatSig ) where
  18
  19 #include "HsVersions.h"
  20
  21 import {-# SOURCE #-}   TcExpr( tcSyntaxOp, tcInferRho)
  22
  23 import HsSyn
  24 import TcHsSyn
  25 import TcRnMonad
  26 import Inst
  27 import Id
  28 import Var
  29 import CoreFVs
  30 import Name
  31 import TcSimplify
  32 import TcEnv
  33 import TcMType
  34 import TcType
  35 import VarSet
  36 import TcUnify
  37 import TcHsType
  38 import TysWiredIn
  39 import Type
  40 import Coercion
  41 import StaticFlags
  42 import TyCon
  43 import DataCon
  44 import DynFlags
  45 import PrelNames
  46 import BasicTypes hiding (SuccessFlag(..))
  47 import SrcLoc
  48 import ErrUtils
  49 import Util
  50 import Maybes
  51 import Outputable
  52 import FastString
  53 import Monad
  54 \end{code}
  55
  56
  57 %************************************************************************
  58 %*                                                                      *
  59                 External interface
  60 %*                                                                      *
  61 %************************************************************************
  62
  63 \begin{code}
  64 tcLetPat :: (Name -> Maybe TcRhoType)
  65          -> LPat Name -> BoxySigmaType
  66          -> TcM a
  67          -> TcM (LPat TcId, a)
  68 tcLetPat sig_fn pat pat_ty thing_inside
  69   = do  { let init_state = PS { pat_ctxt = LetPat sig_fn,
  70                                 pat_eqs  = False }
  71         ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state
  72                                    (\ _ -> thing_inside)
  73
  74         -- Don't know how to deal with pattern-bound existentials yet
  75         ; checkTc (null ex_tvs) (existentialExplode pat)
  76
  77         ; return (pat', res) }
  78
  79 -----------------
  80 tcLamPats :: [LPat Name]                -- Patterns,
  81           -> [BoxySigmaType]            --   and their types
  82           -> BoxyRhoType                -- Result type,
  83           -> (BoxyRhoType -> TcM a)     --   and the checker for the body
  84           -> TcM ([LPat TcId], a)
  85
  86 -- This is the externally-callable wrapper function
  87 -- Typecheck the patterns, extend the environment to bind the variables,
  88 -- do the thing inside, use any existentially-bound dictionaries to
  89 -- discharge parts of the returning LIE, and deal with pattern type
  90 -- signatures
  91
  92 --   1. Initialise the PatState
  93 --   2. Check the patterns
  94 --   3. Check the body
  95 --   4. Check that no existentials escape
  96
  97 tcLamPats pats tys res_ty thing_inside
  98   = tc_lam_pats LamPat (zipEqual "tcLamPats" pats tys)
  99                 res_ty thing_inside
 100
 101 tcLamPat :: LPat Name -> BoxySigmaType
 102          -> BoxyRhoType             -- Result type
 103          -> (BoxyRhoType -> TcM a)  -- Checker for body, given its result type
 104          -> TcM (LPat TcId, a)
 105
 106 tcProcPat = tc_lam_pat ProcPat
 107 tcLamPat  = tc_lam_pat LamPat
 108
 109 tc_lam_pat ctxt pat pat_ty res_ty thing_inside
 110   = do  { ([pat'],thing) <- tc_lam_pats ctxt [(pat, pat_ty)] res_ty thing_inside
 111         ; return (pat', thing) }
 112
 113 -----------------
 114 tc_lam_pats :: PatCtxt
 115             -> [(LPat Name,BoxySigmaType)]
 116             -> BoxyRhoType            -- Result type
 117             -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type
 118             -> TcM ([LPat TcId], a)
 119 tc_lam_pats ctxt pat_ty_prs res_ty thing_inside
 120   =  do { let init_state = PS { pat_ctxt = ctxt, pat_eqs = False }
 121
 122         ; (pats', ex_tvs, res) <- do { traceTc (text "tc_lam_pats" <+> (ppr pat_ty_prs $$ ppr res_ty))
 123                                   ; tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
 124                                     if (pat_eqs pstate' && (not $ isRigidTy res_ty))
 125                                      then nonRigidResult res_ty
 126                                      else thing_inside res_ty }
 127
 128         ; let tys = map snd pat_ty_prs
 129         ; tcCheckExistentialPat pats' ex_tvs tys res_ty
 130
 131         ; return (pats', res) }
 132
 133
 134 -----------------
 135 tcCheckExistentialPat :: [LPat TcId]            -- Patterns (just for error message)
 136                       -> [TcTyVar]              -- Existentially quantified tyvars bound by pattern
 137                       -> [BoxySigmaType]        -- Types of the patterns
 138                       -> BoxyRhoType            -- Type of the body of the match
 139                                                 -- Tyvars in either of these must not escape
 140                       -> TcM ()
 141 -- NB: we *must* pass "pats_tys" not just "body_ty" to tcCheckExistentialPat
 142 -- For example, we must reject this program:
 143 --      data C = forall a. C (a -> Int)
 144 --      f (C g) x = g x
 145 -- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).
 146
 147 tcCheckExistentialPat pats [] pat_tys body_ty
 148   = return ()   -- Short cut for case when there are no existentials
 149
 150 tcCheckExistentialPat pats ex_tvs pat_tys body_ty
 151   = addErrCtxtM (sigPatCtxt pats ex_tvs pat_tys body_ty)        $
 152     checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
 153
 154 data PatState = PS {
 155         pat_ctxt :: PatCtxt,
 156         pat_eqs  :: Bool        -- <=> there are any equational constraints
 157                                 -- Used at the end to say whether the result
 158                                 -- type must be rigid
 159   }
 160
 161 data PatCtxt
 162   = LamPat
 163   | ProcPat                             -- The pattern in (proc pat -> ...)
 164                                         --      see Note [Arrows and patterns]
 165   | LetPat (Name -> Maybe TcRhoType)    -- Used for let(rec) bindings
 166
 167 patSigCtxt :: PatState -> UserTypeCtxt
 168 patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
 169 patSigCtxt other                        = LamPatSigCtxt
 170 \end{code}
 171
 172
 173
 174 %************************************************************************
 175 %*                                                                      *
 176                 Binders
 177 %*                                                                      *
 178 %************************************************************************
 179
 180 \begin{code}
 181 tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
 182 tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
 183   | Just mono_ty <- lookup_sig bndr_name
 184   = do  { mono_name <- newLocalName bndr_name
 185         ; boxyUnify mono_ty pat_ty
 186         ; return (Id.mkLocalId mono_name mono_ty) }
 187
 188   | otherwise
 189   = do  { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
 190         ; mono_name <- newLocalName bndr_name
 191         ; return (Id.mkLocalId mono_name pat_ty') }
 192
 193 tcPatBndr (PS { pat_ctxt = _lam_or_proc }) bndr_name pat_ty
 194   = do  { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
 195                 -- We have an undecorated binder, so we do rule ABS1,
 196                 -- by unboxing the boxy type, forcing any un-filled-in
 197                 -- boxes to become monotypes
 198                 -- NB that pat_ty' can still be a polytype:
 199                 --      data T = MkT (forall a. a->a)
 200                 --      f t = case t of { MkT g -> ... }
 201                 -- Here, the 'g' must get type (forall a. a->a) from the
 202                 -- MkT context
 203         ; return (Id.mkLocalId bndr_name pat_ty') }
 204
 205
 206 -------------------
 207 bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId)
 208 bindInstsOfPatId id thing_inside
 209   | not (isOverloadedTy (idType id))
 210   = do { res <- thing_inside; return (res, emptyLHsBinds) }
 211   | otherwise
 212   = do  { (res, lie) <- getLIE thing_inside
 213         ; binds <- bindInstsOfLocalFuns lie [id]
 214         ; return (res, binds) }
 215
 216 -------------------
 217 unBoxPatBndrType  ty name = unBoxArgType ty (ptext (sLit "The variable") <+> quotes (ppr name))
 218 unBoxWildCardType ty      = unBoxArgType ty (ptext (sLit "A wild-card pattern"))
 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) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
 426         ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
 427                               tc_lpat pat inner_ty pstate thing_inside
 428         ; return (SigPatOut pat' inner_ty, tvs, res) }
 429
 430 tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
 431   = failWithTc (badTypePat pat)
 432
 433 ------------------------
 434 -- Lists, tuples, arrays
 435 tc_pat pstate (ListPat pats _) pat_ty thing_inside
 436   = do  { (elt_ty, coi) <- boxySplitListTy pat_ty
 437         ; let scoi = mkSymCoI coi
 438         ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
 439                                                 pats pstate thing_inside
 440         ; return (mkCoPatCoI scoi (ListPat pats' elt_ty) pat_ty, pats_tvs, res)
 441         }
 442
 443 tc_pat pstate (PArrPat pats _) pat_ty thing_inside
 444   = do  { (elt_ty, coi) <- boxySplitPArrTy pat_ty
 445         ; let scoi = mkSymCoI coi
 446         ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
 447                                                 pats pstate thing_inside
 448         ; when (null pats) (zapToMonotype pat_ty >> return ())  -- c.f. ExplicitPArr in TcExpr
 449         ; return (mkCoPatCoI scoi (PArrPat pats' elt_ty) pat_ty, pats_tvs, res)
 450         }
 451
 452 tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
 453   = do  { let tc = tupleTyCon boxity (length pats)
 454         ; (arg_tys, coi) <- boxySplitTyConApp tc pat_ty
 455         ; let scoi = mkSymCoI coi
 456         ; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys)
 457                                                pstate thing_inside
 458
 459         -- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
 460         -- so that we can experiment with lazy tuple-matching.
 461         -- This is a pretty odd place to make the switch, but
 462         -- it was easy to do.
 463         ; let pat_ty'          = mkTyConApp tc arg_tys
 464                                      -- pat_ty /= pat_ty iff coi /= IdCo
 465               unmangled_result = TuplePat pats' boxity pat_ty'
 466               possibly_mangled_result
 467                 | opt_IrrefutableTuples &&
 468                   isBoxed boxity            = LazyPat (noLoc unmangled_result)
 469                 | otherwise                 = unmangled_result
 470
 471         ; ASSERT( length arg_tys == length pats )      -- Syntactically enforced
 472           return (mkCoPatCoI scoi possibly_mangled_result pat_ty, pats_tvs, res)
 473         }
 474
 475 ------------------------
 476 -- Data constructors
 477 tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
 478   = do  { data_con <- tcLookupDataCon con_name
 479         ; let tycon = dataConTyCon data_con
 480         ; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }
 481
 482 ------------------------
 483 -- Literal patterns
 484 tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
 485   = do  { let lit_ty = hsLitType simple_lit
 486         ; coi <- boxyUnify lit_ty pat_ty
 487                         -- coi is of kind: lit_ty ~ pat_ty
 488         ; res <- thing_inside pstate
 489         ; span <- getSrcSpanM
 490                         -- pattern coercions have to
 491                         -- be of kind: pat_ty ~ lit_ty
 492                         -- hence, sym coi
 493         ; return (mkCoPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty,
 494                    [], res) }
 495
 496 ------------------------
 497 -- Overloaded patterns: n, and n+k
 498 tc_pat pstate pat@(NPat over_lit mb_neg eq) pat_ty thing_inside
 499   = do  { let orig = LiteralOrigin over_lit
 500         ; lit'    <- tcOverloadedLit orig over_lit pat_ty
 501         ; eq'     <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
 502         ; mb_neg' <- case mb_neg of
 503                         Nothing  -> return Nothing      -- Positive literal
 504                         Just neg ->     -- Negative literal
 505                                         -- The 'negate' is re-mappable syntax
 506                             do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
 507                                ; return (Just neg') }
 508         ; res <- thing_inside pstate
 509         ; return (NPat lit' mb_neg' eq', [], res) }
 510
 511 tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
 512   = do  { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
 513         ; let pat_ty' = idType bndr_id
 514               orig    = LiteralOrigin lit
 515         ; lit' <- tcOverloadedLit orig lit pat_ty'
 516
 517         -- The '>=' and '-' parts are re-mappable syntax
 518         ; ge'    <- tcSyntaxOp orig ge    (mkFunTys [pat_ty', pat_ty'] boolTy)
 519         ; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty')
 520
 521         -- The Report says that n+k patterns must be in Integral
 522         -- We may not want this when using re-mappable syntax, though (ToDo?)
 523         ; icls <- tcLookupClass integralClassName
 524         ; instStupidTheta orig [mkClassPred icls [pat_ty']]
 525
 526         ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
 527         ; return (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
 528
 529 tc_pat _ _other_pat _ _ = panic "tc_pat"        -- ConPatOut, SigPatOut, VarPatOut
 530 \end{code}
 531
 532
 533 %************************************************************************
 534 %*                                                                      *
 535         Most of the work for constructors is here
 536         (the rest is in the ConPatIn case of tc_pat)
 537 %*                                                                      *
 538 %************************************************************************
 539
 540 [Pattern matching indexed data types]
 541 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 542 Consider the following declarations:
 543
 544   data family Map k :: * -> *
 545   data instance Map (a, b) v = MapPair (Map a (Pair b v))
 546
 547 and a case expression
 548
 549   case x :: Map (Int, c) w of MapPair m -> ...
 550
 551 As explained by [Wrappers for data instance tycons] in MkIds.lhs, the
 552 worker/wrapper types for MapPair are
 553
 554   $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
 555   $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
 556
 557 So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
 558 :R123Map, which means the straight use of boxySplitTyConApp would give a type
 559 error.  Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
 560 boxySplitTyConApp with the family tycon Map instead, which gives us the family
 561 type list {(Int, c), w}.  To get the correct split for :R123Map, we need to
 562 unify the family type list {(Int, c), w} with the instance types {(a, b), v}
 563 (provided by tyConFamInst_maybe together with the family tycon).  This
 564 unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
 565 the split arguments for the representation tycon :R123Map as {Int, c, w}
 566
 567 In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
 568
 569   Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}
 570
 571 moving between representation and family type into account.  To produce type
 572 correct Core, this coercion needs to be used to case the type of the scrutinee
 573 from the family to the representation type.  This is achieved by
 574 unwrapFamInstScrutinee using a CoPat around the result pattern.
 575
 576 Now it might appear seem as if we could have used the previous GADT type
 577 refinement infrastructure of refineAlt and friends instead of the explicit
 578 unification and CoPat generation.  However, that would be wrong.  Why?  The
 579 whole point of GADT refinement is that the refinement is local to the case
 580 alternative.  In contrast, the substitution generated by the unification of
 581 the family type list and instance types needs to be propagated to the outside.
 582 Imagine that in the above example, the type of the scrutinee would have been
 583 (Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
 584 substitution [x -> (a, b), v -> w].  In contrast to GADT matching, the
 585 instantiation of x with (a, b) must be global; ie, it must be valid in *all*
 586 alternatives of the case expression, whereas in the GADT case it might vary
 587 between alternatives.
 588
 589 RIP GADT refinement: refinements have been replaced by the use of explicit
 590 equality constraints that are used in conjunction with implication constraints
 591 to express the local scope of GADT refinements.
 592
 593 \begin{code}
 594 --      Running example:
 595 -- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
 596 --       with scrutinee of type (T ty)
 597
 598 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
 599          -> BoxySigmaType       -- Type of the pattern
 600          -> HsConPatDetails Name -> (PatState -> TcM a)
 601          -> TcM (Pat TcId, [TcTyVar], a)
 602 tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
 603   = do  { let (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _)
 604                 = dataConFullSig data_con
 605               skol_info  = PatSkol data_con
 606               origin     = SigOrigin skol_info
 607               full_theta = eq_theta ++ dict_theta
 608
 609           -- Instantiate the constructor type variables [a->ty]
 610           -- This may involve doing a family-instance coercion, and building a
 611           -- wrapper
 612         ; (ctxt_res_tys, coi) <- boxySplitTyConAppWithFamily tycon pat_ty
 613         ; let sym_coi = mkSymCoI coi  -- boxy split coercion oriented wrongly
 614               pat_ty' = mkTyConApp tycon ctxt_res_tys
 615                                       -- pat_ty' /= pat_ty iff coi /= IdCo
 616
 617               wrap_res_pat res_pat = mkCoPatCoI sym_coi uwScrut pat_ty
 618                 where
 619                   uwScrut = unwrapFamInstScrutinee tycon ctxt_res_tys res_pat
 620
 621         ; traceTc $ case sym_coi of
 622                       IdCo -> text "sym_coi:IdCo"
 623                       ACo co -> text "sym_coi: ACoI" <+> ppr co
 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; other -> 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 explicit or implicit (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 (checkTc (isRigidTy pat_ty)
 670                                         (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                   -> boxySplitTyConApp tycon pat_ty
 693         Just (fam_tycon, instTys) ->
 694           do { (scrutinee_arg_tys, coi) <- boxySplitTyConApp fam_tycon pat_ty
 695              ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
 696              ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
 697              ; return (freshTvs, coi)
 698              }
 699       where
 700         traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
 701                          ppr tycon <+> ppr pat_ty
 702                        , text "  family instance:" <+>
 703                          ppr (tyConFamInst_maybe tycon)
 704                        ]
 705
 706     -- Wraps the pattern (which must be a ConPatOut pattern) in a coercion
 707     -- pattern if the tycon is an instance of a family.
 708     --
 709     unwrapFamInstScrutinee :: TyCon -> [Type] -> Pat Id -> Pat Id
 710     unwrapFamInstScrutinee tycon args pat
 711       | Just co_con <- tyConFamilyCoercion_maybe tycon
 712 --      , not (isNewTyCon tycon)       -- newtypes are explicitly unwrapped by
 713                                      -- the desugarer
 714           -- NB: We can use CoPat directly, rather than mkCoPat, as we know the
 715           --     coercion is not the identity; mkCoPat is inconvenient as it
 716           --     wants a located pattern.
 717       = CoPat (WpCast $ mkTyConApp co_con args)       -- co fam ty to repr ty
 718               (pat {pat_ty = mkTyConApp tycon args})    -- representation type
 719               pat_ty                                    -- family inst type
 720       | otherwise
 721       = pat
 722
 723
 724 tcConArgs :: DataCon -> [TcSigmaType]
 725           -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
 726
 727 tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
 728   = do  { checkTc (con_arity == no_of_args)     -- Check correct arity
 729                   (arityErr "Constructor" data_con con_arity no_of_args)
 730         ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
 731         ; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys
 732                                               pstate thing_inside
 733         ; return (PrefixCon arg_pats', tvs, res) }
 734   where
 735     con_arity  = dataConSourceArity data_con
 736     no_of_args = length arg_pats
 737
 738 tcConArgs data_con arg_tys (InfixCon p1 p2) pstate thing_inside
 739   = do  { checkTc (con_arity == 2)      -- Check correct arity
 740                   (arityErr "Constructor" data_con con_arity 2)
 741         ; let [arg_ty1,arg_ty2] = arg_tys       -- This can't fail after the arity check
 742         ; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
 743                                               pstate thing_inside
 744         ; return (InfixCon p1' p2', tvs, res) }
 745   where
 746     con_arity  = dataConSourceArity data_con
 747
 748 tcConArgs data_con other_args (InfixCon p1 p2) pstate thing_inside
 749   = pprPanic "tcConArgs" (ppr data_con) -- InfixCon always has two arguments
 750
 751 tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
 752   = do  { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
 753         ; return (RecCon (HsRecFields rpats' dd), tvs, res) }
 754   where
 755     tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
 756     tc_field (HsRecField field_lbl pat pun) pstate thing_inside
 757       = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
 758            ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
 759            ; return (HsRecField sel_id pat' pun, tvs, res) }
 760
 761     find_field_ty :: FieldLabel -> TcM (Id, TcType)
 762     find_field_ty field_lbl
 763         = case [ty | (f,ty) <- field_tys, f == field_lbl] of
 764
 765                 -- No matching field; chances are this field label comes from some
 766                 -- other record type (or maybe none).  As well as reporting an
 767                 -- error we still want to typecheck the pattern, principally to
 768                 -- make sure that all the variables it binds are put into the
 769                 -- environment, else the type checker crashes later:
 770                 --      f (R { foo = (a,b) }) = a+b
 771                 -- If foo isn't one of R's fields, we don't want to crash when
 772                 -- typechecking the "a+b".
 773            [] -> do { addErrTc (badFieldCon data_con field_lbl)
 774                     ; bogus_ty <- newFlexiTyVarTy liftedTypeKind
 775                     ; return (error "Bogus selector Id", bogus_ty) }
 776
 777                 -- The normal case, when the field comes from the right constructor
 778            (pat_ty : extras) ->
 779                 ASSERT( null extras )
 780                 do { sel_id <- tcLookupField field_lbl
 781                    ; return (sel_id, pat_ty) }
 782
 783     field_tys :: [(FieldLabel, TcType)]
 784     field_tys = zip (dataConFieldLabels data_con) arg_tys
 785         -- Don't use zipEqual! If the constructor isn't really a record, then
 786         -- dataConFieldLabels will be empty (and each field in the pattern
 787         -- will generate an error below).
 788
 789 tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id)
 790 tcConArg (arg_pat, arg_ty) pstate thing_inside
 791   = tc_lpat arg_pat arg_ty pstate thing_inside
 792 \end{code}
 793
 794 \begin{code}
 795 addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
 796 -- Instantiate the "stupid theta" of the data con, and throw
 797 -- the constraints into the constraint set
 798 addDataConStupidTheta data_con inst_tys
 799   | null stupid_theta = return ()
 800   | otherwise         = instStupidTheta origin inst_theta
 801   where
 802     origin = OccurrenceOf (dataConName data_con)
 803         -- The origin should always report "occurrence of C"
 804         -- even when C occurs in a pattern
 805     stupid_theta = dataConStupidTheta data_con
 806     tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
 807     inst_theta = substTheta tenv stupid_theta
 808 \end{code}
 809
 810 Note [Arrows and patterns]
 811 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 812 (Oct 07) Arrow noation has the odd property that it involves "holes in the scope".
 813 For example:
 814   expr :: Arrow a => a () Int
 815   expr = proc (y,z) -> do
 816           x <- term -< y
 817           expr' -< x
 818
 819 Here the 'proc (y,z)' binding scopes over the arrow tails but not the
 820 arrow body (e.g 'term').  As things stand (bogusly) all the
 821 constraints from the proc body are gathered together, so constraints
 822 from 'term' will be seen by the tcPat for (y,z).  But we must *not*
 823 bind constraints from 'term' here, becuase the desugarer will not make
 824 these bindings scope over 'term'.
 825
 826 The Right Thing is not to confuse these constraints together. But for
 827 now the Easy Thing is to ensure that we do not have existential or
 828 GADT constraints in a 'proc', and to short-cut the constraint
 829 simplification for such vanilla patterns so that it binds no
 830 constraints. Hence the 'fast path' in tcConPat; but it's also a good
 831 plan for ordinary vanilla patterns to bypass the constraint
 832 simplification step.
 833
 834
 835 %************************************************************************
 836 %*                                                                      *
 837                 Overloaded literals
 838 %*                                                                      *
 839 %************************************************************************
 840
 841 In tcOverloadedLit we convert directly to an Int or Integer if we
 842 know that's what we want.  This may save some time, by not
 843 temporarily generating overloaded literals, but it won't catch all
 844 cases (the rest are caught in lookupInst).
 845
 846 \begin{code}
 847 tcOverloadedLit :: InstOrigin
 848                  -> HsOverLit Name
 849                  -> BoxyRhoType
 850                  -> TcM (HsOverLit TcId)
 851 tcOverloadedLit orig lit@(HsIntegral i fi _) res_ty
 852   | not (fi `isHsVar` fromIntegerName)  -- Do not generate a LitInst for rebindable syntax.
 853         -- Reason: If we do, tcSimplify will call lookupInst, which
 854         --         will call tcSyntaxName, which does unification,
 855         --         which tcSimplify doesn't like
 856         -- ToDo: noLoc sadness
 857   = do  { integer_ty <- tcMetaTy integerTyConName
 858         ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty)
 859         ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty))) res_ty) }
 860
 861   | Just expr <- shortCutIntLit i res_ty
 862   = return (HsIntegral i expr res_ty)
 863
 864   | otherwise
 865   = do  { expr <- newLitInst orig lit res_ty
 866         ; return (HsIntegral i expr res_ty) }
 867
 868 tcOverloadedLit orig lit@(HsFractional r fr _) res_ty
 869   | not (fr `isHsVar` fromRationalName) -- c.f. HsIntegral case
 870   = do  { rat_ty <- tcMetaTy rationalTyConName
 871         ; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty res_ty)
 872                 -- Overloaded literals must have liftedTypeKind, because
 873                 -- we're instantiating an overloaded function here,
 874                 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
 875                 -- However this'll be picked up by tcSyntaxOp if necessary
 876         ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty))) res_ty) }
 877
 878   | Just expr <- shortCutFracLit r res_ty
 879   = return (HsFractional r expr res_ty)
 880
 881   | otherwise
 882   = do  { expr <- newLitInst orig lit res_ty
 883         ; return (HsFractional r expr res_ty) }
 884
 885 tcOverloadedLit orig lit@(HsIsString s fr _) res_ty
 886   | not (fr `isHsVar` fromStringName)   -- c.f. HsIntegral case
 887   = do  { str_ty <- tcMetaTy stringTyConName
 888         ; fr' <- tcSyntaxOp orig fr (mkFunTy str_ty res_ty)
 889         ; return (HsIsString s (HsApp (noLoc fr') (nlHsLit (HsString s))) res_ty) }
 890
 891   | Just expr <- shortCutStringLit s res_ty
 892   = return (HsIsString s expr res_ty)
 893
 894   | otherwise
 895   = do  { expr <- newLitInst orig lit res_ty
 896         ; return (HsIsString s expr res_ty) }
 897
 898 newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
 899 newLitInst orig lit res_ty      -- Make a LitInst
 900   = do  { loc <- getInstLoc orig
 901         ; res_tau <- zapToMonotype res_ty
 902         ; new_uniq <- newUnique
 903         ; let   lit_nm   = mkSystemVarName new_uniq (fsLit "lit")
 904                 lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit,
 905                                     tci_ty = res_tau, tci_loc = loc}
 906         ; extendLIE lit_inst
 907         ; return (HsVar (instToId lit_inst)) }
 908 \end{code}
 909
 910
 911 %************************************************************************
 912 %*                                                                      *
 913                 Note [Pattern coercions]
 914 %*                                                                      *
 915 %************************************************************************
 916
 917 In principle, these program would be reasonable:
 918
 919         f :: (forall a. a->a) -> Int
 920         f (x :: Int->Int) = x 3
 921
 922         g :: (forall a. [a]) -> Bool
 923         g [] = True
 924
 925 In both cases, the function type signature restricts what arguments can be passed
 926 in a call (to polymorphic ones).  The pattern type signature then instantiates this
 927 type.  For example, in the first case,  (forall a. a->a) <= Int -> Int, and we
 928 generate the translated term
 929         f = \x' :: (forall a. a->a).  let x = x' Int in x 3
 930
 931 From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
 932 And it requires a significant amount of code to implement, becuase we need to decorate
 933 the translated pattern with coercion functions (generated from the subsumption check
 934 by tcSub).
 935
 936 So for now I'm just insisting on type *equality* in patterns.  No subsumption.
 937
 938 Old notes about desugaring, at a time when pattern coercions were handled:
 939
 940 A SigPat is a type coercion and must be handled one at at time.  We can't
 941 combine them unless the type of the pattern inside is identical, and we don't
 942 bother to check for that.  For example:
 943
 944         data T = T1 Int | T2 Bool
 945         f :: (forall a. a -> a) -> T -> t
 946         f (g::Int->Int)   (T1 i) = T1 (g i)
 947         f (g::Bool->Bool) (T2 b) = T2 (g b)
 948
 949 We desugar this as follows:
 950
 951         f = \ g::(forall a. a->a) t::T ->
 952             let gi = g Int
 953             in case t of { T1 i -> T1 (gi i)
 954                            other ->
 955             let gb = g Bool
 956             in case t of { T2 b -> T2 (gb b)
 957                            other -> fail }}
 958
 959 Note that we do not treat the first column of patterns as a
 960 column of variables, because the coerced variables (gi, gb)
 961 would be of different types.  So we get rather grotty code.
 962 But I don't think this is a common case, and if it was we could
 963 doubtless improve it.
 964
 965 Meanwhile, the strategy is:
 966         * treat each SigPat coercion (always non-identity coercions)
 967                 as a separate block
 968         * deal with the stuff inside, and then wrap a binding round
 969                 the result to bind the new variable (gi, gb, etc)
 970
 971
 972 %************************************************************************
 973 %*                                                                      *
 974 \subsection{Errors and contexts}
 975 %*                                                                      *
 976 %************************************************************************
 977
 978 \begin{code}
 979 patCtxt :: Pat Name -> Maybe Message    -- Not all patterns are worth pushing a context
 980 patCtxt (VarPat _)  = Nothing
 981 patCtxt (ParPat _)  = Nothing
 982 patCtxt (AsPat _ _) = Nothing
 983 patCtxt pat         = Just (hang (ptext (sLit "In the pattern:"))
 984                                4 (ppr pat))
 985
 986 -----------------------------------------------
 987
 988 existentialExplode pat
 989   = hang (vcat [text "My brain just exploded.",
 990                 text "I can't handle pattern bindings for existentially-quantified constructors.",
 991                 text "Instead, use a case-expression, or do-notation, to unpack the constructor.",
 992                 text "In the binding group for"])
 993         4 (ppr pat)
 994
 995 sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env
 996   = do  { pat_tys' <- mapM zonkTcType pat_tys
 997         ; body_ty' <- zonkTcType body_ty
 998         ; let (env1,  tidy_tys)    = tidyOpenTypes tidy_env (map idType show_ids)
 999               (env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys'
1000               (env3, tidy_body_ty) = tidyOpenType  env2 body_ty'
1001         ; return (env3,
1002                  sep [ptext (sLit "When checking an existential match that binds"),
1003                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
1004                       ptext (sLit "The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
1005                       ptext (sLit "The body has type:") <+> ppr tidy_body_ty
1006                 ]) }
1007   where
1008     bound_ids = collectPatsBinders pats
1009     show_ids = filter is_interesting bound_ids
1010     is_interesting id = any (`elemVarSet` varTypeTyVars id) bound_tvs
1011
1012     ppr_id id ty = ppr id <+> dcolon <+> ppr ty
1013         -- Don't zonk the types so we get the separate, un-unified versions
1014
1015 badFieldCon :: DataCon -> Name -> SDoc
1016 badFieldCon con field
1017   = hsep [ptext (sLit "Constructor") <+> quotes (ppr con),
1018           ptext (sLit "does not have field"), quotes (ppr field)]
1019
1020 polyPatSig :: TcType -> SDoc
1021 polyPatSig sig_ty
1022   = hang (ptext (sLit "Illegal polymorphic type signature in pattern:"))
1023        2 (ppr sig_ty)
1024
1025 badTypePat pat = ptext (sLit "Illegal type pattern") <+> ppr pat
1026
1027 existentialProcPat :: DataCon -> SDoc
1028 existentialProcPat con
1029   = hang (ptext (sLit "Illegal constructor") <+> quotes (ppr con) <+> ptext (sLit "in a 'proc' pattern"))
1030        2 (ptext (sLit "Proc patterns cannot use existentials or GADTs"))
1031
1032 lazyPatErr pat tvs
1033   = failWithTc $
1034     hang (ptext (sLit "A lazy (~) pattern cannot bind existential type variables"))
1035        2 (vcat (map pprSkolTvBinding tvs))
1036
1037 nonRigidMatch con
1038   =  hang (ptext (sLit "GADT pattern match in non-rigid context for") <+> quotes (ppr con))
1039         2 (ptext (sLit "Solution: add a type signature"))
1040
1041 nonRigidResult res_ty
1042   = do  { env0 <- tcInitTidyEnv
1043         ; let (env1, res_ty') = tidyOpenType env0 res_ty
1044               msg = hang (ptext (sLit "GADT pattern match with non-rigid result type")
1045                                 <+> quotes (ppr res_ty'))
1046                          2 (ptext (sLit "Solution: add a type signature"))
1047         ; failWithTcM (env1, msg) }
1048
1049 inaccessibleAlt msg
1050   = hang (ptext (sLit "Inaccessible case alternative:")) 2 msg
1051 \end{code}