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