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