never executed always true always false
1
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE LambdaCase #-}
4 {-# LANGUAGE RankNTypes #-}
5 {-# LANGUAGE TupleSections #-}
6 {-# LANGUAGE TypeFamilies #-}
7
8 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
9
10 {-
11 (c) The University of Glasgow 2006
12 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
13
14 -}
15
16 -- | Typechecking patterns
17 module GHC.Tc.Gen.Pat
18 ( tcLetPat
19 , newLetBndr
20 , LetBndrSpec(..)
21 , tcCheckPat, tcCheckPat_O, tcInferPat
22 , tcPats
23 , addDataConStupidTheta
24 , badFieldCon
25 , polyPatSig
26 )
27 where
28
29 import GHC.Prelude
30
31 import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferRho )
32
33 import GHC.Hs
34 import GHC.Hs.Syn.Type
35 import GHC.Rename.Utils
36 import GHC.Tc.Errors.Types
37 import GHC.Tc.Utils.Zonk
38 import GHC.Tc.Gen.Sig( TcPragEnv, lookupPragEnv, addInlinePrags )
39 import GHC.Tc.Utils.Concrete ( mkWpFun )
40 import GHC.Tc.Utils.Monad
41 import GHC.Tc.Utils.Instantiate
42 import GHC.Types.Error
43 import GHC.Types.Id
44 import GHC.Types.Var
45 import GHC.Types.Name
46 import GHC.Types.Name.Reader
47 import GHC.Core.Multiplicity
48 import GHC.Tc.Utils.Env
49 import GHC.Tc.Utils.TcMType
50 import GHC.Tc.Validity( arityErr )
51 import GHC.Core.TyCo.Ppr ( pprTyVars )
52 import GHC.Tc.Utils.TcType
53 import GHC.Tc.Utils.Unify
54 import GHC.Tc.Gen.HsType
55 import GHC.Builtin.Types
56 import GHC.Tc.Types.Evidence
57 import GHC.Tc.Types.Origin
58 import GHC.Core.TyCon
59 import GHC.Core.Type
60 import GHC.Core.DataCon
61 import GHC.Core.PatSyn
62 import GHC.Core.ConLike
63 import GHC.Builtin.Names
64 import GHC.Types.Basic hiding (SuccessFlag(..))
65 import GHC.Driver.Session
66 import GHC.Types.SrcLoc
67 import GHC.Types.Var.Set
68 import GHC.Utils.Misc
69 import GHC.Utils.Outputable as Outputable
70 import GHC.Utils.Panic
71 import GHC.Utils.Panic.Plain
72 import qualified GHC.LanguageExtensions as LangExt
73 import Control.Arrow ( second )
74 import Control.Monad
75 import GHC.Data.List.SetOps ( getNth )
76
77 {-
78 ************************************************************************
79 * *
80 External interface
81 * *
82 ************************************************************************
83 -}
84
85 tcLetPat :: (Name -> Maybe TcId)
86 -> LetBndrSpec
87 -> LPat GhcRn -> Scaled ExpSigmaType
88 -> TcM a
89 -> TcM (LPat GhcTc, a)
90 tcLetPat sig_fn no_gen pat pat_ty thing_inside
91 = do { bind_lvl <- getTcLevel
92 ; let ctxt = LetPat { pc_lvl = bind_lvl
93 , pc_sig_fn = sig_fn
94 , pc_new = no_gen }
95 penv = PE { pe_lazy = True
96 , pe_ctxt = ctxt
97 , pe_orig = PatOrigin }
98
99 ; tc_lpat pat_ty penv pat thing_inside }
100
101 -----------------
102 tcPats :: HsMatchContext GhcTc
103 -> [LPat GhcRn] -- Patterns,
104 -> [Scaled ExpSigmaType] -- and their types
105 -> TcM a -- and the checker for the body
106 -> TcM ([LPat GhcTc], a)
107
108 -- This is the externally-callable wrapper function
109 -- Typecheck the patterns, extend the environment to bind the variables,
110 -- do the thing inside, use any existentially-bound dictionaries to
111 -- discharge parts of the returning LIE, and deal with pattern type
112 -- signatures
113
114 -- 1. Initialise the PatState
115 -- 2. Check the patterns
116 -- 3. Check the body
117 -- 4. Check that no existentials escape
118
119 tcPats ctxt pats pat_tys thing_inside
120 = tc_lpats pat_tys penv pats thing_inside
121 where
122 penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
123
124 tcInferPat :: HsMatchContext GhcTc -> LPat GhcRn
125 -> TcM a
126 -> TcM ((LPat GhcTc, a), TcSigmaType)
127 tcInferPat ctxt pat thing_inside
128 = tcInfer $ \ exp_ty ->
129 tc_lpat (unrestricted exp_ty) penv pat thing_inside
130 where
131 penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
132
133 tcCheckPat :: HsMatchContext GhcTc
134 -> LPat GhcRn -> Scaled TcSigmaType
135 -> TcM a -- Checker for body
136 -> TcM (LPat GhcTc, a)
137 tcCheckPat ctxt = tcCheckPat_O ctxt PatOrigin
138
139 -- | A variant of 'tcPat' that takes a custom origin
140 tcCheckPat_O :: HsMatchContext GhcTc
141 -> CtOrigin -- ^ origin to use if the type needs inst'ing
142 -> LPat GhcRn -> Scaled TcSigmaType
143 -> TcM a -- Checker for body
144 -> TcM (LPat GhcTc, a)
145 tcCheckPat_O ctxt orig pat (Scaled pat_mult pat_ty) thing_inside
146 = tc_lpat (Scaled pat_mult (mkCheckExpType pat_ty)) penv pat thing_inside
147 where
148 penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig }
149
150
151 {-
152 ************************************************************************
153 * *
154 PatEnv, PatCtxt, LetBndrSpec
155 * *
156 ************************************************************************
157 -}
158
159 data PatEnv
160 = PE { pe_lazy :: Bool -- True <=> lazy context, so no existentials allowed
161 , pe_ctxt :: PatCtxt -- Context in which the whole pattern appears
162 , pe_orig :: CtOrigin -- origin to use if the pat_ty needs inst'ing
163 }
164
165 data PatCtxt
166 = LamPat -- Used for lambdas, case etc
167 (HsMatchContext GhcTc)
168
169 | LetPat -- Used only for let(rec) pattern bindings
170 -- See Note [Typing patterns in pattern bindings]
171 { pc_lvl :: TcLevel
172 -- Level of the binding group
173
174 , pc_sig_fn :: Name -> Maybe TcId
175 -- Tells the expected type
176 -- for binders with a signature
177
178 , pc_new :: LetBndrSpec
179 -- How to make a new binder
180 } -- for binders without signatures
181
182 data LetBndrSpec
183 = LetLclBndr -- We are going to generalise, and wrap in an AbsBinds
184 -- so clone a fresh binder for the local monomorphic Id
185
186 | LetGblBndr TcPragEnv -- Generalisation plan is NoGen, so there isn't going
187 -- to be an AbsBinds; So we must bind the global version
188 -- of the binder right away.
189 -- And here is the inline-pragma information
190
191 instance Outputable LetBndrSpec where
192 ppr LetLclBndr = text "LetLclBndr"
193 ppr (LetGblBndr {}) = text "LetGblBndr"
194
195 makeLazy :: PatEnv -> PatEnv
196 makeLazy penv = penv { pe_lazy = True }
197
198 inPatBind :: PatEnv -> Bool
199 inPatBind (PE { pe_ctxt = LetPat {} }) = True
200 inPatBind (PE { pe_ctxt = LamPat {} }) = False
201
202 {- *********************************************************************
203 * *
204 Binders
205 * *
206 ********************************************************************* -}
207
208 tcPatBndr :: PatEnv -> Name -> Scaled ExpSigmaType -> TcM (HsWrapper, TcId)
209 -- (coi, xp) = tcPatBndr penv x pat_ty
210 -- Then coi : pat_ty ~ typeof(xp)
211 --
212 tcPatBndr penv@(PE { pe_ctxt = LetPat { pc_lvl = bind_lvl
213 , pc_sig_fn = sig_fn
214 , pc_new = no_gen } })
215 bndr_name exp_pat_ty
216 -- For the LetPat cases, see
217 -- Note [Typechecking pattern bindings] in GHC.Tc.Gen.Bind
218
219 | Just bndr_id <- sig_fn bndr_name -- There is a signature
220 = do { wrap <- tc_sub_type penv (scaledThing exp_pat_ty) (idType bndr_id)
221 -- See Note [Subsumption check at pattern variables]
222 ; traceTc "tcPatBndr(sig)" (ppr bndr_id $$ ppr (idType bndr_id) $$ ppr exp_pat_ty)
223 ; return (wrap, bndr_id) }
224
225 | otherwise -- No signature
226 = do { (co, bndr_ty) <- case scaledThing exp_pat_ty of
227 Check pat_ty -> promoteTcType bind_lvl pat_ty
228 Infer infer_res -> assert (bind_lvl == ir_lvl infer_res) $
229 -- If we were under a constructor that bumped the
230 -- level, we'd be in checking mode (see tcConArg)
231 -- hence this assertion
232 do { bndr_ty <- inferResultToType infer_res
233 ; return (mkTcNomReflCo bndr_ty, bndr_ty) }
234 ; let bndr_mult = scaledMult exp_pat_ty
235 ; bndr_id <- newLetBndr no_gen bndr_name bndr_mult bndr_ty
236 ; traceTc "tcPatBndr(nosig)" (vcat [ ppr bind_lvl
237 , ppr exp_pat_ty, ppr bndr_ty, ppr co
238 , ppr bndr_id ])
239 ; return (mkWpCastN co, bndr_id) }
240
241 tcPatBndr _ bndr_name pat_ty
242 = do { let pat_mult = scaledMult pat_ty
243 ; pat_ty <- expTypeToType (scaledThing pat_ty)
244 ; traceTc "tcPatBndr(not let)" (ppr bndr_name $$ ppr pat_ty)
245 ; return (idHsWrapper, mkLocalIdOrCoVar bndr_name pat_mult pat_ty) }
246 -- We should not have "OrCoVar" here, this is a bug (#17545)
247 -- Whether or not there is a sig is irrelevant,
248 -- as this is local
249
250 newLetBndr :: LetBndrSpec -> Name -> Mult -> TcType -> TcM TcId
251 -- Make up a suitable Id for the pattern-binder.
252 -- See Note [Typechecking pattern bindings], item (4) in GHC.Tc.Gen.Bind
253 --
254 -- In the polymorphic case when we are going to generalise
255 -- (plan InferGen, no_gen = LetLclBndr), generate a "monomorphic version"
256 -- of the Id; the original name will be bound to the polymorphic version
257 -- by the AbsBinds
258 -- In the monomorphic case when we are not going to generalise
259 -- (plan NoGen, no_gen = LetGblBndr) there is no AbsBinds,
260 -- and we use the original name directly
261 newLetBndr LetLclBndr name w ty
262 = do { mono_name <- cloneLocalName name
263 ; return (mkLocalId mono_name w ty) }
264 newLetBndr (LetGblBndr prags) name w ty
265 = addInlinePrags (mkLocalId name w ty) (lookupPragEnv prags name)
266
267 tc_sub_type :: PatEnv -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
268 -- tcSubTypeET with the UserTypeCtxt specialised to GenSigCtxt
269 -- Used during typechecking patterns
270 tc_sub_type penv t1 t2 = tcSubTypePat (pe_orig penv) GenSigCtxt t1 t2
271
272 {- Note [Subsumption check at pattern variables]
273 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
274 When we come across a variable with a type signature, we need to do a
275 subsumption, not equality, check against the context type. e.g.
276
277 data T = MkT (forall a. a->a)
278 f :: forall b. [b]->[b]
279 MkT f = blah
280
281 Since 'blah' returns a value of type T, its payload is a polymorphic
282 function of type (forall a. a->a). And that's enough to bind the
283 less-polymorphic function 'f', but we need some impedance matching
284 to witness the instantiation.
285
286
287 ************************************************************************
288 * *
289 The main worker functions
290 * *
291 ************************************************************************
292
293 Note [Nesting]
294 ~~~~~~~~~~~~~~
295 tcPat takes a "thing inside" over which the pattern scopes. This is partly
296 so that tcPat can extend the environment for the thing_inside, but also
297 so that constraints arising in the thing_inside can be discharged by the
298 pattern.
299
300 This does not work so well for the ErrCtxt carried by the monad: we don't
301 want the error-context for the pattern to scope over the RHS.
302 Hence the getErrCtxt/setErrCtxt stuff in tcMultiple
303 -}
304
305 --------------------
306
307 type Checker inp out = forall r.
308 PatEnv
309 -> inp
310 -> TcM r -- Thing inside
311 -> TcM ( out
312 , r -- Result of thing inside
313 )
314
315 tcMultiple :: Checker inp out -> Checker [inp] [out]
316 tcMultiple tc_pat penv args thing_inside
317 = do { err_ctxt <- getErrCtxt
318 ; let loop _ []
319 = do { res <- thing_inside
320 ; return ([], res) }
321
322 loop penv (arg:args)
323 = do { (p', (ps', res))
324 <- tc_pat penv arg $
325 setErrCtxt err_ctxt $
326 loop penv args
327 -- setErrCtxt: restore context before doing the next pattern
328 -- See note [Nesting] above
329
330 ; return (p':ps', res) }
331
332 ; loop penv args }
333
334 --------------------
335 tc_lpat :: Scaled ExpSigmaType
336 -> Checker (LPat GhcRn) (LPat GhcTc)
337 tc_lpat pat_ty penv (L span pat) thing_inside
338 = setSrcSpanA span $
339 do { (pat', res) <- maybeWrapPatCtxt pat (tc_pat pat_ty penv pat)
340 thing_inside
341 ; return (L span pat', res) }
342
343 tc_lpats :: [Scaled ExpSigmaType]
344 -> Checker [LPat GhcRn] [LPat GhcTc]
345 tc_lpats tys penv pats
346 = assertPpr (equalLength pats tys) (ppr pats $$ ppr tys) $
347 tcMultiple (\ penv' (p,t) -> tc_lpat t penv' p)
348 penv
349 (zipEqual "tc_lpats" pats tys)
350
351 --------------------
352 -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
353 checkManyPattern :: Scaled a -> TcM HsWrapper
354 checkManyPattern pat_ty = tcSubMult NonLinearPatternOrigin Many (scaledMult pat_ty)
355
356 tc_pat :: Scaled ExpSigmaType
357 -- ^ Fully refined result type
358 -> Checker (Pat GhcRn) (Pat GhcTc)
359 -- ^ Translated pattern
360
361 tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
362
363 VarPat x (L l name) -> do
364 { (wrap, id) <- tcPatBndr penv name pat_ty
365 ; (res, mult_wrap) <- tcCheckUsage name (scaledMult pat_ty) $
366 tcExtendIdEnv1 name id thing_inside
367 -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
368 ; pat_ty <- readExpType (scaledThing pat_ty)
369 ; return (mkHsWrapPat (wrap <.> mult_wrap) (VarPat x (L l id)) pat_ty, res) }
370
371 ParPat x lpar pat rpar -> do
372 { (pat', res) <- tc_lpat pat_ty penv pat thing_inside
373 ; return (ParPat x lpar pat' rpar, res) }
374
375 BangPat x pat -> do
376 { (pat', res) <- tc_lpat pat_ty penv pat thing_inside
377 ; return (BangPat x pat', res) }
378
379 LazyPat x pat -> do
380 { mult_wrap <- checkManyPattern pat_ty
381 -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
382 ; (pat', (res, pat_ct))
383 <- tc_lpat pat_ty (makeLazy penv) pat $
384 captureConstraints thing_inside
385 -- Ignore refined penv', revert to penv
386
387 ; emitConstraints pat_ct
388 -- captureConstraints/extendConstraints:
389 -- see Note [Hopping the LIE in lazy patterns]
390
391 -- Check that the expected pattern type is itself lifted
392 ; pat_ty <- readExpType (scaledThing pat_ty)
393 ; _ <- unifyType Nothing (tcTypeKind pat_ty) liftedTypeKind
394
395 ; return (mkHsWrapPat mult_wrap (LazyPat x pat') pat_ty, res) }
396
397 WildPat _ -> do
398 { mult_wrap <- checkManyPattern pat_ty
399 -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
400 ; res <- thing_inside
401 ; pat_ty <- expTypeToType (scaledThing pat_ty)
402 ; return (mkHsWrapPat mult_wrap (WildPat pat_ty) pat_ty, res) }
403
404 AsPat x (L nm_loc name) pat -> do
405 { mult_wrap <- checkManyPattern pat_ty
406 -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
407 ; (wrap, bndr_id) <- setSrcSpanA nm_loc (tcPatBndr penv name pat_ty)
408 ; (pat', res) <- tcExtendIdEnv1 name bndr_id $
409 tc_lpat (pat_ty `scaledSet`(mkCheckExpType $ idType bndr_id))
410 penv pat thing_inside
411 -- NB: if we do inference on:
412 -- \ (y@(x::forall a. a->a)) = e
413 -- we'll fail. The as-pattern infers a monotype for 'y', which then
414 -- fails to unify with the polymorphic type for 'x'. This could
415 -- perhaps be fixed, but only with a bit more work.
416 --
417 -- If you fix it, don't forget the bindInstsOfPatIds!
418 ; pat_ty <- readExpType (scaledThing pat_ty)
419 ; return (mkHsWrapPat (wrap <.> mult_wrap) (AsPat x (L nm_loc bndr_id) pat') pat_ty, res) }
420
421 ViewPat _ expr pat -> do
422 { mult_wrap <- checkManyPattern pat_ty
423 -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
424 --
425 -- It should be possible to have view patterns at linear (or otherwise
426 -- non-Many) multiplicity. But it is not clear at the moment what
427 -- restriction need to be put in place, if any, for linear view
428 -- patterns to desugar to type-correct Core.
429
430 ; (expr',expr_ty) <- tcInferRho expr
431 -- Note [View patterns and polymorphism]
432
433 -- Expression must be a function
434 ; let herald = text "A view pattern expression expects"
435 ; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma)
436 <- matchActualFunTySigma herald (Just (ppr expr)) (1,[]) expr_ty
437 -- See Note [View patterns and polymorphism]
438 -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_sigma)
439
440 -- Check that overall pattern is more polymorphic than arg type
441 ; expr_wrap2 <- tc_sub_type penv (scaledThing pat_ty) inf_arg_ty
442 -- expr_wrap2 :: pat_ty "->" inf_arg_ty
443
444 -- Pattern must have inf_res_sigma
445 ; (pat', res) <- tc_lpat (pat_ty `scaledSet` mkCheckExpType inf_res_sigma) penv pat thing_inside
446
447 ; let Scaled w h_pat_ty = pat_ty
448 ; pat_ty <- readExpType h_pat_ty
449 ; expr_wrap2' <- mkWpFun expr_wrap2 idHsWrapper
450 (Scaled w pat_ty) inf_res_sigma (WpFunViewPat $ unLoc expr)
451 -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->"
452 -- (pat_ty -> inf_res_sigma)
453 ; let
454 expr_wrap = expr_wrap2' <.> expr_wrap1 <.> mult_wrap
455
456 ; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) }
457
458 {- Note [View patterns and polymorphism]
459 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
460 Consider this exotic example:
461 pair :: forall a. Bool -> a -> forall b. b -> (a,b)
462
463 f :: Int -> blah
464 f (pair True -> x) = ...here (x :: forall b. b -> (Int,b))
465
466 The expression (pair True) should have type
467 pair True :: Int -> forall b. b -> (Int,b)
468 so that it is ready to consume the incoming Int. It should be an
469 arrow type (t1 -> t2); hence using (tcInferRho expr).
470
471 Then, when taking that arrow apart we want to get a *sigma* type
472 (forall b. b->(Int,b)), because that's what we want to bind 'x' to.
473 Fortunately that's what matchExpectedFunTySigma returns anyway.
474 -}
475
476 -- Type signatures in patterns
477 -- See Note [Pattern coercions] below
478 SigPat _ pat sig_ty -> do
479 { (inner_ty, tv_binds, wcs, wrap) <- tcPatSig (inPatBind penv)
480 sig_ty (scaledThing pat_ty)
481 -- Using tcExtendNameTyVarEnv is appropriate here
482 -- because we're not really bringing fresh tyvars into scope.
483 -- We're *naming* existing tyvars. Note that it is OK for a tyvar
484 -- from an outer scope to mention one of these tyvars in its kind.
485 ; (pat', res) <- tcExtendNameTyVarEnv wcs $
486 tcExtendNameTyVarEnv tv_binds $
487 tc_lpat (pat_ty `scaledSet` mkCheckExpType inner_ty) penv pat thing_inside
488 ; pat_ty <- readExpType (scaledThing pat_ty)
489 ; return (mkHsWrapPat wrap (SigPat inner_ty pat' sig_ty) pat_ty, res) }
490
491 ------------------------
492 -- Lists, tuples, arrays
493
494 -- Necessarily a built-in list pattern, not an overloaded list pattern.
495 -- See Note [Desugaring overloaded list patterns].
496 ListPat _ pats -> do
497 { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv (scaledThing pat_ty)
498 ; (pats', res) <- tcMultiple (tc_lpat (pat_ty `scaledSet` mkCheckExpType elt_ty))
499 penv pats thing_inside
500 ; pat_ty <- readExpType (scaledThing pat_ty)
501 ; return (mkHsWrapPat coi
502 (ListPat elt_ty pats') pat_ty, res)
503 }
504
505 TuplePat _ pats boxity -> do
506 { let arity = length pats
507 tc = tupleTyCon boxity arity
508 -- NB: tupleTyCon does not flatten 1-tuples
509 -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make
510 ; checkTupSize arity
511 ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc)
512 penv (scaledThing pat_ty)
513 -- Unboxed tuples have RuntimeRep vars, which we discard:
514 -- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
515 ; let con_arg_tys = case boxity of Unboxed -> drop arity arg_tys
516 Boxed -> arg_tys
517 ; (pats', res) <- tc_lpats (map (scaledSet pat_ty . mkCheckExpType) con_arg_tys)
518 penv pats thing_inside
519
520 ; dflags <- getDynFlags
521
522 -- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
523 -- so that we can experiment with lazy tuple-matching.
524 -- This is a pretty odd place to make the switch, but
525 -- it was easy to do.
526 ; let
527 unmangled_result = TuplePat con_arg_tys pats' boxity
528 -- pat_ty /= pat_ty iff coi /= IdCo
529 possibly_mangled_result
530 | gopt Opt_IrrefutableTuples dflags &&
531 isBoxed boxity = LazyPat noExtField (noLocA unmangled_result)
532 | otherwise = unmangled_result
533
534 ; pat_ty <- readExpType (scaledThing pat_ty)
535 ; massert (con_arg_tys `equalLength` pats) -- Syntactically enforced
536 ; return (mkHsWrapPat coi possibly_mangled_result pat_ty, res)
537 }
538
539 SumPat _ pat alt arity -> do
540 { let tc = sumTyCon arity
541 ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc)
542 penv (scaledThing pat_ty)
543 ; -- Drop levity vars, we don't care about them here
544 let con_arg_tys = drop arity arg_tys
545 ; (pat', res) <- tc_lpat (pat_ty `scaledSet` mkCheckExpType (con_arg_tys `getNth` (alt - 1)))
546 penv pat thing_inside
547 ; pat_ty <- readExpType (scaledThing pat_ty)
548 ; return (mkHsWrapPat coi (SumPat con_arg_tys pat' alt arity) pat_ty
549 , res)
550 }
551
552 ------------------------
553 -- Data constructors
554 ConPat _ con arg_pats ->
555 tcConPat penv con pat_ty arg_pats thing_inside
556
557 ------------------------
558 -- Literal patterns
559 LitPat x simple_lit -> do
560 { let lit_ty = hsLitType simple_lit
561 ; wrap <- tc_sub_type penv (scaledThing pat_ty) lit_ty
562 ; res <- thing_inside
563 ; pat_ty <- readExpType (scaledThing pat_ty)
564 ; return ( mkHsWrapPat wrap (LitPat x (convertLit simple_lit)) pat_ty
565 , res) }
566
567 ------------------------
568 -- Overloaded patterns: n, and n+k
569
570 -- In the case of a negative literal (the more complicated case),
571 -- we get
572 --
573 -- case v of (-5) -> blah
574 --
575 -- becoming
576 --
577 -- if v == (negate (fromInteger 5)) then blah else ...
578 --
579 -- There are two bits of rebindable syntax:
580 -- (==) :: pat_ty -> neg_lit_ty -> Bool
581 -- negate :: lit_ty -> neg_lit_ty
582 -- where lit_ty is the type of the overloaded literal 5.
583 --
584 -- When there is no negation, neg_lit_ty and lit_ty are the same
585 NPat _ (L l over_lit) mb_neg eq -> do
586 { mult_wrap <- checkManyPattern pat_ty
587 -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
588 --
589 -- It may be possible to refine linear pattern so that they work in
590 -- linear environments. But it is not clear how useful this is.
591 ; let orig = LiteralOrigin over_lit
592 ; ((lit', mb_neg'), eq')
593 <- tcSyntaxOp orig eq [SynType (scaledThing pat_ty), SynAny]
594 (mkCheckExpType boolTy) $
595 \ [neg_lit_ty] _ ->
596 let new_over_lit lit_ty = newOverloadedLit over_lit
597 (mkCheckExpType lit_ty)
598 in case mb_neg of
599 Nothing -> (, Nothing) <$> new_over_lit neg_lit_ty
600 Just neg -> -- Negative literal
601 -- The 'negate' is re-mappable syntax
602 second Just <$>
603 (tcSyntaxOp orig neg [SynRho] (mkCheckExpType neg_lit_ty) $
604 \ [lit_ty] _ -> new_over_lit lit_ty)
605 -- applied to a closed literal: linearity doesn't matter as
606 -- literals are typed in an empty environment, hence have
607 -- all multiplicities.
608
609 ; res <- thing_inside
610 ; pat_ty <- readExpType (scaledThing pat_ty)
611 ; return (mkHsWrapPat mult_wrap (NPat pat_ty (L l lit') mb_neg' eq') pat_ty, res) }
612
613 {-
614 Note [NPlusK patterns]
615 ~~~~~~~~~~~~~~~~~~~~~~
616 From
617
618 case v of x + 5 -> blah
619
620 we get
621
622 if v >= 5 then (\x -> blah) (v - 5) else ...
623
624 There are two bits of rebindable syntax:
625 (>=) :: pat_ty -> lit1_ty -> Bool
626 (-) :: pat_ty -> lit2_ty -> var_ty
627
628 lit1_ty and lit2_ty could conceivably be different.
629 var_ty is the type inferred for x, the variable in the pattern.
630
631 Note that we need to type-check the literal twice, because it is used
632 twice, and may be used at different types. The second HsOverLit stored in the
633 AST is used for the subtraction operation.
634 -}
635
636 -- See Note [NPlusK patterns]
637 NPlusKPat _ (L nm_loc name)
638 (L loc lit) _ ge minus -> do
639 { mult_wrap <- checkManyPattern pat_ty
640 -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
641 ; let pat_exp_ty = scaledThing pat_ty
642 orig = LiteralOrigin lit
643 ; (lit1', ge')
644 <- tcSyntaxOp orig ge [SynType pat_exp_ty, SynRho]
645 (mkCheckExpType boolTy) $
646 \ [lit1_ty] _ ->
647 newOverloadedLit lit (mkCheckExpType lit1_ty)
648 ; ((lit2', minus_wrap, bndr_id), minus')
649 <- tcSyntaxOpGen orig minus [SynType pat_exp_ty, SynRho] SynAny $
650 \ [lit2_ty, var_ty] _ ->
651 do { lit2' <- newOverloadedLit lit (mkCheckExpType lit2_ty)
652 ; (wrap, bndr_id) <- setSrcSpanA nm_loc $
653 tcPatBndr penv name (unrestricted $ mkCheckExpType var_ty)
654 -- co :: var_ty ~ idType bndr_id
655
656 -- minus_wrap is applicable to minus'
657 ; return (lit2', wrap, bndr_id) }
658
659 ; pat_ty <- readExpType pat_exp_ty
660
661 -- The Report says that n+k patterns must be in Integral
662 -- but it's silly to insist on this in the RebindableSyntax case
663 ; unlessM (xoptM LangExt.RebindableSyntax) $
664 do { icls <- tcLookupClass integralClassName
665 ; instStupidTheta orig [mkClassPred icls [pat_ty]] }
666
667 ; res <- tcExtendIdEnv1 name bndr_id thing_inside
668
669 ; let minus'' = case minus' of
670 NoSyntaxExprTc -> pprPanic "tc_pat NoSyntaxExprTc" (ppr minus')
671 -- this should be statically avoidable
672 -- Case (3) from Note [NoSyntaxExpr] in "GHC.Hs.Expr"
673 SyntaxExprTc { syn_expr = minus'_expr
674 , syn_arg_wraps = minus'_arg_wraps
675 , syn_res_wrap = minus'_res_wrap }
676 -> SyntaxExprTc { syn_expr = minus'_expr
677 , syn_arg_wraps = minus'_arg_wraps
678 , syn_res_wrap = minus_wrap <.> minus'_res_wrap }
679 -- Oy. This should really be a record update, but
680 -- we get warnings if we try. #17783
681 pat' = NPlusKPat pat_ty (L nm_loc bndr_id) (L loc lit1') lit2'
682 ge' minus''
683 ; return (mkHsWrapPat mult_wrap pat' pat_ty, res) }
684
685 -- HsSpliced is an annotation produced by 'GHC.Rename.Splice.rnSplicePat'.
686 -- Here we get rid of it and add the finalizers to the global environment.
687 --
688 -- See Note [Delaying modFinalizers in untyped splices] in GHC.Rename.Splice.
689 SplicePat _ splice -> case splice of
690 (HsSpliced _ mod_finalizers (HsSplicedPat pat)) -> do
691 { addModFinalizersWithLclEnv mod_finalizers
692 ; tc_pat pat_ty penv pat thing_inside }
693 _ -> panic "invalid splice in splice pat"
694
695 XPat (HsPatExpanded lpat rpat) -> do
696 { (rpat', res) <- tc_pat pat_ty penv rpat thing_inside
697 ; return (XPat $ ExpansionPat lpat rpat', res) }
698
699 {-
700 Note [Hopping the LIE in lazy patterns]
701 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
702 In a lazy pattern, we must *not* discharge constraints from the RHS
703 from dictionaries bound in the pattern. E.g.
704 f ~(C x) = 3
705 We can't discharge the Num constraint from dictionaries bound by
706 the pattern C!
707
708 So we have to make the constraints from thing_inside "hop around"
709 the pattern. Hence the captureConstraints and emitConstraints.
710
711 The same thing ensures that equality constraints in a lazy match
712 are not made available in the RHS of the match. For example
713 data T a where { T1 :: Int -> T Int; ... }
714 f :: T a -> Int -> a
715 f ~(T1 i) y = y
716 It's obviously not sound to refine a to Int in the right
717 hand side, because the argument might not match T1 at all!
718
719 Finally, a lazy pattern should not bind any existential type variables
720 because they won't be in scope when we do the desugaring
721
722
723 ************************************************************************
724 * *
725 Pattern signatures (pat :: type)
726 * *
727 ************************************************************************
728 -}
729
730 tcPatSig :: Bool -- True <=> pattern binding
731 -> HsPatSigType GhcRn
732 -> ExpSigmaType
733 -> TcM (TcType, -- The type to use for "inside" the signature
734 [(Name,TcTyVar)], -- The new bit of type environment, binding
735 -- the scoped type variables
736 [(Name,TcTyVar)], -- The wildcards
737 HsWrapper) -- Coercion due to unification with actual ty
738 -- Of shape: res_ty ~ sig_ty
739 tcPatSig in_pat_bind sig res_ty
740 = do { (sig_wcs, sig_tvs, sig_ty) <- tcHsPatSigType PatSigCtxt HM_Sig sig OpenKind
741 -- sig_tvs are the type variables free in 'sig',
742 -- and not already in scope. These are the ones
743 -- that should be brought into scope
744
745 ; if null sig_tvs then do {
746 -- Just do the subsumption check and return
747 wrap <- addErrCtxtM (mk_msg sig_ty) $
748 tcSubTypePat PatSigOrigin PatSigCtxt res_ty sig_ty
749 ; return (sig_ty, [], sig_wcs, wrap)
750 } else do
751 -- Type signature binds at least one scoped type variable
752
753 -- A pattern binding cannot bind scoped type variables
754 -- It is more convenient to make the test here
755 -- than in the renamer
756 { when in_pat_bind (addErr (patBindSigErr sig_tvs))
757
758 -- Now do a subsumption check of the pattern signature against res_ty
759 ; wrap <- addErrCtxtM (mk_msg sig_ty) $
760 tcSubTypePat PatSigOrigin PatSigCtxt res_ty sig_ty
761
762 -- Phew!
763 ; return (sig_ty, sig_tvs, sig_wcs, wrap)
764 } }
765 where
766 mk_msg sig_ty tidy_env
767 = do { (tidy_env, sig_ty) <- zonkTidyTcType tidy_env sig_ty
768 ; res_ty <- readExpType res_ty -- should be filled in by now
769 ; (tidy_env, res_ty) <- zonkTidyTcType tidy_env res_ty
770 ; let msg = vcat [ hang (text "When checking that the pattern signature:")
771 4 (ppr sig_ty)
772 , nest 2 (hang (text "fits the type of its context:")
773 2 (ppr res_ty)) ]
774 ; return (tidy_env, msg) }
775
776 patBindSigErr :: [(Name,TcTyVar)] -> TcRnMessage
777 patBindSigErr sig_tvs
778 = TcRnUnknownMessage $ mkPlainError noHints $
779 hang (text "You cannot bind scoped type variable" <> plural sig_tvs
780 <+> pprQuotedList (map fst sig_tvs))
781 2 (text "in a pattern binding signature")
782
783
784 {- *********************************************************************
785 * *
786 Most of the work for constructors is here
787 (the rest is in the ConPatIn case of tc_pat)
788 * *
789 ************************************************************************
790
791 [Pattern matching indexed data types]
792 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
793 Consider the following declarations:
794
795 data family Map k :: * -> *
796 data instance Map (a, b) v = MapPair (Map a (Pair b v))
797
798 and a case expression
799
800 case x :: Map (Int, c) w of MapPair m -> ...
801
802 As explained by [Wrappers for data instance tycons] in GHC.Types.Id.Make, the
803 worker/wrapper types for MapPair are
804
805 $WMapPair :: forall a b v. Map a (Map a b v) -> Map (a, b) v
806 $wMapPair :: forall a b v. Map a (Map a b v) -> :R123Map a b v
807
808 So, the type of the scrutinee is Map (Int, c) w, but the tycon of MapPair is
809 :R123Map, which means the straight use of boxySplitTyConApp would give a type
810 error. Hence, the smart wrapper function boxySplitTyConAppWithFamily calls
811 boxySplitTyConApp with the family tycon Map instead, which gives us the family
812 type list {(Int, c), w}. To get the correct split for :R123Map, we need to
813 unify the family type list {(Int, c), w} with the instance types {(a, b), v}
814 (provided by tyConFamInst_maybe together with the family tycon). This
815 unification yields the substitution [a -> Int, b -> c, v -> w], which gives us
816 the split arguments for the representation tycon :R123Map as {Int, c, w}
817
818 In other words, boxySplitTyConAppWithFamily implicitly takes the coercion
819
820 Co123Map a b v :: {Map (a, b) v ~ :R123Map a b v}
821
822 moving between representation and family type into account. To produce type
823 correct Core, this coercion needs to be used to case the type of the scrutinee
824 from the family to the representation type. This is achieved by
825 unwrapFamInstScrutinee using a CoPat around the result pattern.
826
827 Now it might appear seem as if we could have used the previous GADT type
828 refinement infrastructure of refineAlt and friends instead of the explicit
829 unification and CoPat generation. However, that would be wrong. Why? The
830 whole point of GADT refinement is that the refinement is local to the case
831 alternative. In contrast, the substitution generated by the unification of
832 the family type list and instance types needs to be propagated to the outside.
833 Imagine that in the above example, the type of the scrutinee would have been
834 (Map x w), then we would have unified {x, w} with {(a, b), v}, yielding the
835 substitution [x -> (a, b), v -> w]. In contrast to GADT matching, the
836 instantiation of x with (a, b) must be global; ie, it must be valid in *all*
837 alternatives of the case expression, whereas in the GADT case it might vary
838 between alternatives.
839
840 RIP GADT refinement: refinements have been replaced by the use of explicit
841 equality constraints that are used in conjunction with implication constraints
842 to express the local scope of GADT refinements.
843
844 Note [Freshen existentials]
845 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
846 It is essential that these existentials are freshened.
847 Otherwise, if we have something like
848 case (a :: Ex, b :: Ex) of (MkEx ..., MkEx ...) -> ...
849 we'll give both unpacked existential variables the
850 same name, leading to shadowing.
851
852 -}
853
854 -- Running example:
855 -- MkT :: forall a b c. (a~[b]) => b -> c -> T a
856 -- with scrutinee of type (T ty)
857
858 tcConPat :: PatEnv -> LocatedN Name
859 -> Scaled ExpSigmaType -- Type of the pattern
860 -> HsConPatDetails GhcRn -> TcM a
861 -> TcM (Pat GhcTc, a)
862 tcConPat penv con_lname@(L _ con_name) pat_ty arg_pats thing_inside
863 = do { con_like <- tcLookupConLike con_name
864 ; case con_like of
865 RealDataCon data_con -> tcDataConPat penv con_lname data_con
866 pat_ty arg_pats thing_inside
867 PatSynCon pat_syn -> tcPatSynPat penv con_lname pat_syn
868 pat_ty arg_pats thing_inside
869 }
870
871 tcDataConPat :: PatEnv -> LocatedN Name -> DataCon
872 -> Scaled ExpSigmaType -- Type of the pattern
873 -> HsConPatDetails GhcRn -> TcM a
874 -> TcM (Pat GhcTc, a)
875 tcDataConPat penv (L con_span con_name) data_con pat_ty_scaled
876 arg_pats thing_inside
877 = do { let tycon = dataConTyCon data_con
878 -- For data families this is the representation tycon
879 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _)
880 = dataConFullSig data_con
881 header = L con_span (RealDataCon data_con)
882
883 -- Instantiate the constructor type variables [a->ty]
884 -- This may involve doing a family-instance coercion,
885 -- and building a wrapper
886 ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty_scaled
887 ; pat_ty <- readExpType (scaledThing pat_ty_scaled)
888
889 -- Add the stupid theta
890 ; setSrcSpanA con_span $ addDataConStupidTheta data_con ctxt_res_tys
891
892 -- Check that this isn't a GADT pattern match
893 -- in situations in which that isn't allowed.
894 ; let all_arg_tys = eqSpecPreds eq_spec ++ theta ++ (map scaledThing arg_tys)
895 ; checkGADT (RealDataCon data_con) ex_tvs all_arg_tys penv
896
897 ; tenv1 <- instTyVarsWith PatOrigin univ_tvs ctxt_res_tys
898 -- NB: Do not use zipTvSubst! See #14154
899 -- We want to create a well-kinded substitution, so
900 -- that the instantiated type is well-kinded
901
902 ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX tenv1 ex_tvs
903 -- Get location from monad, not from ex_tvs
904 -- This freshens: See Note [Freshen existentials]
905 -- Why "super"? See Note [Binding when lookup up instances]
906 -- in GHC.Core.InstEnv.
907
908 ; let arg_tys' = substScaledTys tenv arg_tys
909 pat_mult = scaledMult pat_ty_scaled
910 arg_tys_scaled = map (scaleScaled pat_mult) arg_tys'
911
912 ; traceTc "tcConPat" (vcat [ ppr con_name
913 , pprTyVars univ_tvs
914 , pprTyVars ex_tvs
915 , ppr eq_spec
916 , ppr theta
917 , pprTyVars ex_tvs'
918 , ppr ctxt_res_tys
919 , ppr arg_tys'
920 , ppr arg_pats ])
921 ; if null ex_tvs && null eq_spec && null theta
922 then do { -- The common case; no class bindings etc
923 -- (see Note [Arrows and patterns])
924 (arg_pats', res) <- tcConArgs (RealDataCon data_con) arg_tys_scaled
925 tenv penv arg_pats thing_inside
926 ; let res_pat = ConPat { pat_con = header
927 , pat_args = arg_pats'
928 , pat_con_ext = ConPatTc
929 { cpt_tvs = [], cpt_dicts = []
930 , cpt_binds = emptyTcEvBinds
931 , cpt_arg_tys = ctxt_res_tys
932 , cpt_wrap = idHsWrapper
933 }
934 }
935
936 ; return (mkHsWrapPat wrap res_pat pat_ty, res) }
937
938 else do -- The general case, with existential,
939 -- and local equality constraints
940 { let theta' = substTheta tenv (eqSpecPreds eq_spec ++ theta)
941 -- order is *important* as we generate the list of
942 -- dictionary binders from theta'
943 no_equalities = null eq_spec && not (any isEqPred theta)
944 skol_info = PatSkol (RealDataCon data_con) mc
945 mc = case pe_ctxt penv of
946 LamPat mc -> mc
947 LetPat {} -> PatBindRhs
948
949 ; gadts_on <- xoptM LangExt.GADTs
950 ; families_on <- xoptM LangExt.TypeFamilies
951 ; checkTc (no_equalities || gadts_on || families_on)
952 (TcRnUnknownMessage $ mkPlainError noHints $
953 text "A pattern match on a GADT requires the" <+>
954 text "GADTs or TypeFamilies language extension")
955 -- #2905 decided that a *pattern-match* of a GADT
956 -- should require the GADT language flag.
957 -- Re TypeFamilies see also #7156
958
959 ; given <- newEvVars theta'
960 ; (ev_binds, (arg_pats', res))
961 <- checkConstraints skol_info ex_tvs' given $
962 tcConArgs (RealDataCon data_con) arg_tys_scaled tenv penv arg_pats thing_inside
963
964 ; let res_pat = ConPat
965 { pat_con = header
966 , pat_args = arg_pats'
967 , pat_con_ext = ConPatTc
968 { cpt_tvs = ex_tvs'
969 , cpt_dicts = given
970 , cpt_binds = ev_binds
971 , cpt_arg_tys = ctxt_res_tys
972 , cpt_wrap = idHsWrapper
973 }
974 }
975 ; return (mkHsWrapPat wrap res_pat pat_ty, res)
976 } }
977
978 tcPatSynPat :: PatEnv -> LocatedN Name -> PatSyn
979 -> Scaled ExpSigmaType -- Type of the pattern
980 -> HsConPatDetails GhcRn -> TcM a
981 -> TcM (Pat GhcTc, a)
982 tcPatSynPat penv (L con_span con_name) pat_syn pat_ty arg_pats thing_inside
983 = do { let (univ_tvs, req_theta, ex_tvs, prov_theta, arg_tys, ty) = patSynSig pat_syn
984
985 ; (subst, univ_tvs') <- newMetaTyVars univ_tvs
986
987 -- Check that we aren't matching on a GADT-like pattern synonym
988 -- in situations in which that isn't allowed.
989 ; let all_arg_tys = ty : prov_theta ++ (map scaledThing arg_tys)
990 ; checkGADT (PatSynCon pat_syn) ex_tvs all_arg_tys penv
991
992 ; (tenv, ex_tvs') <- tcInstSuperSkolTyVarsX subst ex_tvs
993 -- This freshens: Note [Freshen existentials]
994
995 ; let ty' = substTy tenv ty
996 arg_tys' = substScaledTys tenv arg_tys
997 pat_mult = scaledMult pat_ty
998 arg_tys_scaled = map (scaleScaled pat_mult) arg_tys'
999 prov_theta' = substTheta tenv prov_theta
1000 req_theta' = substTheta tenv req_theta
1001
1002 ; mult_wrap <- checkManyPattern pat_ty
1003 -- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
1004
1005 ; wrap <- tc_sub_type penv (scaledThing pat_ty) ty'
1006 ; traceTc "tcPatSynPat" (ppr pat_syn $$
1007 ppr pat_ty $$
1008 ppr ty' $$
1009 ppr ex_tvs' $$
1010 ppr prov_theta' $$
1011 ppr req_theta' $$
1012 ppr arg_tys')
1013
1014 ; prov_dicts' <- newEvVars prov_theta'
1015
1016 ; let skol_info = case pe_ctxt penv of
1017 LamPat mc -> PatSkol (PatSynCon pat_syn) mc
1018 LetPat {} -> UnkSkol -- Doesn't matter
1019
1020 ; req_wrap <- instCall (OccurrenceOf con_name) (mkTyVarTys univ_tvs') req_theta'
1021 -- Origin (OccurrenceOf con_name):
1022 -- see Note [Call-stack tracing of pattern synonyms]
1023 ; traceTc "instCall" (ppr req_wrap)
1024
1025 ; traceTc "checkConstraints {" Outputable.empty
1026 ; (ev_binds, (arg_pats', res))
1027 <- checkConstraints skol_info ex_tvs' prov_dicts' $
1028 tcConArgs (PatSynCon pat_syn) arg_tys_scaled tenv penv arg_pats thing_inside
1029
1030 ; traceTc "checkConstraints }" (ppr ev_binds)
1031 ; let res_pat = ConPat { pat_con = L con_span $ PatSynCon pat_syn
1032 , pat_args = arg_pats'
1033 , pat_con_ext = ConPatTc
1034 { cpt_tvs = ex_tvs'
1035 , cpt_dicts = prov_dicts'
1036 , cpt_binds = ev_binds
1037 , cpt_arg_tys = mkTyVarTys univ_tvs'
1038 , cpt_wrap = req_wrap
1039 }
1040 }
1041 ; pat_ty <- readExpType (scaledThing pat_ty)
1042 ; return (mkHsWrapPat (wrap <.> mult_wrap) res_pat pat_ty, res) }
1043
1044 {- Note [Call-stack tracing of pattern synonyms]
1045 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1046 Consider
1047 f :: HasCallStack => blah
1048
1049 pattern Annotated :: HasCallStack => (CallStack, a) -> a
1050 pattern Annotated x <- (f -> x)
1051
1052 When we pattern-match against `Annotated` we will call `f`, and must
1053 pass a call-stack. We may want `Annotated` itself to propagate the call
1054 stack, so we give it a HasCallStack constraint too. But then we expect
1055 to see `Annotated` in the call stack.
1056
1057 This is achieve easily, but a bit trickily. When we instantiate
1058 Annotated's "required" constraints, in tcPatSynPat, give them a
1059 CtOrigin of (OccurrenceOf "Annotated"). That way the special magic
1060 in GHC.Tc.Solver.Canonical.canClassNC which deals with CallStack
1061 constraints will kick in: that logic only fires on constraints
1062 whose Origin is (OccurrenceOf f).
1063
1064 See also Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
1065 and Note [Solving CallStack constraints] in GHC.Tc.Solver.Types
1066 -}
1067 ----------------------------
1068 -- | Convenient wrapper for calling a matchExpectedXXX function
1069 matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionN, a))
1070 -> PatEnv -> ExpSigmaType -> TcM (HsWrapper, a)
1071 -- See Note [Matching polytyped patterns]
1072 -- Returns a wrapper : pat_ty ~R inner_ty
1073 matchExpectedPatTy inner_match (PE { pe_orig = orig }) pat_ty
1074 = do { pat_ty <- expTypeToType pat_ty
1075 ; (wrap, pat_rho) <- topInstantiate orig pat_ty
1076 ; (co, res) <- inner_match pat_rho
1077 ; traceTc "matchExpectedPatTy" (ppr pat_ty $$ ppr wrap)
1078 ; return (mkWpCastN (mkTcSymCo co) <.> wrap, res) }
1079
1080 ----------------------------
1081 matchExpectedConTy :: PatEnv
1082 -> TyCon -- The TyCon that this data
1083 -- constructor actually returns
1084 -- In the case of a data family this is
1085 -- the /representation/ TyCon
1086 -> Scaled ExpSigmaType -- The type of the pattern; in the
1087 -- case of a data family this would
1088 -- mention the /family/ TyCon
1089 -> TcM (HsWrapper, [TcSigmaType])
1090 -- See Note [Matching constructor patterns]
1091 -- Returns a wrapper : pat_ty "->" T ty1 ... tyn
1092 matchExpectedConTy (PE { pe_orig = orig }) data_tc exp_pat_ty
1093 | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc
1094 -- Comments refer to Note [Matching constructor patterns]
1095 -- co_tc :: forall a. T [a] ~ T7 a
1096 = do { pat_ty <- expTypeToType (scaledThing exp_pat_ty)
1097 ; (wrap, pat_rho) <- topInstantiate orig pat_ty
1098
1099 ; (subst, tvs') <- newMetaTyVars (tyConTyVars data_tc)
1100 -- tys = [ty1,ty2]
1101
1102 ; traceTc "matchExpectedConTy" (vcat [ppr data_tc,
1103 ppr (tyConTyVars data_tc),
1104 ppr fam_tc, ppr fam_args,
1105 ppr exp_pat_ty,
1106 ppr pat_ty,
1107 ppr pat_rho, ppr wrap])
1108 ; co1 <- unifyType Nothing (mkTyConApp fam_tc (substTys subst fam_args)) pat_rho
1109 -- co1 : T (ty1,ty2) ~N pat_rho
1110 -- could use tcSubType here... but it's the wrong way round
1111 -- for actual vs. expected in error messages.
1112
1113 ; let tys' = mkTyVarTys tvs'
1114 co2 = mkTcUnbranchedAxInstCo co_tc tys' []
1115 -- co2 : T (ty1,ty2) ~R T7 ty1 ty2
1116
1117 full_co = mkTcSubCo (mkTcSymCo co1) `mkTcTransCo` co2
1118 -- full_co :: pat_rho ~R T7 ty1 ty2
1119
1120 ; return ( mkWpCastR full_co <.> wrap, tys') }
1121
1122 | otherwise
1123 = do { pat_ty <- expTypeToType (scaledThing exp_pat_ty)
1124 ; (wrap, pat_rho) <- topInstantiate orig pat_ty
1125 ; (coi, tys) <- matchExpectedTyConApp data_tc pat_rho
1126 ; return (mkWpCastN (mkTcSymCo coi) <.> wrap, tys) }
1127
1128 {-
1129 Note [Matching constructor patterns]
1130 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1131 Suppose (coi, tys) = matchExpectedConType data_tc pat_ty
1132
1133 * In the simple case, pat_ty = tc tys
1134
1135 * If pat_ty is a polytype, we want to instantiate it
1136 This is like part of a subsumption check. Eg
1137 f :: (forall a. [a]) -> blah
1138 f [] = blah
1139
1140 * In a type family case, suppose we have
1141 data family T a
1142 data instance T (p,q) = A p | B q
1143 Then we'll have internally generated
1144 data T7 p q = A p | B q
1145 axiom coT7 p q :: T (p,q) ~ T7 p q
1146
1147 So if pat_ty = T (ty1,ty2), we return (coi, [ty1,ty2]) such that
1148 coi = coi2 . coi1 : T7 t ~ pat_ty
1149 coi1 : T (ty1,ty2) ~ pat_ty
1150 coi2 : T7 ty1 ty2 ~ T (ty1,ty2)
1151
1152 For families we do all this matching here, not in the unifier,
1153 because we never want a whisper of the data_tycon to appear in
1154 error messages; it's a purely internal thing
1155 -}
1156
1157 {-
1158 Note [Typechecking type applications in patterns]
1159 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1160 How should we typecheck type applications in patterns, such as
1161 f :: Either (Maybe a) [b] -> blah
1162 f (Left @x @[y] (v::Maybe x)) = blah
1163
1164 It's quite straightforward, and very similar to the treatment of
1165 pattern signatures.
1166
1167 * Step 1: bind the newly-in-scope type variables x and y to fresh
1168 unification variables, say x0 and y0.
1169
1170 * Step 2: typecheck those type arguments, @x and @[y], to get the
1171 types x0 and [y0].
1172
1173 * Step 3: Unify those types with the type arguments we expect,
1174 in this case (Maybe a) and [b]. These unifications will
1175 (perhaps after the constraint solver has done its work)
1176 unify x0 := Maybe a
1177 y0 := b
1178 Thus we learn that x stands for (Maybe a) and y for b.
1179
1180 Wrinkles:
1181
1182 * Surprisingly, we can discard the coercions arising from
1183 these unifications. The *only* thing the unification does is
1184 to side-effect those unification variables, so that we know
1185 what type x and y stand for; and cause an error if the equality
1186 is not soluble. It's a bit like a Derived constraint arising
1187 from a functional dependency.
1188
1189 * Exactly the same works for existential arguments
1190 data T where
1191 MkT :: a -> a -> T
1192 f :: T -> blah
1193 f (MkT @x v w) = ...
1194 Here we create a fresh unification variable x0 for x, and
1195 unify it with the fresh existential variable bound by the pattern.
1196
1197 * Note that both here and in pattern signatures the unification may
1198 not even end up unifying the variable. For example
1199 type S a b = a
1200 f :: Maybe a -> Bool
1201 f (Just @(S a b) x) = True :: b
1202 In Step 3 we will unify (S a0 b0 ~ a), which succeeds, but has no
1203 effect on the unification variable b0, to which 'b' is bound.
1204 Later, in the RHS, we find that b0 must be Bool, and unify it there.
1205 All is fine.
1206 -}
1207
1208 tcConArgs :: ConLike
1209 -> [Scaled TcSigmaType]
1210 -> TCvSubst -- Instantiating substitution for constructor type
1211 -> Checker (HsConPatDetails GhcRn) (HsConPatDetails GhcTc)
1212 tcConArgs con_like arg_tys tenv penv con_args thing_inside = case con_args of
1213 PrefixCon type_args arg_pats -> do
1214 { checkTc (con_arity == no_of_args) -- Check correct arity
1215 (arityErr (text "constructor") con_like con_arity no_of_args)
1216
1217 -- forgetting to filter out inferred binders led to #20443
1218 ; let con_spec_binders = filter ((== SpecifiedSpec) . binderArgFlag) $
1219 conLikeUserTyVarBinders con_like
1220 ; checkTc (type_args `leLength` con_spec_binders)
1221 (conTyArgArityErr con_like (length con_spec_binders) (length type_args))
1222
1223 ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
1224 ; (type_args', (arg_pats', res))
1225 <- tcMultiple tcConTyArg penv type_args $
1226 tcMultiple tcConArg penv pats_w_tys thing_inside
1227
1228 -- This unification is straight from Figure 7 of
1229 -- "Type Variables in Patterns", Haskell'18
1230 ; _ <- zipWithM (unifyType Nothing) type_args' (substTyVars tenv $
1231 binderVars con_spec_binders)
1232 -- OK to drop coercions here. These unifications are all about
1233 -- guiding inference based on a user-written type annotation
1234 -- See Note [Typechecking type applications in patterns]
1235
1236 ; return (PrefixCon type_args arg_pats', res) }
1237 where
1238 con_arity = conLikeArity con_like
1239 no_of_args = length arg_pats
1240
1241 InfixCon p1 p2 -> do
1242 { checkTc (con_arity == 2) -- Check correct arity
1243 (arityErr (text "constructor") con_like con_arity 2)
1244 ; let [arg_ty1,arg_ty2] = arg_tys -- This can't fail after the arity check
1245 ; ([p1',p2'], res) <- tcMultiple tcConArg penv [(p1,arg_ty1),(p2,arg_ty2)]
1246 thing_inside
1247 ; return (InfixCon p1' p2', res) }
1248 where
1249 con_arity = conLikeArity con_like
1250
1251 RecCon (HsRecFields rpats dd) -> do
1252 { (rpats', res) <- tcMultiple tc_field penv rpats thing_inside
1253 ; return (RecCon (HsRecFields rpats' dd), res) }
1254 where
1255 tc_field :: Checker (LHsRecField GhcRn (LPat GhcRn))
1256 (LHsRecField GhcTc (LPat GhcTc))
1257 tc_field penv
1258 (L l (HsFieldBind ann (L loc (FieldOcc sel (L lr rdr))) pat pun))
1259 thing_inside
1260 = do { sel' <- tcLookupId sel
1261 ; pat_ty <- setSrcSpanA loc $ find_field_ty sel
1262 (occNameFS $ rdrNameOcc rdr)
1263 ; (pat', res) <- tcConArg penv (pat, pat_ty) thing_inside
1264 ; return (L l (HsFieldBind ann (L loc (FieldOcc sel' (L lr rdr))) pat'
1265 pun), res) }
1266
1267
1268 find_field_ty :: Name -> FieldLabelString -> TcM (Scaled TcType)
1269 find_field_ty sel lbl
1270 = case [ty | (fl, ty) <- field_tys, flSelector fl == sel ] of
1271
1272 -- No matching field; chances are this field label comes from some
1273 -- other record type (or maybe none). If this happens, just fail,
1274 -- otherwise we get crashes later (#8570), and similar:
1275 -- f (R { foo = (a,b) }) = a+b
1276 -- If foo isn't one of R's fields, we don't want to crash when
1277 -- typechecking the "a+b".
1278 [] -> failWith (badFieldCon con_like lbl)
1279
1280 -- The normal case, when the field comes from the right constructor
1281 (pat_ty : extras) -> do
1282 traceTc "find_field" (ppr pat_ty <+> ppr extras)
1283 assert (null extras) (return pat_ty)
1284
1285 field_tys :: [(FieldLabel, Scaled TcType)]
1286 field_tys = zip (conLikeFieldLabels con_like) arg_tys
1287 -- Don't use zipEqual! If the constructor isn't really a record, then
1288 -- dataConFieldLabels will be empty (and each field in the pattern
1289 -- will generate an error below).
1290
1291 tcConTyArg :: Checker (HsPatSigType GhcRn) TcType
1292 tcConTyArg penv rn_ty thing_inside
1293 = do { (sig_wcs, sig_ibs, arg_ty) <- tcHsPatSigType TypeAppCtxt HM_TyAppPat rn_ty AnyKind
1294 -- AnyKind is a bit suspect: it really should be the kind gotten
1295 -- from instantiating the constructor type. But this would be
1296 -- hard to get right, because earlier type patterns might influence
1297 -- the kinds of later patterns. In any case, it all gets checked
1298 -- by the calls to unifyType in tcConArgs, which will also unify
1299 -- kinds.
1300 ; when (not (null sig_ibs) && inPatBind penv) $
1301 addErr (TcRnUnknownMessage $ mkPlainError noHints $
1302 text "Binding type variables is not allowed in pattern bindings")
1303 ; result <- tcExtendNameTyVarEnv sig_wcs $
1304 tcExtendNameTyVarEnv sig_ibs $
1305 thing_inside
1306 ; return (arg_ty, result) }
1307
1308 tcConArg :: Checker (LPat GhcRn, Scaled TcSigmaType) (LPat GhcTc)
1309 tcConArg penv (arg_pat, Scaled arg_mult arg_ty)
1310 = tc_lpat (Scaled arg_mult (mkCheckExpType arg_ty)) penv arg_pat
1311
1312 addDataConStupidTheta :: DataCon -> [TcType] -> TcM ()
1313 -- Instantiate the "stupid theta" of the data con, and throw
1314 -- the constraints into the constraint set
1315 addDataConStupidTheta data_con inst_tys
1316 | null stupid_theta = return ()
1317 | otherwise = instStupidTheta origin inst_theta
1318 where
1319 origin = OccurrenceOf (dataConName data_con)
1320 -- The origin should always report "occurrence of C"
1321 -- even when C occurs in a pattern
1322 stupid_theta = dataConStupidTheta data_con
1323 univ_tvs = dataConUnivTyVars data_con
1324 tenv = zipTvSubst univ_tvs (takeList univ_tvs inst_tys)
1325 -- NB: inst_tys can be longer than the univ tyvars
1326 -- because the constructor might have existentials
1327 inst_theta = substTheta tenv stupid_theta
1328
1329 conTyArgArityErr :: ConLike
1330 -> Int -- expected # of arguments
1331 -> Int -- actual # of arguments
1332 -> TcRnMessage
1333 conTyArgArityErr con_like expected_number actual_number
1334 = TcRnUnknownMessage $ mkPlainError noHints $
1335 text "Too many type arguments in constructor pattern for" <+> quotes (ppr con_like) $$
1336 text "Expected no more than" <+> ppr expected_number <> semi <+> text "got" <+> ppr actual_number
1337
1338 {-
1339 Note [Arrows and patterns]
1340 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1341 (Oct 07) Arrow notation has the odd property that it involves
1342 "holes in the scope". For example:
1343 expr :: Arrow a => a () Int
1344 expr = proc (y,z) -> do
1345 x <- term -< y
1346 expr' -< x
1347
1348 Here the 'proc (y,z)' binding scopes over the arrow tails but not the
1349 arrow body (e.g 'term'). As things stand (bogusly) all the
1350 constraints from the proc body are gathered together, so constraints
1351 from 'term' will be seen by the tcPat for (y,z). But we must *not*
1352 bind constraints from 'term' here, because the desugarer will not make
1353 these bindings scope over 'term'.
1354
1355 The Right Thing is not to confuse these constraints together. But for
1356 now the Easy Thing is to ensure that we do not have existential or
1357 GADT constraints in a 'proc', which we do by disallowing any
1358 non-vanilla pattern match (i.e. one that introduces existential
1359 variables or provided constraints), in tcDataConPat and tcPatSynPat.
1360
1361 We also short-cut the constraint simplification for such vanilla patterns,
1362 so that we bind no constraints. Hence the 'fast path' in tcDataConPat;
1363 which applies more generally (not just within 'proc'), as it's a good
1364 plan in general to bypass the constraint simplification step entirely
1365 when it's not needed.
1366
1367 ************************************************************************
1368 * *
1369 Note [Pattern coercions]
1370 * *
1371 ************************************************************************
1372
1373 In principle, these program would be reasonable:
1374
1375 f :: (forall a. a->a) -> Int
1376 f (x :: Int->Int) = x 3
1377
1378 g :: (forall a. [a]) -> Bool
1379 g [] = True
1380
1381 In both cases, the function type signature restricts what arguments can be passed
1382 in a call (to polymorphic ones). The pattern type signature then instantiates this
1383 type. For example, in the first case, (forall a. a->a) <= Int -> Int, and we
1384 generate the translated term
1385 f = \x' :: (forall a. a->a). let x = x' Int in x 3
1386
1387 From a type-system point of view, this is perfectly fine, but it's *very* seldom useful.
1388 And it requires a significant amount of code to implement, because we need to decorate
1389 the translated pattern with coercion functions (generated from the subsumption check
1390 by tcSub).
1391
1392 So for now I'm just insisting on type *equality* in patterns. No subsumption.
1393
1394 Old notes about desugaring, at a time when pattern coercions were handled:
1395
1396 A SigPat is a type coercion and must be handled one at a time. We can't
1397 combine them unless the type of the pattern inside is identical, and we don't
1398 bother to check for that. For example:
1399
1400 data T = T1 Int | T2 Bool
1401 f :: (forall a. a -> a) -> T -> t
1402 f (g::Int->Int) (T1 i) = T1 (g i)
1403 f (g::Bool->Bool) (T2 b) = T2 (g b)
1404
1405 We desugar this as follows:
1406
1407 f = \ g::(forall a. a->a) t::T ->
1408 let gi = g Int
1409 in case t of { T1 i -> T1 (gi i)
1410 other ->
1411 let gb = g Bool
1412 in case t of { T2 b -> T2 (gb b)
1413 other -> fail }}
1414
1415 Note that we do not treat the first column of patterns as a
1416 column of variables, because the coerced variables (gi, gb)
1417 would be of different types. So we get rather grotty code.
1418 But I don't think this is a common case, and if it was we could
1419 doubtless improve it.
1420
1421 Meanwhile, the strategy is:
1422 * treat each SigPat coercion (always non-identity coercions)
1423 as a separate block
1424 * deal with the stuff inside, and then wrap a binding round
1425 the result to bind the new variable (gi, gb, etc)
1426
1427
1428 ************************************************************************
1429 * *
1430 \subsection{Errors and contexts}
1431 * *
1432 ************************************************************************
1433
1434 Note [Existential check]
1435 ~~~~~~~~~~~~~~~~~~~~~~~~
1436 Lazy patterns can't bind existentials. They arise in two ways:
1437 * Let bindings let { C a b = e } in b
1438 * Twiddle patterns f ~(C a b) = e
1439 The pe_lazy field of PatEnv says whether we are inside a lazy
1440 pattern (perhaps deeply)
1441
1442 See also Note [Typechecking pattern bindings] in GHC.Tc.Gen.Bind
1443 -}
1444
1445 maybeWrapPatCtxt :: Pat GhcRn -> (TcM a -> TcM b) -> TcM a -> TcM b
1446 -- Not all patterns are worth pushing a context
1447 maybeWrapPatCtxt pat tcm thing_inside
1448 | not (worth_wrapping pat) = tcm thing_inside
1449 | otherwise = addErrCtxt msg $ tcm $ popErrCtxt thing_inside
1450 -- Remember to pop before doing thing_inside
1451 where
1452 worth_wrapping (VarPat {}) = False
1453 worth_wrapping (ParPat {}) = False
1454 worth_wrapping (AsPat {}) = False
1455 worth_wrapping _ = True
1456 msg = hang (text "In the pattern:") 2 (ppr pat)
1457
1458 -----------------------------------------------
1459
1460 -- | Check that a pattern isn't a GADT, or doesn't have existential variables,
1461 -- in a situation in which that is not permitted (inside a lazy pattern, or
1462 -- in arrow notation).
1463 checkGADT :: ConLike
1464 -> [TyVar] -- ^ existentials
1465 -> [Type] -- ^ argument types
1466 -> PatEnv
1467 -> TcM ()
1468 checkGADT conlike ex_tvs arg_tys = \case
1469 PE { pe_ctxt = LetPat {} }
1470 -> return ()
1471 PE { pe_ctxt = LamPat (ArrowMatchCtxt {}) }
1472 | not $ isVanillaConLike conlike
1473 -- See Note [Arrows and patterns]
1474 -> failWithTc TcRnArrowProcGADTPattern
1475 PE { pe_lazy = True }
1476 | has_existentials
1477 -- See Note [Existential check]
1478 -> failWithTc TcRnLazyGADTPattern
1479 _ -> return ()
1480 where
1481 has_existentials :: Bool
1482 has_existentials = any (`elemVarSet` tyCoVarsOfTypes arg_tys) ex_tvs
1483
1484 badFieldCon :: ConLike -> FieldLabelString -> TcRnMessage
1485 badFieldCon con field
1486 = TcRnUnknownMessage $ mkPlainError noHints $
1487 hsep [text "Constructor" <+> quotes (ppr con),
1488 text "does not have field", quotes (ppr field)]
1489
1490 polyPatSig :: TcType -> SDoc
1491 polyPatSig sig_ty
1492 = hang (text "Illegal polymorphic type signature in pattern:")
1493 2 (ppr sig_ty)