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