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, tcOverloadedLit,
   8                PatCtxt(..), badFieldCon, polyPatSig ) where
   9
  10 #include "HsVersions.h"
  11
  12 import {-# SOURCE #-}   TcExpr( tcSyntaxOp )
  13 import HsSyn            ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), HsExpr(..),
  14                           LHsBinds, emptyLHsBinds, isEmptyLHsBinds,
  15                           collectPatsBinders, nlHsLit )
  16 import TcHsSyn          ( TcId, hsLitType )
  17 import TcRnMonad
  18 import Inst             ( InstOrigin(..), shortCutFracLit, shortCutIntLit,
  19                           newDicts, instToId, tcInstStupidTheta, isHsVar
  20                         )
  21 import Id               ( Id, idType, mkLocalId )
  22 import CoreFVs          ( idFreeTyVars )
  23 import Name             ( Name, mkSystemVarName )
  24 import TcSimplify       ( tcSimplifyCheck, bindInstsOfLocalFuns )
  25 import TcEnv            ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
  26                           tcLookupClass, tcLookupDataCon, tcLookupId, refineEnvironment,
  27                           tcMetaTy )
  28 import TcMType          ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars, newBoxyTyVar, zonkTcType )
  29 import TcType           ( TcType, TcTyVar, TcSigmaType, TcRhoType, BoxyType,
  30                           SkolemInfo(PatSkol),
  31                           BoxySigmaType, BoxyRhoType, argTypeKind, typeKind,
  32                           pprSkolTvBinding, isRefineableTy, isRigidTy, tcTyVarsOfTypes, mkTyVarTy, lookupTyVar,
  33                           emptyTvSubst, substTyVar, substTy, mkTopTvSubst, zipTopTvSubst, zipOpenTvSubst,
  34                           mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy, isArgTypeKind, isUnboxedTupleType,
  35                           mkFunTy, mkFunTys, exactTyVarsOfTypes, tidyOpenType, tidyOpenTypes )
  36 import VarSet           ( elemVarSet, mkVarSet )
  37 import Kind             ( liftedTypeKind, openTypeKind )
  38 import TcUnify          ( boxySplitTyConApp, boxySplitListTy, unifyType,
  39                           unBox, stripBoxyType, zapToMonotype,
  40                           boxyMatchTypes, boxyUnify, boxyUnifyList, checkSigTyVarsWrt )
  41 import TcHsType         ( UserTypeCtxt(..), tcPatSig )
  42 import TysWiredIn       ( boolTy, parrTyCon, tupleTyCon )
  43 import Unify            ( MaybeErr(..), gadtRefineTys )
  44 import Type             ( substTys, substTheta )
  45 import StaticFlags      ( opt_IrrefutableTuples )
  46 import TyCon            ( TyCon )
  47 import DataCon          ( DataCon, dataConTyCon, isVanillaDataCon,
  48                           dataConFieldLabels, dataConSourceArity, dataConSig )
  49 import PrelNames        ( integralClassName, fromIntegerName, integerTyConName,
  50                           fromRationalName, rationalTyConName )
  51 import BasicTypes       ( isBoxed )
  52 import SrcLoc           ( Located(..), SrcSpan, noLoc )
  53 import ErrUtils         ( Message )
  54 import Util             ( takeList, zipEqual )
  55 import Outputable
  56 import FastString
  57 \end{code}
  58
  59
  60 %************************************************************************
  61 %*                                                                      *
  62                 External interface
  63 %*                                                                      *
  64 %************************************************************************
  65
  66 \begin{code}
  67 tcPats  :: PatCtxt
  68         -> [LPat Name]                  -- Patterns,
  69         -> [BoxySigmaType]              --   and their types
  70         -> BoxyRhoType                  -- Result type,
  71         -> (BoxyRhoType -> TcM a)       --   and the checker for the body
  72         -> TcM ([LPat TcId], a)
  73
  74 -- This is the externally-callable wrapper function
  75 -- Typecheck the patterns, extend the environment to bind the variables,
  76 -- do the thing inside, use any existentially-bound dictionaries to
  77 -- discharge parts of the returning LIE, and deal with pattern type
  78 -- signatures
  79
  80 --   1. Initialise the PatState
  81 --   2. Check the patterns
  82 --   3. Apply the refinement
  83 --   4. Check the body
  84 --   5. Check that no existentials escape
  85
  86 tcPats ctxt pats tys res_ty thing_inside
  87   =  do { let init_state = PS { pat_ctxt = ctxt, pat_reft = emptyTvSubst }
  88
  89         ; (pats', ex_tvs, res) <- tc_lpats init_state pats tys $ \ pstate' ->
  90                                   refineEnvironment (pat_reft pstate') $
  91                                   thing_inside (refineType (pat_reft pstate') res_ty)
  92
  93         ; tcCheckExistentialPat ctxt pats' ex_tvs tys res_ty
  94
  95         ; returnM (pats', res) }
  96
  97
  98 -----------------
  99 tcPat :: PatCtxt
 100       -> LPat Name -> BoxySigmaType
 101       -> BoxyRhoType            -- Result type
 102       -> (BoxyRhoType -> TcM a) -- Checker for body, given its result type
 103       -> TcM (LPat TcId, a)
 104 tcPat ctxt pat pat_ty res_ty thing_inside
 105   = do  { ([pat'],thing) <- tcPats ctxt [pat] [pat_ty] res_ty thing_inside
 106         ; return (pat', thing) }
 107
 108
 109 -----------------
 110 tcCheckExistentialPat :: PatCtxt
 111                       -> [LPat TcId]            -- Patterns (just for error message)
 112                       -> [TcTyVar]              -- Existentially quantified tyvars bound by pattern
 113                       -> [BoxySigmaType]        -- Types of the patterns
 114                       -> BoxyRhoType            -- Type of the body of the match
 115                                                 -- Tyvars in either of these must not escape
 116                       -> TcM ()
 117 -- NB: we *must* pass "pats_tys" not just "body_ty" to tcCheckExistentialPat
 118 -- For example, we must reject this program:
 119 --      data C = forall a. C (a -> Int)
 120 --      f (C g) x = g x
 121 -- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).
 122
 123 tcCheckExistentialPat ctxt pats [] pat_tys body_ty
 124   = return ()   -- Short cut for case when there are no existentials
 125
 126 tcCheckExistentialPat (LetPat _) pats ex_tvs pat_tys body_ty
 127         -- Don't know how to deal with pattern-bound existentials yet
 128   = failWithTc (existentialExplode pats)
 129
 130 tcCheckExistentialPat ctxt pats ex_tvs pat_tys body_ty
 131   = addErrCtxtM (sigPatCtxt (collectPatsBinders pats) ex_tvs pat_tys body_ty)   $
 132     checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
 133
 134 data PatState = PS {
 135         pat_ctxt :: PatCtxt,
 136         pat_reft :: GadtRefinement      -- Binds rigid TcTyVars to their refinements
 137   }
 138
 139 data PatCtxt
 140   = LamPat
 141   | LetPat (Name -> Maybe TcRhoType)    -- Used for let(rec) bindings
 142
 143 patSigCtxt :: PatState -> UserTypeCtxt
 144 patSigCtxt (PS { pat_ctxt = LetPat _ }) = BindPatSigCtxt
 145 patSigCtxt other                        = LamPatSigCtxt
 146 \end{code}
 147
 148
 149
 150 %************************************************************************
 151 %*                                                                      *
 152                 Binders
 153 %*                                                                      *
 154 %************************************************************************
 155
 156 \begin{code}
 157 tcPatBndr :: PatState -> Name -> BoxySigmaType -> TcM TcId
 158 tcPatBndr (PS { pat_ctxt = LamPat }) bndr_name pat_ty
 159   = do  { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
 160                 -- We have an undecorated binder, so we do rule ABS1,
 161                 -- by unboxing the boxy type, forcing any un-filled-in
 162                 -- boxes to become monotypes
 163                 -- NB that pat_ty' can still be a polytype:
 164                 --      data T = MkT (forall a. a->a)
 165                 --      f t = case t of { MkT g -> ... }
 166                 -- Here, the 'g' must get type (forall a. a->a) from the
 167                 -- MkT context
 168         ; return (mkLocalId bndr_name pat_ty') }
 169
 170 tcPatBndr (PS { pat_ctxt = LetPat lookup_sig }) bndr_name pat_ty
 171   | Just mono_ty <- lookup_sig bndr_name
 172   = do  { mono_name <- newLocalName bndr_name
 173         ; boxyUnify mono_ty pat_ty
 174         ; return (mkLocalId mono_name mono_ty) }
 175
 176   | otherwise
 177   = do  { pat_ty' <- unBoxPatBndrType pat_ty bndr_name
 178         ; mono_name <- newLocalName bndr_name
 179         ; return (mkLocalId mono_name pat_ty') }
 180
 181
 182 -------------------
 183 bindInstsOfPatId :: TcId -> TcM a -> TcM (a, LHsBinds TcId)
 184 bindInstsOfPatId id thing_inside
 185   | not (isOverloadedTy (idType id))
 186   = do { res <- thing_inside; return (res, emptyLHsBinds) }
 187   | otherwise
 188   = do  { (res, lie) <- getLIE thing_inside
 189         ; binds <- bindInstsOfLocalFuns lie [id]
 190         ; return (res, binds) }
 191
 192 -------------------
 193 unBoxPatBndrType  ty name = unBoxArgType ty (ptext SLIT("The variable") <+> quotes (ppr name))
 194 unBoxWildCardType ty      = unBoxArgType ty (ptext SLIT("A wild-card pattern"))
 195
 196 unBoxArgType :: BoxyType -> SDoc -> TcM TcType
 197 -- In addition to calling unbox, unBoxArgType ensures that the type is of ArgTypeKind;
 198 -- that is, it can't be an unboxed tuple.  For example,
 199 --      case (f x) of r -> ...
 200 -- should fail if 'f' returns an unboxed tuple.
 201 unBoxArgType ty pp_this
 202   = do  { ty' <- unBox ty       -- Returns a zonked type
 203
 204         -- Neither conditional is strictly necesssary (the unify alone will do)
 205         -- but they improve error messages, and allocate fewer tyvars
 206         ; if isUnboxedTupleType ty' then
 207                 failWithTc msg
 208           else if isArgTypeKind (typeKind ty') then
 209                 return ty'
 210           else do       -- OpenTypeKind, so constrain it
 211         { ty2 <- newFlexiTyVarTy argTypeKind
 212         ; unifyType ty' ty2
 213         ; return ty' }}
 214   where
 215     msg = pp_this <+> ptext SLIT("cannot be bound to an unboxed tuple")
 216 \end{code}
 217
 218
 219 %************************************************************************
 220 %*                                                                      *
 221                 The main worker functions
 222 %*                                                                      *
 223 %************************************************************************
 224
 225 Note [Nesting]
 226 ~~~~~~~~~~~~~~
 227 tcPat takes a "thing inside" over which the patter scopes.  This is partly
 228 so that tcPat can extend the environment for the thing_inside, but also
 229 so that constraints arising in the thing_inside can be discharged by the
 230 pattern.
 231
 232 This does not work so well for the ErrCtxt carried by the monad: we don't
 233 want the error-context for the pattern to scope over the RHS.
 234 Hence the getErrCtxt/setErrCtxt stuff in tc_lpats.
 235
 236 \begin{code}
 237 --------------------
 238 tc_lpats :: PatState
 239          -> [LPat Name]
 240          -> [BoxySigmaType]
 241          -> (PatState -> TcM a)
 242          -> TcM ([LPat TcId], [TcTyVar], a)
 243
 244 tc_lpats pstate pats pat_tys thing_inside
 245   = do  { err_ctxt <- getErrCtxt
 246         ; let loop pstate [] []
 247                 = do { res <- thing_inside pstate
 248                      ; return ([], [], res) }
 249
 250               loop pstate (p:ps) (ty:tys)
 251                 = do { (p', p_tvs, (ps', ps_tvs, res))
 252                                 <- tc_lpat pstate p ty $ \ pstate' ->
 253                                    setErrCtxt err_ctxt $
 254                                    loop pstate' ps tys
 255                 -- setErrCtxt: restore context before doing the next pattern
 256                 -- See note [Nesting] above
 257
 258                      ; return (p':ps', p_tvs ++ ps_tvs, res) }
 259
 260               loop _ _ _ = pprPanic "tc_lpats" (ppr pats $$ ppr pat_tys)
 261
 262         ; loop pstate pats pat_tys }
 263
 264 --------------------
 265 tc_lpat :: PatState
 266          -> LPat Name
 267          -> BoxySigmaType
 268          -> (PatState -> TcM a)
 269          -> TcM (LPat TcId, [TcTyVar], a)
 270 tc_lpat pstate (L span pat) pat_ty thing_inside
 271   = setSrcSpan span               $
 272     maybeAddErrCtxt (patCtxt pat) $
 273     do  { let pat_ty' = refineType (pat_reft pstate) pat_ty
 274                 -- Make sure the result type reflects the current refinement
 275         ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
 276         ; return (L span pat', tvs, res) }
 277
 278
 279 --------------------
 280 tc_pat  :: PatState
 281         -> Pat Name -> BoxySigmaType    -- Fully refined result type
 282         -> (PatState -> TcM a)  -- Thing inside
 283         -> TcM (Pat TcId,       -- Translated pattern
 284                 [TcTyVar],      -- Existential binders
 285                 a)              -- Result of thing inside
 286
 287 tc_pat pstate (VarPat name) pat_ty thing_inside
 288   = do  { id <- tcPatBndr pstate name pat_ty
 289         ; (res, binds) <- bindInstsOfPatId id $
 290                           tcExtendIdEnv1 name id $
 291                           (traceTc (text "binding" <+> ppr name <+> ppr (idType id))
 292                            >> thing_inside pstate)
 293         ; let pat' | isEmptyLHsBinds binds = VarPat id
 294                    | otherwise             = VarPatOut id binds
 295         ; return (pat', [], res) }
 296
 297 tc_pat pstate (ParPat pat) pat_ty thing_inside
 298   = do  { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
 299         ; return (ParPat pat', tvs, res) }
 300
 301 tc_pat pstate (BangPat pat) pat_ty thing_inside
 302   = do  { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
 303         ; return (BangPat pat', tvs, res) }
 304
 305 -- There's a wrinkle with irrefutable patterns, namely that we
 306 -- must not propagate type refinement from them.  For example
 307 --      data T a where { T1 :: Int -> T Int; ... }
 308 --      f :: T a -> Int -> a
 309 --      f ~(T1 i) y = y
 310 -- It's obviously not sound to refine a to Int in the right
 311 -- hand side, because the arugment might not match T1 at all!
 312 --
 313 -- Nor should a lazy pattern bind any existential type variables
 314 -- because they won't be in scope when we do the desugaring
 315 tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
 316   = do  { (pat', pat_tvs, res) <- tc_lpat pstate pat pat_ty $ \ _ ->
 317                                   thing_inside pstate
 318                                         -- Ignore refined pstate',
 319                                         -- revert to pstate
 320         -- Check no existentials
 321         ; if (null pat_tvs) then return ()
 322           else lazyPatErr lpat pat_tvs
 323
 324         -- Check that the pattern has a lifted type
 325         ; pat_tv <- newBoxyTyVar liftedTypeKind
 326         ; boxyUnify pat_ty (mkTyVarTy pat_tv)
 327
 328         ; return (LazyPat pat', [], res) }
 329
 330 tc_pat pstate (WildPat _) pat_ty thing_inside
 331   = do  { pat_ty' <- unBoxWildCardType pat_ty   -- Make sure it's filled in with monotypes
 332         ; res <- thing_inside pstate
 333         ; return (WildPat pat_ty', [], res) }
 334
 335 tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
 336   = do  { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
 337         ; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
 338                               tc_lpat pstate pat (idType bndr_id) thing_inside
 339             -- NB: if we do inference on:
 340             --          \ (y@(x::forall a. a->a)) = e
 341             -- we'll fail.  The as-pattern infers a monotype for 'y', which then
 342             -- fails to unify with the polymorphic type for 'x'.  This could
 343             -- perhaps be fixed, but only with a bit more work.
 344             --
 345             -- If you fix it, don't forget the bindInstsOfPatIds!
 346         ; return (AsPat (L nm_loc bndr_id) pat', tvs, res) }
 347
 348 -- Type signatures in patterns
 349 -- See Note [Pattern coercions] below
 350 tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
 351   = do  { (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
 352         ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
 353                               tc_lpat pstate pat inner_ty thing_inside
 354         ; return (SigPatOut pat' inner_ty, tvs, res) }
 355
 356 tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
 357   = failWithTc (badTypePat pat)
 358
 359 ------------------------
 360 -- Lists, tuples, arrays
 361 tc_pat pstate (ListPat pats _) pat_ty thing_inside
 362   = do  { elt_ty <- boxySplitListTy pat_ty
 363         ; let elt_tys = takeList pats (repeat elt_ty)
 364         ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys thing_inside
 365         ; return (ListPat pats' elt_ty, pats_tvs, res) }
 366
 367 tc_pat pstate (PArrPat pats _) pat_ty thing_inside
 368   = do  { [elt_ty] <- boxySplitTyConApp parrTyCon pat_ty
 369         ; let elt_tys = takeList pats (repeat elt_ty)
 370         ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys thing_inside
 371         ; ifM (null pats) (zapToMonotype pat_ty)        -- c.f. ExplicitPArr in TcExpr
 372         ; return (PArrPat pats' elt_ty, pats_tvs, res) }
 373
 374 tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
 375   = do  { arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty
 376         ; (pats', pats_tvs, res) <- tc_lpats pstate pats arg_tys thing_inside
 377
 378         -- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
 379         -- so that we can experiment with lazy tuple-matching.
 380         -- This is a pretty odd place to make the switch, but
 381         -- it was easy to do.
 382         ; let unmangled_result = TuplePat pats' boxity pat_ty
 383               possibly_mangled_result
 384                 | opt_IrrefutableTuples && isBoxed boxity = LazyPat (noLoc unmangled_result)
 385                 | otherwise                               = unmangled_result
 386
 387         ; ASSERT( length arg_tys == length pats )       -- Syntactically enforced
 388           return (possibly_mangled_result, pats_tvs, res) }
 389
 390 ------------------------
 391 -- Data constructors
 392 tc_pat pstate pat_in@(ConPatIn (L con_span con_name) arg_pats) pat_ty thing_inside
 393   = do  { data_con <- tcLookupDataCon con_name
 394         ; let tycon = dataConTyCon data_con
 395         ; tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside }
 396
 397 ------------------------
 398 -- Literal patterns
 399 tc_pat pstate (LitPat simple_lit) pat_ty thing_inside
 400   = do  { boxyUnify (hsLitType simple_lit) pat_ty
 401         ; res <- thing_inside pstate
 402         ; returnM (LitPat simple_lit, [], res) }
 403
 404 ------------------------
 405 -- Overloaded patterns: n, and n+k
 406 tc_pat pstate pat@(NPat over_lit mb_neg eq _) pat_ty thing_inside
 407   = do  { let orig = LiteralOrigin over_lit
 408         ; lit'    <- tcOverloadedLit orig over_lit pat_ty
 409         ; eq'     <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy)
 410         ; mb_neg' <- case mb_neg of
 411                         Nothing  -> return Nothing      -- Positive literal
 412                         Just neg ->     -- Negative literal
 413                                         -- The 'negate' is re-mappable syntax
 414                             do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty)
 415                                ; return (Just neg') }
 416         ; res <- thing_inside pstate
 417         ; returnM (NPat lit' mb_neg' eq' pat_ty, [], res) }
 418
 419 tc_pat pstate pat@(NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
 420   = do  { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
 421         ; let pat_ty' = idType bndr_id
 422               orig    = LiteralOrigin lit
 423         ; lit' <- tcOverloadedLit orig lit pat_ty'
 424
 425         -- The '>=' and '-' parts are re-mappable syntax
 426         ; ge'    <- tcSyntaxOp orig ge    (mkFunTys [pat_ty', pat_ty'] boolTy)
 427         ; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty')
 428
 429         -- The Report says that n+k patterns must be in Integral
 430         -- We may not want this when using re-mappable syntax, though (ToDo?)
 431         ; icls <- tcLookupClass integralClassName
 432         ; dicts <- newDicts orig [mkClassPred icls [pat_ty']]
 433         ; extendLIEs dicts
 434
 435         ; res <- tcExtendIdEnv1 name bndr_id (thing_inside pstate)
 436         ; returnM (NPlusKPat (L nm_loc bndr_id) lit' ge' minus', [], res) }
 437
 438 tc_pat _ _other_pat _ _ = panic "tc_pat"        -- DictPat, ConPatOut, SigPatOut, VarPatOut
 439 \end{code}
 440
 441
 442 %************************************************************************
 443 %*                                                                      *
 444         Most of the work for constructors is here
 445         (the rest is in the ConPatIn case of tc_pat)
 446 %*                                                                      *
 447 %************************************************************************
 448
 449 \begin{code}
 450 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon
 451          -> BoxySigmaType       -- Type of the pattern
 452          -> HsConDetails Name (LPat Name) -> (PatState -> TcM a)
 453          -> TcM (Pat TcId, [TcTyVar], a)
 454 tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
 455   | isVanillaDataCon data_con
 456   = do  { ty_args <- boxySplitTyConApp tycon pat_ty
 457         ; let (tvs, _, arg_tys, _, _) = dataConSig data_con
 458               arg_tvs  = exactTyVarsOfTypes arg_tys
 459                 -- See Note [Silly type synonyms in smart-app] in TcExpr
 460                 -- for why we must use exactTyVarsOfTypes
 461               inst_prs = zipEqual "tcConPat" tvs ty_args
 462               subst    = mkTopTvSubst inst_prs
 463               arg_tys' = substTys subst arg_tys
 464               unconstrained_ty_args = [ty_arg | (tv,ty_arg) <- inst_prs,
 465                                                 not (tv `elemVarSet` arg_tvs)]
 466         ; mapM unBox unconstrained_ty_args      -- Zap these to monotypes
 467         ; tcInstStupidTheta data_con ty_args
 468         ; traceTc (text "tcConPat" <+> vcat [ppr data_con, ppr ty_args, ppr arg_tys'])
 469         ; (arg_pats', tvs, res) <- tcConArgs pstate data_con arg_pats arg_tys' thing_inside
 470         ; return (ConPatOut (L con_span data_con) [] [] emptyLHsBinds
 471                             arg_pats' (mkTyConApp tycon ty_args),
 472                   tvs, res) }
 473
 474   | otherwise   -- GADT case
 475   = do  { ty_args <- boxySplitTyConApp tycon pat_ty
 476         ; span <- getSrcSpanM   -- The whole pattern
 477
 478         -- Instantiate the constructor type variables and result type
 479         ; let (tvs, theta, arg_tys, _, res_tys) = dataConSig data_con
 480               arg_tvs = exactTyVarsOfTypes arg_tys
 481                 -- See Note [Silly type synonyms in smart-app] in TcExpr
 482                 -- for why we must use exactTyVarsOfTypes
 483               skol_info = PatSkol data_con span
 484               arg_flags = [ tv `elemVarSet` arg_tvs | tv <- tvs ]
 485         ; tvs' <- tcInstSkolTyVars skol_info tvs
 486         ; let res_tys' = substTys (zipTopTvSubst tvs (mkTyVarTys tvs')) res_tys
 487
 488         -- Do type refinement!
 489         ; traceTc (text "tcGadtPat" <+> vcat [ppr data_con, ppr tvs', ppr res_tys',
 490                                               text "ty-args:" <+> ppr ty_args ])
 491         ; refineAlt pstate data_con tvs' arg_flags res_tys' ty_args
 492                         $ \ pstate' tv_tys' -> do
 493
 494         -- ToDo: arg_tys should be boxy, but I don't think theta' should be,
 495         --       or the tv_tys' in the call to tcInstStupidTheta
 496         { let tenv'    = zipTopTvSubst tvs tv_tys'
 497               theta'   = substTheta tenv' theta
 498               arg_tys' = substTys   tenv' arg_tys       -- Boxy types
 499
 500         ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
 501                 do { tcInstStupidTheta data_con tv_tys'
 502                         -- The stupid-theta mentions the newly-bound tyvars, so
 503                         -- it must live inside the getLIE, so that the
 504                         -- tcSimplifyCheck will apply the type refinement to it
 505                    ; tcConArgs pstate' data_con arg_pats arg_tys' thing_inside }
 506
 507         ; dicts <- newDicts (SigOrigin skol_info) theta'
 508         ; dict_binds <- tcSimplifyCheck doc tvs' dicts lie_req
 509
 510         ; return (ConPatOut (L con_span data_con)
 511                             tvs' (map instToId dicts) dict_binds
 512                             arg_pats' (mkTyConApp tycon ty_args),
 513                   tvs' ++ inner_tvs, res)
 514         } }
 515   where
 516     doc = ptext SLIT("existential context for") <+> quotes (ppr data_con)
 517
 518 tcConArgs :: PatState -> DataCon
 519            -> HsConDetails Name (LPat Name) -> [TcSigmaType]
 520            -> (PatState -> TcM a)
 521            -> TcM (HsConDetails TcId (LPat Id), [TcTyVar], a)
 522
 523 tcConArgs pstate data_con (PrefixCon arg_pats) arg_tys thing_inside
 524   = do  { checkTc (con_arity == no_of_args)     -- Check correct arity
 525                   (arityErr "Constructor" data_con con_arity no_of_args)
 526         ; (arg_pats', tvs, res) <- tc_lpats pstate arg_pats arg_tys thing_inside
 527         ; return (PrefixCon arg_pats', tvs, res) }
 528   where
 529     con_arity  = dataConSourceArity data_con
 530     no_of_args = length arg_pats
 531
 532 tcConArgs pstate data_con (InfixCon p1 p2) arg_tys thing_inside
 533   = do  { checkTc (con_arity == 2)      -- Check correct arity
 534                   (arityErr "Constructor" data_con con_arity 2)
 535         ; ([p1',p2'], tvs, res) <- tc_lpats pstate [p1,p2] arg_tys thing_inside
 536         ; return (InfixCon p1' p2', tvs, res) }
 537   where
 538     con_arity  = dataConSourceArity data_con
 539
 540 tcConArgs pstate data_con (RecCon rpats) arg_tys thing_inside
 541   = do  { (rpats', tvs, res) <- tc_fields pstate rpats thing_inside
 542         ; return (RecCon rpats', tvs, res) }
 543   where
 544     tc_fields :: PatState -> [(Located Name, LPat Name)]
 545               -> (PatState -> TcM a)
 546               -> TcM ([(Located TcId, LPat TcId)], [TcTyVar], a)
 547     tc_fields pstate [] thing_inside
 548       = do { res <- thing_inside pstate
 549            ; return ([], [], res) }
 550
 551     tc_fields pstate (rpat : rpats) thing_inside
 552       = do { (rpat', tvs1, (rpats', tvs2, res))
 553                 <- tc_field pstate rpat  $ \ pstate' ->
 554                    tc_fields pstate' rpats thing_inside
 555            ; return (rpat':rpats', tvs1 ++ tvs2, res) }
 556
 557     tc_field pstate (field_lbl, pat) thing_inside
 558       = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
 559            ; (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
 560            ; return ((sel_id, pat'), tvs, res) }
 561
 562     find_field_ty field_lbl
 563         = case [ty | (f,ty) <- field_tys, f == field_lbl] of
 564
 565                 -- No matching field; chances are this field label comes from some
 566                 -- other record type (or maybe none).  As well as reporting an
 567                 -- error we still want to typecheck the pattern, principally to
 568                 -- make sure that all the variables it binds are put into the
 569                 -- environment, else the type checker crashes later:
 570                 --      f (R { foo = (a,b) }) = a+b
 571                 -- If foo isn't one of R's fields, we don't want to crash when
 572                 -- typechecking the "a+b".
 573            [] -> do { addErrTc (badFieldCon data_con field_lbl)
 574                     ; bogus_ty <- newFlexiTyVarTy liftedTypeKind
 575                     ; return (error "Bogus selector Id", bogus_ty) }
 576
 577                 -- The normal case, when the field comes from the right constructor
 578            (pat_ty : extras) ->
 579                 ASSERT( null extras )
 580                 do { sel_id <- tcLookupId field_lbl
 581                    ; return (sel_id, pat_ty) }
 582
 583     field_tys = zip (dataConFieldLabels data_con) arg_tys
 584         -- Don't use zipEqual! If the constructor isn't really a record, then
 585         -- dataConFieldLabels will be empty (and each field in the pattern
 586         -- will generate an error below).
 587 \end{code}
 588
 589
 590 %************************************************************************
 591 %*                                                                      *
 592                 Type refinement
 593 %*                                                                      *
 594 %************************************************************************
 595
 596 \begin{code}
 597 refineAlt :: PatState
 598           -> DataCon            -- For tracing only
 599           -> [TcTyVar]          -- Type variables from pattern
 600           -> [Bool]             -- Flags indicating which type variables occur
 601                                 --      in the type of at least one argument
 602           -> [TcType]           -- Result types from the pattern
 603           -> [BoxySigmaType]    -- Result types from the scrutinee (context)
 604           -> (PatState -> [BoxySigmaType] -> TcM a)
 605                         -- Possibly-refined existentials
 606           -> TcM a
 607 refineAlt pstate con pat_tvs arg_flags pat_res_tys ctxt_res_tys thing_inside
 608   | not (all isRigidTy ctxt_res_tys)
 609         -- The context is not a rigid type, so we do no type refinement here.
 610   = do  { let arg_tvs = mkVarSet [ tv | (tv, True) <- pat_tvs `zip` arg_flags]
 611               subst = boxyMatchTypes arg_tvs pat_res_tys ctxt_res_tys
 612
 613               res_tvs = tcTyVarsOfTypes pat_res_tys
 614                 -- The tvs are (already) all fresh skolems. We need a
 615                 -- fresh skolem for each type variable (to bind in the pattern)
 616                 -- even if it's refined away by the type refinement
 617               find_inst tv
 618                 | not (tv `elemVarSet` res_tvs)        = return (mkTyVarTy tv)
 619                 | Just boxy_ty <- lookupTyVar subst tv = return boxy_ty
 620                 | otherwise                            = do { tv <- newBoxyTyVar openTypeKind
 621                                                             ; return (mkTyVarTy tv) }
 622         ; pat_tys' <- mapM find_inst pat_tvs
 623
 624         -- Do the thing inside
 625         ; res <- thing_inside pstate pat_tys'
 626
 627         -- Unbox the types that have been filled in by the thing_inside
 628         -- I.e. the ones whose type variables are mentioned in at least one arg
 629         ; let strip ty in_arg_tv | in_arg_tv = stripBoxyType ty
 630                                  | otherwise = return ty
 631         ; pat_tys'' <- zipWithM strip pat_tys' arg_flags
 632         ; let subst = zipOpenTvSubst pat_tvs pat_tys''
 633         ; boxyUnifyList (substTys subst pat_res_tys) ctxt_res_tys
 634
 635         ; return res }          -- All boxes now filled
 636
 637   | otherwise   -- The context is rigid, so we can do type refinement
 638   = case gadtRefineTys (pat_reft pstate) con pat_tvs pat_res_tys ctxt_res_tys of
 639         Failed msg -> failWithTc (inaccessibleAlt msg)
 640         Succeeded (new_subst, all_bound_here)
 641           | all_bound_here      -- All the new bindings are for pat_tvs, so no need
 642                                 -- to refine the environment or pstate
 643           -> do  { traceTc trace_msg
 644                  ; thing_inside pstate pat_tvs' }
 645           | otherwise   -- New bindings affect the context, so pass down pstate'.
 646                         -- DO NOT refine the envt, because we might be inside a
 647                         -- lazy pattern
 648           -> do { traceTc trace_msg
 649                 ; thing_inside pstate' pat_tvs' }
 650           where
 651              pat_tvs' = map (substTyVar new_subst) pat_tvs
 652              pstate'  = pstate { pat_reft = new_subst }
 653              trace_msg = text "refineTypes:match" <+> ppr con <+> ppr new_subst
 654
 655 refineType :: GadtRefinement -> BoxyRhoType -> BoxyRhoType
 656 -- Refine the type if it is rigid
 657 refineType reft ty
 658   | isRefineableTy ty = substTy reft ty
 659   | otherwise         = ty
 660 \end{code}
 661
 662
 663 %************************************************************************
 664 %*                                                                      *
 665                 Overloaded literals
 666 %*                                                                      *
 667 %************************************************************************
 668
 669 In tcOverloadedLit we convert directly to an Int or Integer if we
 670 know that's what we want.  This may save some time, by not
 671 temporarily generating overloaded literals, but it won't catch all
 672 cases (the rest are caught in lookupInst).
 673
 674 \begin{code}
 675 tcOverloadedLit :: InstOrigin
 676                  -> HsOverLit Name
 677                  -> BoxyRhoType
 678                  -> TcM (HsOverLit TcId)
 679 tcOverloadedLit orig lit@(HsIntegral i fi) res_ty
 680   | not (fi `isHsVar` fromIntegerName)  -- Do not generate a LitInst for rebindable syntax.
 681         -- Reason: If we do, tcSimplify will call lookupInst, which
 682         --         will call tcSyntaxName, which does unification,
 683         --         which tcSimplify doesn't like
 684         -- ToDo: noLoc sadness
 685   = do  { integer_ty <- tcMetaTy integerTyConName
 686         ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty)
 687         ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty)))) }
 688
 689   | Just expr <- shortCutIntLit i res_ty
 690   = return (HsIntegral i expr)
 691
 692   | otherwise
 693   = do  { expr <- newLitInst orig lit res_ty
 694         ; return (HsIntegral i expr) }
 695
 696 tcOverloadedLit orig lit@(HsFractional r fr) res_ty
 697   | not (fr `isHsVar` fromRationalName) -- c.f. HsIntegral case
 698   = do  { rat_ty <- tcMetaTy rationalTyConName
 699         ; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty res_ty)
 700                 -- Overloaded literals must have liftedTypeKind, because
 701                 -- we're instantiating an overloaded function here,
 702                 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
 703                 -- However this'll be picked up by tcSyntaxOp if necessary
 704         ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty)))) }
 705
 706   | Just expr <- shortCutFracLit r res_ty
 707   = return (HsFractional r expr)
 708
 709   | otherwise
 710   = do  { expr <- newLitInst orig lit res_ty
 711         ; return (HsFractional r expr) }
 712
 713 newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
 714 newLitInst orig lit res_ty      -- Make a LitInst
 715   = do  { loc <- getInstLoc orig
 716         ; res_tau <- zapToMonotype res_ty
 717         ; new_uniq <- newUnique
 718         ; let   lit_nm   = mkSystemVarName new_uniq FSLIT("lit")
 719                 lit_inst = LitInst lit_nm lit res_tau loc
 720         ; extendLIE lit_inst
 721         ; return (HsVar (instToId lit_inst)) }
 722 \end{code}
 723
 724
 725 %************************************************************************
 726 %*                                                                      *
 727                 Note [Pattern coercions]
 728 %*                                                                      *
 729 %************************************************************************
 730
 731 In principle, these program would be reasonable:
 732
 733         f :: (forall a. a->a) -> Int
 734         f (x :: Int->Int) = x 3
 735
 736         g :: (forall a. [a]) -> Bool
 737         g [] = True
 738
 739 In both cases, the function type signature restricts what arguments can be passed
 740 in a call (to polymorphic ones).  The pattern type signature then instantiates this
 741 type.  For example, in the first case,  (forall a. a->a) <= Int -> Int, and we
 742 generate the translated term
 743         f = \x' :: (forall a. a->a).  let x = x' Int in x 3
 744
 745 From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
 746 And it requires a significant amount of code to implement, becuase we need to decorate
 747 the translated pattern with coercion functions (generated from the subsumption check
 748 by tcSub).
 749
 750 So for now I'm just insisting on type *equality* in patterns.  No subsumption.
 751
 752 Old notes about desugaring, at a time when pattern coercions were handled:
 753
 754 A SigPat is a type coercion and must be handled one at at time.  We can't
 755 combine them unless the type of the pattern inside is identical, and we don't
 756 bother to check for that.  For example:
 757
 758         data T = T1 Int | T2 Bool
 759         f :: (forall a. a -> a) -> T -> t
 760         f (g::Int->Int)   (T1 i) = T1 (g i)
 761         f (g::Bool->Bool) (T2 b) = T2 (g b)
 762
 763 We desugar this as follows:
 764
 765         f = \ g::(forall a. a->a) t::T ->
 766             let gi = g Int
 767             in case t of { T1 i -> T1 (gi i)
 768                            other ->
 769             let gb = g Bool
 770             in case t of { T2 b -> T2 (gb b)
 771                            other -> fail }}
 772
 773 Note that we do not treat the first column of patterns as a
 774 column of variables, because the coerced variables (gi, gb)
 775 would be of different types.  So we get rather grotty code.
 776 But I don't think this is a common case, and if it was we could
 777 doubtless improve it.
 778
 779 Meanwhile, the strategy is:
 780         * treat each SigPat coercion (always non-identity coercions)
 781                 as a separate block
 782         * deal with the stuff inside, and then wrap a binding round
 783                 the result to bind the new variable (gi, gb, etc)
 784
 785
 786 %************************************************************************
 787 %*                                                                      *
 788 \subsection{Errors and contexts}
 789 %*                                                                      *
 790 %************************************************************************
 791
 792 \begin{code}
 793 patCtxt :: Pat Name -> Maybe Message    -- Not all patterns are worth pushing a context
 794 patCtxt (VarPat _)  = Nothing
 795 patCtxt (ParPat _)  = Nothing
 796 patCtxt (AsPat _ _) = Nothing
 797 patCtxt pat         = Just (hang (ptext SLIT("In the pattern:"))
 798                                4 (ppr pat))
 799
 800 -----------------------------------------------
 801
 802 existentialExplode pats
 803   = hang (vcat [text "My brain just exploded.",
 804                 text "I can't handle pattern bindings for existentially-quantified constructors.",
 805                 text "In the binding group for"])
 806         4 (vcat (map ppr pats))
 807
 808 sigPatCtxt bound_ids bound_tvs pat_tys body_ty tidy_env
 809   = do  { pat_tys' <- mapM zonkTcType pat_tys
 810         ; body_ty' <- zonkTcType body_ty
 811         ; let (env1,  tidy_tys)    = tidyOpenTypes tidy_env (map idType show_ids)
 812               (env2, tidy_pat_tys) = tidyOpenTypes env1 pat_tys'
 813               (env3, tidy_body_ty) = tidyOpenType  env2 body_ty'
 814         ; return (env3,
 815                  sep [ptext SLIT("When checking an existential match that binds"),
 816                       nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)),
 817                       ptext SLIT("The pattern(s) have type(s):") <+> vcat (map ppr tidy_pat_tys),
 818                       ptext SLIT("The body has type:") <+> ppr tidy_body_ty
 819                 ]) }
 820   where
 821     show_ids = filter is_interesting bound_ids
 822     is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs
 823
 824     ppr_id id ty = ppr id <+> dcolon <+> ppr ty
 825         -- Don't zonk the types so we get the separate, un-unified versions
 826
 827 badFieldCon :: DataCon -> Name -> SDoc
 828 badFieldCon con field
 829   = hsep [ptext SLIT("Constructor") <+> quotes (ppr con),
 830           ptext SLIT("does not have field"), quotes (ppr field)]
 831
 832 polyPatSig :: TcType -> SDoc
 833 polyPatSig sig_ty
 834   = hang (ptext SLIT("Illegal polymorphic type signature in pattern:"))
 835          4 (ppr sig_ty)
 836
 837 badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
 838
 839 lazyPatErr pat tvs
 840   = failWithTc $
 841     hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
 842        2 (vcat (map pprSkolTvBinding tvs))
 843
 844 inaccessibleAlt msg
 845   = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
 846 \end{code}