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