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