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