TcPat.hs 50.1 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 <- tcSubTypeET (pe_orig 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 _ (LitPat simple_lit) pat_ty thing_inside
506
  = do  { let lit_ty = hsLitType simple_lit
507
        ; co <- unifyPatType simple_lit lit_ty pat_ty
508 509
                -- coi is of kind: pat_ty ~ lit_ty
        ; res <- thing_inside
510
        ; pat_ty <- readExpType pat_ty
511
        ; return ( mkHsWrapPatCo co (LitPat simple_lit) pat_ty
512
                 , res) }
513 514 515

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

-- 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
533
  = do  { let orig = LiteralOrigin over_lit
534 535 536 537 538 539 540 541 542 543 544 545 546 547
        ; ((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)

548
        ; res <- thing_inside
549 550
        ; pat_ty <- readExpType pat_ty
        ; return (NPat (L l lit') mb_neg' eq' pat_ty, res) }
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 592
{-
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)
593
                  ; (wrap, bndr_id) <- setSrcSpan nm_loc $
594 595 596 597
                                     tcPatBndr penv name (mkCheckExpType var_ty)
                           -- co :: var_ty ~ idType bndr_id

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

600
        -- The Report says that n+k patterns must be in Integral
601 602 603 604
        -- 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]] }
605

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

        ; 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) }
613

614 615 616 617 618 619 620 621 622
-- 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

623
tc_pat _ _other_pat _ _ = panic "tc_pat"        -- ConPatOut, SigPatOut
624 625

----------------
626
unifyPatType :: Outputable a => a -> TcType -> ExpSigmaType -> TcM TcCoercion
627 628 629 630
-- In patterns we want a coercion from the
-- context type (expected) to the actual pattern type
-- But we don't want to reverse the args to unifyType because
-- that controls the actual/expected stuff in error messages
631
unifyPatType thing actual_ty expected_ty
632
  = do { coi <- unifyExpType (Just thing) actual_ty expected_ty
633
       ; return (mkTcSymCo coi) }
634

Austin Seipp's avatar
Austin Seipp committed
635
{-
636 637 638 639
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.
640
        f ~(C x) = 3
641
We can't discharge the Num constraint from dictionaries bound by
642
the pattern C!
643

644
So we have to make the constraints from thing_inside "hop around"
645
the pattern.  Hence the captureConstraints and emitConstraints.
646 647 648

The same thing ensures that equality constraints in a lazy match
are not made available in the RHS of the match. For example
649 650 651
        data T a where { T1 :: Int -> T Int; ... }
        f :: T a -> Int -> a
        f ~(T1 i) y = y
652
It's obviously not sound to refine a to Int in the right
653
hand side, because the argument might not match T1 at all!
654 655 656 657

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

658

Austin Seipp's avatar
Austin Seipp committed
659 660
************************************************************************
*                                                                      *
661 662
        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
663 664
*                                                                      *
************************************************************************
665

666 667 668 669 670 671 672 673 674 675 676
[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 -> ...

677
As explained by [Wrappers for data instance tycons] in MkIds.hs, the
678 679 680 681 682 683 684 685 686 687 688 689 690 691 692
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}

693
In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
694

695
  Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}
696 697 698 699 700 701

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.

702
Now it might appear seem as if we could have used the previous GADT type
703 704 705 706 707 708 709 710 711 712 713 714
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.

715 716 717
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
718
-}
719

720
--      Running example:
721
-- MkT :: forall a b c. (a~[b]) => b -> c -> T a
722
--       with scrutinee of type (T ty)
723

724
tcConPat :: PatEnv -> Located Name
725
         -> ExpSigmaType           -- Type of the pattern
726 727
         -> HsConPatDetails Name -> TcM a
         -> TcM (Pat TcId, a)
cactus's avatar
cactus committed
728 729 730 731 732 733 734 735 736 737
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
738
             -> ExpSigmaType               -- Type of the pattern
739 740
             -> HsConPatDetails Name -> TcM a
             -> TcM (Pat TcId, a)
cactus's avatar
cactus committed
741
tcDataConPat penv (L con_span con_name) data_con pat_ty arg_pats thing_inside
742 743 744
  = do  { let tycon = dataConTyCon data_con
                  -- For data families this is the representation tycon
              (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _)
745
                = dataConFullSig data_con
cactus's avatar
cactus committed
746
              header = L con_span (RealDataCon data_con)
747

748 749 750
          -- 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
751
        ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty
752
        ; pat_ty <- readExpType pat_ty
753

754 755
          -- Add the stupid theta
        ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys
756

757 758
        ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ arg_tys
        ; checkExistentials ex_tvs all_arg_tys penv
759
        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX
niteria's avatar
niteria committed
760
                               (zipTvSubst univ_tvs ctxt_res_tys) ex_tvs
761 762
                     -- Get location from monad, not from ex_tvs

763
        ; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
764
              -- pat_ty' is type of the actual constructor application
765
              -- pat_ty' /= pat_ty iff coi /= IdCo
Simon Peyton Jones's avatar
Simon Peyton Jones committed
766

767
              arg_tys' = substTys tenv arg_tys
768

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
769 770 771
        ; traceTc "tcConPat" (vcat [ ppr con_name
                                   , pprTvBndrs univ_tvs
                                   , pprTvBndrs ex_tvs
772
                                   , ppr eq_spec
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
773 774 775 776
                                   , ppr theta
                                   , pprTvBndrs ex_tvs'
                                   , ppr ctxt_res_tys
                                   , ppr arg_tys'
777
                                   , ppr arg_pats ])
778 779
        ; if null ex_tvs && null eq_spec && null theta
          then do { -- The common case; no class bindings etc
780
                    -- (see Note [Arrows and patterns])
781 782 783 784
                    (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 = [],
785
                                              pat_binds = emptyTcEvBinds,
786
                                              pat_args = arg_pats',
787
                                              pat_arg_tys = ctxt_res_tys,
cactus's avatar
cactus committed
788
                                              pat_wrap = idHsWrapper }
789

790
                  ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
791

792
          else do   -- The general case, with existential,
793
                    -- and local equality constraints
794
        { let theta'     = substTheta tenv (eqSpecPreds eq_spec ++ theta)
795 796
                           -- order is *important* as we generate the list of
                           -- dictionary binders from theta'
797
              no_equalities = not (any isNomEqPred theta')
798 799 800 801
              skol_info = PatSkol (RealDataCon data_con) mc
              mc = case pe_ctxt penv of
                     LamPat mc -> mc
                     LetPat {} -> PatBindRhs
802

803 804
        ; gadts_on    <- xoptM LangExt.GADTs
        ; families_on <- xoptM LangExt.TypeFamilies
805
        ; checkTc (no_equalities || gadts_on || families_on)
sivteck's avatar
sivteck committed
806 807
                  (text "A pattern match on a GADT requires the" <+>
                   text "GADTs or TypeFamilies language extension")
808 809 810
                  -- Trac #2905 decided that a *pattern-match* of a GADT
                  -- should require the GADT language flag.
                  -- Re TypeFamilies see also #7156
811

812
        ; given <- newEvVars theta'
813
        ; (ev_binds, (arg_pats', res))
814
             <- checkConstraints skol_info ex_tvs' given $
cactus's avatar
cactus committed
815
                tcConArgs (RealDataCon data_con) arg_tys' arg_pats penv thing_inside
816

cactus's avatar
cactus committed
817
        ; let res_pat = ConPatOut { pat_con   = header,
818 819 820 821
                                    pat_tvs   = ex_tvs',
                                    pat_dicts = given,
                                    pat_binds = ev_binds,
                                    pat_args  = arg_pats',
822
                                    pat_arg_tys = ctxt_res_tys,
cactus's avatar
cactus committed
823
                                    pat_wrap  = idHsWrapper }
824 825
        ; return (mkHsWrapPat wrap res_pat pat_ty, res)
        } }
826

cactus's avatar
cactus committed
827
tcPatSynPat :: PatEnv -> Located Name -> PatSyn
828
            -> ExpSigmaType                -- Type of the pattern
829 830
            -> HsConPatDetails Name -> TcM a
            -> TcM (Pat TcId, a)
cactus's avatar
cactus committed
831
tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
832
  = do  { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn
cactus's avatar
cactus committed
833

834
        ; (subst, univ_tvs') <- newMetaTyVars univ_tvs
cactus's avatar
cactus committed
835

836 837
        ; let all_arg_tys = ty : prov_theta ++ arg_tys
        ; checkExistentials ex_tvs all_arg_tys penv
cactus's avatar
cactus committed
838
        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
839 840
        ; let ty'         = substTy tenv ty
              arg_tys'    = substTys tenv arg_tys
cactus's avatar
cactus committed
841
              prov_theta' = substTheta tenv prov_theta
842
              req_theta'  = substTheta tenv req_theta
cactus's avatar
cactus committed
843

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
844
        ; wrap <- tcSubTypeET (pe_orig penv) pat_ty ty'
cactus's avatar
cactus committed
845 846 847 848 849 850 851 852 853 854 855 856 857 858
        ; 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

859
        ; req_wrap <- instCall PatOrigin (mkTyVarTys univ_tvs') req_theta'
cactus's avatar
cactus committed
860 861
        ; traceTc "instCall" (ppr req_wrap)

862
        ; traceTc "checkConstraints {" Outputable.empty
cactus's avatar
cactus committed
863 864 865 866 867 868
        ; (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,
869 870 871 872
                                    pat_tvs   = ex_tvs',
                                    pat_dicts = prov_dicts',
                                    pat_binds = ev_binds,
                                    pat_args  = arg_pats',
873
                                    pat_arg_tys = mkTyVarTys univ_tvs',
cactus's avatar
cactus committed
874
                                    pat_wrap  = req_wrap }
875
        ; pat_ty <- readExpType pat_ty
876
        ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
cactus's avatar
cactus committed
877