Use lengthIs and friends in more places
[ghc.git] / compiler / typecheck / TcPat.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 TcPat: Typechecking patterns
7 -}
8
9 {-# LANGUAGE CPP, RankNTypes, TupleSections #-}
10 {-# LANGUAGE FlexibleContexts #-}
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 import HsSyn
21 import TcHsSyn
22 import TcSigs( TcPragEnv, lookupPragEnv, addInlinePrags )
23 import TcRnMonad
24 import Inst
25 import Id
26 import Var
27 import Name
28 import RdrName
29 import TcEnv
30 import TcMType
31 import TcValidity( arityErr )
32 import Type ( pprTyVars )
33 import TcType
34 import TcUnify
35 import TcHsType
36 import TysWiredIn
37 import TcEvidence
38 import TyCon
39 import DataCon
40 import PatSyn
41 import ConLike
42 import PrelNames
43 import BasicTypes hiding (SuccessFlag(..))
44 import DynFlags
45 import SrcLoc
46 import VarSet
47 import Util
48 import Outputable
49 import qualified GHC.LanguageExtensions as LangExt
50 import Control.Arrow ( second )
51 import ListSetOps ( getNth )
52
53 {-
54 ************************************************************************
55 * *
56 External interface
57 * *
58 ************************************************************************
59 -}
60
61 tcLetPat :: (Name -> Maybe TcId)
62 -> LetBndrSpec
63 -> LPat Name -> ExpSigmaType
64 -> TcM a
65 -> TcM (LPat TcId, a)
66 tcLetPat sig_fn no_gen pat pat_ty thing_inside
67 = do { bind_lvl <- getTcLevel
68 ; let ctxt = LetPat { pc_lvl = bind_lvl
69 , pc_sig_fn = sig_fn
70 , pc_new = no_gen }
71 penv = PE { pe_lazy = True
72 , pe_ctxt = ctxt
73 , pe_orig = PatOrigin }
74
75 ; 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 -- This is the externally-callable wrapper function
85 -- Typecheck the patterns, extend the environment to bind the variables,
86 -- do the thing inside, use any existentially-bound dictionaries to
87 -- discharge parts of the returning LIE, and deal with pattern type
88 -- signatures
89
90 -- 1. Initialise the PatState
91 -- 2. Check the patterns
92 -- 3. Check the body
93 -- 4. Check that no existentials escape
94
95 tcPats ctxt pats pat_tys thing_inside
96 = tc_lpats penv pats pat_tys thing_inside
97 where
98 penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
99
100 tcPat :: HsMatchContext Name
101 -> LPat Name -> ExpSigmaType
102 -> TcM a -- Checker for body
103 -> TcM (LPat TcId, a)
104 tcPat ctxt = tcPat_O ctxt PatOrigin
105
106 -- | A variant of 'tcPat' that takes a custom origin
107 tcPat_O :: HsMatchContext Name
108 -> CtOrigin -- ^ origin to use if the type needs inst'ing
109 -> LPat Name -> ExpSigmaType
110 -> TcM a -- Checker for body
111 -> TcM (LPat TcId, a)
112 tcPat_O ctxt orig pat pat_ty thing_inside
113 = tc_lpat pat pat_ty penv thing_inside
114 where
115 penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig }
116
117
118 {-
119 ************************************************************************
120 * *
121 PatEnv, PatCtxt, LetBndrSpec
122 * *
123 ************************************************************************
124 -}
125
126 data PatEnv
127 = PE { pe_lazy :: Bool -- True <=> lazy context, so no existentials allowed
128 , pe_ctxt :: PatCtxt -- Context in which the whole pattern appears
129 , pe_orig :: CtOrigin -- origin to use if the pat_ty needs inst'ing
130 }
131
132 data PatCtxt
133 = 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 { pc_lvl :: TcLevel
139 -- Level of the binding group
140
141 , pc_sig_fn :: Name -> Maybe TcId
142 -- Tells the expected type
143 -- for binders with a signature
144
145 , pc_new :: LetBndrSpec
146 -- How to make a new binder
147 } -- for binders without signatures
148
149 data LetBndrSpec
150 = LetLclBndr -- We are going to generalise, and wrap in an AbsBinds
151 -- so clone a fresh binder for the local monomorphic Id
152
153 | LetGblBndr TcPragEnv -- Generalisation plan is NoGen, so there isn't going
154 -- to be an AbsBinds; So we must bind the global version
155 -- of the binder right away.
156 -- And here is the inline-pragma information
157
158 instance Outputable LetBndrSpec where
159 ppr LetLclBndr = text "LetLclBndr"
160 ppr (LetGblBndr {}) = text "LetGblBndr"
161
162 makeLazy :: PatEnv -> PatEnv
163 makeLazy penv = penv { pe_lazy = True }
164
165 inPatBind :: PatEnv -> Bool
166 inPatBind (PE { pe_ctxt = LetPat {} }) = True
167 inPatBind (PE { pe_ctxt = LamPat {} }) = False
168
169 {- *********************************************************************
170 * *
171 Binders
172 * *
173 ********************************************************************* -}
174
175 tcPatBndr :: PatEnv -> Name -> ExpSigmaType -> TcM (HsWrapper, TcId)
176 -- (coi, xp) = tcPatBndr penv x pat_ty
177 -- Then coi : pat_ty ~ typeof(xp)
178 --
179 tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl = bind_lvl
180 , pc_sig_fn = sig_fn
181 , pc_new = no_gen } })
182 bndr_name exp_pat_ty
183 -- For the LetPat cases, see
184 -- Note [Typechecking pattern bindings] in TcBinds
185
186 | Just bndr_id <- sig_fn bndr_name -- There is a signature
187 = do { wrap <- tcSubTypePat penv exp_pat_ty (idType bndr_id)
188 -- See Note [Subsumption check at pattern variables]
189 ; traceTc "tcPatBndr(sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr exp_pat_ty)
190 ; return (wrap, bndr_id) }
191
192 | otherwise -- No signature
193 = do { (co, bndr_ty) <- case exp_pat_ty of
194 Check pat_ty -> promoteTcType bind_lvl pat_ty
195 Infer infer_res -> ASSERT( bind_lvl == ir_lvl infer_res )
196 -- If we were under a constructor that bumped
197 -- the level, we'd be in checking mode
198 do { bndr_ty <- inferResultToType infer_res
199 ; return (mkTcNomReflCo bndr_ty, bndr_ty) }
200 ; bndr_id <- newLetBndr no_gen bndr_name bndr_ty
201 ; traceTc "tcPatBndr(nosig)" (vcat [ ppr bind_lvl
202 , ppr exp_pat_ty, ppr bndr_ty, ppr co
203 , ppr bndr_id ])
204 ; return (mkWpCastN co, bndr_id) }
205
206 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 -- Whether or not there is a sig is irrelevant,
211 -- as this is local
212
213 newLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId
214 -- Make up a suitable Id for the pattern-binder.
215 -- See Note [Typechecking pattern bindings], item (4) in TcBinds
216 --
217 -- In the polymorphic case when we are going to generalise
218 -- (plan InferGen, no_gen = LetLclBndr), generate a "monomorphic version"
219 -- of the Id; the original name will be bound to the polymorphic version
220 -- by the AbsBinds
221 -- In the monomorphic case when we are not going to generalise
222 -- (plan NoGen, no_gen = LetGblBndr) there is no AbsBinds,
223 -- and we use the original name directly
224 newLetBndr LetLclBndr name ty
225 = do { mono_name <- cloneLocalName name
226 ; return (mkLocalId mono_name ty) }
227 newLetBndr (LetGblBndr prags) name ty
228 = addInlinePrags (mkLocalId name ty) (lookupPragEnv prags name)
229
230 tcSubTypePat :: PatEnv -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
231 -- tcSubTypeET with the UserTypeCtxt specialised to GenSigCtxt
232 -- Used when typechecking patterns
233 tcSubTypePat penv t1 t2 = tcSubTypeET (pe_orig penv) GenSigCtxt t1 t2
234
235 {- Note [Subsumption check at pattern variables]
236 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
237 When we come across a variable with a type signature, we need to do a
238 subsumption, not equality, check against the context type. e.g.
239
240 data T = MkT (forall a. a->a)
241 f :: forall b. [b]->[b]
242 MkT f = blah
243
244 Since 'blah' returns a value of type T, its payload is a polymorphic
245 function of type (forall a. a->a). And that's enough to bind the
246 less-polymorphic function 'f', but we need some impedance matching
247 to witness the instantiation.
248
249
250 ************************************************************************
251 * *
252 The main worker functions
253 * *
254 ************************************************************************
255
256 Note [Nesting]
257 ~~~~~~~~~~~~~~
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 so that constraints arising in the thing_inside can be discharged by the
261 pattern.
262
263 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
266 -}
267
268 --------------------
269 type Checker inp out = forall r.
270 inp
271 -> PatEnv
272 -> TcM r
273 -> TcM (out, r)
274
275 tcMultiple :: Checker inp out -> Checker [inp] [out]
276 tcMultiple tc_pat args penv thing_inside
277 = do { err_ctxt <- getErrCtxt
278 ; let loop _ []
279 = do { res <- thing_inside
280 ; return ([], res) }
281
282 loop penv (arg:args)
283 = do { (p', (ps', res))
284 <- tc_pat arg penv $
285 setErrCtxt err_ctxt $
286 loop penv args
287 -- setErrCtxt: restore context before doing the next pattern
288 -- See note [Nesting] above
289
290 ; return (p':ps', res) }
291
292 ; loop penv args }
293
294 --------------------
295 tc_lpat :: LPat Name
296 -> ExpSigmaType
297 -> PatEnv
298 -> TcM a
299 -> 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 -> TcM a
309 -> TcM ([LPat TcId], a)
310 tc_lpats penv pats tys thing_inside
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 tc_pat :: PatEnv
318 -> Pat Name
319 -> ExpSigmaType -- Fully refined result type
320 -> TcM a -- Thing inside
321 -> TcM (Pat TcId, -- Translated pattern
322 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
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 = do { (pat', res) <- tc_lpat pat pat_ty penv thing_inside
332 ; return (ParPat pat', res) }
333
334 tc_pat penv (BangPat pat) pat_ty thing_inside
335 = do { (pat', res) <- tc_lpat pat pat_ty penv thing_inside
336 ; return (BangPat pat', res) }
337
338 tc_pat penv (LazyPat pat) pat_ty thing_inside
339 = do { (pat', (res, pat_ct))
340 <- tc_lpat pat pat_ty (makeLazy penv) $
341 captureConstraints thing_inside
342 -- Ignore refined penv', revert to penv
343
344 ; emitConstraints pat_ct
345 -- captureConstraints/extendConstraints:
346 -- see Note [Hopping the LIE in lazy patterns]
347
348 -- Check that the expected pattern type is itself lifted
349 ; pat_ty <- readExpType pat_ty
350 ; _ <- 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)
361 ; (pat', res) <- tcExtendIdEnv1 name bndr_id $
362 tc_lpat pat (mkCheckExpType $ idType bndr_id)
363 penv thing_inside
364 -- NB: if we do inference on:
365 -- \ (y@(x::forall a. a->a)) = e
366 -- we'll fail. The as-pattern infers a monotype for 'y', which then
367 -- fails to unify with the polymorphic type for 'x'. This could
368 -- perhaps be fixed, but only with a bit more work.
369 --
370 -- 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 tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside
375 = do {
376 -- Expr must have type `forall a1...aN. OPT' -> B`
377 -- where overall_pat_ty is an instance of OPT'.
378 ; (expr',expr'_inferred) <- tcInferSigma expr
379
380 -- expression must be a function
381 ; let expr_orig = lexprCtOrigin expr
382 herald = text "A view pattern expression expects"
383 ; (expr_wrap1, [inf_arg_ty], inf_res_ty)
384 <- matchActualFunTys herald expr_orig (Just expr) 1 expr'_inferred
385 -- expr_wrap1 :: expr'_inferred "->" (inf_arg_ty -> inf_res_ty)
386
387 -- check that overall pattern is more polymorphic than arg type
388 ; expr_wrap2 <- tcSubTypePat penv overall_pat_ty inf_arg_ty
389 -- expr_wrap2 :: overall_pat_ty "->" inf_arg_ty
390
391 -- pattern must have inf_res_ty
392 ; (pat', res) <- tc_lpat pat (mkCheckExpType inf_res_ty) penv thing_inside
393
394 ; overall_pat_ty <- readExpType overall_pat_ty
395 ; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper
396 overall_pat_ty inf_res_ty doc
397 -- expr_wrap2' :: (inf_arg_ty -> inf_res_ty) "->"
398 -- (overall_pat_ty -> inf_res_ty)
399 expr_wrap = expr_wrap2' <.> expr_wrap1
400 doc = text "When checking the view pattern function:" <+> (ppr expr)
401 ; return (ViewPat (mkLHsWrap expr_wrap expr') pat' overall_pat_ty, res) }
402
403 -- Type signatures in patterns
404 -- 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)
407 sig_ty pat_ty
408 ; (pat', res) <- tcExtendTyVarEnv2 wcs $
409 tcExtendTyVarEnv tv_binds $
410 tc_lpat pat (mkCheckExpType inner_ty) penv thing_inside
411 ; 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
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 = do { tau_pat_ty <- expTypeToType pat_ty
426 ; ((pats', res, elt_ty), e')
427 <- tcSyntaxOpGen ListOrigin e [SynType (mkCheckExpType tau_pat_ty)]
428 SynList $
429 \ [elt_ty] ->
430 do { (pats', res) <- tcMultiple (\p -> tc_lpat p (mkCheckExpType elt_ty))
431 pats penv thing_inside
432 ; return (pats', res, elt_ty) }
433 ; return (ListPat pats' elt_ty (Just (tau_pat_ty,e')), res)
434 }
435
436 tc_pat penv (PArrPat pats _) pat_ty thing_inside
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 = do { let arity = length pats
446 tc = tupleTyCon boxity arity
447 ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc)
448 penv pat_ty
449 -- Unboxed tuples have RuntimeRep vars, which we discard:
450 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
451 ; let con_arg_tys = case boxity of Unboxed -> drop arity arg_tys
452 Boxed -> arg_tys
453 ; (pats', res) <- tc_lpats penv pats (map mkCheckExpType con_arg_tys)
454 thing_inside
455
456 ; dflags <- getDynFlags
457
458 -- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
459 -- so that we can experiment with lazy tuple-matching.
460 -- This is a pretty odd place to make the switch, but
461 -- it was easy to do.
462 ; let
463 unmangled_result = TuplePat pats' boxity con_arg_tys
464 -- pat_ty /= pat_ty iff coi /= IdCo
465 possibly_mangled_result
466 | gopt Opt_IrrefutableTuples dflags &&
467 isBoxed boxity = LazyPat (noLoc unmangled_result)
468 | otherwise = unmangled_result
469
470 ; pat_ty <- readExpType pat_ty
471 ; ASSERT( con_arg_tys `equalLength` pats ) -- Syntactically enforced
472 return (mkHsWrapPat coi possibly_mangled_result pat_ty, res)
473 }
474
475 tc_pat penv (SumPat pat alt arity _) pat_ty thing_inside
476 = do { let tc = sumTyCon arity
477 ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc)
478 penv pat_ty
479 ; -- Drop levity vars, we don't care about them here
480 let con_arg_tys = drop arity arg_tys
481 ; (pat', res) <- tc_lpat pat (mkCheckExpType (con_arg_tys `getNth` (alt - 1)))
482 penv thing_inside
483 ; pat_ty <- readExpType pat_ty
484 ; return (mkHsWrapPat coi (SumPat pat' alt arity con_arg_tys) pat_ty, res)
485 }
486
487 ------------------------
488 -- Data constructors
489 tc_pat penv (ConPatIn con arg_pats) pat_ty thing_inside
490 = 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 ; wrap <- tcSubTypePat penv pat_ty lit_ty
497 ; 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 -- In the case of a negative literal (the more complicated case),
506 -- we get
507 --
508 -- case v of (-5) -> blah
509 --
510 -- becoming
511 --
512 -- if v == (negate (fromInteger 5)) then blah else ...
513 --
514 -- There are two bits of rebindable syntax:
515 -- (==) :: pat_ty -> neg_lit_ty -> Bool
516 -- negate :: lit_ty -> neg_lit_ty
517 -- where lit_ty is the type of the overloaded literal 5.
518 --
519 -- When there is no negation, neg_lit_ty and lit_ty are the same
520 tc_pat _ (NPat (L l over_lit) mb_neg eq _) pat_ty thing_inside
521 = do { let orig = LiteralOrigin over_lit
522 ; ((lit', mb_neg'), eq')
523 <- tcSyntaxOp orig eq [SynType pat_ty, SynAny]
524 (mkCheckExpType boolTy) $
525 \ [neg_lit_ty] ->
526 let new_over_lit lit_ty = newOverloadedLit over_lit
527 (mkCheckExpType lit_ty)
528 in case mb_neg of
529 Nothing -> (, Nothing) <$> new_over_lit neg_lit_ty
530 Just neg -> -- Negative literal
531 -- The 'negate' is re-mappable syntax
532 second Just <$>
533 (tcSyntaxOp orig neg [SynRho] (mkCheckExpType neg_lit_ty) $
534 \ [lit_ty] -> new_over_lit lit_ty)
535
536 ; res <- thing_inside
537 ; pat_ty <- readExpType pat_ty
538 ; return (NPat (L l lit') mb_neg' eq' pat_ty, res) }
539
540 {-
541 Note [NPlusK patterns]
542 ~~~~~~~~~~~~~~~~~~~~~~
543 From
544
545 case v of x + 5 -> blah
546
547 we get
548
549 if v >= 5 then (\x -> blah) (v - 5) else ...
550
551 There are two bits of rebindable syntax:
552 (>=) :: pat_ty -> lit1_ty -> Bool
553 (-) :: pat_ty -> lit2_ty -> var_ty
554
555 lit1_ty and lit2_ty could conceivably be different.
556 var_ty is the type inferred for x, the variable in the pattern.
557
558 If the pushed-down pattern type isn't a tau-type, the two pat_ty's above
559 could conceivably be different specializations. But this is very much
560 like the situation in Note [Case branches must be taus] in TcMatches.
561 So we tauify the pat_ty before proceeding.
562
563 Note that we need to type-check the literal twice, because it is used
564 twice, and may be used at different types. The second HsOverLit stored in the
565 AST is used for the subtraction operation.
566 -}
567
568 -- See Note [NPlusK patterns]
569 tc_pat penv (NPlusKPat (L nm_loc name) (L loc lit) _ ge minus _) pat_ty thing_inside
570 = do { pat_ty <- expTypeToType pat_ty
571 ; let orig = LiteralOrigin lit
572 ; (lit1', ge')
573 <- tcSyntaxOp orig ge [synKnownType pat_ty, SynRho]
574 (mkCheckExpType boolTy) $
575 \ [lit1_ty] ->
576 newOverloadedLit lit (mkCheckExpType lit1_ty)
577 ; ((lit2', minus_wrap, bndr_id), minus')
578 <- tcSyntaxOpGen orig minus [synKnownType pat_ty, SynRho] SynAny $
579 \ [lit2_ty, var_ty] ->
580 do { lit2' <- newOverloadedLit lit (mkCheckExpType lit2_ty)
581 ; (wrap, bndr_id) <- setSrcSpan nm_loc $
582 tcPatBndr penv name (mkCheckExpType var_ty)
583 -- co :: var_ty ~ idType bndr_id
584
585 -- 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 -- but it's silly to insist on this in the RebindableSyntax case
590 ; unlessM (xoptM LangExt.RebindableSyntax) $
591 do { icls <- tcLookupClass integralClassName
592 ; instStupidTheta orig [mkClassPred icls [pat_ty]] }
593
594 ; res <- tcExtendIdEnv1 name bndr_id thing_inside
595
596 ; let minus'' = minus' { syn_res_wrap =
597 minus_wrap <.> syn_res_wrap minus' }
598 pat' = NPlusKPat (L nm_loc bndr_id) (L loc lit1') lit2'
599 ge' minus'' pat_ty
600 ; return (pat', res) }
601
602 -- HsSpliced is an annotation produced by 'RnSplice.rnSplicePat'.
603 -- Here we get rid of it and add the finalizers to the global environment.
604 --
605 -- See Note [Delaying modFinalizers in untyped splices] in RnSplice.
606 tc_pat penv (SplicePat (HsSpliced mod_finalizers (HsSplicedPat pat)))
607 pat_ty thing_inside
608 = do addModFinalizersWithLclEnv mod_finalizers
609 tc_pat penv pat pat_ty thing_inside
610
611 tc_pat _ _other_pat _ _ = panic "tc_pat" -- ConPatOut, SigPatOut
612
613
614 {-
615 Note [Hopping the LIE in lazy patterns]
616 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
617 In a lazy pattern, we must *not* discharge constraints from the RHS
618 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 The same thing ensures that equality constraints in a lazy match
627 are not made available in the RHS of the match. For example
628 data T a where { T1 :: Int -> T Int; ... }
629 f :: T a -> Int -> a
630 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 Finally, a lazy pattern should not bind any existential type variables
635 because they won't be in scope when we do the desugaring
636
637
638 ************************************************************************
639 * *
640 Most of the work for constructors is here
641 (the rest is in the ConPatIn case of tc_pat)
642 * *
643 ************************************************************************
644
645 [Pattern matching indexed data types]
646 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
647 Consider the following declarations:
648
649 data family Map k :: * -> *
650 data instance Map (a, b) v = MapPair (Map a (Pair b v))
651
652 and a case expression
653
654 case x :: Map (Int, c) w of MapPair m -> ...
655
656 As explained by [Wrappers for data instance tycons] in MkIds.hs, the
657 worker/wrapper types for MapPair are
658
659 $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
660 $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
661
662 So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
663 :R123Map, which means the straight use of boxySplitTyConApp would give a type
664 error. Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
665 boxySplitTyConApp with the family tycon Map instead, which gives us the family
666 type list {(Int, c), w}. To get the correct split for :R123Map, we need to
667 unify the family type list {(Int, c), w} with the instance types {(a, b), v}
668 (provided by tyConFamInst_maybe together with the family tycon). This
669 unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
670 the split arguments for the representation tycon :R123Map as {Int, c, w}
671
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 moving between representation and family type into account. To produce type
677 correct Core, this coercion needs to be used to case the type of the scrutinee
678 from the family to the representation type. This is achieved by
679 unwrapFamInstScrutinee using a CoPat around the result pattern.
680
681 Now it might appear seem as if we could have used the previous GADT type
682 refinement infrastructure of refineAlt and friends instead of the explicit
683 unification and CoPat generation. However, that would be wrong. Why? The
684 whole point of GADT refinement is that the refinement is local to the case
685 alternative. In contrast, the substitution generated by the unification of
686 the family type list and instance types needs to be propagated to the outside.
687 Imagine that in the above example, the type of the scrutinee would have been
688 (Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
689 substitution [x -> (a, b), v -> w]. In contrast to GADT matching, the
690 instantiation of x with (a, b) must be global; ie, it must be valid in *all*
691 alternatives of the case expression, whereas in the GADT case it might vary
692 between alternatives.
693
694 RIP GADT refinement: refinements have been replaced by the use of explicit
695 equality constraints that are used in conjunction with implication constraints
696 to express the local scope of GADT refinements.
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 -> HsConPatDetails Name -> TcM a
706 -> TcM (Pat TcId, a)
707 tcConPat penv con_lname@(L _ con_name) pat_ty arg_pats thing_inside
708 = do { con_like <- tcLookupConLike con_name
709 ; case con_like of
710 RealDataCon data_con -> tcDataConPat penv con_lname data_con
711 pat_ty arg_pats thing_inside
712 PatSynCon pat_syn -> tcPatSynPat penv con_lname pat_syn
713 pat_ty arg_pats thing_inside
714 }
715
716 tcDataConPat :: PatEnv -> Located Name -> DataCon
717 -> ExpSigmaType -- Type of the pattern
718 -> HsConPatDetails Name -> TcM a
719 -> TcM (Pat TcId, a)
720 tcDataConPat penv (L con_span con_name) data_con pat_ty arg_pats thing_inside
721 = do { let tycon = dataConTyCon data_con
722 -- For data families this is the representation tycon
723 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _)
724 = dataConFullSig data_con
725 header = L con_span (RealDataCon data_con)
726
727 -- Instantiate the constructor type variables [a->ty]
728 -- This may involve doing a family-instance coercion,
729 -- and building a wrapper
730 ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty
731 ; pat_ty <- readExpType pat_ty
732
733 -- Add the stupid theta
734 ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys
735
736 ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ arg_tys
737 ; checkExistentials ex_tvs all_arg_tys penv
738 ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX
739 (zipTvSubst univ_tvs ctxt_res_tys) ex_tvs
740 -- Get location from monad, not from ex_tvs
741
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
745
746 arg_tys' = substTys tenv arg_tys
747
748 ; traceTc "tcConPat" (vcat [ ppr con_name
749 , pprTyVars univ_tvs
750 , pprTyVars ex_tvs
751 , ppr eq_spec
752 , ppr theta
753 , pprTyVars ex_tvs'
754 , ppr ctxt_res_tys
755 , ppr arg_tys'
756 , ppr arg_pats ])
757 ; if null ex_tvs && null eq_spec && null theta
758 then do { -- The common case; no class bindings etc
759 -- (see Note [Arrows and patterns])
760 (arg_pats', res) <- tcConArgs (RealDataCon data_con) arg_tys'
761 arg_pats penv thing_inside
762 ; let res_pat = ConPatOut { pat_con = header,
763 pat_tvs = [], pat_dicts = [],
764 pat_binds = emptyTcEvBinds,
765 pat_args = arg_pats',
766 pat_arg_tys = ctxt_res_tys,
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 -- order is *important* as we generate the list of
775 -- dictionary binders from theta'
776 no_equalities = not (any isNomEqPred theta')
777 skol_info = PatSkol (RealDataCon data_con) mc
778 mc = case pe_ctxt penv of
779 LamPat mc -> mc
780 LetPat {} -> PatBindRhs
781
782 ; gadts_on <- xoptM LangExt.GADTs
783 ; families_on <- xoptM LangExt.TypeFamilies
784 ; checkTc (no_equalities || gadts_on || families_on)
785 (text "A pattern match on a GADT requires the" <+>
786 text "GADTs or TypeFamilies language extension")
787 -- Trac #2905 decided that a *pattern-match* of a GADT
788 -- should require the GADT language flag.
789 -- Re TypeFamilies see also #7156
790
791 ; given <- newEvVars theta'
792 ; (ev_binds, (arg_pats', res))
793 <- checkConstraints skol_info ex_tvs' given $
794 tcConArgs (RealDataCon data_con) arg_tys' arg_pats penv thing_inside
795
796 ; let res_pat = ConPatOut { pat_con = header,
797 pat_tvs = ex_tvs',
798 pat_dicts = given,
799 pat_binds = ev_binds,
800 pat_args = arg_pats',
801 pat_arg_tys = ctxt_res_tys,
802 pat_wrap = idHsWrapper }
803 ; return (mkHsWrapPat wrap res_pat pat_ty, res)
804 } }
805
806 tcPatSynPat :: PatEnv -> Located Name -> PatSyn
807 -> ExpSigmaType -- Type of the pattern
808 -> HsConPatDetails Name -> TcM a
809 -> TcM (Pat TcId, a)
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
812
813 ; (subst, univ_tvs') <- newMetaTyVars univ_tvs
814
815 ; let all_arg_tys = ty : prov_theta ++ arg_tys
816 ; checkExistentials ex_tvs all_arg_tys penv
817 ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
818 ; let ty' = substTy tenv ty
819 arg_tys' = substTys tenv arg_tys
820 prov_theta' = substTheta tenv prov_theta
821 req_theta' = substTheta tenv req_theta
822
823 ; wrap <- tcSubTypePat penv pat_ty ty'
824 ; traceTc "tcPatSynPat" (ppr pat_syn $$
825 ppr pat_ty $$
826 ppr ty' $$
827 ppr ex_tvs' $$
828 ppr prov_theta' $$
829 ppr req_theta' $$
830 ppr arg_tys')
831
832 ; prov_dicts' <- newEvVars prov_theta'
833
834 ; let skol_info = case pe_ctxt penv of
835 LamPat mc -> PatSkol (PatSynCon pat_syn) mc
836 LetPat {} -> UnkSkol -- Doesn't matter
837
838 ; req_wrap <- instCall PatOrigin (mkTyVarTys univ_tvs') req_theta'
839 ; traceTc "instCall" (ppr req_wrap)
840
841 ; traceTc "checkConstraints {" Outputable.empty
842 ; (ev_binds, (arg_pats', res))
843 <- checkConstraints skol_info ex_tvs' prov_dicts' $
844 tcConArgs (PatSynCon pat_syn) arg_tys' arg_pats penv thing_inside
845
846 ; traceTc "checkConstraints }" (ppr ev_binds)
847 ; let res_pat = ConPatOut { pat_con = L con_span $ PatSynCon pat_syn,
848 pat_tvs = ex_tvs',
849 pat_dicts = prov_dicts',
850 pat_binds = ev_binds,
851 pat_args = arg_pats',
852 pat_arg_tys = mkTyVarTys univ_tvs',
853 pat_wrap = req_wrap }
854 ; pat_ty <- readExpType pat_ty
855 ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
856
857 ----------------------------
858 -- | Convenient wrapper for calling a matchExpectedXXX function
859 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
863 matchExpectedPatTy inner_match (PE { pe_orig = orig }) pat_ty
864 = do { pat_ty <- expTypeToType pat_ty
865 ; (wrap, pat_rho) <- topInstantiate orig pat_ty
866 ; (co, res) <- inner_match pat_rho
867 ; traceTc "matchExpectedPatTy" (ppr pat_ty $$ ppr wrap)
868 ; return (mkWpCastN (mkTcSymCo co) <.> wrap, res) }
869
870 ----------------------------
871 matchExpectedConTy :: PatEnv
872 -> TyCon -- The TyCon that this data
873 -- constructor actually returns
874 -- In the case of a data family this is
875 -- the /representation/ TyCon
876 -> ExpSigmaType -- The type of the pattern; in the case
877 -- of a data family this would mention
878 -- the /family/ TyCon
879 -> TcM (HsWrapper, [TcSigmaType])
880 -- See Note [Matching constructor patterns]
881 -- Returns a wrapper : pat_ty "->" T ty1 ... tyn
882 matchExpectedConTy (PE { pe_orig = orig }) data_tc exp_pat_ty
883 | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc
884 -- Comments refer to Note [Matching constructor patterns]
885 -- co_tc :: forall a. T [a] ~ T7 a
886 = do { pat_ty <- expTypeToType exp_pat_ty
887 ; (wrap, pat_rho) <- topInstantiate orig pat_ty
888
889 ; (subst, tvs') <- newMetaTyVars (tyConTyVars data_tc)
890 -- tys = [ty1,ty2]
891
892 ; traceTc "matchExpectedConTy" (vcat [ppr data_tc,
893 ppr (tyConTyVars data_tc),
894 ppr fam_tc, ppr fam_args,
895 ppr exp_pat_ty,
896 ppr pat_ty,
897 ppr pat_rho, ppr wrap])
898 ; co1 <- unifyType noThing (mkTyConApp fam_tc (substTys subst fam_args)) pat_rho
899 -- co1 : T (ty1,ty2) ~N pat_rho
900 -- could use tcSubType here... but it's the wrong way round
901 -- for actual vs. expected in error messages.
902
903 ; let tys' = mkTyVarTys tvs'
904 co2 = mkTcUnbranchedAxInstCo co_tc tys' []
905 -- co2 : T (ty1,ty2) ~R T7 ty1 ty2
906
907 full_co = mkTcSubCo (mkTcSymCo co1) `mkTcTransCo` co2
908 -- full_co :: pat_rho ~R T7 ty1 ty2
909
910 ; return ( mkWpCastR full_co <.> wrap, tys') }
911
912 | otherwise
913 = do { pat_ty <- expTypeToType exp_pat_ty
914 ; (wrap, pat_rho) <- topInstantiate orig pat_ty
915 ; (coi, tys) <- matchExpectedTyConApp data_tc pat_rho
916 ; return (mkWpCastN (mkTcSymCo coi) <.> wrap, tys) }
917
918 {-
919 Note [Matching constructor patterns]
920 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
921 Suppose (coi, tys) = matchExpectedConType data_tc pat_ty
922
923 * In the simple case, pat_ty = tc tys
924
925 * If pat_ty is a polytype, we want to instantiate it
926 This is like part of a subsumption check. Eg
927 f :: (forall a. [a]) -> blah
928 f [] = blah
929
930 * In a type family case, suppose we have
931 data family T a
932 data instance T (p,q) = A p | B q
933 Then we'll have internally generated
934 data T7 p q = A p | B q
935 axiom coT7 p q :: T (p,q) ~ T7 p q
936
937 So if pat_ty = T (ty1,ty2), we return (coi, [ty1,ty2]) such that
938 coi = coi2 . coi1 : T7 t ~ pat_ty
939 coi1 : T (ty1,ty2) ~ pat_ty
940 coi2 : T7 ty1 ty2 ~ T (ty1,ty2)
941
942 For families we do all this matching here, not in the unifier,
943 because we never want a whisper of the data_tycon to appear in
944 error messages; it's a purely internal thing
945 -}
946
947 tcConArgs :: ConLike -> [TcSigmaType]
948 -> Checker (HsConPatDetails Name) (HsConPatDetails Id)
949
950 tcConArgs con_like arg_tys (PrefixCon arg_pats) penv thing_inside
951 = do { checkTc (con_arity == no_of_args) -- Check correct arity
952 (arityErr "constructor" con_like con_arity no_of_args)
953 ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
954 ; (arg_pats', res) <- tcMultiple tcConArg pats_w_tys
955 penv thing_inside
956 ; return (PrefixCon arg_pats', res) }
957 where
958 con_arity = conLikeArity con_like
959 no_of_args = length arg_pats
960
961 tcConArgs con_like arg_tys (InfixCon p1 p2) penv thing_inside
962 = do { checkTc (con_arity == 2) -- Check correct arity
963 (arityErr "constructor" con_like con_arity 2)
964 ; let [arg_ty1,arg_ty2] = arg_tys -- This can't fail after the arity check
965 ; ([p1',p2'], res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
966 penv thing_inside
967 ; return (InfixCon p1' p2', res) }
968 where
969 con_arity = conLikeArity con_like
970
971 tcConArgs con_like arg_tys (RecCon (HsRecFields rpats dd)) penv thing_inside
972 = do { (rpats', res) <- tcMultiple tc_field rpats penv thing_inside
973 ; return (RecCon (HsRecFields rpats' dd), res) }
974 where
975 tc_field :: Checker (LHsRecField Name (LPat Name))
976 (LHsRecField TcId (LPat TcId))
977 tc_field (L l (HsRecField (L loc (FieldOcc (L lr rdr) sel)) pat pun)) penv
978 thing_inside
979 = do { sel' <- tcLookupId sel
980 ; pat_ty <- setSrcSpan loc $ find_field_ty (occNameFS $ rdrNameOcc rdr)
981 ; (pat', res) <- tcConArg (pat, pat_ty) penv thing_inside
982 ; return (L l (HsRecField (L loc (FieldOcc (L lr rdr) sel')) pat'
983 pun), res) }
984
985 find_field_ty :: FieldLabelString -> TcM TcType
986 find_field_ty lbl
987 = case [ty | (fl, ty) <- field_tys, flLabel fl == lbl] of
988
989 -- No matching field; chances are this field label comes from some
990 -- other record type (or maybe none). If this happens, just fail,
991 -- otherwise we get crashes later (Trac #8570), and similar:
992 -- f (R { foo = (a,b) }) = a+b
993 -- If foo isn't one of R's fields, we don't want to crash when
994 -- typechecking the "a+b".
995 [] -> failWith (badFieldCon con_like lbl)
996
997 -- The normal case, when the field comes from the right constructor
998 (pat_ty : extras) -> do
999 traceTc "find_field" (ppr pat_ty <+> ppr extras)
1000 ASSERT( null extras ) (return pat_ty)
1001
1002 field_tys :: [(FieldLabel, TcType)]
1003 field_tys = zip (conLikeFieldLabels con_like) arg_tys
1004 -- Don't use zipEqual! If the constructor isn't really a record, then
1005 -- dataConFieldLabels will be empty (and each field in the pattern
1006 -- will generate an error below).
1007
1008 tcConArg :: Checker (LPat Name, TcSigmaType) (LPat Id)
1009 tcConArg (arg_pat, arg_ty) penv thing_inside
1010 = tc_lpat arg_pat (mkCheckExpType arg_ty) penv thing_inside
1011
1012 addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
1013 -- Instantiate the "stupid theta" of the data con, and throw
1014 -- the constraints into the constraint set
1015 addDataConStupidTheta data_con inst_tys
1016 | null stupid_theta = return ()
1017 | otherwise = instStupidTheta origin inst_theta
1018 where
1019 origin = OccurrenceOf (dataConName data_con)
1020 -- The origin should always report "occurrence of C"
1021 -- even when C occurs in a pattern
1022 stupid_theta = dataConStupidTheta data_con
1023 univ_tvs = dataConUnivTyVars data_con
1024 tenv = zipTvSubst univ_tvs (takeList univ_tvs inst_tys)
1025 -- NB: inst_tys can be longer than the univ tyvars
1026 -- because the constructor might have existentials
1027 inst_theta = substTheta tenv stupid_theta
1028
1029 {-
1030 Note [Arrows and patterns]
1031 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1032 (Oct 07) Arrow notation has the odd property that it involves
1033 "holes in the scope". For example:
1034 expr :: Arrow a => a () Int
1035 expr = proc (y,z) -> do
1036 x <- term -< y
1037 expr' -< x
1038
1039 Here the 'proc (y,z)' binding scopes over the arrow tails but not the
1040 arrow body (e.g 'term'). As things stand (bogusly) all the
1041 constraints from the proc body are gathered together, so constraints
1042 from 'term' will be seen by the tcPat for (y,z). But we must *not*
1043 bind constraints from 'term' here, because the desugarer will not make
1044 these bindings scope over 'term'.
1045
1046 The Right Thing is not to confuse these constraints together. But for
1047 now the Easy Thing is to ensure that we do not have existential or
1048 GADT constraints in a 'proc', and to short-cut the constraint
1049 simplification for such vanilla patterns so that it binds no
1050 constraints. Hence the 'fast path' in tcConPat; but it's also a good
1051 plan for ordinary vanilla patterns to bypass the constraint
1052 simplification step.
1053
1054 ************************************************************************
1055 * *
1056 Note [Pattern coercions]
1057 * *
1058 ************************************************************************
1059
1060 In principle, these program would be reasonable:
1061
1062 f :: (forall a. a->a) -> Int
1063 f (x :: Int->Int) = x 3
1064
1065 g :: (forall a. [a]) -> Bool
1066 g [] = True
1067
1068 In both cases, the function type signature restricts what arguments can be passed
1069 in a call (to polymorphic ones). The pattern type signature then instantiates this
1070 type. For example, in the first case, (forall a. a->a) <= Int -> Int, and we
1071 generate the translated term
1072 f = \x' :: (forall a. a->a). let x = x' Int in x 3
1073
1074 From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
1075 And it requires a significant amount of code to implement, because we need to decorate
1076 the translated pattern with coercion functions (generated from the subsumption check
1077 by tcSub).
1078
1079 So for now I'm just insisting on type *equality* in patterns. No subsumption.
1080
1081 Old notes about desugaring, at a time when pattern coercions were handled:
1082
1083 A SigPat is a type coercion and must be handled one at at time. We can't
1084 combine them unless the type of the pattern inside is identical, and we don't
1085 bother to check for that. For example:
1086
1087 data T = T1 Int | T2 Bool
1088 f :: (forall a. a -> a) -> T -> t
1089 f (g::Int->Int) (T1 i) = T1 (g i)
1090 f (g::Bool->Bool) (T2 b) = T2 (g b)
1091
1092 We desugar this as follows:
1093
1094 f = \ g::(forall a. a->a) t::T ->
1095 let gi = g Int
1096 in case t of { T1 i -> T1 (gi i)
1097 other ->
1098 let gb = g Bool
1099 in case t of { T2 b -> T2 (gb b)
1100 other -> fail }}
1101
1102 Note that we do not treat the first column of patterns as a
1103 column of variables, because the coerced variables (gi, gb)
1104 would be of different types. So we get rather grotty code.
1105 But I don't think this is a common case, and if it was we could
1106 doubtless improve it.
1107
1108 Meanwhile, the strategy is:
1109 * treat each SigPat coercion (always non-identity coercions)
1110 as a separate block
1111 * deal with the stuff inside, and then wrap a binding round
1112 the result to bind the new variable (gi, gb, etc)
1113
1114
1115 ************************************************************************
1116 * *
1117 \subsection{Errors and contexts}
1118 * *
1119 ************************************************************************
1120
1121 Note [Existential check]
1122 ~~~~~~~~~~~~~~~~~~~~~~~~
1123 Lazy patterns can't bind existentials. They arise in two ways:
1124 * Let bindings let { C a b = e } in b
1125 * Twiddle patterns f ~(C a b) = e
1126 The pe_lazy field of PatEnv says whether we are inside a lazy
1127 pattern (perhaps deeply)
1128
1129 See also Note [Typechecking pattern bindings] in TcBinds
1130 -}
1131
1132 maybeWrapPatCtxt :: Pat Name -> (TcM a -> TcM b) -> TcM a -> TcM b
1133 -- Not all patterns are worth pushing a context
1134 maybeWrapPatCtxt pat tcm thing_inside
1135 | not (worth_wrapping pat) = tcm thing_inside
1136 | otherwise = addErrCtxt msg $ tcm $ popErrCtxt thing_inside
1137 -- Remember to pop before doing thing_inside
1138 where
1139 worth_wrapping (VarPat {}) = False
1140 worth_wrapping (ParPat {}) = False
1141 worth_wrapping (AsPat {}) = False
1142 worth_wrapping _ = True
1143 msg = hang (text "In the pattern:") 2 (ppr pat)
1144
1145 -----------------------------------------------
1146 checkExistentials :: [TyVar] -- existentials
1147 -> [Type] -- argument types
1148 -> PatEnv -> TcM ()
1149 -- See Note [Existential check]]
1150 -- See Note [Arrows and patterns]
1151 checkExistentials ex_tvs tys _
1152 | all (not . (`elemVarSet` tyCoVarsOfTypes tys)) ex_tvs = return ()
1153 checkExistentials _ _ (PE { pe_ctxt = LetPat {}}) = return ()
1154 checkExistentials _ _ (PE { pe_ctxt = LamPat ProcExpr }) = failWithTc existentialProcPat
1155 checkExistentials _ _ (PE { pe_lazy = True }) = failWithTc existentialLazyPat
1156 checkExistentials _ _ _ = return ()
1157
1158 existentialLazyPat :: SDoc
1159 existentialLazyPat
1160 = hang (text "An existential or GADT data constructor cannot be used")
1161 2 (text "inside a lazy (~) pattern")
1162
1163 existentialProcPat :: SDoc
1164 existentialProcPat
1165 = text "Proc patterns cannot use existential or GADT data constructors"
1166
1167 badFieldCon :: ConLike -> FieldLabelString -> SDoc
1168 badFieldCon con field
1169 = hsep [text "Constructor" <+> quotes (ppr con),
1170 text "does not have field", quotes (ppr field)]
1171
1172 polyPatSig :: TcType -> SDoc
1173 polyPatSig sig_ty
1174 = hang (text "Illegal polymorphic type signature in pattern:")
1175 2 (ppr sig_ty)