Turn EvTerm (almost) into CoreExpr (#14691)
[ghc.git] / compiler / typecheck / TcPatSyn.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5 \section[TcPatSyn]{Typechecking pattern synonym declarations}
6 -}
7
8 {-# LANGUAGE CPP #-}
9 {-# LANGUAGE FlexibleContexts #-}
10 {-# LANGUAGE TypeFamilies #-}
11
12 module TcPatSyn ( tcInferPatSynDecl, tcCheckPatSynDecl
13 , tcPatSynBuilderBind, tcPatSynBuilderOcc, nonBidirectionalErr
14 ) where
15
16 import GhcPrelude
17
18 import HsSyn
19 import TcPat
20 import Type( mkEmptyTCvSubst, tidyTyVarBinders, tidyTypes, tidyType )
21 import TcRnMonad
22 import TcSigs( emptyPragEnv, completeSigFromId )
23 import TcType( mkMinimalBySCs )
24 import TcEnv
25 import TcMType
26 import TcHsSyn( zonkTyVarBindersX, zonkTcTypeToTypes
27 , zonkTcTypeToType, emptyZonkEnv )
28 import TysPrim
29 import TysWiredIn ( runtimeRepTy )
30 import Name
31 import SrcLoc
32 import PatSyn
33 import NameSet
34 import Panic
35 import Outputable
36 import FastString
37 import Var
38 import VarEnv( emptyTidyEnv, mkInScopeSet )
39 import Id
40 import IdInfo( RecSelParent(..), setLevityInfoWithType )
41 import TcBinds
42 import BasicTypes
43 import TcSimplify
44 import TcUnify
45 import TcType
46 import TcEvidence
47 import BuildTyCl
48 import VarSet
49 import MkId
50 import TcTyDecls
51 import ConLike
52 import FieldLabel
53 import Bag
54 import Util
55 import ErrUtils
56 import Control.Monad ( zipWithM )
57 import Data.List( partition )
58
59 #include "HsVersions.h"
60
61 {-
62 ************************************************************************
63 * *
64 Type checking a pattern synonym
65 * *
66 ************************************************************************
67 -}
68
69 tcInferPatSynDecl :: PatSynBind GhcRn GhcRn
70 -> TcM (LHsBinds GhcTc, TcGblEnv)
71 tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
72 psb_def = lpat, psb_dir = dir }
73 = addPatSynCtxt lname $
74 do { traceTc "tcInferPatSynDecl {" $ ppr name
75 ; tcCheckPatSynPat lpat
76
77 ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
78 ; (tclvl, wanted, ((lpat', args), pat_ty))
79 <- pushLevelAndCaptureConstraints $
80 tcInferNoInst $ \ exp_ty ->
81 tcPat PatSyn lpat exp_ty $
82 mapM tcLookupId arg_names
83
84 ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
85
86 ; (qtvs, req_dicts, ev_binds, _) <- simplifyInfer tclvl NoRestrictions []
87 named_taus wanted
88
89 ; let (ex_tvs, prov_dicts) = tcCollectEx lpat'
90 ex_tv_set = mkVarSet ex_tvs
91 univ_tvs = filterOut (`elemVarSet` ex_tv_set) qtvs
92 req_theta = map evVarPred req_dicts
93
94 ; prov_dicts <- mapM zonkId prov_dicts
95 ; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts
96 prov_theta = map evVarPred filtered_prov_dicts
97 -- Filtering: see Note [Remove redundant provided dicts]
98
99 -- Report bad universal type variables
100 -- See Note [Type variables whose kind is captured]
101 ; let bad_tvs = [ tv | tv <- univ_tvs
102 , tyCoVarsOfType (tyVarKind tv)
103 `intersectsVarSet` ex_tv_set ]
104 ; mapM_ (badUnivTvErr ex_tvs) bad_tvs
105
106 -- Report coercions that esacpe
107 -- See Note [Coercions that escape]
108 ; args <- mapM zonkId args
109 ; let bad_args = [ (arg, bad_cos) | arg <- args ++ prov_dicts
110 , let bad_cos = filterDVarSet isId $
111 (tyCoVarsOfTypeDSet (idType arg))
112 , not (isEmptyDVarSet bad_cos) ]
113 ; mapM_ dependentArgErr bad_args
114
115 ; traceTc "tcInferPatSynDecl }" $ (ppr name $$ ppr ex_tvs)
116 ; tc_patsyn_finish lname dir is_infix lpat'
117 (mkTyVarBinders Inferred univ_tvs
118 , req_theta, ev_binds, req_dicts)
119 (mkTyVarBinders Inferred ex_tvs
120 , mkTyVarTys ex_tvs, prov_theta, map evId filtered_prov_dicts)
121 (map nlHsVar args, map idType args)
122 pat_ty rec_fields }
123
124 badUnivTvErr :: [TyVar] -> TyVar -> TcM ()
125 -- See Note [Type variables whose kind is captured]
126 badUnivTvErr ex_tvs bad_tv
127 = addErrTc $
128 vcat [ text "Universal type variable" <+> quotes (ppr bad_tv)
129 <+> text "has existentially bound kind:"
130 , nest 2 (ppr_with_kind bad_tv)
131 , hang (text "Existentially-bound variables:")
132 2 (vcat (map ppr_with_kind ex_tvs))
133 , text "Probable fix: give the pattern synoym a type signature"
134 ]
135 where
136 ppr_with_kind tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
137
138 dependentArgErr :: (Id, DTyCoVarSet) -> TcM ()
139 -- See Note [Coercions that escape]
140 dependentArgErr (arg, bad_cos)
141 = addErrTc $
142 vcat [ text "Iceland Jack! Iceland Jack! Stop torturing me!"
143 , hang (text "Pattern-bound variable")
144 2 (ppr arg <+> dcolon <+> ppr (idType arg))
145 , nest 2 $
146 hang (text "has a type that mentions pattern-bound coercion"
147 <> plural bad_co_list <> colon)
148 2 (pprWithCommas ppr bad_co_list)
149 , text "Hint: use -fprint-explicit-coercions to see the coercions"
150 , text "Probable fix: add a pattern signature" ]
151 where
152 bad_co_list = dVarSetElems bad_cos
153
154 {- Note [Remove redundant provided dicts]
155 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
156 Recall that
157 HRefl :: forall k1 k2 (a1:k1) (a2:k2). (k1 ~ k2, a1 ~ a2)
158 => a1 :~~: a2
159 (NB: technically the (k1~k2) existential dictionary is not necessary,
160 but it's there at the moment.)
161
162 Now consider (Trac #14394):
163 pattern Foo = HRefl
164 in a non-poly-kinded module. We don't want to get
165 pattern Foo :: () => (* ~ *, b ~ a) => a :~~: b
166 with that redundant (* ~ *). We'd like to remove it; hence the call to
167 mkMinimalWithSCs.
168
169 Similarly consider
170 data S a where { MkS :: Ord a => a -> S a }
171 pattern Bam x y <- (MkS (x::a), MkS (y::a)))
172
173 The pattern (Bam x y) binds two (Ord a) dictionaries, but we only
174 need one. Agian mkMimimalWithSCs removes the redundant one.
175
176 Note [Type variables whose kind is captured]
177 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
178 Consider
179 data AST a = Sym [a]
180 class Prj s where { prj :: [a] -> Maybe (s a)
181 pattern P x <= Sym (prj -> Just x)
182
183 Here we get a matcher with this type
184 $mP :: forall s a. Prj s => AST a -> (s a -> r) -> r -> r
185
186 No problem. But note that 's' is not fixed by the type of the
187 pattern (AST a), nor is it existentially bound. It's really only
188 fixed by the type of the continuation.
189
190 Trac #14552 showed that this can go wrong if the kind of 's' mentions
191 existentially bound variables. We obviously can't make a type like
192 $mP :: forall (s::k->*) a. Prj s => AST a -> (forall k. s a -> r)
193 -> r -> r
194 But neither is 's' itself existentially bound, so the forall (s::k->*)
195 can't go in the inner forall either. (What would the matcher apply
196 the continuation to?)
197
198 So we just fail in this case, with a pretty terrible error message.
199 Maybe we could do better, but I can't see how. (It'd be possible to
200 default 's' to (Any k), but that probably isn't what the user wanted,
201 and it not straightforward to implement, because by the time we see
202 the problem, simplifyInfer has already skolemised 's'.)
203
204 This stuff can only happen in the presence of view patterns, with
205 TypeInType, so it's a bit of a corner case.
206
207 Note [Coercions that escape]
208 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
209 Trac #14507 showed an example where the inferred type of the matcher
210 for the pattern synonym was somethign like
211 $mSO :: forall (r :: TYPE rep) kk (a :: k).
212 TypeRep k a
213 -> ((Bool ~ k) => TypeRep Bool (a |> co_a2sv) -> r)
214 -> (Void# -> r)
215 -> r
216
217 What is that co_a2sv :: Bool ~# *?? It was bound (via a superclass
218 selection) by the pattern being matched; and indeed it is implicit in
219 the context (Bool ~ k). You could imagine trying to extract it like
220 this:
221 $mSO :: forall (r :: TYPE rep) kk (a :: k).
222 TypeRep k a
223 -> ( co :: ((Bool :: *) ~ (k :: *)) =>
224 let co_a2sv = sc_sel co
225 in TypeRep Bool (a |> co_a2sv) -> r)
226 -> (Void# -> r)
227 -> r
228
229 But we simply don't allow that in types. Maybe one day but not now.
230
231 How to detect this situation? We just look for free coercion variables
232 in the types of any of the arguments to the matcher. The error message
233 is not very helpful, but at least we don't get a Lint error.
234 -}
235
236 tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn
237 -> TcPatSynInfo
238 -> TcM (LHsBinds GhcTc, TcGblEnv)
239 tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
240 , psb_def = lpat, psb_dir = dir }
241 TPSI{ patsig_implicit_bndrs = implicit_tvs
242 , patsig_univ_bndrs = explicit_univ_tvs, patsig_prov = prov_theta
243 , patsig_ex_bndrs = explicit_ex_tvs, patsig_req = req_theta
244 , patsig_body_ty = sig_body_ty }
245 = addPatSynCtxt lname $
246 do { let decl_arity = length arg_names
247 (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
248
249 ; traceTc "tcCheckPatSynDecl" $
250 vcat [ ppr implicit_tvs, ppr explicit_univ_tvs, ppr req_theta
251 , ppr explicit_ex_tvs, ppr prov_theta, ppr sig_body_ty ]
252
253 ; tcCheckPatSynPat lpat
254
255 ; (arg_tys, pat_ty) <- case tcSplitFunTysN decl_arity sig_body_ty of
256 Right stuff -> return stuff
257 Left missing -> wrongNumberOfParmsErr name decl_arity missing
258
259 -- Complain about: pattern P :: () => forall x. x -> P x
260 -- The existential 'x' should not appear in the result type
261 -- Can't check this until we know P's arity
262 ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType pat_ty) explicit_ex_tvs
263 ; checkTc (null bad_tvs) $
264 hang (sep [ text "The result type of the signature for" <+> quotes (ppr name) <> comma
265 , text "namely" <+> quotes (ppr pat_ty) ])
266 2 (text "mentions existential type variable" <> plural bad_tvs
267 <+> pprQuotedList bad_tvs)
268
269 -- See Note [The pattern-synonym signature splitting rule]
270 ; let univ_fvs = closeOverKinds $
271 (tyCoVarsOfTypes (pat_ty : req_theta) `extendVarSetList` explicit_univ_tvs)
272 (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) . binderVar) implicit_tvs
273 univ_bndrs = extra_univ ++ mkTyVarBinders Specified explicit_univ_tvs
274 ex_bndrs = extra_ex ++ mkTyVarBinders Specified explicit_ex_tvs
275 univ_tvs = binderVars univ_bndrs
276 ex_tvs = binderVars ex_bndrs
277
278 -- Right! Let's check the pattern against the signature
279 -- See Note [Checking against a pattern signature]
280 ; req_dicts <- newEvVars req_theta
281 ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
282 ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
283 pushLevelAndCaptureConstraints $
284 tcExtendTyVarEnv univ_tvs $
285 tcExtendKindEnvList [(getName (binderVar ex_tv), APromotionErr PatSynExPE)
286 | ex_tv <- extra_ex] $
287 -- See Note [Pattern synonym existentials do not scope]
288 tcPat PatSyn lpat (mkCheckExpType pat_ty) $
289 do { let in_scope = mkInScopeSet (mkVarSet univ_tvs)
290 empty_subst = mkEmptyTCvSubst in_scope
291 ; (subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst ex_tvs
292 -- newMetaTyVarX: see the "Existential type variables"
293 -- part of Note [Checking against a pattern signature]
294 ; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs])
295 ; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs'])
296 ; let prov_theta' = substTheta subst prov_theta
297 -- Add univ_tvs to the in_scope set to
298 -- satisfy the substitution invariant. There's no need to
299 -- add 'ex_tvs' as they are already in the domain of the
300 -- substitution.
301 -- See also Note [The substitution invariant] in TyCoRep.
302 ; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta'
303 ; args' <- zipWithM (tc_arg subst) arg_names arg_tys
304 ; return (ex_tvs', prov_dicts, args') }
305
306 ; let skol_info = SigSkol (PatSynCtxt name) pat_ty []
307 -- The type here is a bit bogus, but we do not print
308 -- the type for PatSynCtxt, so it doesn't matter
309 -- See TcRnTypes Note [Skolem info for pattern synonyms]
310 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted
311
312 -- Solve the constraints now, because we are about to make a PatSyn,
313 -- which should not contain unification variables and the like (Trac #10997)
314 ; simplifyTopImplic implics
315
316 -- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct
317 -- Otherwise we may get a type error when typechecking the builder,
318 -- when that should be impossible
319
320 ; traceTc "tcCheckPatSynDecl }" $ ppr name
321 ; tc_patsyn_finish lname dir is_infix lpat'
322 (univ_bndrs, req_theta, ev_binds, req_dicts)
323 (ex_bndrs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
324 (args', arg_tys)
325 pat_ty rec_fields }
326 where
327 tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr GhcTcId)
328 tc_arg subst arg_name arg_ty
329 = do { -- Look up the variable actually bound by lpat
330 -- and check that it has the expected type
331 arg_id <- tcLookupId arg_name
332 ; wrap <- tcSubType_NC GenSigCtxt
333 (idType arg_id)
334 (substTyUnchecked subst arg_ty)
335 -- Why do we need tcSubType here?
336 -- See Note [Pattern synonyms and higher rank types]
337 ; return (mkLHsWrap wrap $ nlHsVar arg_id) }
338
339 {- [Pattern synonyms and higher rank types]
340 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
341 Consider
342 data T = MkT (forall a. a->a)
343
344 pattern P :: (Int -> Int) -> T
345 pattern P x <- MkT x
346
347 This should work. But in the matcher we must match against MkT, and then
348 instantiate its argument 'x', to get a function of type (Int -> Int).
349 Equality is not enough! Trac #13752 was an example.
350
351 Note [Pattern synonym existentials do not scope]
352 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
353 Consider this (Trac #14498):
354 pattern SS :: forall (t :: k). () =>
355 => forall (a :: kk -> k) (n :: kk).
356 => TypeRep n -> TypeRep t
357 pattern SS n <- (App (Typeable :: TypeRep (a::kk -> k)) n)
358
359 Here 'k' is implicitly bound in the signature, but (with
360 -XScopedTypeVariables) it does still scope over the pattern-synonym
361 definition. But what about 'kk', which is oexistential? It too is
362 implicitly bound in the signature; should it too scope? And if so,
363 what type variable is it bound to?
364
365 The trouble is that the type variable to which it is bound is itself
366 only brought into scope in part the pattern, so it makes no sense for
367 'kk' to scope over the whole pattern. See the discussion on
368 Trac #14498, esp comment:16ff. Here is a simpler example:
369 data T where { MkT :: x -> (x->Int) -> T }
370 pattern P :: () => forall x. x -> (x->Int) -> T
371 pattern P a b = (MkT a b, True)
372
373 Here it would make no sense to mention 'x' in the True pattern,
374 like this:
375 pattern P a b = (MkT a b, True :: x)
376
377 The 'x' only makes sense "under" the MkT pattern. Conclusion: the
378 existential type variables of a pattern-synonym signature should not
379 scope.
380
381 But it's not that easy to implement, because we don't know
382 exactly what the existentials /are/ until we get to type checking.
383 (See Note [The pattern-synonym signature splitting rule], and
384 the partition of implicit_tvs in tcCheckPatSynDecl.)
385
386 So we do this:
387
388 - The reaner brings all the implicitly-bound kind variables into
389 scope, without trying to distinguish universal from existential
390
391 - tcCheckPatSynDecl uses tcExtendKindEnvList to bind the
392 implicitly-bound existentials to
393 APromotionErr PatSynExPE
394 It's not really a promotion error, but it's a way to bind the Name
395 (which the renamer has not complained about) to something that, when
396 looked up, will cause a complaint (in this case
397 TcHsType.promotionErr)
398
399
400 Note [The pattern-synonym signature splitting rule]
401 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
402 Given a pattern signature, we must split
403 the kind-generalised variables, and
404 the implicitly-bound variables
405 into universal and existential. The rule is this
406 (see discussion on Trac #11224):
407
408 The universal tyvars are the ones mentioned in
409 - univ_tvs: the user-specified (forall'd) universals
410 - req_theta
411 - res_ty
412 The existential tyvars are all the rest
413
414 For example
415
416 pattern P :: () => b -> T a
417 pattern P x = ...
418
419 Here 'a' is universal, and 'b' is existential. But there is a wrinkle:
420 how do we split the arg_tys from req_ty? Consider
421
422 pattern Q :: () => b -> S c -> T a
423 pattern Q x = ...
424
425 This is an odd example because Q has only one syntactic argument, and
426 so presumably is defined by a view pattern matching a function. But
427 it can happen (Trac #11977, #12108).
428
429 We don't know Q's arity from the pattern signature, so we have to wait
430 until we see the pattern declaration itself before deciding res_ty is,
431 and hence which variables are existential and which are universal.
432
433 And that in turn is why TcPatSynInfo has a separate field,
434 patsig_implicit_bndrs, to capture the implicitly bound type variables,
435 because we don't yet know how to split them up.
436
437 It's a slight compromise, because it means we don't really know the
438 pattern synonym's real signature until we see its declaration. So,
439 for example, in hs-boot file, we may need to think what to do...
440 (eg don't have any implicitly-bound variables).
441
442
443 Note [Checking against a pattern signature]
444 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
445 When checking the actual supplied pattern against the pattern synonym
446 signature, we need to be quite careful.
447
448 ----- Provided constraints
449 Example
450
451 data T a where
452 MkT :: Ord a => a -> T a
453
454 pattern P :: () => Eq a => a -> [T a]
455 pattern P x = [MkT x]
456
457 We must check that the (Eq a) that P claims to bind (and to
458 make available to matches against P), is derivable from the
459 actual pattern. For example:
460 f (P (x::a)) = ...here (Eq a) should be available...
461 And yes, (Eq a) is derivable from the (Ord a) bound by P's rhs.
462
463 ----- Existential type variables
464 Unusually, we instantiate the existential tyvars of the pattern with
465 *meta* type variables. For example
466
467 data S where
468 MkS :: Eq a => [a] -> S
469
470 pattern P :: () => Eq x => x -> S
471 pattern P x <- MkS x
472
473 The pattern synonym conceals from its client the fact that MkS has a
474 list inside it. The client just thinks it's a type 'x'. So we must
475 unify x := [a] during type checking, and then use the instantiating type
476 [a] (called ex_tys) when building the matcher. In this case we'll get
477
478 $mP :: S -> (forall x. Ex x => x -> r) -> r -> r
479 $mP x k = case x of
480 MkS a (d:Eq a) (ys:[a]) -> let dl :: Eq [a]
481 dl = $dfunEqList d
482 in k [a] dl ys
483
484 All this applies when type-checking the /matching/ side of
485 a pattern synonym. What about the /building/ side?
486
487 * For Unidirectional, there is no builder
488
489 * For ExplicitBidirectional, the builder is completely separate
490 code, typechecked in tcPatSynBuilderBind
491
492 * For ImplicitBidirectional, the builder is still typechecked in
493 tcPatSynBuilderBind, by converting the pattern to an expression and
494 typechecking it.
495
496 At one point, for ImplicitBidirectional I used SigTvs (instead of
497 TauTvs) in tcCheckPatSynDecl. But (a) strengthening the check here
498 is redundant since tcPatSynBuilderBind does the job, (b) it was
499 still incomplete (SigTvs can unify with each other), and (c) it
500 didn't even work (Trac #13441 was accepted with
501 ExplicitBidirectional, but rejected if expressed in
502 ImplicitBidirectional form. Conclusion: trying to be too clever is
503 a bad idea.
504 -}
505
506 collectPatSynArgInfo :: HsPatSynDetails (Located Name)
507 -> ([Name], [Name], Bool)
508 collectPatSynArgInfo details =
509 case details of
510 PrefixCon names -> (map unLoc names, [], False)
511 InfixCon name1 name2 -> (map unLoc [name1, name2], [], True)
512 RecCon names -> (vars, sels, False)
513 where
514 (vars, sels) = unzip (map splitRecordPatSyn names)
515 where
516 splitRecordPatSyn :: RecordPatSynField (Located Name)
517 -> (Name, Name)
518 splitRecordPatSyn (RecordPatSynField { recordPatSynPatVar = L _ patVar
519 , recordPatSynSelectorId = L _ selId })
520 = (patVar, selId)
521
522 addPatSynCtxt :: Located Name -> TcM a -> TcM a
523 addPatSynCtxt (L loc name) thing_inside
524 = setSrcSpan loc $
525 addErrCtxt (text "In the declaration for pattern synonym"
526 <+> quotes (ppr name)) $
527 thing_inside
528
529 wrongNumberOfParmsErr :: Name -> Arity -> Arity -> TcM a
530 wrongNumberOfParmsErr name decl_arity missing
531 = failWithTc $
532 hang (text "Pattern synonym" <+> quotes (ppr name) <+> ptext (sLit "has")
533 <+> speakNOf decl_arity (text "argument"))
534 2 (text "but its type signature has" <+> int missing <+> text "fewer arrows")
535
536 -------------------------
537 -- Shared by both tcInferPatSyn and tcCheckPatSyn
538 tc_patsyn_finish :: Located Name -- ^ PatSyn Name
539 -> HsPatSynDir GhcRn -- ^ PatSyn type (Uni/Bidir/ExplicitBidir)
540 -> Bool -- ^ Whether infix
541 -> LPat GhcTc -- ^ Pattern of the PatSyn
542 -> ([TcTyVarBinder], [PredType], TcEvBinds, [EvVar])
543 -> ([TcTyVarBinder], [TcType], [PredType], [EvExpr])
544 -> ([LHsExpr GhcTcId], [TcType]) -- ^ Pattern arguments and
545 -- types
546 -> TcType -- ^ Pattern type
547 -> [Name] -- ^ Selector names
548 -- ^ Whether fields, empty if not record PatSyn
549 -> TcM (LHsBinds GhcTc, TcGblEnv)
550 tc_patsyn_finish lname dir is_infix lpat'
551 (univ_tvs, req_theta, req_ev_binds, req_dicts)
552 (ex_tvs, ex_tys, prov_theta, prov_dicts)
553 (args, arg_tys)
554 pat_ty field_labels
555 = do { -- Zonk everything. We are about to build a final PatSyn
556 -- so there had better be no unification variables in there
557
558 (ze, univ_tvs') <- zonkTyVarBindersX emptyZonkEnv univ_tvs
559 ; req_theta' <- zonkTcTypeToTypes ze req_theta
560 ; (ze, ex_tvs') <- zonkTyVarBindersX ze ex_tvs
561 ; prov_theta' <- zonkTcTypeToTypes ze prov_theta
562 ; pat_ty' <- zonkTcTypeToType ze pat_ty
563 ; arg_tys' <- zonkTcTypeToTypes ze arg_tys
564
565 ; let (env1, univ_tvs) = tidyTyVarBinders emptyTidyEnv univ_tvs'
566 (env2, ex_tvs) = tidyTyVarBinders env1 ex_tvs'
567 req_theta = tidyTypes env2 req_theta'
568 prov_theta = tidyTypes env2 prov_theta'
569 arg_tys = tidyTypes env2 arg_tys'
570 pat_ty = tidyType env2 pat_ty'
571
572 ; traceTc "tc_patsyn_finish {" $
573 ppr (unLoc lname) $$ ppr (unLoc lpat') $$
574 ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
575 ppr (ex_tvs, prov_theta, prov_dicts) $$
576 ppr args $$
577 ppr arg_tys $$
578 ppr pat_ty
579
580 -- Make the 'matcher'
581 ; (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat'
582 (binderVars univ_tvs, req_theta, req_ev_binds, req_dicts)
583 (binderVars ex_tvs, ex_tys, prov_theta, prov_dicts)
584 (args, arg_tys)
585 pat_ty
586
587 -- Make the 'builder'
588 ; builder_id <- mkPatSynBuilderId dir lname
589 univ_tvs req_theta
590 ex_tvs prov_theta
591 arg_tys pat_ty
592
593 -- TODO: Make this have the proper information
594 ; let mkFieldLabel name = FieldLabel { flLabel = occNameFS (nameOccName name)
595 , flIsOverloaded = False
596 , flSelector = name }
597 field_labels' = map mkFieldLabel field_labels
598
599
600 -- Make the PatSyn itself
601 ; let patSyn = mkPatSyn (unLoc lname) is_infix
602 (univ_tvs, req_theta)
603 (ex_tvs, prov_theta)
604 arg_tys
605 pat_ty
606 matcher_id builder_id
607 field_labels'
608
609 -- Selectors
610 ; let rn_rec_sel_binds = mkPatSynRecSelBinds patSyn (patSynFieldLabels patSyn)
611 tything = AConLike (PatSynCon patSyn)
612 ; tcg_env <- tcExtendGlobalEnv [tything] $
613 tcRecSelBinds rn_rec_sel_binds
614
615 ; traceTc "tc_patsyn_finish }" empty
616 ; return (matcher_bind, tcg_env) }
617
618 {-
619 ************************************************************************
620 * *
621 Constructing the "matcher" Id and its binding
622 * *
623 ************************************************************************
624 -}
625
626 tcPatSynMatcher :: Located Name
627 -> LPat GhcTc
628 -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
629 -> ([TcTyVar], [TcType], ThetaType, [EvExpr])
630 -> ([LHsExpr GhcTcId], [TcType])
631 -> TcType
632 -> TcM ((Id, Bool), LHsBinds GhcTc)
633 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
634 tcPatSynMatcher (L loc name) lpat
635 (univ_tvs, req_theta, req_ev_binds, req_dicts)
636 (ex_tvs, ex_tys, prov_theta, prov_dicts)
637 (args, arg_tys) pat_ty
638 = do { rr_name <- newNameAt (mkTyVarOcc "rep") loc
639 ; tv_name <- newNameAt (mkTyVarOcc "r") loc
640 ; let rr_tv = mkTcTyVar rr_name runtimeRepTy vanillaSkolemTv
641 rr = mkTyVarTy rr_tv
642 res_tv = mkTcTyVar tv_name (tYPE rr) vanillaSkolemTv
643 res_ty = mkTyVarTy res_tv
644 is_unlifted = null args && null prov_dicts
645 (cont_args, cont_arg_tys)
646 | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
647 | otherwise = (args, arg_tys)
648 cont_ty = mkInfSigmaTy ex_tvs prov_theta $
649 mkFunTys cont_arg_tys res_ty
650
651 fail_ty = mkFunTy voidPrimTy res_ty
652
653 ; matcher_name <- newImplicitBinder name mkMatcherOcc
654 ; scrutinee <- newSysLocalId (fsLit "scrut") pat_ty
655 ; cont <- newSysLocalId (fsLit "cont") cont_ty
656 ; fail <- newSysLocalId (fsLit "fail") fail_ty
657
658 ; let matcher_tau = mkFunTys [pat_ty, cont_ty, fail_ty] res_ty
659 matcher_sigma = mkInfSigmaTy (rr_tv:res_tv:univ_tvs) req_theta matcher_tau
660 matcher_id = mkExportedVanillaId matcher_name matcher_sigma
661 -- See Note [Exported LocalIds] in Id
662
663 inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys
664 cont' = foldl nlHsApp (mkLHsWrap inst_wrap (nlHsVar cont)) cont_args
665
666 fail' = nlHsApps fail [nlHsVar voidPrimId]
667
668 args = map nlVarPat [scrutinee, cont, fail]
669 lwpat = noLoc $ WildPat pat_ty
670 cases = if isIrrefutableHsPat lpat
671 then [mkHsCaseAlt lpat cont']
672 else [mkHsCaseAlt lpat cont',
673 mkHsCaseAlt lwpat fail']
674 body = mkLHsWrap (mkWpLet req_ev_binds) $
675 L (getLoc lpat) $
676 HsCase (nlHsVar scrutinee) $
677 MG{ mg_alts = L (getLoc lpat) cases
678 , mg_arg_tys = [pat_ty]
679 , mg_res_ty = res_ty
680 , mg_origin = Generated
681 }
682 body' = noLoc $
683 HsLam $
684 MG{ mg_alts = noLoc [mkSimpleMatch LambdaExpr
685 args body]
686 , mg_arg_tys = [pat_ty, cont_ty, fail_ty]
687 , mg_res_ty = res_ty
688 , mg_origin = Generated
689 }
690 match = mkMatch (mkPrefixFunRhs (L loc name)) []
691 (mkHsLams (rr_tv:res_tv:univ_tvs)
692 req_dicts body')
693 (noLoc EmptyLocalBinds)
694 mg :: MatchGroup GhcTc (LHsExpr GhcTc)
695 mg = MG{ mg_alts = L (getLoc match) [match]
696 , mg_arg_tys = []
697 , mg_res_ty = res_ty
698 , mg_origin = Generated
699 }
700
701 ; let bind = FunBind{ fun_id = L loc matcher_id
702 , fun_matches = mg
703 , fun_co_fn = idHsWrapper
704 , bind_fvs = emptyNameSet
705 , fun_tick = [] }
706 matcher_bind = unitBag (noLoc bind)
707
708 ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
709 ; traceTc "tcPatSynMatcher" (ppr matcher_bind)
710
711 ; return ((matcher_id, is_unlifted), matcher_bind) }
712
713 mkPatSynRecSelBinds :: PatSyn
714 -> [FieldLabel] -- ^ Visible field labels
715 -> HsValBinds GhcRn
716 mkPatSynRecSelBinds ps fields
717 = ValBindsOut selector_binds sigs
718 where
719 (sigs, selector_binds) = unzip (map mkRecSel fields)
720 mkRecSel fld_lbl = mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl
721
722 isUnidirectional :: HsPatSynDir a -> Bool
723 isUnidirectional Unidirectional = True
724 isUnidirectional ImplicitBidirectional = False
725 isUnidirectional ExplicitBidirectional{} = False
726
727 {-
728 ************************************************************************
729 * *
730 Constructing the "builder" Id
731 * *
732 ************************************************************************
733 -}
734
735 mkPatSynBuilderId :: HsPatSynDir a -> Located Name
736 -> [TyVarBinder] -> ThetaType
737 -> [TyVarBinder] -> ThetaType
738 -> [Type] -> Type
739 -> TcM (Maybe (Id, Bool))
740 mkPatSynBuilderId dir (L _ name)
741 univ_bndrs req_theta ex_bndrs prov_theta
742 arg_tys pat_ty
743 | isUnidirectional dir
744 = return Nothing
745 | otherwise
746 = do { builder_name <- newImplicitBinder name mkBuilderOcc
747 ; let theta = req_theta ++ prov_theta
748 need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
749 builder_sigma = add_void need_dummy_arg $
750 mkForAllTys univ_bndrs $
751 mkForAllTys ex_bndrs $
752 mkFunTys theta $
753 mkFunTys arg_tys $
754 pat_ty
755 builder_id = mkExportedVanillaId builder_name builder_sigma
756 -- See Note [Exported LocalIds] in Id
757
758 builder_id' = modifyIdInfo (`setLevityInfoWithType` pat_ty) builder_id
759
760 ; return (Just (builder_id', need_dummy_arg)) }
761 where
762
763 tcPatSynBuilderBind :: PatSynBind GhcRn GhcRn
764 -> TcM (LHsBinds GhcTc)
765 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
766 tcPatSynBuilderBind (PSB { psb_id = L loc name, psb_def = lpat
767 , psb_dir = dir, psb_args = details })
768 | isUnidirectional dir
769 = return emptyBag
770
771 | Left why <- mb_match_group -- Can't invert the pattern
772 = setSrcSpan (getLoc lpat) $ failWithTc $
773 vcat [ hang (text "Invalid right-hand side of bidirectional pattern synonym"
774 <+> quotes (ppr name) <> colon)
775 2 why
776 , text "RHS pattern:" <+> ppr lpat ]
777
778 | Right match_group <- mb_match_group -- Bidirectional
779 = do { patsyn <- tcLookupPatSyn name
780 ; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn
781 -- Bidirectional, so patSynBuilder returns Just
782
783 match_group' | need_dummy_arg = add_dummy_arg match_group
784 | otherwise = match_group
785
786 bind = FunBind { fun_id = L loc (idName builder_id)
787 , fun_matches = match_group'
788 , fun_co_fn = idHsWrapper
789 , bind_fvs = placeHolderNamesTc
790 , fun_tick = [] }
791
792 sig = completeSigFromId (PatSynCtxt name) builder_id
793
794 ; traceTc "tcPatSynBuilderBind {" $
795 ppr patsyn $$ ppr builder_id <+> dcolon <+> ppr (idType builder_id)
796 ; (builder_binds, _) <- tcPolyCheck emptyPragEnv sig (noLoc bind)
797 ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
798 ; return builder_binds }
799
800 | otherwise = panic "tcPatSynBuilderBind" -- Both cases dealt with
801 where
802 mb_match_group
803 = case dir of
804 ExplicitBidirectional explicit_mg -> Right explicit_mg
805 ImplicitBidirectional -> fmap mk_mg (tcPatToExpr name args lpat)
806 Unidirectional -> panic "tcPatSynBuilderBind"
807
808 mk_mg :: LHsExpr GhcRn -> MatchGroup GhcRn (LHsExpr GhcRn)
809 mk_mg body = mkMatchGroup Generated [builder_match]
810 where
811 builder_args = [L loc (VarPat (L loc n)) | L loc n <- args]
812 builder_match = mkMatch (mkPrefixFunRhs (L loc name))
813 builder_args body
814 (noLoc EmptyLocalBinds)
815
816 args = case details of
817 PrefixCon args -> args
818 InfixCon arg1 arg2 -> [arg1, arg2]
819 RecCon args -> map recordPatSynPatVar args
820
821 add_dummy_arg :: MatchGroup GhcRn (LHsExpr GhcRn)
822 -> MatchGroup GhcRn (LHsExpr GhcRn)
823 add_dummy_arg mg@(MG { mg_alts = L l [L loc match@(Match { m_pats = pats })] })
824 = mg { mg_alts = L l [L loc (match { m_pats = nlWildPatName : pats })] }
825 add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
826 pprMatches other_mg
827
828 tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr GhcTcId, TcSigmaType)
829 -- monadic only for failure
830 tcPatSynBuilderOcc ps
831 | Just (builder_id, add_void_arg) <- builder
832 , let builder_expr = HsConLikeOut (PatSynCon ps)
833 builder_ty = idType builder_id
834 = return $
835 if add_void_arg
836 then ( builder_expr -- still just return builder_expr; the void# arg is added
837 -- by dsConLike in the desugarer
838 , tcFunResultTy builder_ty )
839 else (builder_expr, builder_ty)
840
841 | otherwise -- Unidirectional
842 = nonBidirectionalErr name
843 where
844 name = patSynName ps
845 builder = patSynBuilder ps
846
847 add_void :: Bool -> Type -> Type
848 add_void need_dummy_arg ty
849 | need_dummy_arg = mkFunTy voidPrimTy ty
850 | otherwise = ty
851
852 tcPatToExpr :: Name -> [Located Name] -> LPat GhcRn
853 -> Either MsgDoc (LHsExpr GhcRn)
854 -- Given a /pattern/, return an /expression/ that builds a value
855 -- that matches the pattern. E.g. if the pattern is (Just [x]),
856 -- the expression is (Just [x]). They look the same, but the
857 -- input uses constructors from HsPat and the output uses constructors
858 -- from HsExpr.
859 --
860 -- Returns (Left r) if the pattern is not invertible, for reason r.
861 -- See Note [Builder for a bidirectional pattern synonym]
862 tcPatToExpr name args pat = go pat
863 where
864 lhsVars = mkNameSet (map unLoc args)
865
866 -- Make a prefix con for prefix and infix patterns for simplicity
867 mkPrefixConExpr :: Located Name -> [LPat GhcRn]
868 -> Either MsgDoc (HsExpr GhcRn)
869 mkPrefixConExpr lcon@(L loc _) pats
870 = do { exprs <- mapM go pats
871 ; return (foldl (\x y -> HsApp (L loc x) y)
872 (HsVar lcon) exprs) }
873
874 mkRecordConExpr :: Located Name -> HsRecFields GhcRn (LPat GhcRn)
875 -> Either MsgDoc (HsExpr GhcRn)
876 mkRecordConExpr con fields
877 = do { exprFields <- mapM go fields
878 ; return (RecordCon con PlaceHolder noPostTcExpr exprFields) }
879
880 go :: LPat GhcRn -> Either MsgDoc (LHsExpr GhcRn)
881 go (L loc p) = L loc <$> go1 p
882
883 go1 :: Pat GhcRn -> Either MsgDoc (HsExpr GhcRn)
884 go1 (ConPatIn con info)
885 = case info of
886 PrefixCon ps -> mkPrefixConExpr con ps
887 InfixCon l r -> mkPrefixConExpr con [l,r]
888 RecCon fields -> mkRecordConExpr con fields
889
890 go1 (SigPatIn pat _) = go1 (unLoc pat)
891 -- See Note [Type signatures and the builder expression]
892
893 go1 (VarPat (L l var))
894 | var `elemNameSet` lhsVars
895 = return $ HsVar (L l var)
896 | otherwise
897 = Left (quotes (ppr var) <+> text "is not bound by the LHS of the pattern synonym")
898 go1 (ParPat pat) = fmap HsPar $ go pat
899 go1 (PArrPat pats ptt) = do { exprs <- mapM go pats
900 ; return $ ExplicitPArr ptt exprs }
901 go1 p@(ListPat pats ptt reb)
902 | Nothing <- reb = do { exprs <- mapM go pats
903 ; return $ ExplicitList ptt Nothing exprs }
904 | otherwise = notInvertibleListPat p
905 go1 (TuplePat pats box _) = do { exprs <- mapM go pats
906 ; return $ ExplicitTuple
907 (map (noLoc . Present) exprs) box }
908 go1 (SumPat pat alt arity _) = do { expr <- go1 (unLoc pat)
909 ; return $ ExplicitSum alt arity (noLoc expr) PlaceHolder
910 }
911 go1 (LitPat lit) = return $ HsLit lit
912 go1 (NPat (L _ n) mb_neg _ _)
913 | Just neg <- mb_neg = return $ unLoc $ nlHsSyntaxApps neg [noLoc (HsOverLit n)]
914 | otherwise = return $ HsOverLit n
915 go1 (ConPatOut{}) = panic "ConPatOut in output of renamer"
916 go1 (SigPatOut{}) = panic "SigPatOut in output of renamer"
917 go1 (CoPat{}) = panic "CoPat in output of renamer"
918 go1 (SplicePat (HsSpliced _ (HsSplicedPat pat)))
919 = go1 pat
920 go1 (SplicePat (HsSpliced{})) = panic "Invalid splice variety"
921
922 -- The following patterns are not invertible.
923 go1 p@(BangPat {}) = notInvertible p -- #14112
924 go1 p@(LazyPat {}) = notInvertible p
925 go1 p@(WildPat {}) = notInvertible p
926 go1 p@(AsPat {}) = notInvertible p
927 go1 p@(ViewPat {}) = notInvertible p
928 go1 p@(NPlusKPat {}) = notInvertible p
929 go1 p@(SplicePat (HsTypedSplice {})) = notInvertible p
930 go1 p@(SplicePat (HsUntypedSplice {})) = notInvertible p
931 go1 p@(SplicePat (HsQuasiQuote {})) = notInvertible p
932
933 notInvertible p = Left (not_invertible_msg p)
934
935 not_invertible_msg p
936 = text "Pattern" <+> quotes (ppr p) <+> text "is not invertible"
937 $+$ hang (text "Suggestion: instead use an explicitly bidirectional"
938 <+> text "pattern synonym, e.g.")
939 2 (hang (text "pattern" <+> pp_name <+> pp_args <+> larrow
940 <+> ppr pat <+> text "where")
941 2 (pp_name <+> pp_args <+> equals <+> text "..."))
942 where
943 pp_name = ppr name
944 pp_args = hsep (map ppr args)
945
946 -- We should really be able to invert list patterns, even when
947 -- rebindable syntax is on, but doing so involves a bit of
948 -- refactoring; see Trac #14380. Until then we reject with a
949 -- helpful error message.
950 notInvertibleListPat p
951 = Left (vcat [ not_invertible_msg p
952 , text "Reason: rebindable syntax is on."
953 , text "This is fixable: add use-case to Trac #14380" ])
954
955 {- Note [Builder for a bidirectional pattern synonym]
956 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
957 For a bidirectional pattern synonym we need to produce an /expression/
958 that matches the supplied /pattern/, given values for the arguments
959 of the pattern synoymy. For example
960 pattern F x y = (Just x, [y])
961 The 'builder' for F looks like
962 $builderF x y = (Just x, [y])
963
964 We can't always do this:
965 * Some patterns aren't invertible; e.g. view patterns
966 pattern F x = (reverse -> x:_)
967
968 * The RHS pattern might bind more variables than the pattern
969 synonym, so again we can't invert it
970 pattern F x = (x,y)
971
972 * Ditto wildcards
973 pattern F x = (x,_)
974
975
976 Note [Redundant constraints for builder]
977 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
978 The builder can have redundant constraints, which are awkard to eliminate.
979 Consider
980 pattern P = Just 34
981 To match against this pattern we need (Eq a, Num a). But to build
982 (Just 34) we need only (Num a). Fortunately instTcSigFromId sets
983 sig_warn_redundant to False.
984
985 ************************************************************************
986 * *
987 Helper functions
988 * *
989 ************************************************************************
990
991 Note [As-patterns in pattern synonym definitions]
992 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
993 The rationale for rejecting as-patterns in pattern synonym definitions
994 is that an as-pattern would introduce nonindependent pattern synonym
995 arguments, e.g. given a pattern synonym like:
996
997 pattern K x y = x@(Just y)
998
999 one could write a nonsensical function like
1000
1001 f (K Nothing x) = ...
1002
1003 or
1004 g (K (Just True) False) = ...
1005
1006 Note [Type signatures and the builder expression]
1007 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1008 Consider
1009 pattern L x = Left x :: Either [a] [b]
1010
1011 In tc{Infer/Check}PatSynDecl we will check that the pattern has the
1012 specified type. We check the pattern *as a pattern*, so the type
1013 signature is a pattern signature, and so brings 'a' and 'b' into
1014 scope. But we don't have a way to bind 'a, b' in the LHS, as we do
1015 'x', say. Nevertheless, the sigature may be useful to constrain
1016 the type.
1017
1018 When making the binding for the *builder*, though, we don't want
1019 $buildL x = Left x :: Either [a] [b]
1020 because that wil either mean (forall a b. Either [a] [b]), or we'll
1021 get a complaint that 'a' and 'b' are out of scope. (Actually the
1022 latter; Trac #9867.) No, the job of the signature is done, so when
1023 converting the pattern to an expression (for the builder RHS) we
1024 simply discard the signature.
1025
1026 Note [Record PatSyn Desugaring]
1027 -------------------------------
1028 It is important that prov_theta comes before req_theta as this ordering is used
1029 when desugaring record pattern synonym updates.
1030
1031 Any change to this ordering should make sure to change deSugar/DsExpr.hs if you
1032 want to avoid difficult to decipher core lint errors!
1033 -}
1034
1035 tcCheckPatSynPat :: LPat GhcRn -> TcM ()
1036 tcCheckPatSynPat = go
1037 where
1038 go :: LPat GhcRn -> TcM ()
1039 go = addLocM go1
1040
1041 go1 :: Pat GhcRn -> TcM ()
1042 -- See Note [Bad patterns]
1043 go1 p@(AsPat _ _) = asPatInPatSynErr p
1044 go1 p@NPlusKPat{} = nPlusKPatInPatSynErr p
1045
1046 go1 (ConPatIn _ info) = mapM_ go (hsConPatArgs info)
1047 go1 VarPat{} = return ()
1048 go1 WildPat{} = return ()
1049 go1 (LazyPat pat) = go pat
1050 go1 (ParPat pat) = go pat
1051 go1 (BangPat pat) = go pat
1052 go1 (PArrPat pats _) = mapM_ go pats
1053 go1 (ListPat pats _ _) = mapM_ go pats
1054 go1 (TuplePat pats _ _) = mapM_ go pats
1055 go1 (SumPat pat _ _ _) = go pat
1056 go1 LitPat{} = return ()
1057 go1 NPat{} = return ()
1058 go1 (SigPatIn pat _) = go pat
1059 go1 (ViewPat _ pat _) = go pat
1060 go1 (SplicePat splice)
1061 | HsSpliced mod_finalizers (HsSplicedPat pat) <- splice
1062 = do addModFinalizersWithLclEnv mod_finalizers
1063 go1 pat
1064 | otherwise = panic "non-pattern from spliced thing"
1065 go1 ConPatOut{} = panic "ConPatOut in output of renamer"
1066 go1 SigPatOut{} = panic "SigPatOut in output of renamer"
1067 go1 CoPat{} = panic "CoPat in output of renamer"
1068
1069 asPatInPatSynErr :: (SourceTextX p, OutputableBndrId p) => Pat p -> TcM a
1070 asPatInPatSynErr pat
1071 = failWithTc $
1072 hang (text "Pattern synonym definition cannot contain as-patterns (@):")
1073 2 (ppr pat)
1074
1075 nPlusKPatInPatSynErr :: (SourceTextX p, OutputableBndrId p) => Pat p -> TcM a
1076 nPlusKPatInPatSynErr pat
1077 = failWithTc $
1078 hang (text "Pattern synonym definition cannot contain n+k-pattern:")
1079 2 (ppr pat)
1080
1081 {- Note [Bad patterns]
1082 ~~~~~~~~~~~~~~~~~~~~~~
1083 We don't currently allow as-patterns or n+k patterns in a pattern synonym.
1084 Reason: consider
1085 pattern P x y = x@(Just y)
1086
1087 What would
1088 f (P Nothing False) = e
1089 mean? Presumably something like
1090 f Nothing@(Just False) = e
1091 But as-patterns don't allow a pattern before the @ sign! Perhaps they
1092 should -- with p1@p2 meaning match both p1 and p2 -- but they don't
1093 currently. Hence bannning them in pattern synonyms. Actually lifting
1094 the restriction would be simple and well-defined. See Trac #9793.
1095 -}
1096
1097
1098 nonBidirectionalErr :: Outputable name => name -> TcM a
1099 nonBidirectionalErr name = failWithTc $
1100 text "non-bidirectional pattern synonym"
1101 <+> quotes (ppr name) <+> text "used in an expression"
1102
1103 -- Walk the whole pattern and for all ConPatOuts, collect the
1104 -- existentially-bound type variables and evidence binding variables.
1105 --
1106 -- These are used in computing the type of a pattern synonym and also
1107 -- in generating matcher functions, since success continuations need
1108 -- to be passed these pattern-bound evidences.
1109 tcCollectEx
1110 :: LPat GhcTc
1111 -> ( [TyVar] -- Existentially-bound type variables
1112 -- in correctly-scoped order; e.g. [ k:*, x:k ]
1113 , [EvVar] ) -- and evidence variables
1114
1115 tcCollectEx pat = go pat
1116 where
1117 go :: LPat GhcTc -> ([TyVar], [EvVar])
1118 go = go1 . unLoc
1119
1120 go1 :: Pat GhcTc -> ([TyVar], [EvVar])
1121 go1 (LazyPat p) = go p
1122 go1 (AsPat _ p) = go p
1123 go1 (ParPat p) = go p
1124 go1 (BangPat p) = go p
1125 go1 (ListPat ps _ _) = mergeMany . map go $ ps
1126 go1 (TuplePat ps _ _) = mergeMany . map go $ ps
1127 go1 (SumPat p _ _ _) = go p
1128 go1 (PArrPat ps _) = mergeMany . map go $ ps
1129 go1 (ViewPat _ p _) = go p
1130 go1 con@ConPatOut{} = merge (pat_tvs con, pat_dicts con) $
1131 goConDetails $ pat_args con
1132 go1 (SigPatOut p _) = go p
1133 go1 (CoPat _ p _) = go1 p
1134 go1 (NPlusKPat n k _ geq subtract _)
1135 = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract
1136 go1 _ = empty
1137
1138 goConDetails :: HsConPatDetails GhcTc -> ([TyVar], [EvVar])
1139 goConDetails (PrefixCon ps) = mergeMany . map go $ ps
1140 goConDetails (InfixCon p1 p2) = go p1 `merge` go p2
1141 goConDetails (RecCon HsRecFields{ rec_flds = flds })
1142 = mergeMany . map goRecFd $ flds
1143
1144 goRecFd :: LHsRecField GhcTc (LPat GhcTc) -> ([TyVar], [EvVar])
1145 goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p
1146
1147 merge (vs1, evs1) (vs2, evs2) = (vs1 ++ vs2, evs1 ++ evs2)
1148 mergeMany = foldr merge empty
1149 empty = ([], [])