TcPat.hs 47.7 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

tc_pat _ _other_pat _ _ = panic "tc_pat"        -- ConPatOut, SigPatOut
587 588

----------------
589
unifyPatType :: Outputable a => a -> TcType -> ExpSigmaType -> TcM TcCoercion
590 591 592 593
-- 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
594
unifyPatType thing actual_ty expected_ty
595
  = do { coi <- unifyExpType (Just thing) actual_ty expected_ty
596
       ; return (mkTcSymCo coi) }
597

Austin Seipp's avatar
Austin Seipp committed
598
{-
599 600 601 602
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.
603
        f ~(C x) = 3
604
We can't discharge the Num constraint from dictionaries bound by
605
the pattern C!
606

607
So we have to make the constraints from thing_inside "hop around"
608
the pattern.  Hence the captureConstraints and emitConstraints.
609 610 611

The same thing ensures that equality constraints in a lazy match
are not made available in the RHS of the match. For example
612 613 614
        data T a where { T1 :: Int -> T Int; ... }
        f :: T a -> Int -> a
        f ~(T1 i) y = y
615
It's obviously not sound to refine a to Int in the right
616
hand side, because the argument might not match T1 at all!
617 618 619 620

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

621

Austin Seipp's avatar
Austin Seipp committed
622 623
************************************************************************
*                                                                      *
624 625
        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
626 627
*                                                                      *
************************************************************************
628

629 630 631 632 633 634 635 636 637 638 639
[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 -> ...

640
As explained by [Wrappers for data instance tycons] in MkIds.hs, the
641 642 643 644 645 646 647 648 649 650 651 652 653 654 655
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}

656
In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
657

658
  Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}
659 660 661 662 663 664

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.

665
Now it might appear seem as if we could have used the previous GADT type
666 667 668 669 670 671 672 673 674 675 676 677
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.

678 679 680
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
681
-}
682

683
--      Running example:
684
-- MkT :: forall a b c. (a~[b]) => b -> c -> T a
685
--       with scrutinee of type (T ty)
686

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

711 712 713
          -- 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
714
        ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty
715
        ; pat_ty <- readExpType pat_ty
716

717 718
          -- Add the stupid theta
        ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys
719

720 721
        ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ arg_tys
        ; checkExistentials ex_tvs all_arg_tys penv
722
        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX
niteria's avatar
niteria committed
723
                               (zipTvSubst univ_tvs ctxt_res_tys) ex_tvs
724 725
                     -- Get location from monad, not from ex_tvs

726
        ; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
727
              -- pat_ty' is type of the actual constructor application
728
              -- pat_ty' /= pat_ty iff coi /= IdCo
Simon Peyton Jones's avatar
Simon Peyton Jones committed
729

730
              arg_tys' = substTys tenv arg_tys
731

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

753
                  ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
754

755
          else do   -- The general case, with existential,
756
                    -- and local equality constraints
757
        { let theta'     = substTheta tenv (eqSpecPreds eq_spec ++ theta)
758 759
                           -- order is *important* as we generate the list of
                           -- dictionary binders from theta'
760
              no_equalities = not (any isNomEqPred theta')
761 762 763 764
              skol_info = PatSkol (RealDataCon data_con) mc
              mc = case pe_ctxt penv of
                     LamPat mc -> mc
                     LetPat {} -> PatBindRhs
765

766 767
        ; gadts_on    <- xoptM LangExt.GADTs
        ; families_on <- xoptM LangExt.TypeFamilies
768
        ; checkTc (no_equalities || gadts_on || families_on)
sivteck's avatar
sivteck committed
769 770
                  (text "A pattern match on a GADT requires the" <+>
                   text "GADTs or TypeFamilies language extension")
771 772 773
                  -- Trac #2905 decided that a *pattern-match* of a GADT
                  -- should require the GADT language flag.
                  -- Re TypeFamilies see also #7156
774

775
        ; given <- newEvVars theta'
776
        ; (ev_binds, (arg_pats', res))
777
             <- checkConstraints skol_info ex_tvs' given $
cactus's avatar
cactus committed
778
                tcConArgs (RealDataCon data_con) arg_tys' arg_pats penv thing_inside
779

cactus's avatar
cactus committed
780
        ; let res_pat = ConPatOut { pat_con   = header,
781 782 783 784
                                    pat_tvs   = ex_tvs',
                                    pat_dicts = given,
                                    pat_binds = ev_binds,
                                    pat_args  = arg_pats',
785
                                    pat_arg_tys = ctxt_res_tys,
cactus's avatar
cactus committed
786
                                    pat_wrap  = idHsWrapper }
787 788
        ; return (mkHsWrapPat wrap res_pat pat_ty, res)
        } }
789

cactus's avatar
cactus committed
790
tcPatSynPat :: PatEnv -> Located Name -> PatSyn
791
            -> ExpSigmaType                -- Type of the pattern
792 793
            -> HsConPatDetails Name -> TcM a
            -> TcM (Pat TcId, a)
cactus's avatar
cactus committed
794
tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
795
  = do  { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn
cactus's avatar
cactus committed
796

797
        ; (subst, univ_tvs') <- newMetaTyVars univ_tvs
cactus's avatar
cactus committed
798

799 800
        ; let all_arg_tys = ty : prov_theta ++ arg_tys
        ; checkExistentials ex_tvs all_arg_tys penv
cactus's avatar
cactus committed
801
        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
802 803
        ; let ty'         = substTy tenv ty
              arg_tys'    = substTys tenv arg_tys
cactus's avatar
cactus committed
804
              prov_theta' = substTheta tenv prov_theta
805
              req_theta'  = substTheta tenv req_theta
cactus's avatar
cactus committed
806

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
807
        ; wrap <- tcSubTypeET (pe_orig penv) pat_ty ty'
cactus's avatar
cactus committed
808 809 810 811 812 813 814 815 816 817 818 819 820 821
        ; 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

822
        ; req_wrap <- instCall PatOrigin (mkTyVarTys univ_tvs') req_theta'
cactus's avatar
cactus committed
823 824
        ; traceTc "instCall" (ppr req_wrap)

825
        ; traceTc "checkConstraints {" Outputable.empty
cactus's avatar
cactus committed
826 827 828 829 830 831
        ; (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,
832 833 834 835
                                    pat_tvs   = ex_tvs',
                                    pat_dicts = prov_dicts',
                                    pat_binds = ev_binds,
                                    pat_args  = arg_pats',
836
                                    pat_arg_tys = mkTyVarTys univ_tvs',
cactus's avatar
cactus committed
837
                                    pat_wrap  = req_wrap }
838
        ; pat_ty <- readExpType pat_ty
839
        ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
cactus's avatar
cactus committed
840

841
----------------------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
842 843
-- | Convenient wrapper for calling a matchExpectedXXX function
matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionN, a))
844
                    -> PatEnv -> ExpSigmaType -> TcM (HsWrapper, a)
845
-- See Note [Matching polytyped patterns]
846
-- Returns a wrapper : pat_ty ~R inner_ty