compiler/typecheck/TcPat.lhs

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