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

5 6

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

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

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

16
#include "HsVersions.h"
17

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

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

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

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

       ; tc_lpat pat pat_ty penv thing_inside }
76 77

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

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

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

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

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

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

117

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

249

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

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

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

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

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

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

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

        ; loop penv args }
293 294

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

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

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

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

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

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

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

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

348
        -- Check that the expected pattern type is itself lifted
349 350
        ; pat_ty <- readExpType pat_ty
        ; _ <- unifyType noThing (typeKind pat_ty) liftedTypeKind
351

352
        ; return (LazyPat pat', res) }
353

354
tc_pat _ (WildPat _) pat_ty thing_inside
355
  = do  { res <- thing_inside
356
        ; pat_ty <- expTypeToType pat_ty
357
        ; return (WildPat pat_ty, res) }
358

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

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

380 381 382 383 384 385 386 387
         -- 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
388
        ; expr_wrap2 <- tcSubTypePat penv overall_pat_ty inf_arg_ty
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
Richard Eisenberg's avatar
Richard Eisenberg committed
396
                                    overall_pat_ty inf_res_ty doc
397 398 399
               -- expr_wrap2' :: (inf_arg_ty -> inf_res_ty) "->"
               --                (overall_pat_ty -> inf_res_ty)
              expr_wrap = expr_wrap2' <.> expr_wrap1
Richard Eisenberg's avatar
Richard Eisenberg committed
400
              doc = text "When checking the view pattern function:" <+> (ppr expr)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
401
        ; return (ViewPat (mkLHsWrap expr_wrap expr') pat' overall_pat_ty, res) }
402

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

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

tc_pat penv (ListPat pats _ (Just (_,e))) pat_ty thing_inside
425 426 427 428 429 430 431 432 433
  = 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)
434
        }
435

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

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

456
        ; dflags <- getDynFlags
457

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

470
        ; pat_ty <- readExpType pat_ty
471
        ; ASSERT( length con_arg_tys == length pats ) -- Syntactically enforced
472
          return (mkHsWrapPat coi possibly_mangled_result pat_ty, res)
473
        }
474

475 476 477 478 479 480 481 482 483 484 485 486
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)
        }

487 488
------------------------
-- Data constructors
489 490
tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside
  = tcConPat penv con pat_ty arg_pats thing_inside
491 492 493

------------------------
-- Literal patterns
494
tc_pat penv (LitPat simple_lit) pat_ty thing_inside
495
  = do  { let lit_ty = hsLitType simple_lit
496 497
        ; wrap   <- tcSubTypePat penv pat_ty lit_ty
        ; res    <- thing_inside
498
        ; pat_ty <- readExpType pat_ty
499
        ; return ( mkHsWrapPat wrap (LitPat simple_lit) pat_ty
500
                 , res) }
501 502 503

------------------------
-- Overloaded patterns: n, and n+k
504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520

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

536
        ; res <- thing_inside
537 538
        ; pat_ty <- readExpType pat_ty
        ; return (NPat (L l lit') mb_neg' eq' pat_ty, res) }
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 578 579 580
{-
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)
581
                  ; (wrap, bndr_id) <- setSrcSpan nm_loc $
582 583 584 585
                                     tcPatBndr penv name (mkCheckExpType var_ty)
                           -- co :: var_ty ~ idType bndr_id

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

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

594
        ; res <- tcExtendIdEnv1 name bndr_id thing_inside
595 596 597 598 599 600

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

602 603 604 605 606 607 608 609 610
-- 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

611
tc_pat _ _other_pat _ _ = panic "tc_pat"        -- ConPatOut, SigPatOut
612

613

Austin Seipp's avatar
Austin Seipp committed
614
{-
615 616 617 618
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.
619
        f ~(C x) = 3
620
We can't discharge the Num constraint from dictionaries bound by
621
the pattern C!
622

623
So we have to make the constraints from thing_inside "hop around"
624
the pattern.  Hence the captureConstraints and emitConstraints.
625 626 627

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

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

637

Austin Seipp's avatar
Austin Seipp committed
638 639
************************************************************************
*                                                                      *
640 641
        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
642 643
*                                                                      *
************************************************************************
644

645 646 647 648 649 650 651 652 653 654 655
[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 -> ...

656
As explained by [Wrappers for data instance tycons] in MkIds.hs, the
657 658 659 660 661 662 663 664 665 666 667 668 669 670 671
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}

672
In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
673

674
  Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}
675 676 677 678 679 680

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.

681
Now it might appear seem as if we could have used the previous GADT type
682 683 684 685 686 687 688 689 690 691 692 693
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.

694 695 696
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
697
-}
698

699
--      Running example:
700
-- MkT :: forall a b c. (a~[b]) => b -> c -> T a
701
--       with scrutinee of type (T ty)
702

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

727 728 729
          -- 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
730
        ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty
731
        ; pat_ty <- readExpType pat_ty
732

733 734
          -- Add the stupid theta
        ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys
735

736 737
        ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ arg_tys
        ; checkExistentials ex_tvs all_arg_tys penv
738
        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX
niteria's avatar
niteria committed
739
                               (zipTvSubst univ_tvs ctxt_res_tys) ex_tvs
740 741
                     -- Get location from monad, not from ex_tvs

742
        ; let -- pat_ty' = mkTyConApp tycon ctxt_res_tys
743
              -- pat_ty' is type of the actual constructor application
744
              -- pat_ty' /= pat_ty iff coi /= IdCo
Simon Peyton Jones's avatar
Simon Peyton Jones committed
745

746
              arg_tys' = substTys tenv arg_tys
747

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

769
                  ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
770

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

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

791
        ; given <- newEvVars theta'
792
        ; (ev_binds, (arg_pats', res))
793
             <- checkConstraints skol_info ex_tvs' given $
cactus's avatar
cactus committed
794
                tcConArgs (RealDataCon data_con) arg_tys' arg_pats penv thing_inside
795

cactus's avatar
cactus committed
796
        ; let res_pat = ConPatOut { pat_con   = header,
797 798 799 800
                                    pat_tvs   = ex_tvs',
                                    pat_dicts = given,
                                    pat_binds = ev_binds,
                                    pat_args  = arg_pats',
801
                                    pat_arg_tys = ctxt_res_tys,
cactus's avatar
cactus committed
802
                                    pat_wrap  = idHsWrapper }
803 804
        ; return (mkHsWrapPat wrap res_pat pat_ty, res)
        } }
805

cactus's avatar
cactus committed
806
tcPatSynPat :: PatEnv -> Located Name -> PatSyn
807
            -> ExpSigmaType                -- Type of the pattern
808 809
            -> HsConPatDetails Name -> TcM a
            -> TcM (Pat TcId, a)
cactus's avatar
cactus committed
810
tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside
811
  = do  { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn
cactus's avatar
cactus committed
812

813
        ; (subst, univ_tvs') <- newMetaTyVars univ_tvs
cactus's avatar
cactus committed
814

815 816
        ; let all_arg_tys = ty : prov_theta ++ arg_tys
        ; checkExistentials ex_tvs all_arg_tys penv
cactus's avatar
cactus committed
817
        ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
818 819
        ; let ty'         = substTy tenv ty
              arg_tys'    = substTys tenv arg_tys
cactus's avatar
cactus committed
820
              prov_theta' = substTheta tenv prov_theta
821
              req_theta'  = substTheta tenv req_theta
cactus's avatar
cactus committed
822

823
        ; wrap <- tcSubTypePat penv pat_ty ty'
cactus's avatar
cactus committed
824 825 826 827 828 829 830 831 832 833 834 835 836 837
        ; 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

838
        ; req_wrap <- instCall PatOrigin (mkTyVarTys univ_tvs') req_theta'
cactus's avatar
cactus committed
839 840
        ; traceTc "instCall" (ppr req_wrap)

841
        ; traceTc "checkConstraints {" Outputable.empty
cactus's avatar
cactus committed
842 843 844 845 846 847
        ; (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,
848 849 850 851
                                    pat_tvs   = ex_tvs',
                                    pat_dicts = prov_dicts',
                                    pat_binds = ev_binds,
                                    pat_args  = arg_pats',
852
                                    pat_arg_tys = mkTyVarTys univ_tvs',
cactus's avatar
cactus committed
853
                                    pat_wrap  = req_wrap }
854
        ; pat_ty <- readExpType pat_ty
855
        ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
cactus's avatar
cactus committed
856

857
----------------------------
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
858 859
-- | Convenient wrapper for calling a matchExpectedXXX function
matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionN, a))
860
                    -> PatEnv -> ExpSigmaType -> TcM (HsWrapper, a)
861
-- See Note [Matching polytyped patterns]
862
-- Returns a wrapper : pat_ty ~R inner_ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
863
matchExpectedPatTy inner_match (PE { pe_orig = orig }) pat_ty
864 865
  = do { pat_ty <- expTypeToType pat_ty
       ; (wrap, pat_rho) <- topInstantiate orig pat_ty
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
866