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