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