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