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