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