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