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