6536b676e99fa0222b8e78e7e45c2ef7d997b11f
[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
10 module TcPatSyn ( tcPatSynSig, tcInferPatSynDecl, tcCheckPatSynDecl
11 , tcPatSynBuilderBind, tcPatSynBuilderOcc, nonBidirectionalErr
12 ) where
13
14 import HsSyn
15 import TcPat
16 import TcHsType( tcImplicitTKBndrs, tcExplicitTKBndrs
17 , tcHsContext, tcHsLiftedType, tcHsOpenType )
18 import TcRnMonad
19 import TcEnv
20 import TcMType
21 import TysPrim
22 import TysWiredIn ( runtimeRepTy )
23 import Name
24 import SrcLoc
25 import PatSyn
26 import NameSet
27 import Panic
28 import Outputable
29 import FastString
30 import Var
31 import Id
32 import IdInfo( RecSelParent(..))
33 import TcBinds
34 import BasicTypes
35 import TcSimplify
36 import TcUnify
37 import TcType
38 import Type
39 import TcEvidence
40 import BuildTyCl
41 import VarSet
42 import MkId
43 import TcTyDecls
44 import ConLike
45 import FieldLabel
46 import Bag
47 import Util
48 import ErrUtils
49 import Control.Monad ( unless, zipWithM )
50 import Data.List( partition )
51 import Pair( Pair(..) )
52
53 #include "HsVersions.h"
54
55 {- *********************************************************************
56 * *
57 Type checking a pattern synonym signature
58 * *
59 ************************************************************************
60
61 Note [Pattern synonym signatures]
62 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
63 Pattern synonym signatures are surprisingly tricky (see Trac #11224 for example).
64 In general they look like this:
65
66 pattern P :: forall univ_tvs. req
67 => forall ex_tvs. prov
68 => arg1 -> .. -> argn -> body_ty
69
70 For parsing and renaming we treat the signature as an ordinary LHsSigType.
71
72 Once we get to type checking, we decompose it into its parts, in tcPatSynSig.
73
74 * Note that 'forall univ_tvs' and 'req =>'
75 and 'forall ex_tvs' and 'prov =>'
76 are all optional. We gather the pieces at the the top of tcPatSynSig
77
78 * Initially the implicitly-bound tyvars (added by the renamer) include both
79 universal and existential vars.
80
81 * After we kind-check the pieces and convert to Types, we do kind generalisation.
82
83 * Note [Splitting the implicit tyvars in a pattern synonym]
84 Now the tricky bit: we must split
85 the implicitly-bound variables, and
86 the kind-generalised variables
87 into universal and existential. We do so as follows:
88
89 Note [The pattern-synonym signature splitting rule]
90 the universals are the ones mentioned in
91 - univ_tvs (and the kinds thereof)
92 - req
93 - body_ty
94 the existentials are the rest
95
96 * Moreover see Note
97 -}
98
99 tcPatSynSig :: Name -> LHsSigType Name -> TcM TcPatSynInfo
100 tcPatSynSig name sig_ty
101 | HsIB { hsib_vars = implicit_hs_tvs
102 , hsib_body = hs_ty } <- sig_ty
103 , (univ_hs_tvs, hs_req, hs_ty1) <- splitLHsSigmaTy hs_ty
104 , (ex_hs_tvs, hs_prov, hs_ty2) <- splitLHsSigmaTy hs_ty1
105 , (hs_arg_tys, hs_body_ty) <- splitHsFunType hs_ty2
106 = do { (implicit_tvs, (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty))
107 <- solveEqualities $
108 tcImplicitTKBndrs implicit_hs_tvs $
109 tcExplicitTKBndrs univ_hs_tvs $ \ univ_tvs ->
110 tcExplicitTKBndrs ex_hs_tvs $ \ ex_tvs ->
111 do { req <- tcHsContext hs_req
112 ; prov <- tcHsContext hs_prov
113 ; arg_tys <- mapM tcHsOpenType (hs_arg_tys :: [LHsType Name])
114 ; body_ty <- tcHsLiftedType hs_body_ty
115 ; let bound_tvs
116 = unionVarSets [ allBoundVariabless req
117 , allBoundVariabless prov
118 , allBoundVariabless (body_ty : arg_tys)
119 ]
120 ; return ( (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty)
121 , bound_tvs) }
122
123 -- Kind generalisation; c.f. kindGeneralise
124 ; let free_kvs = tyCoVarsOfTelescope (implicit_tvs ++ univ_tvs ++ ex_tvs) $
125 tyCoVarsOfTypes (body_ty : req ++ prov ++ arg_tys)
126
127 ; kvs <- quantifyTyVars emptyVarSet (Pair free_kvs emptyVarSet)
128
129 -- These are /signatures/ so we zonk to squeeze out any kind
130 -- unification variables. Do this after quantifyTyVars which may
131 -- default kind variables to *.
132 -- ToDo: checkValidType?
133 ; traceTc "about zonk" empty
134 ; implicit_tvs <- mapM zonkTcTyCoVarBndr implicit_tvs
135 ; univ_tvs <- mapM zonkTcTyCoVarBndr univ_tvs
136 ; ex_tvs <- mapM zonkTcTyCoVarBndr ex_tvs
137 ; req <- zonkTcTypes req
138 ; prov <- zonkTcTypes prov
139 ; arg_tys <- zonkTcTypes arg_tys
140 ; body_ty <- zonkTcType body_ty
141
142 -- Complain about: pattern P :: () => forall x. x -> P x
143 -- The renamer thought it was fine, but the existential 'x'
144 -- should not appear in the result type
145 ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType body_ty) ex_tvs
146 ; unless (null bad_tvs) $ addErr $
147 hang (text "The result type" <+> quotes (ppr body_ty))
148 2 (text "mentions existential type variable" <> plural bad_tvs
149 <+> pprQuotedList bad_tvs)
150
151 -- Split [Splitting the implicit tyvars in a pattern synonym]
152 ; let univ_fvs = closeOverKinds $
153 (tyCoVarsOfTypes (body_ty : req) `extendVarSetList` univ_tvs)
154 (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) .
155 binderVar "tcPatSynSig") $
156 mkNamedBinders Invisible kvs ++
157 mkNamedBinders Specified implicit_tvs
158 ; traceTc "tcTySig }" $
159 vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs
160 , text "kvs" <+> ppr_tvs kvs
161 , text "extra_univ" <+> ppr extra_univ
162 , text "univ_tvs" <+> ppr_tvs univ_tvs
163 , text "req" <+> ppr req
164 , text "extra_ex" <+> ppr extra_ex
165 , text "ex_tvs" <+> ppr_tvs ex_tvs
166 , text "prov" <+> ppr prov
167 , text "arg_tys" <+> ppr arg_tys
168 , text "body_ty" <+> ppr body_ty ]
169 ; return (TPSI { patsig_name = name
170 , patsig_univ_bndrs = extra_univ ++
171 mkNamedBinders Specified univ_tvs
172 , patsig_req = req
173 , patsig_ex_bndrs = extra_ex ++
174 mkNamedBinders Specified ex_tvs
175 , patsig_prov = prov
176 , patsig_arg_tys = arg_tys
177 , patsig_body_ty = body_ty }) }
178 where
179
180 ppr_tvs :: [TyVar] -> SDoc
181 ppr_tvs tvs = braces (vcat [ ppr tv <+> dcolon <+> ppr (tyVarKind tv)
182 | tv <- tvs])
183
184
185 {-
186 ************************************************************************
187 * *
188 Type checking a pattern synonym
189 * *
190 ************************************************************************
191 -}
192
193 tcInferPatSynDecl :: PatSynBind Name Name
194 -> TcM (LHsBinds Id, TcGblEnv)
195 tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
196 psb_def = lpat, psb_dir = dir }
197 = addPatSynCtxt lname $
198 do { traceTc "tcInferPatSynDecl {" $ ppr name
199 ; tcCheckPatSynPat lpat
200
201 ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
202 ; (tclvl, wanted, ((lpat', args), pat_ty))
203 <- pushLevelAndCaptureConstraints $
204 do { pat_ty <- newOpenInferExpType
205 ; stuff <- tcPat PatSyn lpat pat_ty $
206 mapM tcLookupId arg_names
207 ; pat_ty <- readExpType pat_ty
208 ; return (stuff, pat_ty) }
209
210 ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
211
212 ; (qtvs, req_dicts, ev_binds) <- simplifyInfer tclvl False [] named_taus wanted
213
214 ; let (ex_vars, prov_dicts) = tcCollectEx lpat'
215 univ_tvs = filter (not . (`elemVarSet` ex_vars)) qtvs
216 ex_tvs = varSetElems ex_vars
217 prov_theta = map evVarPred prov_dicts
218 req_theta = map evVarPred req_dicts
219
220 ; traceTc "tcInferPatSynDecl }" $ ppr name
221 ; tc_patsyn_finish lname dir is_infix lpat'
222 (univ_tvs, mkNamedBinders Invisible univ_tvs
223 , req_theta, ev_binds, req_dicts)
224 (ex_tvs, mkNamedBinders Invisible ex_tvs
225 , mkTyVarTys ex_tvs, prov_theta, map EvId prov_dicts)
226 (map nlHsVar args, map idType args)
227 pat_ty rec_fields }
228
229
230 tcCheckPatSynDecl :: PatSynBind Name Name
231 -> TcPatSynInfo
232 -> TcM (LHsBinds Id, TcGblEnv)
233 tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
234 , psb_def = lpat, psb_dir = dir }
235 TPSI{ patsig_univ_bndrs = univ_bndrs, patsig_prov = prov_theta
236 , patsig_ex_bndrs = ex_bndrs, patsig_req = req_theta
237 , patsig_arg_tys = arg_tys, patsig_body_ty = pat_ty }
238 = addPatSynCtxt lname $
239 do { let origin = ProvCtxtOrigin psb
240 skol_info = SigSkol (PatSynCtxt name) (mkCheckExpType $
241 mkFunTys arg_tys pat_ty)
242 decl_arity = length arg_names
243 ty_arity = length arg_tys
244 (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
245
246 univ_tvs = map (binderVar "tcCheckPatSynDecl 1") univ_bndrs
247 ex_tvs = map (binderVar "tcCheckPatSynDecl 2") ex_bndrs
248
249 ; traceTc "tcCheckPatSynDecl" $
250 vcat [ ppr univ_bndrs, ppr req_theta, ppr ex_bndrs
251 , ppr prov_theta, ppr arg_tys, ppr pat_ty ]
252
253 ; checkTc (decl_arity == ty_arity)
254 (wrongNumberOfParmsErr name decl_arity ty_arity)
255
256 ; tcCheckPatSynPat lpat
257
258 -- Right! Let's check the pattern against the signature
259 -- See Note [Checking against a pattern signature]
260 ; req_dicts <- newEvVars req_theta
261 ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
262 ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
263 pushLevelAndCaptureConstraints $
264 tcExtendTyVarEnv univ_tvs $
265 tcPat PatSyn lpat (mkCheckExpType pat_ty) $
266 do { (subst, ex_tvs') <- if isUnidirectional dir
267 then newMetaTyVars ex_tvs
268 else newMetaSigTyVars ex_tvs
269 -- See the "Existential type variables" part of
270 -- Note [Checking against a pattern signature]
271 ; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs])
272 ; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs'])
273 ; prov_dicts <- mapM (emitWanted origin)
274 (substTheta (extendTCvInScopeList subst univ_tvs) prov_theta)
275 -- Add the free vars of 'prov_theta' to the in_scope set to
276 -- satisfy the substition invariant. There's no need to
277 -- add 'ex_tvs' as they are already in the domain of the
278 -- substitution.
279 -- See also Note [The substitution invariant] in TyCoRep.
280 ; args' <- zipWithM (tc_arg subst) arg_names arg_tys
281 ; return (ex_tvs', prov_dicts, args') }
282
283 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted
284
285 -- Solve the constraints now, because we are about to make a PatSyn,
286 -- which should not contain unification variables and the like (Trac #10997)
287 -- Since all the inputs are implications the returned bindings will be empty
288 ; _ <- simplifyTop (mkImplicWC implics)
289
290 -- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct
291 -- Otherwise we may get a type error when typechecking the builder,
292 -- when that should be impossible
293
294 ; traceTc "tcCheckPatSynDecl }" $ ppr name
295 ; tc_patsyn_finish lname dir is_infix lpat'
296 (univ_tvs, univ_bndrs, req_theta, ev_binds, req_dicts)
297 (ex_tvs, ex_bndrs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
298 (args', arg_tys)
299 pat_ty rec_fields }
300 where
301 tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr TcId)
302 tc_arg subst arg_name arg_ty
303 = do { -- Look up the variable actually bound by lpat
304 -- and check that it has the expected type
305 arg_id <- tcLookupId arg_name
306 ; coi <- unifyType (Just arg_id)
307 (idType arg_id)
308 (substTyUnchecked subst arg_ty)
309 ; return (mkLHsWrapCo coi $ nlHsVar arg_id) }
310
311 {- Note [Checking against a pattern signature]
312 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
313 When checking the actual supplied pattern against the pattern synonym
314 signature, we need to be quite careful.
315
316 ----- Provided constraints
317 Example
318
319 data T a where
320 MkT :: Ord a => a -> T a
321
322 pattern P :: () => Eq a => a -> [T a]
323 pattern P x = [MkT x]
324
325 We must check that the (Eq a) that P claims to bind (and to
326 make available to matches against P), is derivable from the
327 actual pattern. For example:
328 f (P (x::a)) = ...here (Eq a) should be available...
329 And yes, (Eq a) is derivable from the (Ord a) bound by P's rhs.
330
331 ----- Existential type variables
332 Unusually, we instantiate the existential tyvars of the pattern with
333 *meta* type variables. For example
334
335 data S where
336 MkS :: Eq a => [a] -> S
337
338 pattern P :: () => Eq x => x -> S
339 pattern P x <- MkS x
340
341 The pattern synonym conceals from its client the fact that MkS has a
342 list inside it. The client just thinks it's a type 'x'. So we must
343 unify x := [a] during type checking, and then use the instantiating type
344 [a] (called ex_tys) when building the matcher. In this case we'll get
345
346 $mP :: S -> (forall x. Ex x => x -> r) -> r -> r
347 $mP x k = case x of
348 MkS a (d:Eq a) (ys:[a]) -> let dl :: Eq [a]
349 dl = $dfunEqList d
350 in k [a] dl ys
351
352 This "concealing" story works for /uni-directional/ pattern synonmys,
353 but obviously not for bidirectional ones. So in the bidirectional case
354 we use SigTv, rather than a generic TauTv, meta-tyvar so that. And
355 we should really check that those SigTvs don't get unified with each
356 other.
357
358 -}
359
360 collectPatSynArgInfo :: HsPatSynDetails (Located Name) -> ([Name], [Name], Bool)
361 collectPatSynArgInfo details =
362 case details of
363 PrefixPatSyn names -> (map unLoc names, [], False)
364 InfixPatSyn name1 name2 -> (map unLoc [name1, name2], [], True)
365 RecordPatSyn names ->
366 let (vars, sels) = unzip (map splitRecordPatSyn names)
367 in (vars, sels, False)
368
369 where
370 splitRecordPatSyn :: RecordPatSynField (Located Name) -> (Name, Name)
371 splitRecordPatSyn (RecordPatSynField { recordPatSynPatVar = L _ patVar
372 , recordPatSynSelectorId = L _ selId })
373 = (patVar, selId)
374
375 addPatSynCtxt :: Located Name -> TcM a -> TcM a
376 addPatSynCtxt (L loc name) thing_inside
377 = setSrcSpan loc $
378 addErrCtxt (text "In the declaration for pattern synonym"
379 <+> quotes (ppr name)) $
380 thing_inside
381
382 wrongNumberOfParmsErr :: Name -> Arity -> Arity -> SDoc
383 wrongNumberOfParmsErr name decl_arity ty_arity
384 = hang (text "Pattern synonym" <+> quotes (ppr name) <+> ptext (sLit "has")
385 <+> speakNOf decl_arity (text "argument"))
386 2 (text "but its type signature has" <+> speakN ty_arity)
387
388 -------------------------
389 -- Shared by both tcInferPatSyn and tcCheckPatSyn
390 tc_patsyn_finish :: Located Name -- ^ PatSyn Name
391 -> HsPatSynDir Name -- ^ PatSyn type (Uni/Bidir/ExplicitBidir)
392 -> Bool -- ^ Whether infix
393 -> LPat Id -- ^ Pattern of the PatSyn
394 -> ([TcTyVar], [TcTyBinder], [PredType], TcEvBinds, [EvVar])
395 -> ([TcTyVar], [TcTyBinder], [TcType], [PredType], [EvTerm])
396 -> ([LHsExpr TcId], [TcType]) -- ^ Pattern arguments and types
397 -> TcType -- ^ Pattern type
398 -> [Name] -- ^ Selector names
399 -- ^ Whether fields, empty if not record PatSyn
400 -> TcM (LHsBinds Id, TcGblEnv)
401 tc_patsyn_finish lname dir is_infix lpat'
402 (univ_tvs, univ_bndrs, req_theta, req_ev_binds, req_dicts)
403 (ex_tvs, ex_bndrs, ex_tys, prov_theta, prov_dicts)
404 (args, arg_tys)
405 pat_ty field_labels
406 = do { -- Zonk everything. We are about to build a final PatSyn
407 -- so there had better be no unification variables in there
408 univ_tvs <- mapMaybeM zonkQuantifiedTyVar univ_tvs
409 ; ex_tvs <- mapMaybeM zonkQuantifiedTyVar ex_tvs
410 ; prov_theta <- zonkTcTypes prov_theta
411 ; req_theta <- zonkTcTypes req_theta
412 ; pat_ty <- zonkTcType pat_ty
413 ; arg_tys <- zonkTcTypes arg_tys
414
415 -- We need to update the univ and ex binders after zonking.
416 -- But zonking may have defaulted some erstwhile binders,
417 -- so we need to make sure the tyvars and tybinders remain
418 -- lined up
419 ; let update_binders :: [TyVar] -> [TcTyBinder] -> [TyBinder]
420 update_binders [] _ = []
421 update_binders all_tvs@(tv:tvs) (bndr:bndrs)
422 | tv == bndr_var
423 = mkNamedBinder (binderVisibility bndr) tv : update_binders tvs bndrs
424 | otherwise
425 = update_binders all_tvs bndrs
426 where
427 bndr_var = binderVar "tc_patsyn_finish" bndr
428 update_binders tvs _ = pprPanic "tc_patsyn_finish" (ppr lname $$ ppr tvs)
429
430 univ_bndrs' = update_binders univ_tvs univ_bndrs
431 ex_bndrs' = update_binders ex_tvs ex_bndrs
432
433 ; traceTc "tc_patsyn_finish {" $
434 ppr (unLoc lname) $$ ppr (unLoc lpat') $$
435 ppr (univ_tvs, univ_bndrs', req_theta, req_ev_binds, req_dicts) $$
436 ppr (ex_tvs, ex_bndrs', prov_theta, prov_dicts) $$
437 ppr args $$
438 ppr arg_tys $$
439 ppr pat_ty
440
441 -- Make the 'matcher'
442 ; (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat'
443 (univ_tvs, req_theta, req_ev_binds, req_dicts)
444 (ex_tvs, ex_tys, prov_theta, prov_dicts)
445 (args, arg_tys)
446 pat_ty
447
448
449 -- Make the 'builder'
450 ; builder_id <- mkPatSynBuilderId dir lname
451 univ_bndrs' req_theta
452 ex_bndrs' prov_theta
453 arg_tys pat_ty
454
455 -- TODO: Make this have the proper information
456 ; let mkFieldLabel name = FieldLabel (occNameFS (nameOccName name)) False name
457 field_labels' = (map mkFieldLabel field_labels)
458
459
460 -- Make the PatSyn itself
461 ; let patSyn = mkPatSyn (unLoc lname) is_infix
462 (univ_tvs, univ_bndrs', req_theta)
463 (ex_tvs, ex_bndrs', prov_theta)
464 arg_tys
465 pat_ty
466 matcher_id builder_id
467 field_labels'
468
469 -- Selectors
470 ; let (sigs, selector_binds) =
471 unzip (mkPatSynRecSelBinds patSyn (patSynFieldLabels patSyn))
472 ; let tything = AConLike (PatSynCon patSyn)
473 ; tcg_env <-
474 tcExtendGlobalEnv [tything] $
475 tcRecSelBinds
476 (ValBindsOut (zip (repeat NonRecursive) selector_binds) sigs)
477
478 ; traceTc "tc_patsyn_finish }" empty
479 ; return (matcher_bind, tcg_env) }
480
481 {-
482 ************************************************************************
483 * *
484 Constructing the "matcher" Id and its binding
485 * *
486 ************************************************************************
487 -}
488
489 tcPatSynMatcher :: Located Name
490 -> LPat Id
491 -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
492 -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
493 -> ([LHsExpr TcId], [TcType])
494 -> TcType
495 -> TcM ((Id, Bool), LHsBinds Id)
496 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
497 tcPatSynMatcher (L loc name) lpat
498 (univ_tvs, req_theta, req_ev_binds, req_dicts)
499 (ex_tvs, ex_tys, prov_theta, prov_dicts)
500 (args, arg_tys) pat_ty
501 = do { rr_uniq <- newUnique
502 ; tv_uniq <- newUnique
503 ; let rr_name = mkInternalName rr_uniq (mkTyVarOcc "rep") loc
504 tv_name = mkInternalName tv_uniq (mkTyVarOcc "r") loc
505 rr_tv = mkTcTyVar rr_name runtimeRepTy (SkolemTv False)
506 rr = mkTyVarTy rr_tv
507 res_tv = mkTcTyVar tv_name (tYPE rr) (SkolemTv False)
508 is_unlifted = null args && null prov_dicts
509 res_ty = mkTyVarTy res_tv
510 (cont_args, cont_arg_tys)
511 | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
512 | otherwise = (args, arg_tys)
513 cont_ty = mkInvSigmaTy ex_tvs prov_theta $
514 mkFunTys cont_arg_tys res_ty
515
516 fail_ty = mkFunTy voidPrimTy res_ty
517
518 ; matcher_name <- newImplicitBinder name mkMatcherOcc
519 ; scrutinee <- newSysLocalId (fsLit "scrut") pat_ty
520 ; cont <- newSysLocalId (fsLit "cont") cont_ty
521 ; fail <- newSysLocalId (fsLit "fail") fail_ty
522
523 ; let matcher_tau = mkFunTys [pat_ty, cont_ty, fail_ty] res_ty
524 matcher_sigma = mkInvSigmaTy (rr_tv:res_tv:univ_tvs) req_theta matcher_tau
525 matcher_id = mkExportedVanillaId matcher_name matcher_sigma
526 -- See Note [Exported LocalIds] in Id
527
528 inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys
529 cont' = foldl nlHsApp (mkLHsWrap inst_wrap (nlHsVar cont)) cont_args
530
531 fail' = nlHsApps fail [nlHsVar voidPrimId]
532
533 args = map nlVarPat [scrutinee, cont, fail]
534 lwpat = noLoc $ WildPat pat_ty
535 cases = if isIrrefutableHsPat lpat
536 then [mkSimpleHsAlt lpat cont']
537 else [mkSimpleHsAlt lpat cont',
538 mkSimpleHsAlt lwpat fail']
539 body = mkLHsWrap (mkWpLet req_ev_binds) $
540 L (getLoc lpat) $
541 HsCase (nlHsVar scrutinee) $
542 MG{ mg_alts = L (getLoc lpat) cases
543 , mg_arg_tys = [pat_ty]
544 , mg_res_ty = res_ty
545 , mg_origin = Generated
546 }
547 body' = noLoc $
548 HsLam $
549 MG{ mg_alts = noLoc [mkSimpleMatch args body]
550 , mg_arg_tys = [pat_ty, cont_ty, res_ty]
551 , mg_res_ty = res_ty
552 , mg_origin = Generated
553 }
554 match = mkMatch [] (mkHsLams (rr_tv:res_tv:univ_tvs) req_dicts body')
555 (noLoc EmptyLocalBinds)
556 mg = MG{ mg_alts = L (getLoc match) [match]
557 , mg_arg_tys = []
558 , mg_res_ty = res_ty
559 , mg_origin = Generated
560 }
561
562 ; let bind = FunBind{ fun_id = L loc matcher_id
563 , fun_matches = mg
564 , fun_co_fn = idHsWrapper
565 , bind_fvs = emptyNameSet
566 , fun_tick = [] }
567 matcher_bind = unitBag (noLoc bind)
568
569 ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
570 ; traceTc "tcPatSynMatcher" (ppr matcher_bind)
571
572 ; return ((matcher_id, is_unlifted), matcher_bind) }
573
574 mkPatSynRecSelBinds :: PatSyn
575 -> [FieldLabel]
576 -- ^ Visible field labels
577 -> [(LSig Name, LHsBinds Name)]
578 mkPatSynRecSelBinds ps fields = map mkRecSel fields
579 where
580 mkRecSel fld_lbl =
581 case mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl of
582 (name, (_rec_flag, binds)) -> (name, binds)
583
584 isUnidirectional :: HsPatSynDir a -> Bool
585 isUnidirectional Unidirectional = True
586 isUnidirectional ImplicitBidirectional = False
587 isUnidirectional ExplicitBidirectional{} = False
588
589 {-
590 ************************************************************************
591 * *
592 Constructing the "builder" Id
593 * *
594 ************************************************************************
595 -}
596
597 mkPatSynBuilderId :: HsPatSynDir a -> Located Name
598 -> [TyBinder] -> ThetaType
599 -> [TyBinder] -> ThetaType
600 -> [Type] -> Type
601 -> TcM (Maybe (Id, Bool))
602 mkPatSynBuilderId dir (L _ name)
603 univ_bndrs req_theta ex_bndrs prov_theta
604 arg_tys pat_ty
605 | isUnidirectional dir
606 = return Nothing
607 | otherwise
608 = do { builder_name <- newImplicitBinder name mkBuilderOcc
609 ; let theta = req_theta ++ prov_theta
610 need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
611 builder_sigma = add_void need_dummy_arg $
612 mkForAllTys univ_bndrs $
613 mkForAllTys ex_bndrs $
614 mkFunTys theta $
615 mkFunTys arg_tys $
616 pat_ty
617 builder_id = mkExportedVanillaId builder_name builder_sigma
618 -- See Note [Exported LocalIds] in Id
619
620 ; return (Just (builder_id, need_dummy_arg)) }
621 where
622
623 tcPatSynBuilderBind :: TcSigFun
624 -> PatSynBind Name Name
625 -> TcM (LHsBinds Id)
626 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
627 tcPatSynBuilderBind sig_fun PSB{ psb_id = L loc name, psb_def = lpat
628 , psb_dir = dir, psb_args = details }
629 | isUnidirectional dir
630 = return emptyBag
631
632 | Left why <- mb_match_group -- Can't invert the pattern
633 = setSrcSpan (getLoc lpat) $ failWithTc $
634 vcat [ hang (text "Invalid right-hand side of bidirectional pattern synonym"
635 <+> quotes (ppr name) <> colon)
636 2 why
637 , text "RHS pattern:" <+> ppr lpat ]
638
639 | Right match_group <- mb_match_group -- Bidirectional
640 = do { patsyn <- tcLookupPatSyn name
641 ; traceTc "tcPatSynBuilderBind {" $ ppr patsyn
642 ; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn
643 -- Bidirectional, so patSynBuilder returns Just
644
645 match_group' | need_dummy_arg = add_dummy_arg match_group
646 | otherwise = match_group
647
648 bind = FunBind { fun_id = L loc (idName builder_id)
649 , fun_matches = match_group'
650 , fun_co_fn = idHsWrapper
651 , bind_fvs = placeHolderNamesTc
652 , fun_tick = [] }
653
654 ; sig <- get_builder_sig sig_fun name builder_id need_dummy_arg
655
656 ; (builder_binds, _) <- tcPolyCheck NonRecursive emptyPragEnv sig (noLoc bind)
657 ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
658 ; return builder_binds }
659
660 | otherwise = panic "tcPatSynBuilderBind" -- Both cases dealt with
661 where
662 mb_match_group
663 = case dir of
664 ExplicitBidirectional explicit_mg -> Right explicit_mg
665 ImplicitBidirectional -> fmap mk_mg (tcPatToExpr args lpat)
666 Unidirectional -> panic "tcPatSynBuilderBind"
667
668 mk_mg :: LHsExpr Name -> MatchGroup Name (LHsExpr Name)
669 mk_mg body = mkMatchGroupName Generated [builder_match]
670 where
671 builder_args = [L loc (VarPat (L loc n)) | L loc n <- args]
672 builder_match = mkMatch builder_args body (noLoc EmptyLocalBinds)
673
674 args = case details of
675 PrefixPatSyn args -> args
676 InfixPatSyn arg1 arg2 -> [arg1, arg2]
677 RecordPatSyn args -> map recordPatSynPatVar args
678
679 add_dummy_arg :: MatchGroup Name (LHsExpr Name)
680 -> MatchGroup Name (LHsExpr Name)
681 add_dummy_arg mg@(MG { mg_alts = L l [L loc match@(Match { m_pats = pats })] })
682 = mg { mg_alts = L l [L loc (match { m_pats = nlWildPatName : pats })] }
683 add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
684 pprMatches (PatSyn :: HsMatchContext Name) other_mg
685
686 get_builder_sig :: TcSigFun -> Name -> Id -> Bool -> TcM TcIdSigInfo
687 get_builder_sig sig_fun name builder_id need_dummy_arg
688 | Just (TcPatSynSig sig) <- sig_fun name
689 , TPSI { patsig_univ_bndrs = univ_bndrs
690 , patsig_req = req
691 , patsig_ex_bndrs = ex_bndrs
692 , patsig_prov = prov
693 , patsig_arg_tys = arg_tys
694 , patsig_body_ty = body_ty } <- sig
695 = -- Constuct a TcIdSigInfo from a TcPatSynInfo
696 -- This does unfortunately mean that we have to know how to
697 -- make the builder Id's type from the TcPatSynInfo, which
698 -- duplicates the construction in mkPatSynBuilderId
699 -- But we really want to use the scoped type variables from
700 -- the actual sigature, so this is really the Right Thing
701 return (TISI { sig_bndr = CompleteSig builder_id
702 , sig_skols = [ (tyVarName tv, tv)
703 | bndr <- univ_bndrs ++ ex_bndrs
704 , let tv = binderVar "get_builder_sig" bndr ]
705 , sig_theta = req ++ prov
706 , sig_tau = add_void need_dummy_arg $
707 mkFunTys arg_tys body_ty
708 , sig_ctxt = PatSynCtxt name
709 , sig_loc = getSrcSpan name })
710 | otherwise
711 = -- No signature, so fake up a TcIdSigInfo from the builder Id
712 instTcTySigFromId builder_id
713 -- See Note [Redundant constraints for builder]
714
715 tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr TcId, TcSigmaType)
716 -- monadic only for failure
717 tcPatSynBuilderOcc ps
718 | Just (builder_id, add_void_arg) <- builder
719 , let builder_expr = HsVar (noLoc builder_id)
720 builder_ty = idType builder_id
721 = return $
722 if add_void_arg
723 then ( HsApp (noLoc $ builder_expr) (nlHsVar voidPrimId)
724 , tcFunResultTy builder_ty )
725 else (builder_expr, builder_ty)
726
727 | otherwise -- Unidirectional
728 = nonBidirectionalErr name
729 where
730 name = patSynName ps
731 builder = patSynBuilder ps
732
733 add_void :: Bool -> Type -> Type
734 add_void need_dummy_arg ty
735 | need_dummy_arg = mkFunTy voidPrimTy ty
736 | otherwise = ty
737
738 tcPatToExpr :: [Located Name] -> LPat Name -> Either MsgDoc (LHsExpr Name)
739 -- Given a /pattern/, return an /expression/ that builds a value
740 -- that matches the pattern. E.g. if the pattern is (Just [x]),
741 -- the expression is (Just [x]). They look the same, but the
742 -- input uses constructors from HsPat and the output uses constructors
743 -- from HsExpr.
744 --
745 -- Returns (Left r) if the pattern is not invertible, for reason r.
746 -- See Note [Builder for a bidirectional pattern synonym]
747 tcPatToExpr args pat = go pat
748 where
749 lhsVars = mkNameSet (map unLoc args)
750
751 -- Make a prefix con for prefix and infix patterns for simplicity
752 mkPrefixConExpr :: Located Name -> [LPat Name] -> Either MsgDoc (HsExpr Name)
753 mkPrefixConExpr lcon@(L loc _) pats
754 = do { exprs <- mapM go pats
755 ; return (foldl (\x y -> HsApp (L loc x) y)
756 (HsVar lcon) exprs) }
757
758 mkRecordConExpr :: Located Name -> HsRecFields Name (LPat Name)
759 -> Either MsgDoc (HsExpr Name)
760 mkRecordConExpr con fields
761 = do { exprFields <- mapM go fields
762 ; return (RecordCon con PlaceHolder noPostTcExpr exprFields) }
763
764 go :: LPat Name -> Either MsgDoc (LHsExpr Name)
765 go (L loc p) = L loc <$> go1 p
766
767 go1 :: Pat Name -> Either MsgDoc (HsExpr Name)
768 go1 (ConPatIn con info)
769 = case info of
770 PrefixCon ps -> mkPrefixConExpr con ps
771 InfixCon l r -> mkPrefixConExpr con [l,r]
772 RecCon fields -> mkRecordConExpr con fields
773
774 go1 (SigPatIn pat _) = go1 (unLoc pat)
775 -- See Note [Type signatures and the builder expression]
776
777 go1 (VarPat (L l var))
778 | var `elemNameSet` lhsVars
779 = return $ HsVar (L l var)
780 | otherwise
781 = Left (quotes (ppr var) <+> text "is not bound by the LHS of the pattern synonym")
782 go1 (ParPat pat) = fmap HsPar $ go pat
783 go1 (LazyPat pat) = go1 (unLoc pat)
784 go1 (BangPat pat) = go1 (unLoc pat)
785 go1 (PArrPat pats ptt) = do { exprs <- mapM go pats
786 ; return $ ExplicitPArr ptt exprs }
787 go1 (ListPat pats ptt reb) = do { exprs <- mapM go pats
788 ; return $ ExplicitList ptt (fmap snd reb) exprs }
789 go1 (TuplePat pats box _) = do { exprs <- mapM go pats
790 ; return $ ExplicitTuple
791 (map (noLoc . Present) exprs) box }
792 go1 (LitPat lit) = return $ HsLit lit
793 go1 (NPat (L _ n) mb_neg _ _)
794 | Just neg <- mb_neg = return $ unLoc $ nlHsSyntaxApps neg [noLoc (HsOverLit n)]
795 | otherwise = return $ HsOverLit n
796 go1 (ConPatOut{}) = panic "ConPatOut in output of renamer"
797 go1 (SigPatOut{}) = panic "SigPatOut in output of renamer"
798 go1 (CoPat{}) = panic "CoPat in output of renamer"
799 go1 p = Left (text "pattern" <+> quotes (ppr p) <+> text "is not invertible")
800
801 {- Note [Builder for a bidirectional pattern synonym]
802 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
803 For a bidirectional pattern synonym we need to produce an /expression/
804 that matches the supplied /pattern/, given values for the arguments
805 of the pattern synoymy. For example
806 pattern F x y = (Just x, [y])
807 The 'builder' for F looks like
808 $builderF x y = (Just x, [y])
809
810 We can't always do this:
811 * Some patterns aren't invertible; e.g. view patterns
812 pattern F x = (reverse -> x:_)
813
814 * The RHS pattern might bind more variables than the pattern
815 synonym, so again we can't invert it
816 pattern F x = (x,y)
817
818 * Ditto wildcards
819 pattern F x = (x,_)
820
821
822 Note [Redundant constraints for builder]
823 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
824 The builder can have redundant constraints, which are awkard to eliminate.
825 Consider
826 pattern P = Just 34
827 To match against this pattern we need (Eq a, Num a). But to build
828 (Just 34) we need only (Num a). Fortunately instTcSigFromId sets
829 sig_warn_redundant to False.
830
831 ************************************************************************
832 * *
833 Helper functions
834 * *
835 ************************************************************************
836
837 Note [As-patterns in pattern synonym definitions]
838 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
839 The rationale for rejecting as-patterns in pattern synonym definitions
840 is that an as-pattern would introduce nonindependent pattern synonym
841 arguments, e.g. given a pattern synonym like:
842
843 pattern K x y = x@(Just y)
844
845 one could write a nonsensical function like
846
847 f (K Nothing x) = ...
848
849 or
850 g (K (Just True) False) = ...
851
852 Note [Type signatures and the builder expression]
853 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
854 Consider
855 pattern L x = Left x :: Either [a] [b]
856
857 In tc{Infer/Check}PatSynDecl we will check that the pattern has the
858 specified type. We check the pattern *as a pattern*, so the type
859 signature is a pattern signature, and so brings 'a' and 'b' into
860 scope. But we don't have a way to bind 'a, b' in the LHS, as we do
861 'x', say. Nevertheless, the sigature may be useful to constrain
862 the type.
863
864 When making the binding for the *builder*, though, we don't want
865 $buildL x = Left x :: Either [a] [b]
866 because that wil either mean (forall a b. Either [a] [b]), or we'll
867 get a complaint that 'a' and 'b' are out of scope. (Actually the
868 latter; Trac #9867.) No, the job of the signature is done, so when
869 converting the pattern to an expression (for the builder RHS) we
870 simply discard the signature.
871
872 Note [Record PatSyn Desugaring]
873 -------------------------------
874 It is important that prov_theta comes before req_theta as this ordering is used
875 when desugaring record pattern synonym updates.
876
877 Any change to this ordering should make sure to change deSugar/DsExpr.hs if you
878 want to avoid difficult to decipher core lint errors!
879 -}
880
881 tcCheckPatSynPat :: LPat Name -> TcM ()
882 tcCheckPatSynPat = go
883 where
884 go :: LPat Name -> TcM ()
885 go = addLocM go1
886
887 go1 :: Pat Name -> TcM ()
888 go1 (ConPatIn _ info) = mapM_ go (hsConPatArgs info)
889 go1 VarPat{} = return ()
890 go1 WildPat{} = return ()
891 go1 p@(AsPat _ _) = asPatInPatSynErr p
892 go1 (LazyPat pat) = go pat
893 go1 (ParPat pat) = go pat
894 go1 (BangPat pat) = go pat
895 go1 (PArrPat pats _) = mapM_ go pats
896 go1 (ListPat pats _ _) = mapM_ go pats
897 go1 (TuplePat pats _ _) = mapM_ go pats
898 go1 LitPat{} = return ()
899 go1 NPat{} = return ()
900 go1 (SigPatIn pat _) = go pat
901 go1 (ViewPat _ pat _) = go pat
902 go1 p@SplicePat{} = thInPatSynErr p
903 go1 p@NPlusKPat{} = nPlusKPatInPatSynErr p
904 go1 ConPatOut{} = panic "ConPatOut in output of renamer"
905 go1 SigPatOut{} = panic "SigPatOut in output of renamer"
906 go1 CoPat{} = panic "CoPat in output of renamer"
907
908 asPatInPatSynErr :: OutputableBndr name => Pat name -> TcM a
909 asPatInPatSynErr pat
910 = failWithTc $
911 hang (text "Pattern synonym definition cannot contain as-patterns (@):")
912 2 (ppr pat)
913
914 thInPatSynErr :: OutputableBndr name => Pat name -> TcM a
915 thInPatSynErr pat
916 = failWithTc $
917 hang (text "Pattern synonym definition cannot contain Template Haskell:")
918 2 (ppr pat)
919
920 nPlusKPatInPatSynErr :: OutputableBndr name => Pat name -> TcM a
921 nPlusKPatInPatSynErr pat
922 = failWithTc $
923 hang (text "Pattern synonym definition cannot contain n+k-pattern:")
924 2 (ppr pat)
925
926 nonBidirectionalErr :: Outputable name => name -> TcM a
927 nonBidirectionalErr name = failWithTc $
928 text "non-bidirectional pattern synonym"
929 <+> quotes (ppr name) <+> text "used in an expression"
930
931 -- Walk the whole pattern and for all ConPatOuts, collect the
932 -- existentially-bound type variables and evidence binding variables.
933 --
934 -- These are used in computing the type of a pattern synonym and also
935 -- in generating matcher functions, since success continuations need
936 -- to be passed these pattern-bound evidences.
937 tcCollectEx :: LPat Id -> (TyVarSet, [EvVar])
938 tcCollectEx pat = go pat
939 where
940 go :: LPat Id -> (TyVarSet, [EvVar])
941 go = go1 . unLoc
942
943 go1 :: Pat Id -> (TyVarSet, [EvVar])
944 go1 (LazyPat p) = go p
945 go1 (AsPat _ p) = go p
946 go1 (ParPat p) = go p
947 go1 (BangPat p) = go p
948 go1 (ListPat ps _ _) = mconcat . map go $ ps
949 go1 (TuplePat ps _ _) = mconcat . map go $ ps
950 go1 (PArrPat ps _) = mconcat . map go $ ps
951 go1 (ViewPat _ p _) = go p
952 go1 con@ConPatOut{} = mappend (mkVarSet (pat_tvs con), pat_dicts con) $
953 goConDetails $ pat_args con
954 go1 (SigPatOut p _) = go p
955 go1 (CoPat _ p _) = go1 p
956 go1 (NPlusKPat n k _ geq subtract _)
957 = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract
958 go1 _ = mempty
959
960 goConDetails :: HsConPatDetails Id -> (TyVarSet, [EvVar])
961 goConDetails (PrefixCon ps) = mconcat . map go $ ps
962 goConDetails (InfixCon p1 p2) = go p1 `mappend` go p2
963 goConDetails (RecCon HsRecFields{ rec_flds = flds })
964 = mconcat . map goRecFd $ flds
965
966 goRecFd :: LHsRecField Id (LPat Id) -> (TyVarSet, [EvVar])
967 goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p