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