Make a smart mkAppTyM
[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 HsSyn
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 {}) = 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@(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 (Trac #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 _) = panic "tcInferPatSynDecl"
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 Trac #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 (Trac #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 Trac #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 tcExtendKindEnvList [(getName (binderVar ex_tv), APromotionErr PatSynExPE)
388 | ex_tv <- extra_ex] $
389 -- See Note [Pattern synonym existentials do not scope]
390 tcPat PatSyn lpat (mkCheckExpType pat_ty) $
391 do { let in_scope = mkInScopeSet (mkVarSet univ_tvs)
392 empty_subst = mkEmptyTCvSubst in_scope
393 ; (subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst ex_tvs
394 -- newMetaTyVarX: see the "Existential type variables"
395 -- part of Note [Checking against a pattern signature]
396 ; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs])
397 ; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs'])
398 ; let prov_theta' = substTheta subst prov_theta
399 -- Add univ_tvs to the in_scope set to
400 -- satisfy the substitution invariant. There's no need to
401 -- add 'ex_tvs' as they are already in the domain of the
402 -- substitution.
403 -- See also Note [The substitution invariant] in TyCoRep.
404 ; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta'
405 ; args' <- zipWithM (tc_arg subst) arg_names arg_tys
406 ; return (ex_tvs', prov_dicts, args') }
407
408 ; let skol_info = SigSkol (PatSynCtxt name) pat_ty []
409 -- The type here is a bit bogus, but we do not print
410 -- the type for PatSynCtxt, so it doesn't matter
411 -- See TcRnTypes Note [Skolem info for pattern synonyms]
412 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted
413
414 -- Solve the constraints now, because we are about to make a PatSyn,
415 -- which should not contain unification variables and the like (Trac #10997)
416 ; simplifyTopImplic implics
417
418 -- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct
419 -- Otherwise we may get a type error when typechecking the builder,
420 -- when that should be impossible
421
422 ; traceTc "tcCheckPatSynDecl }" $ ppr name
423 ; tc_patsyn_finish lname dir is_infix lpat'
424 (univ_bndrs, req_theta, ev_binds, req_dicts)
425 (ex_bndrs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
426 (args', arg_tys)
427 pat_ty rec_fields }
428 where
429 tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr GhcTcId)
430 tc_arg subst arg_name arg_ty
431 = do { -- Look up the variable actually bound by lpat
432 -- and check that it has the expected type
433 arg_id <- tcLookupId arg_name
434 ; wrap <- tcSubType_NC GenSigCtxt
435 (idType arg_id)
436 (substTyUnchecked subst arg_ty)
437 -- Why do we need tcSubType here?
438 -- See Note [Pattern synonyms and higher rank types]
439 ; return (mkLHsWrap wrap $ nlHsVar arg_id) }
440 tcCheckPatSynDecl (XPatSynBind _) _ = panic "tcCheckPatSynDecl"
441
442 {- [Pattern synonyms and higher rank types]
443 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
444 Consider
445 data T = MkT (forall a. a->a)
446
447 pattern P :: (Int -> Int) -> T
448 pattern P x <- MkT x
449
450 This should work. But in the matcher we must match against MkT, and then
451 instantiate its argument 'x', to get a function of type (Int -> Int).
452 Equality is not enough! Trac #13752 was an example.
453
454 Note [Pattern synonym existentials do not scope]
455 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
456 Consider this (Trac #14498):
457 pattern SS :: forall (t :: k). () =>
458 => forall (a :: kk -> k) (n :: kk).
459 => TypeRep n -> TypeRep t
460 pattern SS n <- (App (Typeable :: TypeRep (a::kk -> k)) n)
461
462 Here 'k' is implicitly bound in the signature, but (with
463 -XScopedTypeVariables) it does still scope over the pattern-synonym
464 definition. But what about 'kk', which is oexistential? It too is
465 implicitly bound in the signature; should it too scope? And if so,
466 what type variable is it bound to?
467
468 The trouble is that the type variable to which it is bound is itself
469 only brought into scope in part the pattern, so it makes no sense for
470 'kk' to scope over the whole pattern. See the discussion on
471 Trac #14498, esp comment:16ff. Here is a simpler example:
472 data T where { MkT :: x -> (x->Int) -> T }
473 pattern P :: () => forall x. x -> (x->Int) -> T
474 pattern P a b = (MkT a b, True)
475
476 Here it would make no sense to mention 'x' in the True pattern,
477 like this:
478 pattern P a b = (MkT a b, True :: x)
479
480 The 'x' only makes sense "under" the MkT pattern. Conclusion: the
481 existential type variables of a pattern-synonym signature should not
482 scope.
483
484 But it's not that easy to implement, because we don't know
485 exactly what the existentials /are/ until we get to type checking.
486 (See Note [The pattern-synonym signature splitting rule], and
487 the partition of implicit_tvs in tcCheckPatSynDecl.)
488
489 So we do this:
490
491 - The reaner brings all the implicitly-bound kind variables into
492 scope, without trying to distinguish universal from existential
493
494 - tcCheckPatSynDecl uses tcExtendKindEnvList to bind the
495 implicitly-bound existentials to
496 APromotionErr PatSynExPE
497 It's not really a promotion error, but it's a way to bind the Name
498 (which the renamer has not complained about) to something that, when
499 looked up, will cause a complaint (in this case
500 TcHsType.promotionErr)
501
502
503 Note [The pattern-synonym signature splitting rule]
504 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
505 Given a pattern signature, we must split
506 the kind-generalised variables, and
507 the implicitly-bound variables
508 into universal and existential. The rule is this
509 (see discussion on Trac #11224):
510
511 The universal tyvars are the ones mentioned in
512 - univ_tvs: the user-specified (forall'd) universals
513 - req_theta
514 - res_ty
515 The existential tyvars are all the rest
516
517 For example
518
519 pattern P :: () => b -> T a
520 pattern P x = ...
521
522 Here 'a' is universal, and 'b' is existential. But there is a wrinkle:
523 how do we split the arg_tys from req_ty? Consider
524
525 pattern Q :: () => b -> S c -> T a
526 pattern Q x = ...
527
528 This is an odd example because Q has only one syntactic argument, and
529 so presumably is defined by a view pattern matching a function. But
530 it can happen (Trac #11977, #12108).
531
532 We don't know Q's arity from the pattern signature, so we have to wait
533 until we see the pattern declaration itself before deciding res_ty is,
534 and hence which variables are existential and which are universal.
535
536 And that in turn is why TcPatSynInfo has a separate field,
537 patsig_implicit_bndrs, to capture the implicitly bound type variables,
538 because we don't yet know how to split them up.
539
540 It's a slight compromise, because it means we don't really know the
541 pattern synonym's real signature until we see its declaration. So,
542 for example, in hs-boot file, we may need to think what to do...
543 (eg don't have any implicitly-bound variables).
544
545
546 Note [Checking against a pattern signature]
547 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
548 When checking the actual supplied pattern against the pattern synonym
549 signature, we need to be quite careful.
550
551 ----- Provided constraints
552 Example
553
554 data T a where
555 MkT :: Ord a => a -> T a
556
557 pattern P :: () => Eq a => a -> [T a]
558 pattern P x = [MkT x]
559
560 We must check that the (Eq a) that P claims to bind (and to
561 make available to matches against P), is derivable from the
562 actual pattern. For example:
563 f (P (x::a)) = ...here (Eq a) should be available...
564 And yes, (Eq a) is derivable from the (Ord a) bound by P's rhs.
565
566 ----- Existential type variables
567 Unusually, we instantiate the existential tyvars of the pattern with
568 *meta* type variables. For example
569
570 data S where
571 MkS :: Eq a => [a] -> S
572
573 pattern P :: () => Eq x => x -> S
574 pattern P x <- MkS x
575
576 The pattern synonym conceals from its client the fact that MkS has a
577 list inside it. The client just thinks it's a type 'x'. So we must
578 unify x := [a] during type checking, and then use the instantiating type
579 [a] (called ex_tys) when building the matcher. In this case we'll get
580
581 $mP :: S -> (forall x. Ex x => x -> r) -> r -> r
582 $mP x k = case x of
583 MkS a (d:Eq a) (ys:[a]) -> let dl :: Eq [a]
584 dl = $dfunEqList d
585 in k [a] dl ys
586
587 All this applies when type-checking the /matching/ side of
588 a pattern synonym. What about the /building/ side?
589
590 * For Unidirectional, there is no builder
591
592 * For ExplicitBidirectional, the builder is completely separate
593 code, typechecked in tcPatSynBuilderBind
594
595 * For ImplicitBidirectional, the builder is still typechecked in
596 tcPatSynBuilderBind, by converting the pattern to an expression and
597 typechecking it.
598
599 At one point, for ImplicitBidirectional I used TyVarTvs (instead of
600 TauTvs) in tcCheckPatSynDecl. But (a) strengthening the check here
601 is redundant since tcPatSynBuilderBind does the job, (b) it was
602 still incomplete (TyVarTvs can unify with each other), and (c) it
603 didn't even work (Trac #13441 was accepted with
604 ExplicitBidirectional, but rejected if expressed in
605 ImplicitBidirectional form. Conclusion: trying to be too clever is
606 a bad idea.
607 -}
608
609 collectPatSynArgInfo :: HsPatSynDetails (Located Name)
610 -> ([Name], [Name], Bool)
611 collectPatSynArgInfo details =
612 case details of
613 PrefixCon names -> (map unLoc names, [], False)
614 InfixCon name1 name2 -> (map unLoc [name1, name2], [], True)
615 RecCon names -> (vars, sels, False)
616 where
617 (vars, sels) = unzip (map splitRecordPatSyn names)
618 where
619 splitRecordPatSyn :: RecordPatSynField (Located Name)
620 -> (Name, Name)
621 splitRecordPatSyn (RecordPatSynField
622 { recordPatSynPatVar = (dL->L _ patVar)
623 , recordPatSynSelectorId = (dL->L _ selId) })
624 = (patVar, selId)
625
626 addPatSynCtxt :: Located Name -> TcM a -> TcM a
627 addPatSynCtxt (dL->L loc name) thing_inside
628 = setSrcSpan loc $
629 addErrCtxt (text "In the declaration for pattern synonym"
630 <+> quotes (ppr name)) $
631 thing_inside
632
633 wrongNumberOfParmsErr :: Name -> Arity -> Arity -> TcM a
634 wrongNumberOfParmsErr name decl_arity missing
635 = failWithTc $
636 hang (text "Pattern synonym" <+> quotes (ppr name) <+> ptext (sLit "has")
637 <+> speakNOf decl_arity (text "argument"))
638 2 (text "but its type signature has" <+> int missing <+> text "fewer arrows")
639
640 -------------------------
641 -- Shared by both tcInferPatSyn and tcCheckPatSyn
642 tc_patsyn_finish :: Located Name -- ^ PatSyn Name
643 -> HsPatSynDir GhcRn -- ^ PatSyn type (Uni/Bidir/ExplicitBidir)
644 -> Bool -- ^ Whether infix
645 -> LPat GhcTc -- ^ Pattern of the PatSyn
646 -> ([TcTyVarBinder], [PredType], TcEvBinds, [EvVar])
647 -> ([TcTyVarBinder], [TcType], [PredType], [EvTerm])
648 -> ([LHsExpr GhcTcId], [TcType]) -- ^ Pattern arguments and
649 -- types
650 -> TcType -- ^ Pattern type
651 -> [Name] -- ^ Selector names
652 -- ^ Whether fields, empty if not record PatSyn
653 -> TcM (LHsBinds GhcTc, TcGblEnv)
654 tc_patsyn_finish lname dir is_infix lpat'
655 (univ_tvs, req_theta, req_ev_binds, req_dicts)
656 (ex_tvs, ex_tys, prov_theta, prov_dicts)
657 (args, arg_tys)
658 pat_ty field_labels
659 = do { -- Zonk everything. We are about to build a final PatSyn
660 -- so there had better be no unification variables in there
661
662 (ze, univ_tvs') <- zonkTyVarBinders univ_tvs
663 ; req_theta' <- zonkTcTypesToTypesX ze req_theta
664 ; (ze, ex_tvs') <- zonkTyVarBindersX ze ex_tvs
665 ; prov_theta' <- zonkTcTypesToTypesX ze prov_theta
666 ; pat_ty' <- zonkTcTypeToTypeX ze pat_ty
667 ; arg_tys' <- zonkTcTypesToTypesX ze arg_tys
668
669 ; let (env1, univ_tvs) = tidyTyCoVarBinders emptyTidyEnv univ_tvs'
670 (env2, ex_tvs) = tidyTyCoVarBinders env1 ex_tvs'
671 req_theta = tidyTypes env2 req_theta'
672 prov_theta = tidyTypes env2 prov_theta'
673 arg_tys = tidyTypes env2 arg_tys'
674 pat_ty = tidyType env2 pat_ty'
675
676 ; traceTc "tc_patsyn_finish {" $
677 ppr (unLoc lname) $$ ppr (unLoc lpat') $$
678 ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
679 ppr (ex_tvs, prov_theta, prov_dicts) $$
680 ppr args $$
681 ppr arg_tys $$
682 ppr pat_ty
683
684 -- Make the 'matcher'
685 ; (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat'
686 (binderVars univ_tvs, req_theta, req_ev_binds, req_dicts)
687 (binderVars ex_tvs, ex_tys, prov_theta, prov_dicts)
688 (args, arg_tys)
689 pat_ty
690
691 -- Make the 'builder'
692 ; builder_id <- mkPatSynBuilderId dir lname
693 univ_tvs req_theta
694 ex_tvs prov_theta
695 arg_tys pat_ty
696
697 -- TODO: Make this have the proper information
698 ; let mkFieldLabel name = FieldLabel { flLabel = occNameFS (nameOccName name)
699 , flIsOverloaded = False
700 , flSelector = name }
701 field_labels' = map mkFieldLabel field_labels
702
703
704 -- Make the PatSyn itself
705 ; let patSyn = mkPatSyn (unLoc lname) is_infix
706 (univ_tvs, req_theta)
707 (ex_tvs, prov_theta)
708 arg_tys
709 pat_ty
710 matcher_id builder_id
711 field_labels'
712
713 -- Selectors
714 ; let rn_rec_sel_binds = mkPatSynRecSelBinds patSyn (patSynFieldLabels patSyn)
715 tything = AConLike (PatSynCon patSyn)
716 ; tcg_env <- tcExtendGlobalEnv [tything] $
717 tcRecSelBinds rn_rec_sel_binds
718
719 ; traceTc "tc_patsyn_finish }" empty
720 ; return (matcher_bind, tcg_env) }
721
722 {-
723 ************************************************************************
724 * *
725 Constructing the "matcher" Id and its binding
726 * *
727 ************************************************************************
728 -}
729
730 tcPatSynMatcher :: Located Name
731 -> LPat GhcTc
732 -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
733 -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
734 -> ([LHsExpr GhcTcId], [TcType])
735 -> TcType
736 -> TcM ((Id, Bool), LHsBinds GhcTc)
737 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
738 tcPatSynMatcher (dL->L loc name) lpat
739 (univ_tvs, req_theta, req_ev_binds, req_dicts)
740 (ex_tvs, ex_tys, prov_theta, prov_dicts)
741 (args, arg_tys) pat_ty
742 = do { rr_name <- newNameAt (mkTyVarOcc "rep") loc
743 ; tv_name <- newNameAt (mkTyVarOcc "r") loc
744 ; let rr_tv = mkTyVar rr_name runtimeRepTy
745 rr = mkTyVarTy rr_tv
746 res_tv = mkTyVar tv_name (tYPE rr)
747 res_ty = mkTyVarTy res_tv
748 is_unlifted = null args && null prov_dicts
749 (cont_args, cont_arg_tys)
750 | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
751 | otherwise = (args, arg_tys)
752 cont_ty = mkInfSigmaTy ex_tvs prov_theta $
753 mkFunTys cont_arg_tys res_ty
754
755 fail_ty = mkFunTy voidPrimTy res_ty
756
757 ; matcher_name <- newImplicitBinder name mkMatcherOcc
758 ; scrutinee <- newSysLocalId (fsLit "scrut") pat_ty
759 ; cont <- newSysLocalId (fsLit "cont") cont_ty
760 ; fail <- newSysLocalId (fsLit "fail") fail_ty
761
762 ; let matcher_tau = mkFunTys [pat_ty, cont_ty, fail_ty] res_ty
763 matcher_sigma = mkInfSigmaTy (rr_tv:res_tv:univ_tvs) req_theta matcher_tau
764 matcher_id = mkExportedVanillaId matcher_name matcher_sigma
765 -- See Note [Exported LocalIds] in Id
766
767 inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys
768 cont' = foldl' nlHsApp (mkLHsWrap inst_wrap (nlHsVar cont)) cont_args
769
770 fail' = nlHsApps fail [nlHsVar voidPrimId]
771
772 args = map nlVarPat [scrutinee, cont, fail]
773 lwpat = noLoc $ WildPat pat_ty
774 cases = if isIrrefutableHsPat lpat
775 then [mkHsCaseAlt lpat cont']
776 else [mkHsCaseAlt lpat cont',
777 mkHsCaseAlt lwpat fail']
778 body = mkLHsWrap (mkWpLet req_ev_binds) $
779 cL (getLoc lpat) $
780 HsCase noExt (nlHsVar scrutinee) $
781 MG{ mg_alts = cL (getLoc lpat) cases
782 , mg_ext = MatchGroupTc [pat_ty] res_ty
783 , mg_origin = Generated
784 }
785 body' = noLoc $
786 HsLam noExt $
787 MG{ mg_alts = noLoc [mkSimpleMatch LambdaExpr
788 args body]
789 , mg_ext = MatchGroupTc [pat_ty, cont_ty, fail_ty] res_ty
790 , mg_origin = Generated
791 }
792 match = mkMatch (mkPrefixFunRhs (cL loc name)) []
793 (mkHsLams (rr_tv:res_tv:univ_tvs)
794 req_dicts body')
795 (noLoc (EmptyLocalBinds noExt))
796 mg :: MatchGroup GhcTc (LHsExpr GhcTc)
797 mg = MG{ mg_alts = cL (getLoc match) [match]
798 , mg_ext = MatchGroupTc [] res_ty
799 , mg_origin = Generated
800 }
801
802 ; let bind = FunBind{ fun_ext = emptyNameSet
803 , fun_id = cL loc matcher_id
804 , fun_matches = mg
805 , fun_co_fn = idHsWrapper
806 , fun_tick = [] }
807 matcher_bind = unitBag (noLoc bind)
808
809 ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
810 ; traceTc "tcPatSynMatcher" (ppr matcher_bind)
811
812 ; return ((matcher_id, is_unlifted), matcher_bind) }
813
814 mkPatSynRecSelBinds :: PatSyn
815 -> [FieldLabel] -- ^ Visible field labels
816 -> [(Id, LHsBind GhcRn)]
817 mkPatSynRecSelBinds ps fields
818 = [ mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl
819 | fld_lbl <- fields ]
820
821 isUnidirectional :: HsPatSynDir a -> Bool
822 isUnidirectional Unidirectional = True
823 isUnidirectional ImplicitBidirectional = False
824 isUnidirectional ExplicitBidirectional{} = False
825
826 {-
827 ************************************************************************
828 * *
829 Constructing the "builder" Id
830 * *
831 ************************************************************************
832 -}
833
834 mkPatSynBuilderId :: HsPatSynDir a -> Located Name
835 -> [TyVarBinder] -> ThetaType
836 -> [TyVarBinder] -> ThetaType
837 -> [Type] -> Type
838 -> TcM (Maybe (Id, Bool))
839 mkPatSynBuilderId dir (dL->L _ name)
840 univ_bndrs req_theta ex_bndrs prov_theta
841 arg_tys pat_ty
842 | isUnidirectional dir
843 = return Nothing
844 | otherwise
845 = do { builder_name <- newImplicitBinder name mkBuilderOcc
846 ; let theta = req_theta ++ prov_theta
847 need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
848 builder_sigma = add_void need_dummy_arg $
849 mkForAllTys univ_bndrs $
850 mkForAllTys ex_bndrs $
851 mkFunTys theta $
852 mkFunTys arg_tys $
853 pat_ty
854 builder_id = mkExportedVanillaId builder_name builder_sigma
855 -- See Note [Exported LocalIds] in Id
856
857 builder_id' = modifyIdInfo (`setLevityInfoWithType` pat_ty) builder_id
858
859 ; return (Just (builder_id', need_dummy_arg)) }
860 where
861
862 tcPatSynBuilderBind :: PatSynBind GhcRn GhcRn
863 -> TcM (LHsBinds GhcTc)
864 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
865 tcPatSynBuilderBind (PSB { psb_id = (dL->L loc name)
866 , psb_def = lpat
867 , psb_dir = dir
868 , psb_args = details })
869 | isUnidirectional dir
870 = return emptyBag
871
872 | Left why <- mb_match_group -- Can't invert the pattern
873 = setSrcSpan (getLoc lpat) $ failWithTc $
874 vcat [ hang (text "Invalid right-hand side of bidirectional pattern synonym"
875 <+> quotes (ppr name) <> colon)
876 2 why
877 , text "RHS pattern:" <+> ppr lpat ]
878
879 | Right match_group <- mb_match_group -- Bidirectional
880 = do { patsyn <- tcLookupPatSyn name
881 ; case patSynBuilder patsyn of {
882 Nothing -> return emptyBag ;
883 -- This case happens if we found a type error in the
884 -- pattern synonym, recovered, and put a placeholder
885 -- with patSynBuilder=Nothing in the environment
886
887 Just (builder_id, need_dummy_arg) -> -- Normal case
888 do { -- Bidirectional, so patSynBuilder returns Just
889 let match_group' | need_dummy_arg = add_dummy_arg match_group
890 | otherwise = match_group
891
892 bind = FunBind { fun_ext = placeHolderNamesTc
893 , fun_id = cL loc (idName builder_id)
894 , fun_matches = match_group'
895 , fun_co_fn = idHsWrapper
896 , fun_tick = [] }
897
898 sig = completeSigFromId (PatSynCtxt name) builder_id
899
900 ; traceTc "tcPatSynBuilderBind {" $
901 ppr patsyn $$ ppr builder_id <+> dcolon <+> ppr (idType builder_id)
902 ; (builder_binds, _) <- tcPolyCheck emptyPragEnv sig (noLoc bind)
903 ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
904 ; return builder_binds } } }
905
906 | otherwise = panic "tcPatSynBuilderBind" -- Both cases dealt with
907 where
908 mb_match_group
909 = case dir of
910 ExplicitBidirectional explicit_mg -> Right explicit_mg
911 ImplicitBidirectional -> fmap mk_mg (tcPatToExpr name args lpat)
912 Unidirectional -> panic "tcPatSynBuilderBind"
913
914 mk_mg :: LHsExpr GhcRn -> MatchGroup GhcRn (LHsExpr GhcRn)
915 mk_mg body = mkMatchGroup Generated [builder_match]
916 where
917 builder_args = [cL loc (VarPat noExt (cL loc n))
918 | (dL->L loc n) <- args]
919 builder_match = mkMatch (mkPrefixFunRhs (cL loc name))
920 builder_args body
921 (noLoc (EmptyLocalBinds noExt))
922
923 args = case details of
924 PrefixCon args -> args
925 InfixCon arg1 arg2 -> [arg1, arg2]
926 RecCon args -> map recordPatSynPatVar args
927
928 add_dummy_arg :: MatchGroup GhcRn (LHsExpr GhcRn)
929 -> MatchGroup GhcRn (LHsExpr GhcRn)
930 add_dummy_arg mg@(MG { mg_alts =
931 (dL->L l [dL->L loc
932 match@(Match { m_pats = pats })]) })
933 = mg { mg_alts = cL l [cL loc (match { m_pats = nlWildPatName : pats })] }
934 add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
935 pprMatches other_mg
936 tcPatSynBuilderBind (XPatSynBind _) = panic "tcPatSynBuilderBind"
937
938 tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr GhcTcId, TcSigmaType)
939 -- monadic only for failure
940 tcPatSynBuilderOcc ps
941 | Just (builder_id, add_void_arg) <- builder
942 , let builder_expr = HsConLikeOut noExt (PatSynCon ps)
943 builder_ty = idType builder_id
944 = return $
945 if add_void_arg
946 then ( builder_expr -- still just return builder_expr; the void# arg is added
947 -- by dsConLike in the desugarer
948 , tcFunResultTy builder_ty )
949 else (builder_expr, builder_ty)
950
951 | otherwise -- Unidirectional
952 = nonBidirectionalErr name
953 where
954 name = patSynName ps
955 builder = patSynBuilder ps
956
957 add_void :: Bool -> Type -> Type
958 add_void need_dummy_arg ty
959 | need_dummy_arg = mkFunTy voidPrimTy ty
960 | otherwise = ty
961
962 tcPatToExpr :: Name -> [Located Name] -> LPat GhcRn
963 -> Either MsgDoc (LHsExpr GhcRn)
964 -- Given a /pattern/, return an /expression/ that builds a value
965 -- that matches the pattern. E.g. if the pattern is (Just [x]),
966 -- the expression is (Just [x]). They look the same, but the
967 -- input uses constructors from HsPat and the output uses constructors
968 -- from HsExpr.
969 --
970 -- Returns (Left r) if the pattern is not invertible, for reason r.
971 -- See Note [Builder for a bidirectional pattern synonym]
972 tcPatToExpr name args pat = go pat
973 where
974 lhsVars = mkNameSet (map unLoc args)
975
976 -- Make a prefix con for prefix and infix patterns for simplicity
977 mkPrefixConExpr :: Located Name -> [LPat GhcRn]
978 -> Either MsgDoc (HsExpr GhcRn)
979 mkPrefixConExpr lcon@(dL->L loc _) pats
980 = do { exprs <- mapM go pats
981 ; return (foldl' (\x y -> HsApp noExt (cL loc x) y)
982 (HsVar noExt lcon) exprs) }
983
984 mkRecordConExpr :: Located Name -> HsRecFields GhcRn (LPat GhcRn)
985 -> Either MsgDoc (HsExpr GhcRn)
986 mkRecordConExpr con fields
987 = do { exprFields <- mapM go fields
988 ; return (RecordCon noExt con exprFields) }
989
990 go :: LPat GhcRn -> Either MsgDoc (LHsExpr GhcRn)
991 go (dL->L loc p) = cL loc <$> go1 p
992
993 go1 :: Pat GhcRn -> Either MsgDoc (HsExpr GhcRn)
994 go1 (ConPatIn con info)
995 = case info of
996 PrefixCon ps -> mkPrefixConExpr con ps
997 InfixCon l r -> mkPrefixConExpr con [l,r]
998 RecCon fields -> mkRecordConExpr con fields
999
1000 go1 (SigPat _ pat _) = go1 (unLoc pat)
1001 -- See Note [Type signatures and the builder expression]
1002
1003 go1 (VarPat _ (dL->L l var))
1004 | var `elemNameSet` lhsVars
1005 = return $ HsVar noExt (cL l var)
1006 | otherwise
1007 = Left (quotes (ppr var) <+> text "is not bound by the LHS of the pattern synonym")
1008 go1 (ParPat _ pat) = fmap (HsPar noExt) $ go pat
1009 go1 p@(ListPat reb pats)
1010 | Nothing <- reb = do { exprs <- mapM go pats
1011 ; return $ ExplicitList noExt Nothing exprs }
1012 | otherwise = notInvertibleListPat p
1013 go1 (TuplePat _ pats box) = do { exprs <- mapM go pats
1014 ; return $ ExplicitTuple noExt
1015 (map (noLoc . (Present noExt)) exprs)
1016 box }
1017 go1 (SumPat _ pat alt arity) = do { expr <- go1 (unLoc pat)
1018 ; return $ ExplicitSum noExt alt arity
1019 (noLoc expr)
1020 }
1021 go1 (LitPat _ lit) = return $ HsLit noExt lit
1022 go1 (NPat _ (dL->L _ n) mb_neg _)
1023 | Just neg <- mb_neg = return $ unLoc $ nlHsSyntaxApps neg
1024 [noLoc (HsOverLit noExt n)]
1025 | otherwise = return $ HsOverLit noExt n
1026 go1 (ConPatOut{}) = panic "ConPatOut in output of renamer"
1027 go1 (CoPat{}) = panic "CoPat in output of renamer"
1028 go1 (SplicePat _ (HsSpliced _ _ (HsSplicedPat pat)))
1029 = go1 pat
1030 go1 (SplicePat _ (HsSpliced{})) = panic "Invalid splice variety"
1031 go1 (SplicePat _ (HsSplicedT{})) = panic "Invalid splice variety"
1032
1033 -- The following patterns are not invertible.
1034 go1 p@(BangPat {}) = notInvertible p -- #14112
1035 go1 p@(LazyPat {}) = notInvertible p
1036 go1 p@(WildPat {}) = notInvertible p
1037 go1 p@(AsPat {}) = notInvertible p
1038 go1 p@(ViewPat {}) = notInvertible p
1039 go1 p@(NPlusKPat {}) = notInvertible p
1040 go1 p@(XPat {}) = notInvertible p
1041 go1 p@(SplicePat _ (HsTypedSplice {})) = notInvertible p
1042 go1 p@(SplicePat _ (HsUntypedSplice {})) = notInvertible p
1043 go1 p@(SplicePat _ (HsQuasiQuote {})) = notInvertible p
1044 go1 p@(SplicePat _ (XSplice {})) = notInvertible p
1045
1046 notInvertible p = Left (not_invertible_msg p)
1047
1048 not_invertible_msg p
1049 = text "Pattern" <+> quotes (ppr p) <+> text "is not invertible"
1050 $+$ hang (text "Suggestion: instead use an explicitly bidirectional"
1051 <+> text "pattern synonym, e.g.")
1052 2 (hang (text "pattern" <+> pp_name <+> pp_args <+> larrow
1053 <+> ppr pat <+> text "where")
1054 2 (pp_name <+> pp_args <+> equals <+> text "..."))
1055 where
1056 pp_name = ppr name
1057 pp_args = hsep (map ppr args)
1058
1059 -- We should really be able to invert list patterns, even when
1060 -- rebindable syntax is on, but doing so involves a bit of
1061 -- refactoring; see Trac #14380. Until then we reject with a
1062 -- helpful error message.
1063 notInvertibleListPat p
1064 = Left (vcat [ not_invertible_msg p
1065 , text "Reason: rebindable syntax is on."
1066 , text "This is fixable: add use-case to Trac #14380" ])
1067
1068 {- Note [Builder for a bidirectional pattern synonym]
1069 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1070 For a bidirectional pattern synonym we need to produce an /expression/
1071 that matches the supplied /pattern/, given values for the arguments
1072 of the pattern synonym. For example
1073 pattern F x y = (Just x, [y])
1074 The 'builder' for F looks like
1075 $builderF x y = (Just x, [y])
1076
1077 We can't always do this:
1078 * Some patterns aren't invertible; e.g. view patterns
1079 pattern F x = (reverse -> x:_)
1080
1081 * The RHS pattern might bind more variables than the pattern
1082 synonym, so again we can't invert it
1083 pattern F x = (x,y)
1084
1085 * Ditto wildcards
1086 pattern F x = (x,_)
1087
1088
1089 Note [Redundant constraints for builder]
1090 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1091 The builder can have redundant constraints, which are awkard to eliminate.
1092 Consider
1093 pattern P = Just 34
1094 To match against this pattern we need (Eq a, Num a). But to build
1095 (Just 34) we need only (Num a). Fortunately instTcSigFromId sets
1096 sig_warn_redundant to False.
1097
1098 ************************************************************************
1099 * *
1100 Helper functions
1101 * *
1102 ************************************************************************
1103
1104 Note [As-patterns in pattern synonym definitions]
1105 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1106 The rationale for rejecting as-patterns in pattern synonym definitions
1107 is that an as-pattern would introduce nonindependent pattern synonym
1108 arguments, e.g. given a pattern synonym like:
1109
1110 pattern K x y = x@(Just y)
1111
1112 one could write a nonsensical function like
1113
1114 f (K Nothing x) = ...
1115
1116 or
1117 g (K (Just True) False) = ...
1118
1119 Note [Type signatures and the builder expression]
1120 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1121 Consider
1122 pattern L x = Left x :: Either [a] [b]
1123
1124 In tc{Infer/Check}PatSynDecl we will check that the pattern has the
1125 specified type. We check the pattern *as a pattern*, so the type
1126 signature is a pattern signature, and so brings 'a' and 'b' into
1127 scope. But we don't have a way to bind 'a, b' in the LHS, as we do
1128 'x', say. Nevertheless, the sigature may be useful to constrain
1129 the type.
1130
1131 When making the binding for the *builder*, though, we don't want
1132 $buildL x = Left x :: Either [a] [b]
1133 because that wil either mean (forall a b. Either [a] [b]), or we'll
1134 get a complaint that 'a' and 'b' are out of scope. (Actually the
1135 latter; Trac #9867.) No, the job of the signature is done, so when
1136 converting the pattern to an expression (for the builder RHS) we
1137 simply discard the signature.
1138
1139 Note [Record PatSyn Desugaring]
1140 -------------------------------
1141 It is important that prov_theta comes before req_theta as this ordering is used
1142 when desugaring record pattern synonym updates.
1143
1144 Any change to this ordering should make sure to change deSugar/DsExpr.hs if you
1145 want to avoid difficult to decipher core lint errors!
1146 -}
1147
1148
1149 nonBidirectionalErr :: Outputable name => name -> TcM a
1150 nonBidirectionalErr name = failWithTc $
1151 text "non-bidirectional pattern synonym"
1152 <+> quotes (ppr name) <+> text "used in an expression"
1153
1154 -- Walk the whole pattern and for all ConPatOuts, collect the
1155 -- existentially-bound type variables and evidence binding variables.
1156 --
1157 -- These are used in computing the type of a pattern synonym and also
1158 -- in generating matcher functions, since success continuations need
1159 -- to be passed these pattern-bound evidences.
1160 tcCollectEx
1161 :: LPat GhcTc
1162 -> ( [TyVar] -- Existentially-bound type variables
1163 -- in correctly-scoped order; e.g. [ k:*, x:k ]
1164 , [EvVar] ) -- and evidence variables
1165
1166 tcCollectEx pat = go pat
1167 where
1168 go :: LPat GhcTc -> ([TyVar], [EvVar])
1169 go = go1 . unLoc
1170
1171 go1 :: Pat GhcTc -> ([TyVar], [EvVar])
1172 go1 (LazyPat _ p) = go p
1173 go1 (AsPat _ _ p) = go p
1174 go1 (ParPat _ p) = go p
1175 go1 (BangPat _ p) = go p
1176 go1 (ListPat _ ps) = mergeMany . map go $ ps
1177 go1 (TuplePat _ ps _) = mergeMany . map go $ ps
1178 go1 (SumPat _ p _ _) = go p
1179 go1 (ViewPat _ _ p) = go p
1180 go1 con@ConPatOut{} = merge (pat_tvs con, pat_dicts con) $
1181 goConDetails $ pat_args con
1182 go1 (SigPat _ p _) = go p
1183 go1 (CoPat _ _ p _) = go1 p
1184 go1 (NPlusKPat _ n k _ geq subtract)
1185 = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract
1186 go1 _ = empty
1187
1188 goConDetails :: HsConPatDetails GhcTc -> ([TyVar], [EvVar])
1189 goConDetails (PrefixCon ps) = mergeMany . map go $ ps
1190 goConDetails (InfixCon p1 p2) = go p1 `merge` go p2
1191 goConDetails (RecCon HsRecFields{ rec_flds = flds })
1192 = mergeMany . map goRecFd $ flds
1193
1194 goRecFd :: LHsRecField GhcTc (LPat GhcTc) -> ([TyVar], [EvVar])
1195 goRecFd (dL->L _ HsRecField{ hsRecFieldArg = p }) = go p
1196
1197 merge (vs1, evs1) (vs2, evs2) = (vs1 ++ vs2, evs1 ++ evs2)
1198 mergeMany = foldr merge empty
1199 empty = ([], [])