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) <- 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 _ pat@(TypePat _) _ _
 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 (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                         -- pattern coercions have to
 490                         -- be of kind: pat_ty ~ lit_ty
 491                         -- hence, sym coi
 492         ; return (mkCoPatCoI (mkSymCoI coi) (LitPat simple_lit) pat_ty,
 493                    [], res) }
 494
 495 ------------------------
 496 -- Overloaded patterns: n, and n+k
 497 tc_pat pstate (NPat over_lit mb_neg eq) pat_ty thing_inside
 498   = do  { let orig = LiteralOrigin over_lit
 499         ; lit'    <- tcOverloadedLit orig over_lit pat_ty
 500         ; eq'     <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
 501         ; mb_neg' <- case mb_neg of
 502                         Nothing  -> return Nothing      -- Positive literal
 503                         Just neg ->     -- Negative literal
 504                                         -- The 'negate' is re-mappable syntax
 505                             do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
 506                                ; return (Just neg') }
 507         ; res <- thing_inside pstate
 508         ; return (NPat lit' mb_neg' eq', [], res) }
 509
 510 tc_pat pstate (NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
 511   = do  { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
 512         ; let pat_ty' = idType bndr_id
 513               orig    = LiteralOrigin lit
 514         ; lit' <- tcOverloadedLit orig lit pat_ty'
 515
 516         -- The '>=' and '-' parts are re-mappable syntax
 517         ; ge'    <- tcSyntaxOp orig ge    (mkFunTys [pat_ty', pat_ty'] boolTy)
 518         ; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty')
 519
 520         -- The Report says that n+k patterns must be in Integral
 521         -- We may not want this when using re-mappable syntax, though (ToDo?)
 522         ; icls <- tcLookupClass integralClassName
 523         ; instStupidTheta orig [mkClassPred icls [pat_ty']]
 524
 525         ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
 526         ; return (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
 527
 528 tc_pat _ _other_pat _ _ = panic "tc_pat"        -- ConPatOut, SigPatOut, VarPatOut
 529 \end{code}
 530
 531
 532 %************************************************************************
 533 %*                                                                      *
 534         Most of the work for constructors is here
 535         (the rest is in the ConPatIn case of tc_pat)
 536 %*                                                                      *
 537 %************************************************************************
 538
 539 [Pattern matching indexed data types]
 540 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 541 Consider the following declarations:
 542
 543   data family Map k :: * -> *
 544   data instance Map (a, b) v = MapPair (Map a (Pair b v))
 545
 546 and a case expression
 547
 548   case x :: Map (Int, c) w of MapPair m -> ...
 549
 550 As explained by [Wrappers for data instance tycons] in MkIds.lhs, the
 551 worker/wrapper types for MapPair are
 552
 553   $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
 554   $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
 555
 556 So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
 557 :R123Map, which means the straight use of boxySplitTyConApp would give a type
 558 error.  Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
 559 boxySplitTyConApp with the family tycon Map instead, which gives us the family
 560 type list {(Int, c), w}.  To get the correct split for :R123Map, we need to
 561 unify the family type list {(Int, c), w} with the instance types {(a, b), v}
 562 (provided by tyConFamInst_maybe together with the family tycon).  This
 563 unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
 564 the split arguments for the representation tycon :R123Map as {Int, c, w}
 565
 566 In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
 567
 568   Co123Map a b v :: {Map (a, b) v :=: :R123Map a b v}
 569
 570 moving between representation and family type into account.  To produce type
 571 correct Core, this coercion needs to be used to case the type of the scrutinee
 572 from the family to the representation type.  This is achieved by
 573 unwrapFamInstScrutinee using a CoPat around the result pattern.
 574
 575 Now it might appear seem as if we could have used the previous GADT type
 576 refinement infrastructure of refineAlt and friends instead of the explicit
 577 unification and CoPat generation.  However, that would be wrong.  Why?  The
 578 whole point of GADT refinement is that the refinement is local to the case
 579 alternative.  In contrast, the substitution generated by the unification of
 580 the family type list and instance types needs to be propagated to the outside.
 581 Imagine that in the above example, the type of the scrutinee would have been
 582 (Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
 583 substitution [x -> (a, b), v -> w].  In contrast to GADT matching, the
 584 instantiation of x with (a, b) must be global; ie, it must be valid in *all*
 585 alternatives of the case expression, whereas in the GADT case it might vary
 586 between alternatives.
 587
 588 RIP GADT refinement: refinements have been replaced by the use of explicit
 589 equality constraints that are used in conjunction with implication constraints
 590 to express the local scope of GADT refinements.
 591
 592 \begin{code}
 593 --      Running example:
 594 -- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
 595 --       with scrutinee of type (T ty)
 596
 597 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
 598          -> BoxySigmaType       -- Type of the pattern
 599          -> HsConPatDetails Name -> (PatState -> TcM a)
 600          -> TcM (Pat TcId, [TcTyVar], a)
 601 tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
 602   = do  { let (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _)
 603                 = dataConFullSig data_con
 604               skol_info  = PatSkol data_con
 605               origin     = SigOrigin skol_info
 606               full_theta = eq_theta ++ dict_theta
 607
 608           -- Instantiate the constructor type variables [a->ty]
 609           -- This may involve doing a family-instance coercion, and building a
 610           -- wrapper
 611         ; (ctxt_res_tys, coi) <- boxySplitTyConAppWithFamily tycon pat_ty
 612         ; let sym_coi = mkSymCoI coi  -- boxy split coercion oriented wrongly
 613               pat_ty' = mkTyConApp tycon ctxt_res_tys
 614                                       -- pat_ty' /= pat_ty iff coi /= IdCo
 615
 616               wrap_res_pat res_pat = mkCoPatCoI sym_coi uwScrut pat_ty
 617                 where
 618                   uwScrut = unwrapFamInstScrutinee tycon ctxt_res_tys res_pat
 619
 620         ; traceTc $ case sym_coi of
 621                       IdCo -> text "sym_coi:IdCo"
 622                       ACo co -> text "sym_coi: ACoI" <+> ppr co
 623
 624           -- Add the stupid theta
 625         ; addDataConStupidTheta data_con ctxt_res_tys
 626
 627         ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs
 628                      -- Get location from monad, not from ex_tvs
 629
 630         ; let tenv     = zipTopTvSubst (univ_tvs ++ ex_tvs)
 631                                        (ctxt_res_tys ++ mkTyVarTys ex_tvs')
 632               arg_tys' = substTys tenv arg_tys
 633
 634         ; if null ex_tvs && null eq_spec && null full_theta
 635           then do { -- The common case; no class bindings etc
 636                     -- (see Note [Arrows and patterns])
 637                     (arg_pats', inner_tvs, res) <- tcConArgs data_con arg_tys'
 638                                                     arg_pats pstate thing_inside
 639                   ; let res_pat = ConPatOut { pat_con = L con_span data_con,
 640                                               pat_tvs = [], pat_dicts = [],
 641                                               pat_binds = emptyLHsBinds,
 642                                               pat_args = arg_pats',
 643                                               pat_ty = pat_ty' }
 644
 645                     ; return (wrap_res_pat res_pat, inner_tvs, res) }
 646
 647           else do   -- The general case, with existential, and local equality
 648                     -- constraints
 649         { checkTc (case pat_ctxt pstate of { ProcPat -> False; _ -> True })
 650                   (existentialProcPat data_con)
 651
 652           -- Need to test for rigidity if *any* constraints in theta as class
 653           -- constraints may have superclass equality constraints.  However,
 654           -- we don't want to check for rigidity if we got here only because
 655           -- ex_tvs was non-null.
 656 --        ; unless (null theta') $
 657           -- FIXME: AT THE MOMENT WE CHEAT!  We only perform the rigidity test
 658           --   if we explicit or implicit (by a GADT def) have equality
 659           --   constraints.
 660         ; let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec]
 661               theta'   = substTheta tenv (eq_preds ++ full_theta)
 662                            -- order is *important* as we generate the list of
 663                            -- dictionary binders from theta'
 664               no_equalities = not (any isEqPred theta')
 665               pstate' | no_equalities = pstate
 666                       | otherwise     = pstate { pat_eqs = True }
 667
 668         ; unless no_equalities (checkTc (isRigidTy pat_ty)
 669                                         (nonRigidMatch data_con))
 670
 671         ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
 672                 tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
 673
 674         ; loc <- getInstLoc origin
 675         ; dicts <- newDictBndrs loc theta'
 676         ; dict_binds <- tcSimplifyCheckPat loc ex_tvs' dicts lie_req
 677
 678         ; let res_pat = ConPatOut { pat_con = L con_span data_con,
 679                                     pat_tvs = ex_tvs',
 680                                     pat_dicts = map instToVar dicts,
 681                                     pat_binds = dict_binds,
 682                                     pat_args = arg_pats', pat_ty = pat_ty' }
 683         ; return (wrap_res_pat res_pat, ex_tvs' ++ inner_tvs, res)
 684         } }
 685   where
 686     -- Split against the family tycon if the pattern constructor
 687     -- belongs to a family instance tycon.
 688     boxySplitTyConAppWithFamily tycon pat_ty =
 689       traceTc traceMsg >>
 690       case tyConFamInst_maybe tycon of
 691         Nothing                   -> boxySplitTyConApp tycon pat_ty
 692         Just (fam_tycon, instTys) ->
 693           do { (scrutinee_arg_tys, coi) <- boxySplitTyConApp fam_tycon pat_ty
 694              ; (_, freshTvs, subst) <- tcInstTyVars (tyConTyVars tycon)
 695              ; boxyUnifyList (substTys subst instTys) scrutinee_arg_tys
 696              ; return (freshTvs, coi)
 697              }
 698       where
 699         traceMsg = sep [ text "tcConPat:boxySplitTyConAppWithFamily:" <+>
 700                          ppr tycon <+> ppr pat_ty
 701                        , text "  family instance:" <+>
 702                          ppr (tyConFamInst_maybe tycon)
 703                        ]
 704
 705     -- Wraps the pattern (which must be a ConPatOut pattern) in a coercion
 706     -- pattern if the tycon is an instance of a family.
 707     --
 708     unwrapFamInstScrutinee :: TyCon -> [Type] -> Pat Id -> Pat Id
 709     unwrapFamInstScrutinee tycon args pat
 710       | Just co_con <- tyConFamilyCoercion_maybe tycon
 711 --      , not (isNewTyCon tycon)       -- newtypes are explicitly unwrapped by
 712                                      -- the desugarer
 713           -- NB: We can use CoPat directly, rather than mkCoPat, as we know the
 714           --     coercion is not the identity; mkCoPat is inconvenient as it
 715           --     wants a located pattern.
 716       = CoPat (WpCast $ mkTyConApp co_con args)       -- co fam ty to repr ty
 717               (pat {pat_ty = mkTyConApp tycon args})    -- representation type
 718               pat_ty                                    -- family inst type
 719       | otherwise
 720       = pat
 721
 722
 723 tcConArgs :: DataCon -> [TcSigmaType]
 724           -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
 725
 726 tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
 727   = do  { checkTc (con_arity == no_of_args)     -- Check correct arity
 728                   (arityErr "Constructor" data_con con_arity no_of_args)
 729         ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
 730         ; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys
 731                                               pstate thing_inside
 732         ; return (PrefixCon arg_pats', tvs, res) }
 733   where
 734     con_arity  = dataConSourceArity data_con
 735     no_of_args = length arg_pats
 736
 737 tcConArgs data_con arg_tys (InfixCon p1 p2) pstate thing_inside
 738   = do  { checkTc (con_arity == 2)      -- Check correct arity
 739                   (arityErr "Constructor" data_con con_arity 2)
 740         ; let [arg_ty1,arg_ty2] = arg_tys       -- This can't fail after the arity check
 741         ; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
 742                                               pstate thing_inside
 743         ; return (InfixCon p1' p2', tvs, res) }
 744   where
 745     con_arity  = dataConSourceArity data_con
 746
 747 tcConArgs data_con arg_tys (RecCon (HsRecFields rpats dd)) pstate thing_inside
 748   = do  { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
 749         ; return (RecCon (HsRecFields rpats' dd), tvs, res) }
 750   where
 751     tc_field :: Checker (HsRecField FieldLabel (LPat Name)) (HsRecField TcId (LPat TcId))
 752     tc_field (HsRecField field_lbl pat pun) pstate thing_inside
 753       = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
 754            ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
 755            ; return (HsRecField sel_id pat' pun, tvs, res) }
 756
 757     find_field_ty :: FieldLabel -> TcM (Id, TcType)
 758     find_field_ty field_lbl
 759         = case [ty | (f,ty) <- field_tys, f == field_lbl] of
 760
 761                 -- No matching field; chances are this field label comes from some
 762                 -- other record type (or maybe none).  As well as reporting an
 763                 -- error we still want to typecheck the pattern, principally to
 764                 -- make sure that all the variables it binds are put into the
 765                 -- environment, else the type checker crashes later:
 766                 --      f (R { foo = (a,b) }) = a+b
 767                 -- If foo isn't one of R's fields, we don't want to crash when
 768                 -- typechecking the "a+b".
 769            [] -> do { addErrTc (badFieldCon data_con field_lbl)
 770                     ; bogus_ty <- newFlexiTyVarTy liftedTypeKind
 771                     ; return (error "Bogus selector Id", bogus_ty) }
 772
 773                 -- The normal case, when the field comes from the right constructor
 774            (pat_ty : extras) ->
 775                 ASSERT( null extras )
 776                 do { sel_id <- tcLookupField field_lbl
 777                    ; return (sel_id, pat_ty) }
 778
 779     field_tys :: [(FieldLabel, TcType)]
 780     field_tys = zip (dataConFieldLabels data_con) arg_tys
 781         -- Don't use zipEqual! If the constructor isn't really a record, then
 782         -- dataConFieldLabels will be empty (and each field in the pattern
 783         -- will generate an error below).
 784
 785 tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id)
 786 tcConArg (arg_pat, arg_ty) pstate thing_inside
 787   = tc_lpat arg_pat arg_ty pstate thing_inside
 788 \end{code}
 789
 790 \begin{code}
 791 addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
 792 -- Instantiate the "stupid theta" of the data con, and throw
 793 -- the constraints into the constraint set
 794 addDataConStupidTheta data_con inst_tys
 795   | null stupid_theta = return ()
 796   | otherwise         = instStupidTheta origin inst_theta
 797   where
 798     origin = OccurrenceOf (dataConName data_con)
 799         -- The origin should always report "occurrence of C"
 800         -- even when C occurs in a pattern
 801     stupid_theta = dataConStupidTheta data_con
 802     tenv = mkTopTvSubst (dataConUnivTyVars data_con `zip` inst_tys)
 803          -- NB: inst_tys can be longer than the univ tyvars
 804          --     because the constructor might have existentials
 805     inst_theta = substTheta tenv stupid_theta
 806 \end{code}
 807
 808 Note [Arrows and patterns]
 809 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 810 (Oct 07) Arrow noation has the odd property that it involves "holes in the scope".
 811 For example:
 812   expr :: Arrow a => a () Int
 813   expr = proc (y,z) -> do
 814           x <- term -< y
 815           expr' -< x
 816
 817 Here the 'proc (y,z)' binding scopes over the arrow tails but not the
 818 arrow body (e.g 'term').  As things stand (bogusly) all the
 819 constraints from the proc body are gathered together, so constraints
 820 from 'term' will be seen by the tcPat for (y,z).  But we must *not*
 821 bind constraints from 'term' here, becuase the desugarer will not make
 822 these bindings scope over 'term'.
 823
 824 The Right Thing is not to confuse these constraints together. But for
 825 now the Easy Thing is to ensure that we do not have existential or
 826 GADT constraints in a 'proc', and to short-cut the constraint
 827 simplification for such vanilla patterns so that it binds no
 828 constraints. Hence the 'fast path' in tcConPat; but it's also a good
 829 plan for ordinary vanilla patterns to bypass the constraint
 830 simplification step.
 831
 832
 833 %************************************************************************
 834 %*                                                                      *
 835                 Overloaded literals
 836 %*                                                                      *
 837 %************************************************************************
 838
 839 In tcOverloadedLit we convert directly to an Int or Integer if we
 840 know that's what we want.  This may save some time, by not
 841 temporarily generating overloaded literals, but it won't catch all
 842 cases (the rest are caught in lookupInst).
 843
 844 \begin{code}
 845 tcOverloadedLit :: InstOrigin
 846                  -> HsOverLit Name
 847                  -> BoxyRhoType
 848                  -> TcM (HsOverLit TcId)
 849 tcOverloadedLit orig lit@(OverLit { ol_val = val, ol_rebindable = rebindable
 850                                   , ol_witness = meth_name }) res_ty
 851   | rebindable
 852         -- 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  { hs_lit <- mkOverLit val
 858         ; let lit_ty = hsLitType hs_lit
 859         ; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
 860                 -- Overloaded literals must have liftedTypeKind, because
 861                 -- we're instantiating an overloaded function here,
 862                 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
 863                 -- However this'll be picked up by tcSyntaxOp if necessary
 864         ; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
 865         ; return (lit { ol_witness = witness, ol_type = res_ty }) }
 866
 867   | Just expr <- shortCutLit val res_ty
 868   = return (lit { ol_witness = expr, ol_type = res_ty })
 869
 870   | otherwise
 871   = do  { loc <- getInstLoc orig
 872         ; res_tau <- zapToMonotype res_ty
 873         ; new_uniq <- newUnique
 874         ; let   lit_nm   = mkSystemVarName new_uniq (fsLit "lit")
 875                 lit_inst = LitInst {tci_name = lit_nm, tci_lit = lit,
 876                                     tci_ty = res_tau, tci_loc = loc}
 877                 witness = HsVar (instToId lit_inst)
 878         ; extendLIE lit_inst
 879         ; return (lit { ol_witness = witness, ol_type = res_ty }) }
 880 \end{code}
 881
 882
 883 %************************************************************************
 884 %*                                                                      *
 885                 Note [Pattern coercions]
 886 %*                                                                      *
 887 %************************************************************************
 888
 889 In principle, these program would be reasonable:
 890
 891         f :: (forall a. a->a) -> Int
 892         f (x :: Int->Int) = x 3
 893
 894         g :: (forall a. [a]) -> Bool
 895         g [] = True
 896
 897 In both cases, the function type signature restricts what arguments can be passed
 898 in a call (to polymorphic ones).  The pattern type signature then instantiates this
 899 type.  For example, in the first case,  (forall a. a->a) <= Int -> Int, and we
 900 generate the translated term
 901         f = \x' :: (forall a. a->a).  let x = x' Int in x 3
 902
 903 From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
 904 And it requires a significant amount of code to implement, becuase we need to decorate
 905 the translated pattern with coercion functions (generated from the subsumption check
 906 by tcSub).
 907
 908 So for now I'm just insisting on type *equality* in patterns.  No subsumption.
 909
 910 Old notes about desugaring, at a time when pattern coercions were handled:
 911
 912 A SigPat is a type coercion and must be handled one at at time.  We can't
 913 combine them unless the type of the pattern inside is identical, and we don't
 914 bother to check for that.  For example:
 915
 916         data T = T1 Int | T2 Bool
 917         f :: (forall a. a -> a) -> T -> t
 918         f (g::Int->Int)   (T1 i) = T1 (g i)
 919         f (g::Bool->Bool) (T2 b) = T2 (g b)
 920
 921 We desugar this as follows:
 922
 923         f = \ g::(forall a. a->a) t::T ->
 924             let gi = g Int
 925             in case t of { T1 i -> T1 (gi i)
 926                            other ->
 927             let gb = g Bool
 928             in case t of { T2 b -> T2 (gb b)
 929                            other -> fail }}
 930
 931 Note that we do not treat the first column of patterns as a
 932 column of variables, because the coerced variables (gi, gb)
 933 would be of different types.  So we get rather grotty code.
 934 But I don't think this is a common case, and if it was we could
 935 doubtless improve it.
 936
 937 Meanwhile, the strategy is:
 938         * treat each SigPat coercion (always non-identity coercions)
 939                 as a separate block
 940         * deal with the stuff inside, and then wrap a binding round
 941                 the result to bind the new variable (gi, gb, etc)
 942
 943
 944 %************************************************************************
 945 %*                                                                      *
 946 \subsection{Errors and contexts}
 947 %*                                                                      *
 948 %************************************************************************
 949
 950 \begin{code}
 951 patCtxt :: Pat Name -> Maybe Message    -- Not all patterns are worth pushing a context
 952 patCtxt (VarPat _)  = Nothing
 953 patCtxt (ParPat _)  = Nothing
 954 patCtxt (AsPat _ _) = Nothing
 955 patCtxt pat         = Just (hang (ptext (sLit "In the pattern:"))
 956                                4 (ppr pat))
 957
 958 -----------------------------------------------
 959
 960 existentialExplode :: LPat Name -> SDoc
 961 existentialExplode pat
 962   = hang (vcat [text "My brain just exploded.",
 963                 text "I can't handle pattern bindings for existentially-quantified constructors.",
 964                 text "Instead, use a case-expression, or do-notation, to unpack the constructor.",
 965                 text "In the binding group for"])
 966         4 (ppr pat)
 967
 968 sigPatCtxt :: [LPat Var] -> [Var] -> [TcType] -> TcType -> TidyEnv
 969            -> TcM (TidyEnv, SDoc)
 970 sigPatCtxt pats bound_tvs pat_tys body_ty tidy_env
 971   = do  { pat_tys' <- mapM zonkTcType pat_tys
 972         ; body_ty' <- zonkTcType body_ty
 973         ; let (env1,  tidy_tys)    = tidyOpenTypes tidy_env (map idType show_ids)
 974               (env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys'
 975               (env3, tidy_body_ty) = tidyOpenType  env2 body_ty'
 976         ; return (env3,
 977                  sep [ptext (sLit "When checking an existential match that binds"),
 978                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
 979                       ptext (sLit "The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
 980                       ptext (sLit "The body has type:") <+> ppr tidy_body_ty
 981                 ]) }
 982   where
 983     bound_ids = collectPatsBinders pats
 984     show_ids = filter is_interesting bound_ids
 985     is_interesting id = any (`elemVarSet` varTypeTyVars id) bound_tvs
 986
 987     ppr_id id ty = ppr id <+> dcolon <+> ppr ty
 988         -- Don't zonk the types so we get the separate, un-unified versions
 989
 990 badFieldCon :: DataCon -> Name -> SDoc
 991 badFieldCon con field
 992   = hsep [ptext (sLit "Constructor") <+> quotes (ppr con),
 993           ptext (sLit "does not have field"), quotes (ppr field)]
 994
 995 polyPatSig :: TcType -> SDoc
 996 polyPatSig sig_ty
 997   = hang (ptext (sLit "Illegal polymorphic type signature in pattern:"))
 998        2 (ppr sig_ty)
 999
1000 badTypePat :: Pat Name -> SDoc
1001 badTypePat pat = ptext (sLit "Illegal type pattern") <+> ppr pat
1002
1003 existentialProcPat :: DataCon -> SDoc
1004 existentialProcPat con
1005   = hang (ptext (sLit "Illegal constructor") <+> quotes (ppr con) <+> ptext (sLit "in a 'proc' pattern"))
1006        2 (ptext (sLit "Proc patterns cannot use existentials or GADTs"))
1007
1008 lazyPatErr :: Pat name -> [TcTyVar] -> TcM ()
1009 lazyPatErr _ tvs
1010   = failWithTc $
1011     hang (ptext (sLit "A lazy (~) pattern cannot bind existential type variables"))
1012        2 (vcat (map pprSkolTvBinding tvs))
1013
1014 nonRigidMatch :: DataCon -> SDoc
1015 nonRigidMatch con
1016   =  hang (ptext (sLit "GADT pattern match in non-rigid context for") <+> quotes (ppr con))
1017         2 (ptext (sLit "Solution: add a type signature"))
1018
1019 nonRigidResult :: Type -> TcM a
1020 nonRigidResult res_ty
1021   = do  { env0 <- tcInitTidyEnv
1022         ; let (env1, res_ty') = tidyOpenType env0 res_ty
1023               msg = hang (ptext (sLit "GADT pattern match with non-rigid result type")
1024                                 <+> quotes (ppr res_ty'))
1025                          2 (ptext (sLit "Solution: add a type signature"))
1026         ; failWithTcM (env1, msg) }
1027 \end{code}