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