TcPat.hs 48.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
import ListSetOps ( getNth )
51

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

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

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

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

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

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

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

111

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

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

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

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

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

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

140
tcPatBndr :: PatEnv -> Name -> ExpSigmaType -> TcM (HsWrapper, TcId)
141 142 143
-- (coi, xp) = tcPatBndr penv x pat_ty
-- Then coi : pat_ty ~ typeof(xp)
--
144
tcPatBndr (PE { pe_ctxt = LetPat lookup_sig
145
              , pe_orig = orig }) bndr_name pat_ty
146
          -- See Note [Typing patterns in pattern bindings]
147 148 149 150
  | 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) }
151

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

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

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

There can still be signatures for the binders:
     data T = MkT (forall a. a->a) Int
214
     x :: forall a. a->a
215 216 217 218 219 220 221 222 223 224
     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
225
   generalisation step will do the checking and impedance matching
226 227 228 229 230 231
   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
232
   context type.)
233

234

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

452
        ; dflags <- getDynFlags
453

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

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

471 472 473 474 475 476 477 478 479 480 481 482
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)
        }

483 484
------------------------
-- Data constructors
485 486
tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside
  = tcConPat penv con pat_ty arg_pats thing_inside
487 488 489

------------------------
-- Literal patterns
490
tc_pat _ (LitPat simple_lit) pat_ty thing_inside
491
  = do  { let lit_ty = hsLitType simple_lit
492
        ; co <- unifyPatType simple_lit lit_ty pat_ty
493 494
                -- coi is of kind: pat_ty ~ lit_ty
        ; res <- thing_inside
495
        ; pat_ty <- readExpType pat_ty
496
        ; return ( mkHsWrapPatCo co (LitPat simple_lit) pat_ty
497
                 , res) }
498 499 500

------------------------
-- Overloaded patterns: n, and n+k
501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517

-- 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
518
  = do  { let orig = LiteralOrigin over_lit
519 520 521 522 523 524 525 526 527 528 529 530 531 532
        ; ((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)

533
        ; res <- thing_inside
534 535
        ; pat_ty <- readExpType pat_ty
        ; return (NPat (L l lit') mb_neg' eq' pat_ty, res) }
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 565 566 567 568 569 570 571 572 573 574 575 576 577
{-
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)
578
                  ; (wrap, bndr_id) <- setSrcSpan nm_loc $
579 580 581 582
                                     tcPatBndr penv name (mkCheckExpType var_ty)
                           -- co :: var_ty ~ idType bndr_id

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

585
        -- The Report says that n+k patterns must be in Integral
586 587 588 589
        -- 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]] }
590

591
        ; res <- tcExtendIdEnv1 name bndr_id thing_inside
592 593 594 595 596 597

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

599 600 601 602 603 604 605 606 607
-- 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

608
tc_pat _ _other_pat _ _ = panic "tc_pat"        -- ConPatOut, SigPatOut
609 610

----------------
611
unifyPatType :: Outputable a => a -> TcType -> ExpSigmaType -> TcM TcCoercion
612 613 614 615
-- 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
616
unifyPatType thing actual_ty expected_ty
617
  = do { coi <- unifyExpType (Just thing) actual_ty expected_ty
618
       ; return (mkTcSymCo coi) }
619

Austin Seipp's avatar
Austin Seipp committed
620
{-
621 622 623 624
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.
625
        f ~(C x) = 3
626
We can't discharge the Num constraint from dictionaries bound by
627
the pattern C!
628

629
So we have to make the constraints from thing_inside "hop around"
630
the pattern.  Hence the captureConstraints and emitConstraints.
631 632 633

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

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

643

Austin Seipp's avatar
Austin Seipp committed
644 645
************************************************************************
*                                                                      *
646 647
        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
648 649
*                                                                      *
************************************************************************
650

651 652 653 654 655 656 657 658 659 660 661
[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 -> ...

662
As explained by [Wrappers for data instance tycons] in MkIds.hs, the
663 664 665 666 667 668 669 670 671 672 673 674 675 676 677
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}

678
In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
679

680
  Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}
681 682 683 684 685 686

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.

687
Now it might appear seem as if we could have used the previous GADT type
688 689 690 691 692 693 694 695 696 697 698 699
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.

700 701 702
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
703
-}
704

705
--      Running example:
706
-- MkT :: forall a b c. (a~[b]) => b -> c -> T a
707
--       with scrutinee of type (T ty)
708

709
tcConPat :: PatEnv -> Located Name
710
         -> ExpSigmaType           -- Type of the pattern
711 712
         -> HsConPatDetails Name -> TcM a
         -> TcM (Pat TcId, a)
cactus's avatar
cactus committed
713 714 715 716 717 718 719 720 721 722
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
723
             -> ExpSigmaType               -- Type of the pattern
724 725
             -> HsConPatDetails Name -> TcM a
             -> TcM (Pat TcId, a)
cactus's avatar
cactus committed
726
tcDataConPat penv (L con_span con_name) data_con pat_ty arg_pats thing_inside
727 728 729
  = do  { let tycon = dataConTyCon data_con
                  -- For data families this is the representation tycon
              (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _)
730
                = dataConFullSig data_con
cactus's avatar
cactus committed
731
              header = L con_span (RealDataCon data_con)
732

733 734 735
          -- 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
736
        ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty
737
        ; pat_ty <- readExpType pat_ty
738

739 740
          -- Add the stupid theta
        ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys
741

742 743
        ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ arg_tys
        ; checkExistentials ex_tvs all_arg_tys penv
744
        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX
niteria's avatar
niteria committed
745
                               (zipTvSubst univ_tvs ctxt_res_tys) ex_tvs
746 747
                     -- Get location from monad, not from ex_tvs

748
        ; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
749
              -- pat_ty' is type of the actual constructor application
750
              -- pat_ty' /= pat_ty iff coi /= IdCo
Simon Peyton Jones's avatar
Simon Peyton Jones committed
751

752
              arg_tys' = substTys tenv arg_tys
753

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
754 755 756
        ; traceTc "tcConPat" (vcat [ ppr con_name
                                   , pprTvBndrs univ_tvs
                                   , pprTvBndrs ex_tvs
757
                                   , ppr eq_spec
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
758 759 760 761
                                   , ppr theta
                                   , pprTvBndrs ex_tvs'
                                   , ppr ctxt_res_tys
                                   , ppr arg_tys'
762
                                   , ppr arg_pats ])
763 764
        ; if null ex_tvs && null eq_spec && null theta
          then do { -- The common case; no class bindings etc
765
                    -- (see Note [Arrows and patterns])
766 767 768 769
                    (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 = [],
770
                                              pat_binds = emptyTcEvBinds,
771
                                              pat_args = arg_pats',
772
                                              pat_arg_tys = ctxt_res_tys,
cactus's avatar
cactus committed
773
                                              pat_wrap = idHsWrapper }
774

775
                  ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
776

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

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

797
        ; given <- newEvVars theta'
798
        ; (ev_binds, (arg_pats', res))
799
             <- checkConstraints skol_info ex_tvs' given $
cactus's avatar
cactus committed
800
                tcConArgs (RealDataCon data_con) arg_tys' arg_pats penv thing_inside
801

cactus's avatar
cactus committed
802
        ; let res_pat = ConPatOut { pat_con   = header,
803 804 805 806
                                    pat_tvs   = ex_tvs',
                                    pat_dicts = given,
                                    pat_binds = ev_binds,
                                    pat_args  = arg_pats',
807
                                    pat_arg_tys = ctxt_res_tys,
cactus's avatar
cactus committed
808
                                    pat_wrap  = idHsWrapper }
809 810
        ; return (mkHsWrapPat wrap res_pat pat_ty, res)
        } }
811

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

819
        ; (subst, univ_tvs') <- newMetaTyVars univ_tvs
cactus's avatar
cactus committed
820

821 822
        ; let all_arg_tys = ty : prov_theta ++ arg_tys
        ; checkExistentials ex_tvs all_arg_tys penv
cactus's avatar
cactus committed
823
        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
824 825
        ; let ty'         = substTy tenv ty
              arg_tys'    = substTys tenv arg_tys
cactus's avatar
cactus committed
826
              prov_theta' = substTheta tenv prov_theta
827
              req_theta'  = substTheta tenv req_theta
cactus's avatar
cactus committed
828

eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
829
        ; wrap <- tcSubTypeET (pe_orig penv) pat_ty ty'
cactus's avatar
cactus committed
830 831 832 833 834 835 836 837 838 839 840 841 842 843
        ; 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

844
        ; req_wrap <- instCall PatOrigin (mkTyVarTys univ_tvs') req_theta'
cactus's avatar
cactus committed
845 846
        ; traceTc "instCall" (ppr req_wrap)

847
        ; traceTc "checkConstraints {" Outputable.empty
cactus's avatar
cactus committed
848 849 850 851 852 853
        ; (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,
854 855 856 857
                                    pat_tvs   = ex_tvs',
                                    pat_dicts = prov_dicts',
                                    pat_binds = ev_binds,
                                    pat_args  = arg_pats',
858
                                    pat_arg_tys = mkTyVarTys univ_tvs',
cactus's avatar
cactus committed