TcPat.hs 49.6 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998

5 6

TcPat: Typechecking patterns
Austin Seipp's avatar
Austin Seipp committed
7
-}
8

9
{-# LANGUAGE CPP, RankNTypes, TupleSections #-}
10
{-# LANGUAGE FlexibleContexts #-}
Ian Lynagh's avatar
Ian Lynagh committed
11

12
module TcPat ( tcLetPat, newLetBndr, LetBndrSpec(..)
13
             , tcPat, tcPat_O, tcPats
14
             , addDataConStupidTheta, badFieldCon, polyPatSig ) where
15

16
#include "HsVersions.h"
17

18
import {-# SOURCE #-}   TcExpr( tcSyntaxOp, tcSyntaxOpGen, tcInferSigma )
19 20 21

import HsSyn
import TcHsSyn
22
import TcSigs( TcPragEnv, lookupPragEnv, addInlinePrags )
23
import TcRnMonad
24 25 26 27
import Inst
import Id
import Var
import Name
Adam Gundry's avatar
Adam Gundry committed
28
import RdrName
29 30
import TcEnv
import TcMType
31
import TcValidity( arityErr )
32 33 34 35
import TcType
import TcUnify
import TcHsType
import TysWiredIn
36
import TcEvidence
37 38
import TyCon
import DataCon
cactus's avatar
cactus committed
39 40
import PatSyn
import ConLike
41 42
import PrelNames
import BasicTypes hiding (SuccessFlag(..))
43
import DynFlags
44
import SrcLoc
45
import VarSet
46
import Util
sof's avatar
sof committed
47
import Outputable
48
import qualified GHC.LanguageExtensions as LangExt
Ian Lynagh's avatar
Ian Lynagh committed
49
import Control.Monad
50
import Control.Arrow  ( second )
51
import ListSetOps ( getNth )
52

Austin Seipp's avatar
Austin Seipp committed
53 54 55
{-
************************************************************************
*                                                                      *
56
                External interface
Austin Seipp's avatar
Austin Seipp committed
57 58 59
*                                                                      *
************************************************************************
-}
60

61
tcLetPat :: (Name -> Maybe TcId)
62
         -> LetBndrSpec
63
         -> LPat Name -> ExpSigmaType
64 65
         -> TcM a
         -> TcM (LPat TcId, a)
66 67 68 69 70 71 72 73 74 75
tcLetPat sig_fn no_gen pat pat_ty thing_inside
  = do { bind_lvl <- getTcLevel
       ; let ctxt = LetPat { pc_lvl    = bind_lvl
                           , pc_sig_fn = sig_fn
                           , pc_new    = no_gen }
             penv = PE { pe_lazy = True
                       , pe_ctxt = ctxt
                       , pe_orig = PatOrigin }

       ; tc_lpat pat pat_ty penv thing_inside }
76 77

-----------------
78
tcPats :: HsMatchContext Name
79
       -> [LPat Name]            -- Patterns,
80
       -> [ExpSigmaType]         --   and their types
81
       -> TcM a                  --   and the checker for the body
82
       -> TcM ([LPat TcId], a)
83 84 85

-- This is the externally-callable wrapper function
-- Typecheck the patterns, extend the environment to bind the variables,
86
-- do the thing inside, use any existentially-bound dictionaries to
87 88 89 90 91
-- discharge parts of the returning LIE, and deal with pattern type
-- signatures

--   1. Initialise the PatState
--   2. Check the patterns
92 93
--   3. Check the body
--   4. Check that no existentials escape
94

95
tcPats ctxt pats pat_tys thing_inside
96 97
  = tc_lpats penv pats pat_tys thing_inside
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
98
    penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
99

100
tcPat :: HsMatchContext Name
101
      -> LPat Name -> ExpSigmaType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
102
      -> TcM a                     -- Checker for body
103
      -> TcM (LPat TcId, a)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
104 105 106 107 108
tcPat ctxt = tcPat_O ctxt PatOrigin

-- | A variant of 'tcPat' that takes a custom origin
tcPat_O :: HsMatchContext Name
        -> CtOrigin              -- ^ origin to use if the type needs inst'ing
109
        -> LPat Name -> ExpSigmaType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
110 111 112
        -> TcM a                 -- Checker for body
        -> TcM (LPat TcId, a)
tcPat_O ctxt orig pat pat_ty thing_inside
113 114
  = tc_lpat pat pat_ty penv thing_inside
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
115
    penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig }
116

117

118 119 120 121 122 123 124 125
{-
************************************************************************
*                                                                      *
                PatEnv, PatCtxt, LetBndrSpec
*                                                                      *
************************************************************************
-}

126
data PatEnv
127 128
  = PE { pe_lazy :: Bool        -- True <=> lazy context, so no existentials allowed
       , pe_ctxt :: PatCtxt     -- Context in which the whole pattern appears
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
129
       , pe_orig :: CtOrigin    -- origin to use if the pat_ty needs inst'ing
130
       }
131 132 133

data PatCtxt
  = LamPat   -- Used for lambdas, case etc
134
       (HsMatchContext Name)
135

136
  | LetPat   -- Used only for let(rec) pattern bindings
137
             -- See Note [Typing patterns in pattern bindings]
138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160
       { pc_lvl    :: TcLevel
                   -- Level of the binding group

       , pc_sig_fn :: Name -> Maybe TcId
                   -- Tells the expected type
                   -- for binders with a signature

       , pc_new :: LetBndrSpec
                -- How to make a new binder
       }        -- for binders without signatures

data LetBndrSpec
  = LetLclBndr            -- We are going to generalise, and wrap in an AbsBinds
                          -- so clone a fresh binder for the local monomorphic Id

  | LetGblBndr TcPragEnv  -- Generalisation plan is NoGen, so there isn't going
                          -- to be an AbsBinds; So we must bind the global version
                          -- of the binder right away.
                          -- And here is the inline-pragma information

instance Outputable LetBndrSpec where
  ppr LetLclBndr      = text "LetLclBndr"
  ppr (LetGblBndr {}) = text "LetGblBndr"
161

162 163 164
makeLazy :: PatEnv -> PatEnv
makeLazy penv = penv { pe_lazy = True }

165 166 167
inPatBind :: PatEnv -> Bool
inPatBind (PE { pe_ctxt = LetPat {} }) = True
inPatBind (PE { pe_ctxt = LamPat {} }) = False
168

169
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
170
*                                                                      *
171
                Binders
Austin Seipp's avatar
Austin Seipp committed
172
*                                                                      *
173
********************************************************************* -}
174

175
tcPatBndr :: PatEnv -> Name -> ExpSigmaType -> TcM (HsWrapper, TcId)
176 177 178
-- (coi, xp) = tcPatBndr penv x pat_ty
-- Then coi : pat_ty ~ typeof(xp)
--
179 180 181 182 183 184 185 186 187 188 189
tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl    = bind_lvl
                                      , pc_sig_fn = sig_fn
                                      , pc_new    = no_gen } })
          bndr_name exp_pat_ty
  -- For the LetPat cases, see
  -- Note [Typechecking pattern bindings] in TcBinds

  | Just bndr_id <- sig_fn bndr_name   -- There is a signature
  = do { wrap <- tcSubTypePat penv exp_pat_ty (idType bndr_id)
           -- See Note [Subsumption check at pattern variables]
       ; traceTc "tcPatBndr(sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr exp_pat_ty)
190
       ; return (wrap, bndr_id) }
191

192 193 194 195 196 197 198 199 200 201 202 203 204 205 206
  | otherwise                          -- No signature
  = do { (co, bndr_ty) <- case exp_pat_ty of
             Check pat_ty    -> promoteTcType bind_lvl pat_ty
             Infer infer_res -> ASSERT( bind_lvl == ir_lvl infer_res )
                                -- If we were under a constructor that bumped
                                -- the level, we'd be in checking mode
                                do { bndr_ty <- inferResultToType infer_res
                                   ; return (mkTcNomReflCo bndr_ty, bndr_ty) }
       ; bndr_id <- newLetBndr no_gen bndr_name bndr_ty
       ; traceTc "tcPatBndr(nosig)" (vcat [ ppr bind_lvl
                                          , ppr exp_pat_ty, ppr bndr_ty, ppr co
                                          , ppr bndr_id ])
       ; return (mkWpCastN co, bndr_id) }

tcPatBndr _ bndr_name pat_ty
207
  = do { pat_ty <- expTypeToType pat_ty
208
       ; traceTc "tcPatBndr(not let)" (ppr bndr_name $$ ppr pat_ty)
209
       ; return (idHsWrapper, mkLocalId bndr_name pat_ty) }
210 211
               -- Whether or not there is a sig is irrelevant,
               -- as this is local
212

213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240
newLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId
-- Make up a suitable Id for the pattern-binder.
-- See Note [Typechecking pattern bindings], item (4) in TcBinds
--
-- In the polymorphic case when we are going to generalise
--    (plan InferGen, no_gen = LetLclBndr), generate a "monomorphic version"
--    of the Id; the original name will be bound to the polymorphic version
--    by the AbsBinds
-- In the monomorphic case when we are not going to generalise
--    (plan NoGen, no_gen = LetGblBndr) there is no AbsBinds,
--    and we use the original name directly
newLetBndr LetLclBndr name ty
  = do { mono_name <- cloneLocalName name
       ; return (mkLocalId mono_name ty) }
newLetBndr (LetGblBndr prags) name ty
  = addInlinePrags (mkLocalId name ty) (lookupPragEnv prags name)

tcSubTypePat :: PatEnv -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
-- tcSubTypeET with the UserTypeCtxt specialised to GenSigCtxt
-- Used when typechecking patterns
tcSubTypePat penv t1 t2 = tcSubTypeET (pe_orig penv) GenSigCtxt t1 t2

{- Note [Subsumption check at pattern variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we come across a variable with a type signature, we need to do a
subsumption, not equality, check against the context type.  e.g.

    data T = MkT (forall a. a->a)
241 242
      f :: forall b. [b]->[b]
      MkT f = blah
243 244 245 246 247

Since 'blah' returns a value of type T, its payload is a polymorphic
function of type (forall a. a->a).  And that's enough to bind the
less-polymorphic function 'f', but we need some impedence matching
to witness the instantiation.
248

249

Austin Seipp's avatar
Austin Seipp committed
250 251
************************************************************************
*                                                                      *
252
                The main worker functions
Austin Seipp's avatar
Austin Seipp committed
253 254
*                                                                      *
************************************************************************
255

256 257
Note [Nesting]
~~~~~~~~~~~~~~
lennart@augustsson.net's avatar
lennart@augustsson.net committed
258
tcPat takes a "thing inside" over which the pattern scopes.  This is partly
259
so that tcPat can extend the environment for the thing_inside, but also
260 261 262 263
so that constraints arising in the thing_inside can be discharged by the
pattern.

This does not work so well for the ErrCtxt carried by the monad: we don't
264
want the error-context for the pattern to scope over the RHS.
265
Hence the getErrCtxt/setErrCtxt stuff in tcMultiple
Austin Seipp's avatar
Austin Seipp committed
266
-}
267 268

--------------------
269
type Checker inp out =  forall r.
270 271 272 273
                          inp
                       -> PatEnv
                       -> TcM r
                       -> TcM (out, r)
274 275

tcMultiple :: Checker inp out -> Checker [inp] [out]
276
tcMultiple tc_pat args penv thing_inside
277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292
  = do  { err_ctxt <- getErrCtxt
        ; let loop _ []
                = do { res <- thing_inside
                     ; return ([], res) }

              loop penv (arg:args)
                = do { (p', (ps', res))
                                <- tc_pat arg penv $
                                   setErrCtxt err_ctxt $
                                   loop penv args
                -- setErrCtxt: restore context before doing the next pattern
                -- See note [Nesting] above

                     ; return (p':ps', res) }

        ; loop penv args }
293 294

--------------------
295
tc_lpat :: LPat Name
296
        -> ExpSigmaType
297 298 299
        -> PatEnv
        -> TcM a
        -> TcM (LPat TcId, a)
300
tc_lpat (L span pat) pat_ty penv thing_inside
301
  = setSrcSpan span $
302
    do  { (pat', res) <- maybeWrapPatCtxt pat (tc_pat penv pat pat_ty)
303
                                          thing_inside
304
        ; return (L span pat', res) }
305 306

tc_lpats :: PatEnv
307
         -> [LPat Name] -> [ExpSigmaType]
308 309 310
         -> TcM a
         -> TcM ([LPat TcId], a)
tc_lpats penv pats tys thing_inside
Simon Peyton Jones's avatar
Simon Peyton Jones committed
311
  = ASSERT2( equalLength pats tys, ppr pats $$ ppr tys )
312
    tcMultiple (\(p,t) -> tc_lpat p t)
313
                (zipEqual "tc_lpats" pats tys)
314
                penv thing_inside
315 316

--------------------
317 318
tc_pat  :: PatEnv
        -> Pat Name
319
        -> ExpSigmaType  -- Fully refined result type
320 321 322
        -> TcM a                -- Thing inside
        -> TcM (Pat TcId,       -- Translated pattern
                a)              -- Result of thing inside
323

324
tc_pat penv (VarPat (L l name)) pat_ty thing_inside
325
  = do  { (wrap, id) <- tcPatBndr penv name pat_ty
batterseapower's avatar
batterseapower committed
326
        ; res <- tcExtendIdEnv1 name id thing_inside
327
        ; pat_ty <- readExpType pat_ty
328
        ; return (mkHsWrapPat wrap (VarPat (L l id)) pat_ty, res) }
329 330

tc_pat penv (ParPat pat) pat_ty thing_inside
331 332
  = do  { (pat', res) <- tc_lpat pat pat_ty penv thing_inside
        ; return (ParPat pat', res) }
333 334

tc_pat penv (BangPat pat) pat_ty thing_inside
335 336
  = do  { (pat', res) <- tc_lpat pat pat_ty penv thing_inside
        ; return (BangPat pat', res) }
337

338
tc_pat penv lpat@(LazyPat pat) pat_ty thing_inside
339 340 341 342
  = do  { (pat', (res, pat_ct))
                <- tc_lpat pat pat_ty (makeLazy penv) $
                   captureConstraints thing_inside
                -- Ignore refined penv', revert to penv
343

344 345
        ; emitConstraints pat_ct
        -- captureConstraints/extendConstraints:
346
        --   see Note [Hopping the LIE in lazy patterns]
347

348
        -- Check there are no unlifted types under the lazy pattern
Gabor Greif's avatar
Gabor Greif committed
349
        -- This is a very unsatisfactory test.  We have to zonk because
350 351 352 353 354 355 356 357 358
        -- the binder-tys are typically just a unification variable,
        -- which should by now have been unified... but it might be
        -- deferred for the constraint solver...Ugh!  Also
        -- collecting the pattern binders again is not very cool.
        -- But it's all very much a corner case: a lazy pattern with
        -- unboxed types inside it
        ; bndr_tys <- mapM (zonkTcType . idType) (collectPatBinders pat')
        ; when (any isUnliftedType bndr_tys)
               (lazyUnliftedPatErr lpat)
359

360
        -- Check that the expected pattern type is itself lifted
361 362
        ; pat_ty <- readExpType pat_ty
        ; _ <- unifyType noThing (typeKind pat_ty) liftedTypeKind
363

364
        ; return (LazyPat pat', res) }
365

366
tc_pat _ (WildPat _) pat_ty thing_inside
367
  = do  { res <- thing_inside
368
        ; pat_ty <- expTypeToType pat_ty
369
        ; return (WildPat pat_ty, res) }
370

371
tc_pat penv (AsPat (L nm_loc name) pat) pat_ty thing_inside
372
  = do  { (wrap, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty)
batterseapower's avatar
batterseapower committed
373
        ; (pat', res) <- tcExtendIdEnv1 name bndr_id $
374 375
                         tc_lpat pat (mkCheckExpType $ idType bndr_id)
                                 penv thing_inside
376 377 378 379 380 381 382
            -- NB: if we do inference on:
            --          \ (y@(x::forall a. a->a)) = e
            -- we'll fail.  The as-pattern infers a monotype for 'y', which then
            -- fails to unify with the polymorphic type for 'x'.  This could
            -- perhaps be fixed, but only with a bit more work.
            --
            -- If you fix it, don't forget the bindInstsOfPatIds!
383
        ; pat_ty <- readExpType pat_ty
384
        ; return (mkHsWrapPat wrap (AsPat (L nm_loc bndr_id) pat') pat_ty, res) }
385 386 387

tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside
  = do  {
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
388
         -- Expr must have type `forall a1...aN. OPT' -> B`
389
         -- where overall_pat_ty is an instance of OPT'.
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
390
        ; (expr',expr'_inferred) <- tcInferSigma expr
391

392 393 394 395 396 397 398 399
         -- expression must be a function
        ; let expr_orig = exprCtOrigin (unLoc expr)
              herald    = text "A view pattern expression expects"
        ; (expr_wrap1, [inf_arg_ty], inf_res_ty)
            <- matchActualFunTys herald expr_orig (Just expr) 1 expr'_inferred
            -- expr_wrap1 :: expr'_inferred "->" (inf_arg_ty -> inf_res_ty)

         -- check that overall pattern is more polymorphic than arg type
400
        ; expr_wrap2 <- tcSubTypePat penv overall_pat_ty inf_arg_ty
401 402 403 404 405 406 407 408 409 410 411
            -- expr_wrap2 :: overall_pat_ty "->" inf_arg_ty

         -- pattern must have inf_res_ty
        ; (pat', res) <- tc_lpat pat (mkCheckExpType inf_res_ty) penv thing_inside

        ; overall_pat_ty <- readExpType overall_pat_ty
        ; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper
                                    overall_pat_ty inf_res_ty
               -- expr_wrap2' :: (inf_arg_ty -> inf_res_ty) "->"
               --                (overall_pat_ty -> inf_res_ty)
              expr_wrap = expr_wrap2' <.> expr_wrap1
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
412
        ; return (ViewPat (mkLHsWrap expr_wrap expr') pat' overall_pat_ty, res) }
413

414 415
-- Type signatures in patterns
-- See Note [Pattern coercions] below
416
tc_pat penv (SigPatIn pat sig_ty) pat_ty thing_inside
417
  = do  { (inner_ty, tv_binds, wcs, wrap) <- tcPatSig (inPatBind penv)
thomasw's avatar
thomasw committed
418
                                                            sig_ty pat_ty
419 420
        ; (pat', res) <- tcExtendTyVarEnv2 wcs     $
                         tcExtendTyVarEnv tv_binds $
421 422
                         tc_lpat pat (mkCheckExpType inner_ty) penv thing_inside
        ; pat_ty <- readExpType pat_ty
423
        ; return (mkHsWrapPat wrap (SigPatOut pat' inner_ty) pat_ty, res) }
424 425 426

------------------------
-- Lists, tuples, arrays
427
tc_pat penv (ListPat pats _ Nothing) pat_ty thing_inside
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
428
  = do  { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv pat_ty
429
        ; (pats', res) <- tcMultiple (\p -> tc_lpat p (mkCheckExpType elt_ty))
430
                                     pats penv thing_inside
431
        ; pat_ty <- readExpType pat_ty
432
        ; return (mkHsWrapPat coi (ListPat pats' elt_ty Nothing) pat_ty, res)
433 434 435
        }

tc_pat penv (ListPat pats _ (Just (_,e))) pat_ty thing_inside
436 437 438 439 440 441 442 443 444
  = do  { tau_pat_ty <- expTypeToType pat_ty
        ; ((pats', res, elt_ty), e')
            <- tcSyntaxOpGen ListOrigin e [SynType (mkCheckExpType tau_pat_ty)]
                                          SynList $
                 \ [elt_ty] ->
                 do { (pats', res) <- tcMultiple (\p -> tc_lpat p (mkCheckExpType elt_ty))
                                                 pats penv thing_inside
                    ; return (pats', res, elt_ty) }
        ; return (ListPat pats' elt_ty (Just (tau_pat_ty,e')), res)
445
        }
446

447
tc_pat penv (PArrPat pats _) pat_ty thing_inside
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
448
  = do  { (coi, elt_ty) <- matchExpectedPatTy matchExpectedPArrTy penv pat_ty
449
        ; (pats', res) <- tcMultiple (\p -> tc_lpat p (mkCheckExpType elt_ty))
450
                                     pats penv thing_inside
451
        ; pat_ty <- readExpType pat_ty
452
        ; return (mkHsWrapPat coi (PArrPat pats' elt_ty) pat_ty, res)
453
        }
454

455
tc_pat penv (TuplePat pats boxity _) pat_ty thing_inside
456 457
  = do  { let arity = length pats
              tc = tupleTyCon boxity arity
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
458 459
        ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc)
                                               penv pat_ty
460 461
                     -- Unboxed tuples have RuntimeRep vars, which we discard:
                     -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
462 463
        ; let con_arg_tys = case boxity of Unboxed -> drop arity arg_tys
                                           Boxed   -> arg_tys
464 465
        ; (pats', res) <- tc_lpats penv pats (map mkCheckExpType con_arg_tys)
                                   thing_inside
466

467
        ; dflags <- getDynFlags
468

469 470 471 472 473
        -- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
        -- so that we can experiment with lazy tuple-matching.
        -- This is a pretty odd place to make the switch, but
        -- it was easy to do.
        ; let
474
              unmangled_result = TuplePat pats' boxity con_arg_tys
475
                                 -- pat_ty /= pat_ty iff coi /= IdCo
476 477
              possibly_mangled_result
                | gopt Opt_IrrefutableTuples dflags &&
478
                  isBoxed boxity            = LazyPat (noLoc unmangled_result)
479
                | otherwise                 = unmangled_result
480

481
        ; pat_ty <- readExpType pat_ty
482
        ; ASSERT( length con_arg_tys == length pats ) -- Syntactically enforced
483
          return (mkHsWrapPat coi possibly_mangled_result pat_ty, res)
484
        }
485

486 487 488 489 490 491 492 493 494 495 496 497
tc_pat penv (SumPat pat alt arity _) pat_ty thing_inside
  = do  { let tc = sumTyCon arity
        ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc)
                                               penv pat_ty
        ; -- Drop levity vars, we don't care about them here
          let con_arg_tys = drop arity arg_tys
        ; (pat', res) <- tc_lpat pat (mkCheckExpType (con_arg_tys `getNth` (alt - 1)))
                                 penv thing_inside
        ; pat_ty <- readExpType pat_ty
        ; return (mkHsWrapPat coi (SumPat pat' alt arity con_arg_tys) pat_ty, res)
        }

498 499
------------------------
-- Data constructors
500 501
tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside
  = tcConPat penv con pat_ty arg_pats thing_inside
502 503 504

------------------------
-- Literal patterns
505
tc_pat penv (LitPat simple_lit) pat_ty thing_inside
506
  = do  { let lit_ty = hsLitType simple_lit
507 508
        ; wrap   <- tcSubTypePat penv pat_ty lit_ty
        ; res    <- thing_inside
509
        ; pat_ty <- readExpType pat_ty
510
        ; return ( mkHsWrapPat wrap (LitPat simple_lit) pat_ty
511
                 , res) }
512 513 514

------------------------
-- Overloaded patterns: n, and n+k
515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531

-- In the case of a negative literal (the more complicated case),
-- we get
--
--   case v of (-5) -> blah
--
-- becoming
--
--   if v == (negate (fromInteger 5)) then blah else ...
--
-- There are two bits of rebindable syntax:
--   (==)   :: pat_ty -> neg_lit_ty -> Bool
--   negate :: lit_ty -> neg_lit_ty
-- where lit_ty is the type of the overloaded literal 5.
--
-- When there is no negation, neg_lit_ty and lit_ty are the same
tc_pat _ (NPat (L l over_lit) mb_neg eq _) pat_ty thing_inside
532
  = do  { let orig = LiteralOrigin over_lit
533 534 535 536 537 538 539 540 541 542 543 544 545 546
        ; ((lit', mb_neg'), eq')
            <- tcSyntaxOp orig eq [SynType pat_ty, SynAny]
                          (mkCheckExpType boolTy) $
               \ [neg_lit_ty] ->
               let new_over_lit lit_ty = newOverloadedLit over_lit
                                           (mkCheckExpType lit_ty)
               in case mb_neg of
                 Nothing  -> (, Nothing) <$> new_over_lit neg_lit_ty
                 Just neg -> -- Negative literal
                             -- The 'negate' is re-mappable syntax
                   second Just <$>
                   (tcSyntaxOp orig neg [SynRho] (mkCheckExpType neg_lit_ty) $
                    \ [lit_ty] -> new_over_lit lit_ty)

547
        ; res <- thing_inside
548 549
        ; pat_ty <- readExpType pat_ty
        ; return (NPat (L l lit') mb_neg' eq' pat_ty, res) }
550

551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591
{-
Note [NPlusK patterns]
~~~~~~~~~~~~~~~~~~~~~~
From

  case v of x + 5 -> blah

we get

  if v >= 5 then (\x -> blah) (v - 5) else ...

There are two bits of rebindable syntax:
  (>=) :: pat_ty -> lit1_ty -> Bool
  (-)  :: pat_ty -> lit2_ty -> var_ty

lit1_ty and lit2_ty could conceivably be different.
var_ty is the type inferred for x, the variable in the pattern.

If the pushed-down pattern type isn't a tau-type, the two pat_ty's above
could conceivably be different specializations. But this is very much
like the situation in Note [Case branches must be taus] in TcMatches.
So we tauify the pat_ty before proceeding.

Note that we need to type-check the literal twice, because it is used
twice, and may be used at different types. The second HsOverLit stored in the
AST is used for the subtraction operation.
-}

-- See Note [NPlusK patterns]
tc_pat penv (NPlusKPat (L nm_loc name) (L loc lit) _ ge minus _) pat_ty thing_inside
  = do  { pat_ty <- expTypeToType pat_ty
        ; let orig = LiteralOrigin lit
        ; (lit1', ge')
            <- tcSyntaxOp orig ge [synKnownType pat_ty, SynRho]
                                  (mkCheckExpType boolTy) $
               \ [lit1_ty] ->
               newOverloadedLit lit (mkCheckExpType lit1_ty)
        ; ((lit2', minus_wrap, bndr_id), minus')
            <- tcSyntaxOpGen orig minus [synKnownType pat_ty, SynRho] SynAny $
               \ [lit2_ty, var_ty] ->
               do { lit2' <- newOverloadedLit lit (mkCheckExpType lit2_ty)
592
                  ; (wrap, bndr_id) <- setSrcSpan nm_loc $
593 594 595 596
                                     tcPatBndr penv name (mkCheckExpType var_ty)
                           -- co :: var_ty ~ idType bndr_id

                           -- minus_wrap is applicable to minus'
597
                  ; return (lit2', wrap, bndr_id) }
598

599
        -- The Report says that n+k patterns must be in Integral
600 601 602 603
        -- but it's silly to insist on this in the RebindableSyntax case
        ; unlessM (xoptM LangExt.RebindableSyntax) $
          do { icls <- tcLookupClass integralClassName
             ; instStupidTheta orig [mkClassPred icls [pat_ty]] }
604

605
        ; res <- tcExtendIdEnv1 name bndr_id thing_inside
606 607 608 609 610 611

        ; let minus'' = minus' { syn_res_wrap =
                                    minus_wrap <.> syn_res_wrap minus' }
              pat' = NPlusKPat (L nm_loc bndr_id) (L loc lit1') lit2'
                               ge' minus'' pat_ty
        ; return (pat', res) }
612

613 614 615 616 617 618 619 620 621
-- HsSpliced is an annotation produced by 'RnSplice.rnSplicePat'.
-- Here we get rid of it and add the finalizers to the global environment.
--
-- See Note [Delaying modFinalizers in untyped splices] in RnSplice.
tc_pat penv (SplicePat (HsSpliced mod_finalizers (HsSplicedPat pat)))
            pat_ty thing_inside
  = do addModFinalizersWithLclEnv mod_finalizers
       tc_pat penv pat pat_ty thing_inside

622
tc_pat _ _other_pat _ _ = panic "tc_pat"        -- ConPatOut, SigPatOut
623

624

Austin Seipp's avatar
Austin Seipp committed
625
{-
626 627 628 629
Note [Hopping the LIE in lazy patterns]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In a lazy pattern, we must *not* discharge constraints from the RHS
from dictionaries bound in the pattern.  E.g.
630
        f ~(C x) = 3
631
We can't discharge the Num constraint from dictionaries bound by
632
the pattern C!
633

634
So we have to make the constraints from thing_inside "hop around"
635
the pattern.  Hence the captureConstraints and emitConstraints.
636 637 638

The same thing ensures that equality constraints in a lazy match
are not made available in the RHS of the match. For example
639 640 641
        data T a where { T1 :: Int -> T Int; ... }
        f :: T a -> Int -> a
        f ~(T1 i) y = y
642
It's obviously not sound to refine a to Int in the right
643
hand side, because the argument might not match T1 at all!
644 645 646 647

Finally, a lazy pattern should not bind any existential type variables
because they won't be in scope when we do the desugaring

648

Austin Seipp's avatar
Austin Seipp committed
649 650
************************************************************************
*                                                                      *
651 652
        Most of the work for constructors is here
        (the rest is in the ConPatIn case of tc_pat)
Austin Seipp's avatar
Austin Seipp committed
653 654
*                                                                      *
************************************************************************
655

656 657 658 659 660 661 662 663 664 665 666
[Pattern matching indexed data types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following declarations:

  data family Map k :: * -> *
  data instance Map (a, b) v = MapPair (Map a (Pair b v))

and a case expression

  case x :: Map (Int, c) w of MapPair m -> ...

667
As explained by [Wrappers for data instance tycons] in MkIds.hs, the
668 669 670 671 672 673 674 675 676 677 678 679 680 681 682
worker/wrapper types for MapPair are

  $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
  $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v

So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
:R123Map, which means the straight use of boxySplitTyConApp would give a type
error.  Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
boxySplitTyConApp with the family tycon Map instead, which gives us the family
type list {(Int, c), w}.  To get the correct split for :R123Map, we need to
unify the family type list {(Int, c), w} with the instance types {(a, b), v}
(provided by tyConFamInst_maybe together with the family tycon).  This
unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
the split arguments for the representation tycon :R123Map as {Int, c, w}

683
In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
684

685
  Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}
686 687 688 689 690 691

moving between representation and family type into account.  To produce type
correct Core, this coercion needs to be used to case the type of the scrutinee
from the family to the representation type.  This is achieved by
unwrapFamInstScrutinee using a CoPat around the result pattern.

692
Now it might appear seem as if we could have used the previous GADT type
693 694 695 696 697 698 699 700 701 702 703 704
refinement infrastructure of refineAlt and friends instead of the explicit
unification and CoPat generation.  However, that would be wrong.  Why?  The
whole point of GADT refinement is that the refinement is local to the case
alternative.  In contrast, the substitution generated by the unification of
the family type list and instance types needs to be propagated to the outside.
Imagine that in the above example, the type of the scrutinee would have been
(Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
substitution [x -> (a, b), v -> w].  In contrast to GADT matching, the
instantiation of x with (a, b) must be global; ie, it must be valid in *all*
alternatives of the case expression, whereas in the GADT case it might vary
between alternatives.

705 706 707
RIP GADT refinement: refinements have been replaced by the use of explicit
equality constraints that are used in conjunction with implication constraints
to express the local scope of GADT refinements.
Austin Seipp's avatar
Austin Seipp committed
708
-}
709

710
--      Running example:
711
-- MkT :: forall a b c. (a~[b]) => b -> c -> T a
712
--       with scrutinee of type (T ty)
713

714
tcConPat :: PatEnv -> Located Name
715
         -> ExpSigmaType           -- Type of the pattern
716 717
         -> HsConPatDetails Name -> TcM a
         -> TcM (Pat TcId, a)
cactus's avatar
cactus committed
718 719 720 721 722 723 724 725 726 727
tcConPat penv con_lname@(L _ con_name) pat_ty arg_pats thing_inside
  = do  { con_like <- tcLookupConLike con_name
        ; case con_like of
            RealDataCon data_con -> tcDataConPat penv con_lname data_con
                                                 pat_ty arg_pats thing_inside
            PatSynCon pat_syn -> tcPatSynPat penv con_lname pat_syn
                                             pat_ty arg_pats thing_inside
        }

tcDataConPat :: PatEnv -> Located Name -> DataCon
728
             -> ExpSigmaType               -- Type of the pattern
729 730
             -> HsConPatDetails Name -> TcM a
             -> TcM (Pat TcId, a)
cactus's avatar
cactus committed
731
tcDataConPat penv (L con_span con_name) data_con pat_ty arg_pats thing_inside
732 733 734
  = do  { let tycon = dataConTyCon data_con
                  -- For data families this is the representation tycon
              (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _)
735
                = dataConFullSig data_con
cactus's avatar
cactus committed
736
              header = L con_span (RealDataCon data_con)
737

738 739 740
          -- Instantiate the constructor type variables [a->ty]
          -- This may involve doing a family-instance coercion,
          -- and building a wrapper
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
741
        ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty
742
        ; pat_ty <- readExpType pat_ty
743

744 745
          -- Add the stupid theta
        ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys
746

747 748
        ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ arg_tys
        ; checkExistentials ex_tvs all_arg_tys penv
749
        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX
niteria's avatar
niteria committed
750
                               (zipTvSubst univ_tvs ctxt_res_tys) ex_tvs
751 752
                     -- Get location from monad, not from ex_tvs

753
        ; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
754
              -- pat_ty' is type of the actual constructor application
755
              -- pat_ty' /= pat_ty iff coi /= IdCo
Simon Peyton Jones's avatar
Simon Peyton Jones committed
756

757
              arg_tys' = substTys tenv arg_tys
758

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
759 760 761
        ; traceTc "tcConPat" (vcat [ ppr con_name
                                   , pprTvBndrs univ_tvs
                                   , pprTvBndrs ex_tvs
762
                                   , ppr eq_spec
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
763 764 765 766
                                   , ppr theta
                                   , pprTvBndrs ex_tvs'
                                   , ppr ctxt_res_tys
                                   , ppr arg_tys'
767
                                   , ppr arg_pats ])
768 769
        ; if null ex_tvs && null eq_spec && null theta
          then do { -- The common case; no class bindings etc
770
                    -- (see Note [Arrows and patterns])
771 772 773 774
                    (arg_pats', res) <- tcConArgs (RealDataCon data_con) arg_tys'
                                                  arg_pats penv thing_inside
                  ; let res_pat = ConPatOut { pat_con = header,
                                              pat_tvs = [], pat_dicts = [],
775
                                              pat_binds = emptyTcEvBinds,
776
                                              pat_args = arg_pats',
777
                                              pat_arg_tys = ctxt_res_tys,
cactus's avatar
cactus committed
778
                                              pat_wrap = idHsWrapper }
779

780
                  ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
781

782
          else do   -- The general case, with existential,
783
                    -- and local equality constraints
784
        { let theta'     = substTheta tenv (eqSpecPreds eq_spec ++ theta)
785 786
                           -- order is *important* as we generate the list of
                           -- dictionary binders from theta'
787
              no_equalities = not (any isNomEqPred theta')
788 789 790 791
              skol_info = PatSkol (RealDataCon data_con) mc
              mc = case pe_ctxt penv of
                     LamPat mc -> mc
                     LetPat {} -> PatBindRhs
792

793 794
        ; gadts_on    <- xoptM LangExt.GADTs
        ; families_on <- xoptM LangExt.TypeFamilies
795
        ; checkTc (no_equalities || gadts_on || families_on)
sivteck's avatar
sivteck committed
796 797
                  (text "A pattern match on a GADT requires the" <+>
                   text "GADTs or TypeFamilies language extension")
798 799 800
                  -- Trac #2905 decided that a *pattern-match* of a GADT
                  -- should require the GADT language flag.
                  -- Re TypeFamilies see also #7156
801

802
        ; given <- newEvVars theta'
803
        ; (ev_binds, (arg_pats', res))
804
             <- checkConstraints skol_info ex_tvs' given $
cactus's avatar
cactus committed
805
                tcConArgs (RealDataCon data_con) arg_tys' arg_pats penv thing_inside
806

cactus's avatar
cactus committed
807
        ; let res_pat = ConPatOut { pat_con   = header,
808 809 810 811
                                    pat_tvs   = ex_tvs',
                                    pat_dicts = given,
                                    pat_binds = ev_binds,
                                    pat_args  = arg_pats',
812
                                    pat_arg_tys = ctxt_res_tys,
cactus's avatar
cactus committed
813
                                    pat_wrap  = idHsWrapper }
814 815
        ; return (mkHsWrapPat wrap res_pat pat_ty, res)
        } }
816

cactus's avatar
cactus committed
817
tcPatSynPat :: PatEnv -> Located Name -> PatSyn
818
            -> ExpSigmaType                -- Type of the pattern
819 820
            -> HsConPatDetails Name -> TcM a
            -> TcM (Pat TcId, a)
cactus's avatar
cactus committed
821
tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
822
  = do  { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn
cactus's avatar
cactus committed
823

824
        ; (subst, univ_tvs') <- newMetaTyVars univ_tvs
cactus's avatar
cactus committed
825

826 827
        ; let all_arg_tys = ty : prov_theta ++ arg_tys
        ; checkExistentials ex_tvs all_arg_tys penv
cactus's avatar
cactus committed
828
        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
829 830
        ; let ty'         = substTy tenv ty
              arg_tys'    = substTys tenv arg_tys
cactus's avatar
cactus committed
831
              prov_theta' = substTheta tenv prov_theta
832
              req_theta'  = substTheta tenv req_theta
cactus's avatar
cactus committed
833

834
        ; wrap <- tcSubTypePat penv pat_ty ty'
cactus's avatar
cactus committed
835 836 837 838 839 840 841 842 843 844 845 846 847 848
        ; traceTc "tcPatSynPat" (ppr pat_syn $$
                                 ppr pat_ty $$
                                 ppr ty' $$
                                 ppr ex_tvs' $$
                                 ppr prov_theta' $$
                                 ppr req_theta' $$
                                 ppr arg_tys')

        ; prov_dicts' <- newEvVars prov_theta'

        ; let skol_info = case pe_ctxt penv of
                            LamPat mc -> PatSkol (PatSynCon pat_syn) mc
                            LetPat {} -> UnkSkol -- Doesn't matter

849
        ; req_wrap <- instCall PatOrigin (mkTyVarTys univ_tvs') req_theta'
cactus's avatar
cactus committed
850 851
        ; traceTc "instCall" (ppr req_wrap)

852
        ; traceTc "checkConstraints {" Outputable.empty
cactus's avatar
cactus committed
853 854 855 856 857 858
        ; (ev_binds, (arg_pats', res))
             <- checkConstraints skol_info ex_tvs' prov_dicts' $
                tcConArgs (PatSynCon pat_syn) arg_tys' arg_pats penv thing_inside

        ; traceTc "checkConstraints }" (ppr ev_binds)
        ; let res_pat = ConPatOut { pat_con   = L con_span $ PatSynCon pat_syn,
859 860 861 862
                                    pat_tvs   = ex_tvs',
                                    pat_dicts = prov_dicts',
                                    pat_binds = ev_binds,
                                    pat_args  = arg_pats',
863
                                    pat_arg_tys = mkTyVarTys univ_tvs',
cactus's avatar
cactus committed
864
                                    pat_wrap  = req_wrap }
865
        ; pat_ty <- readExpType pat_ty
866
        ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
cactus's avatar
cactus committed
867

868
----------------------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
869 870
-- | Convenient wrapper for calling a matchExpectedXXX function
matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionN, a))
871
                    -> PatEnv -> ExpSigmaType -> TcM (HsWrapper, a)
872
-- See Note [Matching polytyped patterns]
873
-- Returns a wrapper : pat_ty ~R inner_ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
874
matchExpectedPatTy inner_match (PE { pe_orig = orig }) pat_ty
875 876
  = do { pat_ty <- expTypeToType pat_ty
       ; (wrap, pat_rho) <- topInstantiate orig pat_ty