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