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