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