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