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