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