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