TcPat.hs 48.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
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 TcRnMonad
23 24 25 26
import Inst
import Id
import Var
import Name
Adam Gundry's avatar
Adam Gundry committed
27
import RdrName
28 29
import TcEnv
import TcMType
30
import TcValidity( arityErr )
31 32 33 34
import TcType
import TcUnify
import TcHsType
import TysWiredIn
35
import TcEvidence
36 37
import TyCon
import DataCon
cactus's avatar
cactus committed
38 39
import PatSyn
import ConLike
40 41
import PrelNames
import BasicTypes hiding (SuccessFlag(..))
42
import DynFlags
43
import SrcLoc
44
import VarSet
45
import Util
sof's avatar
sof committed
46
import Outputable
47
import qualified GHC.LanguageExtensions as LangExt
Ian Lynagh's avatar
Ian Lynagh committed
48
import Control.Monad
49
import Control.Arrow  ( second )
50

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

59
tcLetPat :: (Name -> Maybe TcId)
60
         -> LPat Name -> ExpSigmaType
61 62
         -> TcM a
         -> TcM (LPat TcId, a)
63
tcLetPat sig_fn pat pat_ty thing_inside
64
  = tc_lpat pat pat_ty penv thing_inside
65
  where
66
    penv = PE { pe_lazy = True
67
              , pe_ctxt = LetPat sig_fn
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
68
              , pe_orig = PatOrigin }
69 70

-----------------
71
tcPats :: HsMatchContext Name
72
       -> [LPat Name]            -- Patterns,
73
       -> [ExpSigmaType]         --   and their types
74
       -> TcM a                  --   and the checker for the body
75
       -> TcM ([LPat TcId], a)
76 77 78

-- This is the externally-callable wrapper function
-- Typecheck the patterns, extend the environment to bind the variables,
79
-- do the thing inside, use any existentially-bound dictionaries to
80 81 82 83 84
-- discharge parts of the returning LIE, and deal with pattern type
-- signatures

--   1. Initialise the PatState
--   2. Check the patterns
85 86
--   3. Check the body
--   4. Check that no existentials escape
87

88
tcPats ctxt pats pat_tys thing_inside
89 90
  = tc_lpats penv pats pat_tys thing_inside
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
91
    penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
92

93
tcPat :: HsMatchContext Name
94
      -> LPat Name -> ExpSigmaType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
95
      -> TcM a                     -- Checker for body
96
      -> TcM (LPat TcId, a)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
97 98 99 100 101
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
102
        -> LPat Name -> ExpSigmaType
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
103 104 105
        -> TcM a                 -- Checker for body
        -> TcM (LPat TcId, a)
tcPat_O ctxt orig pat pat_ty thing_inside
106 107
  = tc_lpat pat pat_ty penv thing_inside
  where
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
108
    penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig }
109

110

111
-----------------
112
data PatEnv
113 114
  = 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
115
       , pe_orig :: CtOrigin    -- origin to use if the pat_ty needs inst'ing
116
       }
117 118 119

data PatCtxt
  = LamPat   -- Used for lambdas, case etc
120
       (HsMatchContext Name)
121

122
  | LetPat   -- Used only for let(rec) pattern bindings
123
             -- See Note [Typing patterns in pattern bindings]
124
       (Name -> Maybe TcId)    -- Tells the expected type for this binder
125

126 127 128
makeLazy :: PatEnv -> PatEnv
makeLazy penv = penv { pe_lazy = True }

129 130 131
inPatBind :: PatEnv -> Bool
inPatBind (PE { pe_ctxt = LetPat {} }) = True
inPatBind (PE { pe_ctxt = LamPat {} }) = False
132

133
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
134
*                                                                      *
135
                Binders
Austin Seipp's avatar
Austin Seipp committed
136
*                                                                      *
137
********************************************************************* -}
138

139
tcPatBndr :: PatEnv -> Name -> ExpSigmaType -> TcM (HsWrapper, TcId)
140 141 142
-- (coi, xp) = tcPatBndr penv x pat_ty
-- Then coi : pat_ty ~ typeof(xp)
--
143
tcPatBndr (PE { pe_ctxt = LetPat lookup_sig
144
              , pe_orig = orig }) bndr_name pat_ty
145
          -- See Note [Typing patterns in pattern bindings]
146 147 148 149
  | Just bndr_id <- lookup_sig bndr_name
  = do { wrap <- tcSubTypeET orig pat_ty (idType bndr_id)
       ; traceTc "tcPatBndr(lsl,sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr pat_ty)
       ; return (wrap, bndr_id) }
150

151 152
  | otherwise  -- No signature
  = pprPanic "tcPatBndr" (ppr bndr_name)
153 154

tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty
155
  = do { pat_ty <- expTypeToType pat_ty
156
       ; traceTc "tcPatBndr(not let)" (ppr bndr_name $$ ppr pat_ty)
157
       ; return (idHsWrapper, mkLocalId bndr_name pat_ty) }
158 159
               -- Whether or not there is a sig is irrelevant,
               -- as this is local
160

161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
{- Note [Partial signatures for pattern bindings]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider a function binding and a pattern binding, both
with a partial type signature

   f1 :: (True, _) -> Char
   f1 = \x -> x

   f2 :: (True, _) -> Char
   Just f2 = Just (\x->x)

Obviously, both should be rejected.  That happens naturally for the
function binding, f1, because we typecheck the RHS with "expected"
type '(True, apha) -> Char', which correctly fails.

But what of the pattern binding for f2?  We infer the type of the
pattern, and check tha the RHS has that type.  So we must feed in the
type of f2 when inferring the type of the pattern!  We do this right
here, in tcPatBndr, for a LetLclBndr. The signature already has fresh
unification variables for the wildcards (if any).

Extra notes

* For /complete/ type signatures, we could im principle ignore all this
  and just infer the most general type for f2, and check (in
  TcBinds.mkExport) whether it has the claimed type.

  But not so for /partial/ signatures; to get the wildcard unification
  variables into the game we really must inject them here. If we don't
  we never get /any/ value assigned to the wildcards; and programs that
  are bogus, like f2, are accepted.

  Moreover, by feeding in the expected type we do less fruitless
  creation of unification variables, and improve error messages.

* We need to do a subsumption, not equality, check.  If
      data T = MkT (forall a. a->a)
      f :: forall b. [b]->[b]
      MkT f = blah
  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.

205 206 207 208
Note [Typing patterns in pattern bindings]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are typing a pattern binding
    pat = rhs
209
Then the PatCtxt will be (LetPat sig_fn).
210 211 212

There can still be signatures for the binders:
     data T = MkT (forall a. a->a) Int
213
     x :: forall a. a->a
214 215 216 217 218 219 220 221 222 223
     y :: Int
     MkT x y = <rhs>

Two cases, dealt with by the LetPat case of tcPatBndr

 * If we are generalising (generalisation plan is InferGen or
   CheckGen), then the let_bndr_spec will be LetLclBndr.  In that case
   we want to bind a cloned, local version of the variable, with the
   type given by the pattern context, *not* by the signature (even if
   there is one; see Trac #7268). The mkExport part of the
Gabor Greif's avatar
Gabor Greif committed
224
   generalisation step will do the checking and impedance matching
225 226 227 228 229 230
   against the signature.

 * If for some some reason we are not generalising (plan = NoGen), the
   LetBndrSpec will be LetGblBndr.  In that case we must bind the
   global version of the Id, and do so with precisely the type given
   in the signature.  (Then we unify with the type from the pattern
231
   context type.)
232

233

Austin Seipp's avatar
Austin Seipp committed
234 235
************************************************************************
*                                                                      *
236
                The main worker functions
Austin Seipp's avatar
Austin Seipp committed
237 238
*                                                                      *
************************************************************************
239

240 241
Note [Nesting]
~~~~~~~~~~~~~~
lennart@augustsson.net's avatar
lennart@augustsson.net committed
242
tcPat takes a "thing inside" over which the pattern scopes.  This is partly
243
so that tcPat can extend the environment for the thing_inside, but also
244 245 246 247
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
248
want the error-context for the pattern to scope over the RHS.
249
Hence the getErrCtxt/setErrCtxt stuff in tcMultiple
Austin Seipp's avatar
Austin Seipp committed
250
-}
251 252

--------------------
253
type Checker inp out =  forall r.
254 255 256 257
                          inp
                       -> PatEnv
                       -> TcM r
                       -> TcM (out, r)
258 259

tcMultiple :: Checker inp out -> Checker [inp] [out]
260
tcMultiple tc_pat args penv thing_inside
261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276
  = 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 }
277 278

--------------------
279
tc_lpat :: LPat Name
280
        -> ExpSigmaType
281 282 283
        -> PatEnv
        -> TcM a
        -> TcM (LPat TcId, a)
284
tc_lpat (L span pat) pat_ty penv thing_inside
285
  = setSrcSpan span $
286
    do  { (pat', res) <- maybeWrapPatCtxt pat (tc_pat penv pat pat_ty)
287
                                          thing_inside
288
        ; return (L span pat', res) }
289 290

tc_lpats :: PatEnv
291
         -> [LPat Name] -> [ExpSigmaType]
292 293 294
         -> TcM a
         -> TcM ([LPat TcId], a)
tc_lpats penv pats tys thing_inside
Simon Peyton Jones's avatar
Simon Peyton Jones committed
295
  = ASSERT2( equalLength pats tys, ppr pats $$ ppr tys )
296
    tcMultiple (\(p,t) -> tc_lpat p t)
297
                (zipEqual "tc_lpats" pats tys)
298
                penv thing_inside
299 300

--------------------
301 302
tc_pat  :: PatEnv
        -> Pat Name
303
        -> ExpSigmaType  -- Fully refined result type
304 305 306
        -> TcM a                -- Thing inside
        -> TcM (Pat TcId,       -- Translated pattern
                a)              -- Result of thing inside
307

308
tc_pat penv (VarPat (L l name)) pat_ty thing_inside
309
  = do  { (wrap, id) <- tcPatBndr penv name pat_ty
batterseapower's avatar
batterseapower committed
310
        ; res <- tcExtendIdEnv1 name id thing_inside
311
        ; pat_ty <- readExpType pat_ty
312
        ; return (mkHsWrapPat wrap (VarPat (L l id)) pat_ty, res) }
313 314

tc_pat penv (ParPat pat) pat_ty thing_inside
315 316
  = do  { (pat', res) <- tc_lpat pat pat_ty penv thing_inside
        ; return (ParPat pat', res) }
317 318

tc_pat penv (BangPat pat) pat_ty thing_inside
319 320
  = do  { (pat', res) <- tc_lpat pat pat_ty penv thing_inside
        ; return (BangPat pat', res) }
321

322
tc_pat penv lpat@(LazyPat pat) pat_ty thing_inside
323 324 325 326
  = do  { (pat', (res, pat_ct))
                <- tc_lpat pat pat_ty (makeLazy penv) $
                   captureConstraints thing_inside
                -- Ignore refined penv', revert to penv
327

328 329
        ; emitConstraints pat_ct
        -- captureConstraints/extendConstraints:
330
        --   see Note [Hopping the LIE in lazy patterns]
331

332
        -- Check there are no unlifted types under the lazy pattern
Gabor Greif's avatar
Gabor Greif committed
333
        -- This is a very unsatisfactory test.  We have to zonk because
334 335 336 337 338 339 340 341 342
        -- 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)
343

344
        -- Check that the expected pattern type is itself lifted
345 346
        ; pat_ty <- readExpType pat_ty
        ; _ <- unifyType noThing (typeKind pat_ty) liftedTypeKind
347

348
        ; return (LazyPat pat', res) }
349

350
tc_pat _ (WildPat _) pat_ty thing_inside
351
  = do  { res <- thing_inside
352
        ; pat_ty <- expTypeToType pat_ty
353
        ; return (WildPat pat_ty, res) }
354

355
tc_pat penv (AsPat (L nm_loc name) pat) pat_ty thing_inside
356
  = do  { (wrap, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty)
batterseapower's avatar
batterseapower committed
357
        ; (pat', res) <- tcExtendIdEnv1 name bndr_id $
358 359
                         tc_lpat pat (mkCheckExpType $ idType bndr_id)
                                 penv thing_inside
360 361 362 363 364 365 366
            -- 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!
367
        ; pat_ty <- readExpType pat_ty
368
        ; return (mkHsWrapPat wrap (AsPat (L nm_loc bndr_id) pat') pat_ty, res) }
369 370 371

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

376 377 378 379 380 381 382 383
         -- 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
384
        ; expr_wrap2 <- tcSubTypeET (pe_orig penv) overall_pat_ty inf_arg_ty
385 386 387 388 389 390 391 392 393 394 395
            -- 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
396
        ; return (ViewPat (mkLHsWrap expr_wrap expr') pat' overall_pat_ty, res) }
397

398 399
-- Type signatures in patterns
-- See Note [Pattern coercions] below
400
tc_pat penv (SigPatIn pat sig_ty) pat_ty thing_inside
401
  = do  { (inner_ty, tv_binds, wcs, wrap) <- tcPatSig (inPatBind penv)
thomasw's avatar
thomasw committed
402
                                                            sig_ty pat_ty
403 404
        ; (pat', res) <- tcExtendTyVarEnv2 wcs     $
                         tcExtendTyVarEnv tv_binds $
405 406
                         tc_lpat pat (mkCheckExpType inner_ty) penv thing_inside
        ; pat_ty <- readExpType pat_ty
407
        ; return (mkHsWrapPat wrap (SigPatOut pat' inner_ty) pat_ty, res) }
408 409 410

------------------------
-- Lists, tuples, arrays
411
tc_pat penv (ListPat pats _ Nothing) pat_ty thing_inside
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
412
  = do  { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv pat_ty
413
        ; (pats', res) <- tcMultiple (\p -> tc_lpat p (mkCheckExpType elt_ty))
414
                                     pats penv thing_inside
415
        ; pat_ty <- readExpType pat_ty
416
        ; return (mkHsWrapPat coi (ListPat pats' elt_ty Nothing) pat_ty, res)
417 418 419
        }

tc_pat penv (ListPat pats _ (Just (_,e))) pat_ty thing_inside
420 421 422 423 424 425 426 427 428
  = 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)
429
        }
430

431
tc_pat penv (PArrPat pats _) pat_ty thing_inside
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
432
  = do  { (coi, elt_ty) <- matchExpectedPatTy matchExpectedPArrTy penv pat_ty
433
        ; (pats', res) <- tcMultiple (\p -> tc_lpat p (mkCheckExpType elt_ty))
434
                                     pats penv thing_inside
435
        ; pat_ty <- readExpType pat_ty
436
        ; return (mkHsWrapPat coi (PArrPat pats' elt_ty) pat_ty, res)
437
        }
438

439
tc_pat penv (TuplePat pats boxity _) pat_ty thing_inside
440 441
  = do  { let arity = length pats
              tc = tupleTyCon boxity arity
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
442 443
        ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc)
                                               penv pat_ty
444 445
                     -- Unboxed tuples have RuntimeRep vars, which we discard:
                     -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
446 447
        ; let con_arg_tys = case boxity of Unboxed -> drop arity arg_tys
                                           Boxed   -> arg_tys
448 449
        ; (pats', res) <- tc_lpats penv pats (map mkCheckExpType con_arg_tys)
                                   thing_inside
450

451
        ; dflags <- getDynFlags
452

453 454 455 456 457
        -- 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
458
              unmangled_result = TuplePat pats' boxity con_arg_tys
459
                                 -- pat_ty /= pat_ty iff coi /= IdCo
460 461
              possibly_mangled_result
                | gopt Opt_IrrefutableTuples dflags &&
462
                  isBoxed boxity            = LazyPat (noLoc unmangled_result)
463
                | otherwise                 = unmangled_result
464

465
        ; pat_ty <- readExpType pat_ty
466
        ; ASSERT( length con_arg_tys == length pats ) -- Syntactically enforced
467
          return (mkHsWrapPat coi possibly_mangled_result pat_ty, res)
468
        }
469 470 471

------------------------
-- Data constructors
472 473
tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside
  = tcConPat penv con pat_ty arg_pats thing_inside
474 475 476

------------------------
-- Literal patterns
477
tc_pat _ (LitPat simple_lit) pat_ty thing_inside
478
  = do  { let lit_ty = hsLitType simple_lit
479
        ; co <- unifyPatType simple_lit lit_ty pat_ty
480 481
                -- coi is of kind: pat_ty ~ lit_ty
        ; res <- thing_inside
482
        ; pat_ty <- readExpType pat_ty
483
        ; return ( mkHsWrapPatCo co (LitPat simple_lit) pat_ty
484
                 , res) }
485 486 487

------------------------
-- Overloaded patterns: n, and n+k
488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504

-- 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
505
  = do  { let orig = LiteralOrigin over_lit
506 507 508 509 510 511 512 513 514 515 516 517 518 519
        ; ((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)

520
        ; res <- thing_inside
521 522
        ; pat_ty <- readExpType pat_ty
        ; return (NPat (L l lit') mb_neg' eq' pat_ty, res) }
523

524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564
{-
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)
565
                  ; (wrap, bndr_id) <- setSrcSpan nm_loc $
566 567 568 569
                                     tcPatBndr penv name (mkCheckExpType var_ty)
                           -- co :: var_ty ~ idType bndr_id

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

572
        -- The Report says that n+k patterns must be in Integral
573 574 575 576
        -- 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]] }
577

578
        ; res <- tcExtendIdEnv1 name bndr_id thing_inside
579 580 581 582 583 584

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

586 587 588 589 590 591 592 593 594
-- 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

595
tc_pat _ _other_pat _ _ = panic "tc_pat"        -- ConPatOut, SigPatOut
596 597

----------------
598
unifyPatType :: Outputable a => a -> TcType -> ExpSigmaType -> TcM TcCoercion
599 600 601 602
-- 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
603
unifyPatType thing actual_ty expected_ty
604
  = do { coi <- unifyExpType (Just thing) actual_ty expected_ty
605
       ; return (mkTcSymCo coi) }
606

Austin Seipp's avatar
Austin Seipp committed
607
{-
608 609 610 611
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.
612
        f ~(C x) = 3
613
We can't discharge the Num constraint from dictionaries bound by
614
the pattern C!
615

616
So we have to make the constraints from thing_inside "hop around"
617
the pattern.  Hence the captureConstraints and emitConstraints.
618 619 620

The same thing ensures that equality constraints in a lazy match
are not made available in the RHS of the match. For example
621 622 623
        data T a where { T1 :: Int -> T Int; ... }
        f :: T a -> Int -> a
        f ~(T1 i) y = y
624
It's obviously not sound to refine a to Int in the right
625
hand side, because the argument might not match T1 at all!
626 627 628 629

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

630

Austin Seipp's avatar
Austin Seipp committed
631 632
************************************************************************
*                                                                      *
633 634
        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
635 636
*                                                                      *
************************************************************************
637

638 639 640 641 642 643 644 645 646 647 648
[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 -> ...

649
As explained by [Wrappers for data instance tycons] in MkIds.hs, the
650 651 652 653 654 655 656 657 658 659 660 661 662 663 664
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}

665
In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
666

667
  Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}
668 669 670 671 672 673

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.

674
Now it might appear seem as if we could have used the previous GADT type
675 676 677 678 679 680 681 682 683 684 685 686
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.

687 688 689
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
690
-}
691

692
--      Running example:
693
-- MkT :: forall a b c. (a~[b]) => b -> c -> T a
694
--       with scrutinee of type (T ty)
695

696
tcConPat :: PatEnv -> Located Name
697
         -> ExpSigmaType           -- Type of the pattern
698 699
         -> HsConPatDetails Name -> TcM a
         -> TcM (Pat TcId, a)
cactus's avatar
cactus committed
700 701 702 703 704 705 706 707 708 709
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
710
             -> ExpSigmaType               -- Type of the pattern
711 712
             -> HsConPatDetails Name -> TcM a
             -> TcM (Pat TcId, a)
cactus's avatar
cactus committed
713
tcDataConPat penv (L con_span con_name) data_con pat_ty arg_pats thing_inside
714 715 716
  = do  { let tycon = dataConTyCon data_con
                  -- For data families this is the representation tycon
              (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _)
717
                = dataConFullSig data_con
cactus's avatar
cactus committed
718
              header = L con_span (RealDataCon data_con)
719

720 721 722
          -- 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
723
        ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty
724
        ; pat_ty <- readExpType pat_ty
725

726 727
          -- Add the stupid theta
        ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys
728

729 730
        ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ arg_tys
        ; checkExistentials ex_tvs all_arg_tys penv
731
        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX
niteria's avatar
niteria committed
732
                               (zipTvSubst univ_tvs ctxt_res_tys) ex_tvs
733 734
                     -- Get location from monad, not from ex_tvs

735
        ; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
736
              -- pat_ty' is type of the actual constructor application
737
              -- pat_ty' /= pat_ty iff coi /= IdCo
Simon Peyton Jones's avatar
Simon Peyton Jones committed
738

739
              arg_tys' = substTys tenv arg_tys
740

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
741 742 743
        ; traceTc "tcConPat" (vcat [ ppr con_name
                                   , pprTvBndrs univ_tvs
                                   , pprTvBndrs ex_tvs
744
                                   , ppr eq_spec
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
745 746 747 748
                                   , ppr theta
                                   , pprTvBndrs ex_tvs'
                                   , ppr ctxt_res_tys
                                   , ppr arg_tys'
749
                                   , ppr arg_pats ])
750 751
        ; if null ex_tvs && null eq_spec && null theta
          then do { -- The common case; no class bindings etc
752
                    -- (see Note [Arrows and patterns])
753 754 755 756
                    (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 = [],
757
                                              pat_binds = emptyTcEvBinds,
758
                                              pat_args = arg_pats',
759
                                              pat_arg_tys = ctxt_res_tys,
cactus's avatar
cactus committed
760
                                              pat_wrap = idHsWrapper }
761

762
                  ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
763

764
          else do   -- The general case, with existential,
765
                    -- and local equality constraints
766
        { let theta'     = substTheta tenv (eqSpecPreds eq_spec ++ theta)
767 768
                           -- order is *important* as we generate the list of
                           -- dictionary binders from theta'
769
              no_equalities = not (any isNomEqPred theta')
770 771 772 773
              skol_info = PatSkol (RealDataCon data_con) mc
              mc = case pe_ctxt penv of
                     LamPat mc -> mc
                     LetPat {} -> PatBindRhs
774

775 776
        ; gadts_on    <- xoptM LangExt.GADTs
        ; families_on <- xoptM LangExt.TypeFamilies
777
        ; checkTc (no_equalities || gadts_on || families_on)
sivteck's avatar
sivteck committed
778 779
                  (text "A pattern match on a GADT requires the" <+>
                   text "GADTs or TypeFamilies language extension")
780 781 782
                  -- Trac #2905 decided that a *pattern-match* of a GADT
                  -- should require the GADT language flag.
                  -- Re TypeFamilies see also #7156
783

784
        ; given <- newEvVars theta'
785
        ; (ev_binds, (arg_pats', res))
786
             <- checkConstraints skol_info ex_tvs' given $
cactus's avatar
cactus committed
787
                tcConArgs (RealDataCon data_con) arg_tys' arg_pats penv thing_inside
788

cactus's avatar
cactus committed
789
        ; let res_pat = ConPatOut { pat_con   = header,
790 791 792 793
                                    pat_tvs   = ex_tvs',
                                    pat_dicts = given,
                                    pat_binds = ev_binds,
                                    pat_args  = arg_pats',
794
                                    pat_arg_tys = ctxt_res_tys,
cactus's avatar
cactus committed
795
                                    pat_wrap  = idHsWrapper }
796 797
        ; return (mkHsWrapPat wrap res_pat pat_ty, res)
        } }
798

cactus's avatar
cactus committed
799
tcPatSynPat :: PatEnv -> Located Name -> PatSyn
800
            -> ExpSigmaType                -- Type of the pattern
801 802
            -> HsConPatDetails Name -> TcM a
            -> TcM (Pat TcId, a)
cactus's avatar
cactus committed
803
tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
804
  = do  { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn
cactus's avatar
cactus committed
805

806
        ; (subst, univ_tvs') <- newMetaTyVars univ_tvs
cactus's avatar
cactus committed
807

808 809
        ; let all_arg_tys = ty : prov_theta ++ arg_tys
        ; checkExistentials ex_tvs all_arg_tys penv
cactus's avatar
cactus committed
810
        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
811 812
        ; let ty'         = substTy tenv ty
              arg_tys'    = substTys tenv arg_tys
cactus's avatar
cactus committed
813
              prov_theta' = substTheta tenv prov_theta
814
              req_theta'  = substTheta tenv req_theta
cactus's avatar
cactus committed
815

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
816
        ; wrap <- tcSubTypeET (pe_orig penv) pat_ty ty'
cactus's avatar
cactus committed
817 818 819 820 821 822 823 824 825 826 827 828 829 830
        ; 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

831
        ; req_wrap <- instCall PatOrigin (mkTyVarTys univ_tvs') req_theta'
cactus's avatar
cactus committed
832 833
        ; traceTc "instCall" (ppr req_wrap)

834
        ; traceTc "checkConstraints {" Outputable.empty
cactus's avatar
cactus committed
835 836 837 838 839 840
        ; (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,
841 842 843 844
                                    pat_tvs   = ex_tvs',
                                    pat_dicts = prov_dicts',
                                    pat_binds = ev_binds,
                                    pat_args  = arg_pats',
845
                                    pat_arg_tys = mkTyVarTys univ_tvs',
cactus's avatar
cactus committed
846
                                    pat_wrap  = req_wrap }
847
        ; pat_ty <- readExpType pat_ty
848
        ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
cactus's avatar
cactus committed
849

850
----------------------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
851 852
-- | Convenient wrapper for calling a matchExpectedXXX function
matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionN, a))
eir@cis.upenn.edu's avatar