Implement QuantifiedConstraints
[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
76 ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
77 ; (tclvl, wanted, ((lpat', args), pat_ty))
78 <- pushLevelAndCaptureConstraints $
79 tcInferNoInst $ \ exp_ty ->
80 tcPat PatSyn lpat exp_ty $
81 mapM tcLookupId arg_names
82
83 ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
84
85 ; (qtvs, req_dicts, ev_binds, _) <- simplifyInfer tclvl NoRestrictions []
86 named_taus wanted
87
88 ; let (ex_tvs, prov_dicts) = tcCollectEx lpat'
89 ex_tv_set = mkVarSet ex_tvs
90 univ_tvs = filterOut (`elemVarSet` ex_tv_set) qtvs
91 req_theta = map evVarPred req_dicts
92
93 ; prov_dicts <- mapM zonkId prov_dicts
94 ; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts
95 prov_theta = map evVarPred filtered_prov_dicts
96 -- Filtering: see Note [Remove redundant provided dicts]
97
98 -- Report bad universal type variables
99 -- See Note [Type variables whose kind is captured]
100 ; let bad_tvs = [ tv | tv <- univ_tvs
101 , tyCoVarsOfType (tyVarKind tv)
102 `intersectsVarSet` ex_tv_set ]
103 ; mapM_ (badUnivTvErr ex_tvs) bad_tvs
104
105 -- Report coercions that esacpe
106 -- See Note [Coercions that escape]
107 ; args <- mapM zonkId args
108 ; let bad_args = [ (arg, bad_cos) | arg <- args ++ prov_dicts
109 , let bad_cos = filterDVarSet isId $
110 (tyCoVarsOfTypeDSet (idType arg))
111 , not (isEmptyDVarSet bad_cos) ]
112 ; mapM_ dependentArgErr bad_args
113
114 ; traceTc "tcInferPatSynDecl }" $ (ppr name $$ ppr ex_tvs)
115 ; tc_patsyn_finish lname dir is_infix lpat'
116 (mkTyVarBinders Inferred univ_tvs
117 , req_theta, ev_binds, req_dicts)
118 (mkTyVarBinders Inferred ex_tvs
119 , mkTyVarTys ex_tvs, prov_theta
120 , map (EvExpr . evId) filtered_prov_dicts)
121 (map nlHsVar args, map idType args)
122 pat_ty rec_fields }
123 tcInferPatSynDecl (XPatSynBind _) = panic "tcInferPatSynDecl"
124
125 badUnivTvErr :: [TyVar] -> TyVar -> TcM ()
126 -- See Note [Type variables whose kind is captured]
127 badUnivTvErr ex_tvs bad_tv
128 = addErrTc $
129 vcat [ text "Universal type variable" <+> quotes (ppr bad_tv)
130 <+> text "has existentially bound kind:"
131 , nest 2 (ppr_with_kind bad_tv)
132 , hang (text "Existentially-bound variables:")
133 2 (vcat (map ppr_with_kind ex_tvs))
134 , text "Probable fix: give the pattern synoym a type signature"
135 ]
136 where
137 ppr_with_kind tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
138
139 dependentArgErr :: (Id, DTyCoVarSet) -> TcM ()
140 -- See Note [Coercions that escape]
141 dependentArgErr (arg, bad_cos)
142 = addErrTc $
143 vcat [ text "Iceland Jack! Iceland Jack! Stop torturing me!"
144 , hang (text "Pattern-bound variable")
145 2 (ppr arg <+> dcolon <+> ppr (idType arg))
146 , nest 2 $
147 hang (text "has a type that mentions pattern-bound coercion"
148 <> plural bad_co_list <> colon)
149 2 (pprWithCommas ppr bad_co_list)
150 , text "Hint: use -fprint-explicit-coercions to see the coercions"
151 , text "Probable fix: add a pattern signature" ]
152 where
153 bad_co_list = dVarSetElems bad_cos
154
155 {- Note [Remove redundant provided dicts]
156 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
157 Recall that
158 HRefl :: forall k1 k2 (a1:k1) (a2:k2). (k1 ~ k2, a1 ~ a2)
159 => a1 :~~: a2
160 (NB: technically the (k1~k2) existential dictionary is not necessary,
161 but it's there at the moment.)
162
163 Now consider (Trac #14394):
164 pattern Foo = HRefl
165 in a non-poly-kinded module. We don't want to get
166 pattern Foo :: () => (* ~ *, b ~ a) => a :~~: b
167 with that redundant (* ~ *). We'd like to remove it; hence the call to
168 mkMinimalWithSCs.
169
170 Similarly consider
171 data S a where { MkS :: Ord a => a -> S a }
172 pattern Bam x y <- (MkS (x::a), MkS (y::a)))
173
174 The pattern (Bam x y) binds two (Ord a) dictionaries, but we only
175 need one. Agian mkMimimalWithSCs removes the redundant one.
176
177 Note [Type variables whose kind is captured]
178 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
179 Consider
180 data AST a = Sym [a]
181 class Prj s where { prj :: [a] -> Maybe (s a)
182 pattern P x <= Sym (prj -> Just x)
183
184 Here we get a matcher with this type
185 $mP :: forall s a. Prj s => AST a -> (s a -> r) -> r -> r
186
187 No problem. But note that 's' is not fixed by the type of the
188 pattern (AST a), nor is it existentially bound. It's really only
189 fixed by the type of the continuation.
190
191 Trac #14552 showed that this can go wrong if the kind of 's' mentions
192 existentially bound variables. We obviously can't make a type like
193 $mP :: forall (s::k->*) a. Prj s => AST a -> (forall k. s a -> r)
194 -> r -> r
195 But neither is 's' itself existentially bound, so the forall (s::k->*)
196 can't go in the inner forall either. (What would the matcher apply
197 the continuation to?)
198
199 So we just fail in this case, with a pretty terrible error message.
200 Maybe we could do better, but I can't see how. (It'd be possible to
201 default 's' to (Any k), but that probably isn't what the user wanted,
202 and it not straightforward to implement, because by the time we see
203 the problem, simplifyInfer has already skolemised 's'.)
204
205 This stuff can only happen in the presence of view patterns, with
206 TypeInType, so it's a bit of a corner case.
207
208 Note [Coercions that escape]
209 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
210 Trac #14507 showed an example where the inferred type of the matcher
211 for the pattern synonym was somethign like
212 $mSO :: forall (r :: TYPE rep) kk (a :: k).
213 TypeRep k a
214 -> ((Bool ~ k) => TypeRep Bool (a |> co_a2sv) -> r)
215 -> (Void# -> r)
216 -> r
217
218 What is that co_a2sv :: Bool ~# *?? It was bound (via a superclass
219 selection) by the pattern being matched; and indeed it is implicit in
220 the context (Bool ~ k). You could imagine trying to extract it like
221 this:
222 $mSO :: forall (r :: TYPE rep) kk (a :: k).
223 TypeRep k a
224 -> ( co :: ((Bool :: *) ~ (k :: *)) =>
225 let co_a2sv = sc_sel co
226 in TypeRep Bool (a |> co_a2sv) -> r)
227 -> (Void# -> r)
228 -> r
229
230 But we simply don't allow that in types. Maybe one day but not now.
231
232 How to detect this situation? We just look for free coercion variables
233 in the types of any of the arguments to the matcher. The error message
234 is not very helpful, but at least we don't get a Lint error.
235 -}
236
237 tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn
238 -> TcPatSynInfo
239 -> TcM (LHsBinds GhcTc, TcGblEnv)
240 tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
241 , psb_def = lpat, psb_dir = dir }
242 TPSI{ patsig_implicit_bndrs = implicit_tvs
243 , patsig_univ_bndrs = explicit_univ_tvs, patsig_prov = prov_theta
244 , patsig_ex_bndrs = explicit_ex_tvs, patsig_req = req_theta
245 , patsig_body_ty = sig_body_ty }
246 = addPatSynCtxt lname $
247 do { let decl_arity = length arg_names
248 (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
249
250 ; traceTc "tcCheckPatSynDecl" $
251 vcat [ ppr implicit_tvs, ppr explicit_univ_tvs, ppr req_theta
252 , ppr explicit_ex_tvs, ppr prov_theta, ppr sig_body_ty ]
253
254 ; (arg_tys, pat_ty) <- case tcSplitFunTysN decl_arity sig_body_ty of
255 Right stuff -> return stuff
256 Left missing -> wrongNumberOfParmsErr name decl_arity missing
257
258 -- Complain about: pattern P :: () => forall x. x -> P x
259 -- The existential 'x' should not appear in the result type
260 -- Can't check this until we know P's arity
261 ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType pat_ty) explicit_ex_tvs
262 ; checkTc (null bad_tvs) $
263 hang (sep [ text "The result type of the signature for" <+> quotes (ppr name) <> comma
264 , text "namely" <+> quotes (ppr pat_ty) ])
265 2 (text "mentions existential type variable" <> plural bad_tvs
266 <+> pprQuotedList bad_tvs)
267
268 -- See Note [The pattern-synonym signature splitting rule] in TcSigs
269 ; let univ_fvs = closeOverKinds $
270 (tyCoVarsOfTypes (pat_ty : req_theta) `extendVarSetList` explicit_univ_tvs)
271 (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) . binderVar) implicit_tvs
272 univ_bndrs = extra_univ ++ mkTyVarBinders Specified explicit_univ_tvs
273 ex_bndrs = extra_ex ++ mkTyVarBinders Specified explicit_ex_tvs
274 univ_tvs = binderVars univ_bndrs
275 ex_tvs = binderVars ex_bndrs
276
277 -- Right! Let's check the pattern against the signature
278 -- See Note [Checking against a pattern signature]
279 ; req_dicts <- newEvVars req_theta
280 ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
281 ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
282 pushLevelAndCaptureConstraints $
283 tcExtendTyVarEnv univ_tvs $
284 tcExtendKindEnvList [(getName (binderVar ex_tv), APromotionErr PatSynExPE)
285 | ex_tv <- extra_ex] $
286 -- See Note [Pattern synonym existentials do not scope]
287 tcPat PatSyn lpat (mkCheckExpType pat_ty) $
288 do { let in_scope = mkInScopeSet (mkVarSet univ_tvs)
289 empty_subst = mkEmptyTCvSubst in_scope
290 ; (subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst ex_tvs
291 -- newMetaTyVarX: see the "Existential type variables"
292 -- part of Note [Checking against a pattern signature]
293 ; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs])
294 ; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs'])
295 ; let prov_theta' = substTheta subst prov_theta
296 -- Add univ_tvs to the in_scope set to
297 -- satisfy the substitution invariant. There's no need to
298 -- add 'ex_tvs' as they are already in the domain of the
299 -- substitution.
300 -- See also Note [The substitution invariant] in TyCoRep.
301 ; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta'
302 ; args' <- zipWithM (tc_arg subst) arg_names arg_tys
303 ; return (ex_tvs', prov_dicts, args') }
304
305 ; let skol_info = SigSkol (PatSynCtxt name) pat_ty []
306 -- The type here is a bit bogus, but we do not print
307 -- the type for PatSynCtxt, so it doesn't matter
308 -- See TcRnTypes Note [Skolem info for pattern synonyms]
309 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted
310
311 -- Solve the constraints now, because we are about to make a PatSyn,
312 -- which should not contain unification variables and the like (Trac #10997)
313 ; simplifyTopImplic implics
314
315 -- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct
316 -- Otherwise we may get a type error when typechecking the builder,
317 -- when that should be impossible
318
319 ; traceTc "tcCheckPatSynDecl }" $ ppr name
320 ; tc_patsyn_finish lname dir is_infix lpat'
321 (univ_bndrs, req_theta, ev_binds, req_dicts)
322 (ex_bndrs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
323 (args', arg_tys)
324 pat_ty rec_fields }
325 where
326 tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr GhcTcId)
327 tc_arg subst arg_name arg_ty
328 = do { -- Look up the variable actually bound by lpat
329 -- and check that it has the expected type
330 arg_id <- tcLookupId arg_name
331 ; wrap <- tcSubType_NC GenSigCtxt
332 (idType arg_id)
333 (substTyUnchecked subst arg_ty)
334 -- Why do we need tcSubType here?
335 -- See Note [Pattern synonyms and higher rank types]
336 ; return (mkLHsWrap wrap $ nlHsVar arg_id) }
337 tcCheckPatSynDecl (XPatSynBind _) _ = panic "tcCheckPatSynDecl"
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], [EvTerm])
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, [EvTerm])
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 = mkTyVar rr_name runtimeRepTy
641 rr = mkTyVarTy rr_tv
642 res_tv = mkTyVar tv_name (tYPE rr)
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 noExt (nlHsVar scrutinee) $
677 MG{ mg_alts = L (getLoc lpat) cases
678 , mg_ext = MatchGroupTc [pat_ty] res_ty
679 , mg_origin = Generated
680 }
681 body' = noLoc $
682 HsLam noExt $
683 MG{ mg_alts = noLoc [mkSimpleMatch LambdaExpr
684 args body]
685 , mg_ext = MatchGroupTc [pat_ty, cont_ty, fail_ty] res_ty
686 , mg_origin = Generated
687 }
688 match = mkMatch (mkPrefixFunRhs (L loc name)) []
689 (mkHsLams (rr_tv:res_tv:univ_tvs)
690 req_dicts body')
691 (noLoc (EmptyLocalBinds noExt))
692 mg :: MatchGroup GhcTc (LHsExpr GhcTc)
693 mg = MG{ mg_alts = L (getLoc match) [match]
694 , mg_ext = MatchGroupTc [] res_ty
695 , mg_origin = Generated
696 }
697
698 ; let bind = FunBind{ fun_ext = emptyNameSet
699 , fun_id = L loc matcher_id
700 , fun_matches = mg
701 , fun_co_fn = idHsWrapper
702 , fun_tick = [] }
703 matcher_bind = unitBag (noLoc bind)
704
705 ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
706 ; traceTc "tcPatSynMatcher" (ppr matcher_bind)
707
708 ; return ((matcher_id, is_unlifted), matcher_bind) }
709
710 mkPatSynRecSelBinds :: PatSyn
711 -> [FieldLabel] -- ^ Visible field labels
712 -> HsValBinds GhcRn
713 mkPatSynRecSelBinds ps fields
714 = XValBindsLR (NValBinds selector_binds sigs)
715 where
716 (sigs, selector_binds) = unzip (map mkRecSel fields)
717 mkRecSel fld_lbl = mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl
718
719 isUnidirectional :: HsPatSynDir a -> Bool
720 isUnidirectional Unidirectional = True
721 isUnidirectional ImplicitBidirectional = False
722 isUnidirectional ExplicitBidirectional{} = False
723
724 {-
725 ************************************************************************
726 * *
727 Constructing the "builder" Id
728 * *
729 ************************************************************************
730 -}
731
732 mkPatSynBuilderId :: HsPatSynDir a -> Located Name
733 -> [TyVarBinder] -> ThetaType
734 -> [TyVarBinder] -> ThetaType
735 -> [Type] -> Type
736 -> TcM (Maybe (Id, Bool))
737 mkPatSynBuilderId dir (L _ name)
738 univ_bndrs req_theta ex_bndrs prov_theta
739 arg_tys pat_ty
740 | isUnidirectional dir
741 = return Nothing
742 | otherwise
743 = do { builder_name <- newImplicitBinder name mkBuilderOcc
744 ; let theta = req_theta ++ prov_theta
745 need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
746 builder_sigma = add_void need_dummy_arg $
747 mkForAllTys univ_bndrs $
748 mkForAllTys ex_bndrs $
749 mkFunTys theta $
750 mkFunTys arg_tys $
751 pat_ty
752 builder_id = mkExportedVanillaId builder_name builder_sigma
753 -- See Note [Exported LocalIds] in Id
754
755 builder_id' = modifyIdInfo (`setLevityInfoWithType` pat_ty) builder_id
756
757 ; return (Just (builder_id', need_dummy_arg)) }
758 where
759
760 tcPatSynBuilderBind :: PatSynBind GhcRn GhcRn
761 -> TcM (LHsBinds GhcTc)
762 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
763 tcPatSynBuilderBind (PSB { psb_id = L loc name, psb_def = lpat
764 , psb_dir = dir, psb_args = details })
765 | isUnidirectional dir
766 = return emptyBag
767
768 | Left why <- mb_match_group -- Can't invert the pattern
769 = setSrcSpan (getLoc lpat) $ failWithTc $
770 vcat [ hang (text "Invalid right-hand side of bidirectional pattern synonym"
771 <+> quotes (ppr name) <> colon)
772 2 why
773 , text "RHS pattern:" <+> ppr lpat ]
774
775 | Right match_group <- mb_match_group -- Bidirectional
776 = do { patsyn <- tcLookupPatSyn name
777 ; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn
778 -- Bidirectional, so patSynBuilder returns Just
779
780 match_group' | need_dummy_arg = add_dummy_arg match_group
781 | otherwise = match_group
782
783 bind = FunBind { fun_ext = placeHolderNamesTc
784 , fun_id = L loc (idName builder_id)
785 , fun_matches = match_group'
786 , fun_co_fn = idHsWrapper
787 , fun_tick = [] }
788
789 sig = completeSigFromId (PatSynCtxt name) builder_id
790
791 ; traceTc "tcPatSynBuilderBind {" $
792 ppr patsyn $$ ppr builder_id <+> dcolon <+> ppr (idType builder_id)
793 ; (builder_binds, _) <- tcPolyCheck emptyPragEnv sig (noLoc bind)
794 ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
795 ; return builder_binds }
796
797 | otherwise = panic "tcPatSynBuilderBind" -- Both cases dealt with
798 where
799 mb_match_group
800 = case dir of
801 ExplicitBidirectional explicit_mg -> Right explicit_mg
802 ImplicitBidirectional -> fmap mk_mg (tcPatToExpr name args lpat)
803 Unidirectional -> panic "tcPatSynBuilderBind"
804
805 mk_mg :: LHsExpr GhcRn -> MatchGroup GhcRn (LHsExpr GhcRn)
806 mk_mg body = mkMatchGroup Generated [builder_match]
807 where
808 builder_args = [L loc (VarPat noExt (L loc n)) | L loc n <- args]
809 builder_match = mkMatch (mkPrefixFunRhs (L loc name))
810 builder_args body
811 (noLoc (EmptyLocalBinds noExt))
812
813 args = case details of
814 PrefixCon args -> args
815 InfixCon arg1 arg2 -> [arg1, arg2]
816 RecCon args -> map recordPatSynPatVar args
817
818 add_dummy_arg :: MatchGroup GhcRn (LHsExpr GhcRn)
819 -> MatchGroup GhcRn (LHsExpr GhcRn)
820 add_dummy_arg mg@(MG { mg_alts = L l [L loc match@(Match { m_pats = pats })] })
821 = mg { mg_alts = L l [L loc (match { m_pats = nlWildPatName : pats })] }
822 add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
823 pprMatches other_mg
824 tcPatSynBuilderBind (XPatSynBind _) = panic "tcPatSynBuilderBind"
825
826 tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr GhcTcId, TcSigmaType)
827 -- monadic only for failure
828 tcPatSynBuilderOcc ps
829 | Just (builder_id, add_void_arg) <- builder
830 , let builder_expr = HsConLikeOut noExt (PatSynCon ps)
831 builder_ty = idType builder_id
832 = return $
833 if add_void_arg
834 then ( builder_expr -- still just return builder_expr; the void# arg is added
835 -- by dsConLike in the desugarer
836 , tcFunResultTy builder_ty )
837 else (builder_expr, builder_ty)
838
839 | otherwise -- Unidirectional
840 = nonBidirectionalErr name
841 where
842 name = patSynName ps
843 builder = patSynBuilder ps
844
845 add_void :: Bool -> Type -> Type
846 add_void need_dummy_arg ty
847 | need_dummy_arg = mkFunTy voidPrimTy ty
848 | otherwise = ty
849
850 tcPatToExpr :: Name -> [Located Name] -> LPat GhcRn
851 -> Either MsgDoc (LHsExpr GhcRn)
852 -- Given a /pattern/, return an /expression/ that builds a value
853 -- that matches the pattern. E.g. if the pattern is (Just [x]),
854 -- the expression is (Just [x]). They look the same, but the
855 -- input uses constructors from HsPat and the output uses constructors
856 -- from HsExpr.
857 --
858 -- Returns (Left r) if the pattern is not invertible, for reason r.
859 -- See Note [Builder for a bidirectional pattern synonym]
860 tcPatToExpr name args pat = go pat
861 where
862 lhsVars = mkNameSet (map unLoc args)
863
864 -- Make a prefix con for prefix and infix patterns for simplicity
865 mkPrefixConExpr :: Located Name -> [LPat GhcRn]
866 -> Either MsgDoc (HsExpr GhcRn)
867 mkPrefixConExpr lcon@(L loc _) pats
868 = do { exprs <- mapM go pats
869 ; return (foldl (\x y -> HsApp noExt (L loc x) y)
870 (HsVar noExt lcon) exprs) }
871
872 mkRecordConExpr :: Located Name -> HsRecFields GhcRn (LPat GhcRn)
873 -> Either MsgDoc (HsExpr GhcRn)
874 mkRecordConExpr con fields
875 = do { exprFields <- mapM go fields
876 ; return (RecordCon noExt con exprFields) }
877
878 go :: LPat GhcRn -> Either MsgDoc (LHsExpr GhcRn)
879 go (L loc p) = L loc <$> go1 p
880
881 go1 :: Pat GhcRn -> Either MsgDoc (HsExpr GhcRn)
882 go1 (ConPatIn con info)
883 = case info of
884 PrefixCon ps -> mkPrefixConExpr con ps
885 InfixCon l r -> mkPrefixConExpr con [l,r]
886 RecCon fields -> mkRecordConExpr con fields
887
888 go1 (SigPat _ pat) = go1 (unLoc pat)
889 -- See Note [Type signatures and the builder expression]
890
891 go1 (VarPat _ (L l var))
892 | var `elemNameSet` lhsVars
893 = return $ HsVar noExt (L l var)
894 | otherwise
895 = Left (quotes (ppr var) <+> text "is not bound by the LHS of the pattern synonym")
896 go1 (ParPat _ pat) = fmap (HsPar noExt) $ go pat
897 go1 p@(ListPat reb pats)
898 | Nothing <- reb = do { exprs <- mapM go pats
899 ; return $ ExplicitList noExt Nothing exprs }
900 | otherwise = notInvertibleListPat p
901 go1 (TuplePat _ pats box) = do { exprs <- mapM go pats
902 ; return $ ExplicitTuple noExt
903 (map (noLoc . (Present noExt)) exprs)
904 box }
905 go1 (SumPat _ pat alt arity) = do { expr <- go1 (unLoc pat)
906 ; return $ ExplicitSum noExt alt arity
907 (noLoc expr)
908 }
909 go1 (LitPat _ lit) = return $ HsLit noExt lit
910 go1 (NPat _ (L _ n) mb_neg _)
911 | Just neg <- mb_neg = return $ unLoc $ nlHsSyntaxApps neg
912 [noLoc (HsOverLit noExt n)]
913 | otherwise = return $ HsOverLit noExt n
914 go1 (ConPatOut{}) = panic "ConPatOut in output of renamer"
915 go1 (CoPat{}) = panic "CoPat in output of renamer"
916 go1 (SplicePat _ (HsSpliced _ _ (HsSplicedPat pat)))
917 = go1 pat
918 go1 (SplicePat _ (HsSpliced{})) = panic "Invalid splice variety"
919
920 -- The following patterns are not invertible.
921 go1 p@(BangPat {}) = notInvertible p -- #14112
922 go1 p@(LazyPat {}) = notInvertible p
923 go1 p@(WildPat {}) = notInvertible p
924 go1 p@(AsPat {}) = notInvertible p
925 go1 p@(ViewPat {}) = notInvertible p
926 go1 p@(NPlusKPat {}) = notInvertible p
927 go1 p@(XPat {}) = notInvertible p
928 go1 p@(SplicePat _ (HsTypedSplice {})) = notInvertible p
929 go1 p@(SplicePat _ (HsUntypedSplice {})) = notInvertible p
930 go1 p@(SplicePat _ (HsQuasiQuote {})) = notInvertible p
931 go1 p@(SplicePat _ (XSplice {})) = 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
1036 nonBidirectionalErr :: Outputable name => name -> TcM a
1037 nonBidirectionalErr name = failWithTc $
1038 text "non-bidirectional pattern synonym"
1039 <+> quotes (ppr name) <+> text "used in an expression"
1040
1041 -- Walk the whole pattern and for all ConPatOuts, collect the
1042 -- existentially-bound type variables and evidence binding variables.
1043 --
1044 -- These are used in computing the type of a pattern synonym and also
1045 -- in generating matcher functions, since success continuations need
1046 -- to be passed these pattern-bound evidences.
1047 tcCollectEx
1048 :: LPat GhcTc
1049 -> ( [TyVar] -- Existentially-bound type variables
1050 -- in correctly-scoped order; e.g. [ k:*, x:k ]
1051 , [EvVar] ) -- and evidence variables
1052
1053 tcCollectEx pat = go pat
1054 where
1055 go :: LPat GhcTc -> ([TyVar], [EvVar])
1056 go = go1 . unLoc
1057
1058 go1 :: Pat GhcTc -> ([TyVar], [EvVar])
1059 go1 (LazyPat _ p) = go p
1060 go1 (AsPat _ _ p) = go p
1061 go1 (ParPat _ p) = go p
1062 go1 (BangPat _ p) = go p
1063 go1 (ListPat _ ps) = mergeMany . map go $ ps
1064 go1 (TuplePat _ ps _) = mergeMany . map go $ ps
1065 go1 (SumPat _ p _ _) = go p
1066 go1 (ViewPat _ _ p) = go p
1067 go1 con@ConPatOut{} = merge (pat_tvs con, pat_dicts con) $
1068 goConDetails $ pat_args con
1069 go1 (SigPat _ p) = go p
1070 go1 (CoPat _ _ p _) = go1 p
1071 go1 (NPlusKPat _ n k _ geq subtract)
1072 = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract
1073 go1 _ = empty
1074
1075 goConDetails :: HsConPatDetails GhcTc -> ([TyVar], [EvVar])
1076 goConDetails (PrefixCon ps) = mergeMany . map go $ ps
1077 goConDetails (InfixCon p1 p2) = go p1 `merge` go p2
1078 goConDetails (RecCon HsRecFields{ rec_flds = flds })
1079 = mergeMany . map goRecFd $ flds
1080
1081 goRecFd :: LHsRecField GhcTc (LPat GhcTc) -> ([TyVar], [EvVar])
1082 goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p
1083
1084 merge (vs1, evs1) (vs2, evs2) = (vs1 ++ vs2, evs1 ++ evs2)
1085 mergeMany = foldr merge empty
1086 empty = ([], [])