compiler/typecheck/TcPat.lhs

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