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