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