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