ghc/compiler/typecheck/TcPat.lhs

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