ghc/compiler/typecheck/TcPat.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[TcPat]{Typechecking patterns}
   5
   6 \begin{code}
   7 module TcPat ( tcPat, tcPats, PatCtxt(..), badFieldCon, polyPatSig ) where
   8
   9 #include "HsVersions.h"
  10
  11 import HsSyn            ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..),
  12                           HsExpr(..), LHsBinds, emptyLHsBinds, isEmptyLHsBinds )
  13 import HsUtils
  14 import TcHsSyn          ( TcId, hsLitType )
  15 import TcRnMonad
  16 import Inst             ( InstOrigin(..),
  17                           newMethodFromName, newOverloadedLit, newDicts,
  18                           instToId, tcInstStupidTheta, tcSyntaxName
  19                         )
  20 import Id               ( Id, idType, mkLocalId )
  21 import Name             ( Name )
  22 import TcSimplify       ( tcSimplifyCheck, bindInstsOfLocalFuns )
  23 import TcEnv            ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv,
  24                           tcLookupClass, tcLookupDataCon, tcLookupId )
  25 import TcMType          ( newTyFlexiVarTy, arityErr, tcSkolTyVars )
  26 import TcType           ( TcType, TcTyVar, TcSigmaType, TcTauType, zipTopTvSubst,
  27                           SkolemInfo(PatSkol), isSkolemTyVar, pprSkolemTyVar,
  28                           mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy )
  29 import Kind             ( argTypeKind, liftedTypeKind )
  30 import TcUnify          ( tcSubPat, Expected(..), zapExpectedType,
  31                           zapExpectedTo, zapToListTy, zapToTyConApp )
  32 import TcHsType         ( UserTypeCtxt(..), TcSigInfo( sig_tau ), TcSigFun, tcHsPatSigType )
  33 import TysWiredIn       ( stringTy, parrTyCon, tupleTyCon )
  34 import Unify            ( MaybeErr(..), tcRefineTys, tcMatchTys )
  35 import Type             ( substTys, substTheta )
  36 import CmdLineOpts      ( opt_IrrefutableTuples )
  37 import TyCon            ( TyCon )
  38 import DataCon          ( DataCon, dataConTyCon, isVanillaDataCon, dataConInstOrigArgTys,
  39                           dataConFieldLabels, dataConSourceArity, dataConSig )
  40 import PrelNames        ( eqStringName, eqName, geName, negateName, minusName,
  41                           integralClassName )
  42 import BasicTypes       ( isBoxed )
  43 import SrcLoc           ( Located(..), SrcSpan, noLoc, unLoc, getLoc )
  44 import ErrUtils         ( Message )
  45 import Outputable
  46 import FastString
  47 \end{code}
  48
  49
  50 %************************************************************************
  51 %*                                                                      *
  52                 External interface
  53 %*                                                                      *
  54 %************************************************************************
  55
  56 Note [Nesting]
  57
  58 tcPat takes a "thing inside" over which the patter scopes.  This is partly
  59 so that tcPat can extend the environment for the thing_inside, but also
  60 so that constraints arising in the thing_inside can be discharged by the
  61 pattern.
  62
  63 This does not work so well for the ErrCtxt carried by the monad: we don't
  64 want the error-context for the pattern to scope over the RHS.
  65 Hence the getErrCtxt/setErrCtxt stuff in tcPat.
  66
  67 \begin{code}
  68 tcPat   :: PatCtxt
  69         -> LPat Name -> Expected TcSigmaType
  70         -> TcM a                -- Thing inside
  71         -> TcM (LPat TcId,      -- Translated pattern
  72                 [TcTyVar],      -- Existential binders
  73                 a)              -- Result of thing inside
  74
  75 tcPat ctxt pat exp_ty thing_inside
  76   = do  { err_ctxt <- getErrCtxt
  77         ; maybeAddErrCtxt (patCtxt (unLoc pat)) $
  78             tc_lpat ctxt pat exp_ty $
  79               setErrCtxt err_ctxt thing_inside }
  80         -- Restore error context before doing thing_inside
  81         -- See note [Nesting] above
  82
  83 --------------------
  84 tcPats  :: PatCtxt
  85         -> [LPat Name]
  86         -> [Expected TcSigmaType]       -- Excess types discarded
  87         -> TcM a
  88         -> TcM ([LPat TcId], [TcTyVar], a)
  89
  90 tcPats ctxt [] _ thing_inside
  91   = do  { res <- thing_inside
  92         ; return ([], [], res) }
  93
  94 tcPats ctxt (p:ps) (ty:tys) thing_inside
  95   = do  { (p', p_tvs, (ps', ps_tvs, res))
  96                 <- tcPat ctxt p ty $
  97                    tcPats ctxt ps tys thing_inside
  98         ; return (p':ps', p_tvs ++ ps_tvs, res) }
  99
 100 --------------------
 101 tcCheckPats :: PatCtxt
 102             -> [LPat Name] -> [TcSigmaType]
 103             -> TcM a
 104             -> TcM ([LPat TcId], [TcTyVar], a)
 105 tcCheckPats ctxt pats tys thing_inside  -- A trivial wrapper
 106   = tcPats ctxt pats (map Check tys) thing_inside
 107 \end{code}
 108
 109
 110 %************************************************************************
 111 %*                                                                      *
 112                 Binders
 113 %*                                                                      *
 114 %************************************************************************
 115
 116 \begin{code}
 117 data PatCtxt = LamPat Bool      -- Used for lambda, case, do-notation etc
 118              | LetPat TcSigFun  -- Used for let(rec) bindings
 119         -- True <=> we are checking the case expression,
 120         --              so can do full-blown refinement
 121         -- False <=> inferring, do no refinement
 122
 123 -------------------
 124 tcPatBndr :: PatCtxt -> Name -> Expected TcSigmaType -> TcM TcId
 125 tcPatBndr (LamPat _) bndr_name pat_ty
 126   = do  { pat_ty' <- zapExpectedType pat_ty argTypeKind
 127                 -- If pat_ty is Expected, this returns the appropriate
 128                 -- SigmaType.  In Infer mode, we create a fresh type variable.
 129                 -- Note the SigmaType: we can get
 130                 --      data T = MkT (forall a. a->a)
 131                 --      f t = case t of { MkT g -> ... }
 132                 -- Here, the 'g' must get type (forall a. a->a) from the
 133                 -- MkT context
 134         ; return (mkLocalId bndr_name pat_ty') }
 135
 136 tcPatBndr (LetPat lookup_sig) bndr_name pat_ty
 137   | Just sig <- lookup_sig bndr_name
 138   = do  { let mono_ty = sig_tau sig
 139         ; mono_name <- newLocalName bndr_name
 140         ; tcSubPat mono_ty pat_ty
 141         ; return (mkLocalId mono_name mono_ty) }
 142
 143   | otherwise
 144   = do  { mono_name <- newLocalName bndr_name
 145         ; pat_ty' <- zapExpectedType pat_ty argTypeKind
 146         ; return (mkLocalId mono_name pat_ty') }
 147
 148
 149 -------------------
 150 bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId)
 151 bindInstsOfPatId id thing_inside
 152   | not (isOverloadedTy (idType id))
 153   = do { res <- thing_inside; return (res, emptyLHsBinds) }
 154   | otherwise
 155   = do  { (res, lie) <- getLIE thing_inside
 156         ; binds <- bindInstsOfLocalFuns lie [id]
 157         ; return (res, binds) }
 158 \end{code}
 159
 160
 161 %************************************************************************
 162 %*                                                                      *
 163                 tc_pat: the main worker function
 164 %*                                                                      *
 165 %************************************************************************
 166
 167 \begin{code}
 168 tc_lpat :: PatCtxt
 169         -> LPat Name -> Expected TcSigmaType
 170         -> TcM a                -- Thing inside
 171         -> TcM (LPat TcId,      -- Translated pattern
 172                 [TcTyVar],      -- Existential binders
 173                 a)              -- Result of thing inside
 174
 175 tc_lpat ctxt (L span pat) pat_ty thing_inside
 176   = setSrcSpan span $
 177         -- It's OK to keep setting the SrcSpan;
 178         -- it just overwrites the previous value
 179     do  { (pat', tvs, res) <- tc_pat ctxt pat pat_ty thing_inside
 180         ; return (L span pat', tvs, res) }
 181
 182 ---------------------
 183 tc_pat ctxt (VarPat name) pat_ty thing_inside
 184   = do  { id <- tcPatBndr ctxt name pat_ty
 185         ; (res, binds) <- bindInstsOfPatId id $
 186                           tcExtendIdEnv1 name id $
 187                           (traceTc (text "binding" <+> ppr name <+> ppr (idType id))
 188                            >> thing_inside)
 189         ; let pat' | isEmptyLHsBinds binds = VarPat id
 190                    | otherwise             = VarPatOut id binds
 191         ; return (pat', [], res) }
 192
 193 tc_pat ctxt (ParPat pat) pat_ty thing_inside
 194   = do  { (pat', tvs, res) <- tc_lpat ctxt pat pat_ty thing_inside
 195         ; return (ParPat pat', tvs, res) }
 196
 197 -- There's a wrinkle with irrefuatable patterns, namely that we
 198 -- must not propagate type refinement from them.  For example
 199 --      data T a where { T1 :: Int -> T Int; ... }
 200 --      f :: T a -> Int -> a
 201 --      f ~(T1 i) y = y
 202 -- It's obviously not sound to refine a to Int in the right
 203 -- hand side, because the arugment might not match T1 at all!
 204 --
 205 -- Nor should a lazy pattern bind any existential type variables
 206 -- because they won't be in scope when we do the desugaring
 207 tc_pat ctxt lpat@(LazyPat pat) pat_ty thing_inside
 208   = do  { reft <- getTypeRefinement
 209         ; (pat', pat_tvs, res) <- tc_lpat ctxt pat pat_ty $
 210                                   setTypeRefinement reft thing_inside
 211         ; if (null pat_tvs) then return ()
 212           else lazyPatErr lpat pat_tvs
 213         ; return (LazyPat pat', [], res) }
 214
 215 tc_pat ctxt (WildPat _) pat_ty thing_inside
 216   = do  { pat_ty' <- zapExpectedType pat_ty argTypeKind
 217         -- Note argTypeKind, so that
 218         --      f _ = 3
 219         -- is rejected when f applied to an unboxed tuple
 220         -- However, this means that
 221         --      (case g x of _ -> ...)
 222         -- is rejected g returns an unboxed tuple, which is perhpas
 223         -- annoying.  I suppose we could pass the context into tc_pat...
 224         ; res <- thing_inside
 225         ; return (WildPat pat_ty', [], res) }
 226
 227 tc_pat ctxt (AsPat (L nm_loc name) pat) pat_ty thing_inside
 228   = do  { bndr_id <- setSrcSpan nm_loc (tcPatBndr ctxt name pat_ty)
 229         ; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
 230                               tc_lpat ctxt pat (Check (idType bndr_id)) thing_inside
 231             -- NB: if we do inference on:
 232             --          \ (y@(x::forall a. a->a)) = e
 233             -- we'll fail.  The as-pattern infers a monotype for 'y', which then
 234             -- fails to unify with the polymorphic type for 'x'.  This could
 235             -- perhaps be fixed, but only with a bit more work.
 236             --
 237             -- If you fix it, don't forget the bindInstsOfPatIds!
 238         ; return (AsPat (L nm_loc bndr_id) pat', tvs, res) }
 239
 240 tc_pat ctxt (SigPatIn pat sig) pat_ty thing_inside
 241   = do  {       -- See Note [Pattern coercions] below
 242           (sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt sig
 243         ; tcSubPat sig_ty pat_ty
 244         ; (pat', tvs, res) <- tcExtendTyVarEnv sig_tvs $
 245                               tc_lpat ctxt pat (Check sig_ty) thing_inside
 246         ; return (SigPatOut pat' sig_ty, tvs, res) }
 247
 248 tc_pat ctxt pat@(TypePat ty) pat_ty thing_inside
 249   = failWithTc (badTypePat pat)
 250
 251 ------------------------
 252 -- Lists, tuples, arrays
 253 tc_pat ctxt (ListPat pats _) pat_ty thing_inside
 254   = do  { elem_ty <- zapToListTy pat_ty
 255         ; (pats', pats_tvs, res) <- tcCheckPats ctxt pats (repeat elem_ty) thing_inside
 256         ; return (ListPat pats' elem_ty, pats_tvs, res) }
 257
 258 tc_pat ctxt (PArrPat pats _) pat_ty thing_inside
 259   = do  { [elem_ty] <- zapToTyConApp parrTyCon pat_ty
 260         ; (pats', pats_tvs, res) <- tcCheckPats ctxt pats (repeat elem_ty) thing_inside
 261         ; return (PArrPat pats' elem_ty, pats_tvs, res) }
 262
 263 tc_pat ctxt (TuplePat pats boxity) pat_ty thing_inside
 264   = do  { let arity = length pats
 265               tycon = tupleTyCon boxity arity
 266         ; arg_tys <- zapToTyConApp tycon pat_ty
 267         ; (pats', pats_tvs, res) <- tcCheckPats ctxt pats arg_tys thing_inside
 268
 269         -- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
 270         -- so that we can experiment with lazy tuple-matching.
 271         -- This is a pretty odd place to make the switch, but
 272         -- it was easy to do.
 273         ; let unmangled_result = TuplePat pats' boxity
 274               possibly_mangled_result
 275                 | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result)
 276                 | otherwise                               = unmangled_result
 277
 278         ; ASSERT( length arg_tys == arity )     -- Syntactically enforced
 279           return (possibly_mangled_result, pats_tvs, res) }
 280
 281 ------------------------
 282 -- Data constructors
 283 tc_pat ctxt pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
 284   = do  { data_con <- tcLookupDataCon con_name
 285         ; let tycon = dataConTyCon data_con
 286         ; ty_args <- zapToTyConApp tycon pat_ty
 287         ; (pat', tvs, res) <- tcConPat ctxt con_span data_con tycon ty_args arg_pats thing_inside
 288         ; return (pat', tvs, res) }
 289
 290
 291 ------------------------
 292 -- Literal patterns
 293 tc_pat ctxt pat@(LitPat lit@(HsString _)) pat_ty thing_inside
 294   = do  {       -- Strings are mapped to NPatOuts, which have a guard expression
 295           zapExpectedTo pat_ty stringTy
 296         ; eq_id <- tcLookupId eqStringName
 297         ; res <- thing_inside
 298         ; returnM (NPatOut lit stringTy (nlHsVar eq_id `HsApp` nlHsLit lit), [], res) }
 299
 300 tc_pat ctxt (LitPat simple_lit) pat_ty thing_inside
 301   = do  {       -- All other simple lits
 302           zapExpectedTo pat_ty (hsLitType simple_lit)
 303         ; res <- thing_inside
 304         ; returnM (LitPat simple_lit, [], res) }
 305
 306 ------------------------
 307 -- Overloaded patterns: n, and n+k
 308 tc_pat ctxt pat@(NPatIn over_lit mb_neg) pat_ty thing_inside
 309   = do  { pat_ty' <- zapExpectedType pat_ty liftedTypeKind
 310         ; let origin = LiteralOrigin over_lit
 311         ; pos_lit_expr <- newOverloadedLit origin over_lit pat_ty'
 312         ; eq <- newMethodFromName origin pat_ty' eqName
 313         ; lit_expr <- case mb_neg of
 314                         Nothing  -> returnM pos_lit_expr        -- Positive literal
 315                         Just neg ->     -- Negative literal
 316                                         -- The 'negate' is re-mappable syntax
 317                             do { (_, neg_expr) <- tcSyntaxName origin pat_ty'
 318                                                                (negateName, HsVar neg)
 319                                ; returnM (mkHsApp (noLoc neg_expr) pos_lit_expr) }
 320
 321         ; let   -- The literal in an NPatIn is always positive...
 322                 -- But in NPatOut, the literal is used to find identical patterns
 323                 --      so we must negate the literal when necessary!
 324                 lit' = case (over_lit, mb_neg) of
 325                          (HsIntegral i _,   Nothing) -> HsInteger i pat_ty'
 326                          (HsIntegral i _,   Just _)  -> HsInteger (-i) pat_ty'
 327                          (HsFractional f _, Nothing) -> HsRat f pat_ty'
 328                          (HsFractional f _, Just _)  -> HsRat (-f) pat_ty'
 329
 330         ; res <- thing_inside
 331         ; returnM (NPatOut lit' pat_ty' (HsApp (nlHsVar eq) lit_expr), [], res) }
 332
 333 tc_pat ctxt pat@(NPlusKPatIn (L nm_loc name) lit@(HsIntegral i _) minus_name) pat_ty thing_inside
 334   = do  { bndr_id <- setSrcSpan nm_loc (tcPatBndr ctxt name pat_ty)
 335         ; let pat_ty' = idType bndr_id
 336               origin = LiteralOrigin lit
 337         ; over_lit_expr <- newOverloadedLit origin lit pat_ty'
 338         ; ge <- newMethodFromName origin pat_ty' geName
 339
 340         -- The '-' part is re-mappable syntax
 341         ; (_, minus_expr) <- tcSyntaxName origin pat_ty' (minusName, HsVar minus_name)
 342
 343         -- The Report says that n+k patterns must be in Integral
 344         -- We may not want this when using re-mappable syntax, though (ToDo?)
 345         ; icls <- tcLookupClass integralClassName
 346         ; dicts <- newDicts origin [mkClassPred icls [pat_ty']]
 347         ; extendLIEs dicts
 348
 349         ; res <- tcExtendIdEnv1 name bndr_id thing_inside
 350         ; returnM (NPlusKPatOut (L nm_loc bndr_id) i
 351                                 (SectionR (nlHsVar ge) over_lit_expr)
 352                                 (SectionR (noLoc minus_expr) over_lit_expr),
 353                    [], res) }
 354 \end{code}
 355
 356
 357 %************************************************************************
 358 %*                                                                      *
 359         Most of the work for constructors is here
 360         (the rest is in the ConPatIn case of tc_pat)
 361 %*                                                                      *
 362 %************************************************************************
 363
 364 \begin{code}
 365 tcConPat :: PatCtxt -> SrcSpan -> DataCon -> TyCon -> [TcTauType]
 366          -> HsConDetails Name (LPat Name) -> TcM a
 367          -> TcM (Pat TcId, [TcTyVar], a)
 368 tcConPat ctxt span data_con tycon ty_args arg_pats thing_inside
 369   | isVanillaDataCon data_con
 370   = do  { let arg_tys = dataConInstOrigArgTys data_con ty_args
 371         ; tcInstStupidTheta data_con ty_args
 372         ; traceTc (text "tcConPat" <+> vcat [ppr data_con, ppr ty_args, ppr arg_tys])
 373         ; (arg_pats', tvs, res) <- tcConArgs ctxt data_con arg_pats arg_tys thing_inside
 374         ; return (ConPatOut (L span data_con) [] [] emptyLHsBinds
 375                             arg_pats' (mkTyConApp tycon ty_args),
 376                   tvs, res) }
 377
 378   | otherwise   -- GADT case
 379   = do  { let (tvs, theta, arg_tys, _, res_tys) = dataConSig data_con
 380         ; span <- getSrcSpanM
 381         ; let rigid_info = PatSkol data_con span
 382         ; tvs' <- tcSkolTyVars rigid_info tvs
 383         ; let tv_tys'  = mkTyVarTys tvs'
 384               tenv     = zipTopTvSubst tvs tv_tys'
 385               theta'   = substTheta tenv theta
 386               arg_tys' = substTys tenv arg_tys
 387               res_tys' = substTys tenv res_tys
 388         ; dicts <- newDicts (SigOrigin rigid_info) theta'
 389
 390         -- Do type refinement!
 391         ; traceTc (text "tcGadtPat" <+> vcat [ppr data_con, ppr tvs', ppr arg_tys', ppr res_tys',
 392                                               text "ty-args:" <+> ppr ty_args ])
 393         ; refineAlt ctxt data_con tvs' ty_args res_tys' $ do
 394
 395         { ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
 396                 do { tcInstStupidTheta data_con tv_tys'
 397                         -- The stupid-theta mentions the newly-bound tyvars, so
 398                         -- it must live inside the getLIE, so that the
 399                         --  tcSimplifyCheck will apply the type refinement to it
 400                    ; tcConArgs ctxt data_con arg_pats arg_tys' thing_inside }
 401
 402         ; dict_binds <- tcSimplifyCheck doc tvs' dicts lie_req
 403
 404         ; return (ConPatOut (L span data_con)
 405                             tvs' (map instToId dicts) dict_binds
 406                             arg_pats' (mkTyConApp tycon ty_args),
 407                   tvs' ++ inner_tvs, res) } }
 408   where
 409     doc = ptext SLIT("existential context for") <+> quotes (ppr data_con)
 410
 411 tcConArgs :: PatCtxt -> DataCon
 412            -> HsConDetails Name (LPat Name) -> [TcSigmaType]
 413            -> TcM a
 414            -> TcM (HsConDetails TcId (LPat Id), [TcTyVar], a)
 415
 416 tcConArgs ctxt data_con (PrefixCon arg_pats) arg_tys thing_inside
 417   = do  { checkTc (con_arity == no_of_args)     -- Check correct arity
 418                   (arityErr "Constructor" data_con con_arity no_of_args)
 419         ; (arg_pats', tvs, res) <- tcCheckPats ctxt arg_pats arg_tys thing_inside
 420         ; return (PrefixCon arg_pats', tvs, res) }
 421   where
 422     con_arity  = dataConSourceArity data_con
 423     no_of_args = length arg_pats
 424
 425 tcConArgs ctxt data_con (InfixCon p1 p2) arg_tys thing_inside
 426   = do  { checkTc (con_arity == 2)      -- Check correct arity
 427                   (arityErr "Constructor" data_con con_arity 2)
 428         ; ([p1',p2'], tvs, res) <- tcCheckPats ctxt [p1,p2] arg_tys thing_inside
 429         ; return (InfixCon p1' p2', tvs, res) }
 430   where
 431     con_arity  = dataConSourceArity data_con
 432
 433 tcConArgs ctxt data_con (RecCon rpats) arg_tys thing_inside
 434   = do  { (rpats', tvs, res) <- tc_fields rpats thing_inside
 435         ; return (RecCon rpats', tvs, res) }
 436   where
 437     tc_fields :: [(Located Name, LPat Name)] -> TcM a
 438               -> TcM ([(Located TcId, LPat TcId)], [TcTyVar], a)
 439     tc_fields [] thing_inside
 440       = do { res <- thing_inside
 441            ; return ([], [], res) }
 442
 443     tc_fields (rpat : rpats) thing_inside
 444       = do { (rpat', tvs1, (rpats', tvs2, res))
 445                 <- tc_field rpat (tc_fields rpats thing_inside)
 446            ; return (rpat':rpats', tvs1 ++ tvs2, res) }
 447
 448     tc_field (field_lbl, pat) thing_inside
 449       = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
 450            ; (pat', tvs, res) <- tcPat ctxt pat (Check pat_ty) thing_inside
 451            ; return ((sel_id, pat'), tvs, res) }
 452
 453     find_field_ty field_lbl
 454         = case [ty | (f,ty) <- field_tys, f == field_lbl] of
 455
 456                 -- No matching field; chances are this field label comes from some
 457                 -- other record type (or maybe none).  As well as reporting an
 458                 -- error we still want to typecheck the pattern, principally to
 459                 -- make sure that all the variables it binds are put into the
 460                 -- environment, else the type checker crashes later:
 461                 --      f (R { foo = (a,b) }) = a+b
 462                 -- If foo isn't one of R's fields, we don't want to crash when
 463                 -- typechecking the "a+b".
 464            [] -> do { addErrTc (badFieldCon data_con field_lbl)
 465                     ; bogus_ty <- newTyFlexiVarTy liftedTypeKind
 466                     ; return (error "Bogus selector Id", bogus_ty) }
 467
 468                 -- The normal case, when the field comes from the right constructor
 469            (pat_ty : extras) ->
 470                 ASSERT( null extras )
 471                 do { sel_id <- tcLookupId field_lbl
 472                    ; return (sel_id, pat_ty) }
 473
 474     field_tys = zip (dataConFieldLabels data_con) arg_tys
 475         -- Don't use zipEqual! If the constructor isn't really a record, then
 476         -- dataConFieldLabels will be empty (and each field in the pattern
 477         -- will generate an error below).
 478 \end{code}
 479
 480
 481 %************************************************************************
 482 %*                                                                      *
 483                 Type refinement
 484 %*                                                                      *
 485 %************************************************************************
 486
 487 \begin{code}
 488 refineAlt :: PatCtxt -> DataCon
 489             -> [TcTyVar]        -- Freshly bound type variables
 490             -> [TcType]         -- Types from the scrutinee (context)
 491             -> [TcType]         -- Types from the pattern
 492             -> TcM a -> TcM a
 493 refineAlt ctxt con ex_tvs ctxt_tys pat_tys thing_inside
 494   = do  { old_subst <- getTypeRefinement
 495         ; let refiner | can_i_refine ctxt = tcRefineTys
 496                       | otherwise         = tcMatchTys
 497         ; case refiner ex_tvs old_subst pat_tys ctxt_tys of
 498                 Failed msg -> failWithTc (inaccessibleAlt msg)
 499                 Succeeded new_subst -> do {
 500           traceTc (text "refineTypes:match" <+> ppr con <+> ppr new_subst)
 501         ; setTypeRefinement new_subst thing_inside } }
 502
 503   where
 504     can_i_refine (LamPat can_refine) = can_refine
 505     can_i_refine other_ctxt          = False
 506 \end{code}
 507
 508 %************************************************************************
 509 %*                                                                      *
 510                 Note [Pattern coercions]
 511 %*                                                                      *
 512 %************************************************************************
 513
 514 In principle, these program would be reasonable:
 515
 516         f :: (forall a. a->a) -> Int
 517         f (x :: Int->Int) = x 3
 518
 519         g :: (forall a. [a]) -> Bool
 520         g [] = True
 521
 522 In both cases, the function type signature restricts what arguments can be passed
 523 in a call (to polymorphic ones).  The pattern type signature then instantiates this
 524 type.  For example, in the first case,  (forall a. a->a) <= Int -> Int, and we
 525 generate the translated term
 526         f = \x' :: (forall a. a->a).  let x = x' Int in x 3
 527
 528 From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
 529 And it requires a significant amount of code to implement, becuase we need to decorate
 530 the translated pattern with coercion functions (generated from the subsumption check
 531 by tcSub).
 532
 533 So for now I'm just insisting on type *equality* in patterns.  No subsumption.
 534
 535 Old notes about desugaring, at a time when pattern coercions were handled:
 536
 537 A SigPat is a type coercion and must be handled one at at time.  We can't
 538 combine them unless the type of the pattern inside is identical, and we don't
 539 bother to check for that.  For example:
 540
 541         data T = T1 Int | T2 Bool
 542         f :: (forall a. a -> a) -> T -> t
 543         f (g::Int->Int)   (T1 i) = T1 (g i)
 544         f (g::Bool->Bool) (T2 b) = T2 (g b)
 545
 546 We desugar this as follows:
 547
 548         f = \ g::(forall a. a->a) t::T ->
 549             let gi = g Int
 550             in case t of { T1 i -> T1 (gi i)
 551                            other ->
 552             let gb = g Bool
 553             in case t of { T2 b -> T2 (gb b)
 554                            other -> fail }}
 555
 556 Note that we do not treat the first column of patterns as a
 557 column of variables, because the coerced variables (gi, gb)
 558 would be of different types.  So we get rather grotty code.
 559 But I don't think this is a common case, and if it was we could
 560 doubtless improve it.
 561
 562 Meanwhile, the strategy is:
 563         * treat each SigPat coercion (always non-identity coercions)
 564                 as a separate block
 565         * deal with the stuff inside, and then wrap a binding round
 566                 the result to bind the new variable (gi, gb, etc)
 567
 568
 569 %************************************************************************
 570 %*                                                                      *
 571 \subsection{Errors and contexts}
 572 %*                                                                      *
 573 %************************************************************************
 574
 575 \begin{code}
 576 patCtxt :: Pat Name -> Maybe Message    -- Not all patterns are worth pushing a context
 577 patCtxt (VarPat _)  = Nothing
 578 patCtxt (ParPat _)  = Nothing
 579 patCtxt (AsPat _ _) = Nothing
 580 patCtxt pat         = Just (hang (ptext SLIT("When checking the pattern:"))
 581                                4 (ppr pat))
 582
 583 badFieldCon :: DataCon -> Name -> SDoc
 584 badFieldCon con field
 585   = hsep [ptext SLIT("Constructor") <+> quotes (ppr con),
 586           ptext SLIT("does not have field"), quotes (ppr field)]
 587
 588 polyPatSig :: TcType -> SDoc
 589 polyPatSig sig_ty
 590   = hang (ptext SLIT("Illegal polymorphic type signature in pattern:"))
 591          4 (ppr sig_ty)
 592
 593 badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
 594
 595 lazyPatErr pat tvs
 596   = failWithTc $
 597     hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
 598        2 (vcat (map get tvs))
 599   where
 600    get tv = ASSERT( isSkolemTyVar tv ) pprSkolemTyVar tv
 601
 602 inaccessibleAlt msg
 603   = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
 604 \end{code}