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