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