c5a0c270b4dd967fafecdfa6c3d4237d2eff6904
[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( binderVar, mkNamedBinders, binderVisibility, mkEmptyTCvSubst
18 , tidyTyCoVarBndrs, 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 False [] named_taus wanted
85
86 ; let ((ex_tvs, ex_vars), prov_dicts) = tcCollectEx lpat'
87 univ_tvs = filter (not . (`elemVarSet` ex_vars)) qtvs
88 prov_theta = map evVarPred prov_dicts
89 req_theta = map evVarPred req_dicts
90
91 ; traceTc "tcInferPatSynDecl }" $ ppr name
92 ; tc_patsyn_finish lname dir is_infix lpat'
93 (univ_tvs, mkNamedBinders Invisible univ_tvs
94 , req_theta, ev_binds, req_dicts)
95 (ex_tvs, mkNamedBinders Invisible ex_tvs
96 , mkTyVarTys ex_tvs, prov_theta, map EvId prov_dicts)
97 (map nlHsVar args, map idType args)
98 pat_ty rec_fields }
99
100
101 tcCheckPatSynDecl :: PatSynBind Name Name
102 -> TcPatSynInfo
103 -> TcM (LHsBinds Id, TcGblEnv)
104 tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
105 , psb_def = lpat, psb_dir = dir }
106 TPSI{ patsig_implicit_bndrs = implicit_tvs
107 , patsig_univ_bndrs = explicit_univ_tvs, patsig_prov = prov_theta
108 , patsig_ex_bndrs = explicit_ex_tvs, patsig_req = req_theta
109 , patsig_body_ty = sig_body_ty }
110 = addPatSynCtxt lname $
111 do { let decl_arity = length arg_names
112 (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
113
114 ; traceTc "tcCheckPatSynDecl" $
115 vcat [ ppr implicit_tvs, ppr explicit_univ_tvs, ppr req_theta
116 , ppr explicit_ex_tvs, ppr prov_theta, ppr sig_body_ty ]
117
118 ; tcCheckPatSynPat lpat
119
120 ; (arg_tys, pat_ty) <- case tcSplitFunTysN decl_arity sig_body_ty of
121 Right stuff -> return stuff
122 Left missing -> wrongNumberOfParmsErr name decl_arity missing
123
124 -- Complain about: pattern P :: () => forall x. x -> P x
125 -- The existential 'x' should not appear in the result type
126 -- Can't check this until we know P's arity
127 ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType pat_ty) explicit_ex_tvs
128 ; checkTc (null bad_tvs) $
129 hang (sep [ text "The result type of the signature for" <+> quotes (ppr name) <> comma
130 , text "namely" <+> quotes (ppr pat_ty) ])
131 2 (text "mentions existential type variable" <> plural bad_tvs
132 <+> pprQuotedList bad_tvs)
133
134 -- See Note [The pattern-synonym signature splitting rule]
135 ; let get_tv = binderVar "tcCheckPatSynDecl"
136 univ_fvs = closeOverKinds $
137 (tyCoVarsOfTypes (pat_ty : req_theta) `extendVarSetList` explicit_univ_tvs)
138 (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) . get_tv) implicit_tvs
139 univ_bndrs = extra_univ ++ mkNamedBinders Specified explicit_univ_tvs
140 ex_bndrs = extra_ex ++ mkNamedBinders Specified explicit_ex_tvs
141 univ_tvs = map get_tv univ_bndrs
142 ex_tvs = map get_tv 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_tvs, univ_bndrs, req_theta, ev_binds, req_dicts)
189 (ex_tvs, 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 -> ([TcTyVar], [TcTyBinder], [PredType], TcEvBinds, [EvVar])
288 -> ([TcTyVar], [TcTyBinder], [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_tvs, univ_bndrs, req_theta, req_ev_binds, req_dicts)
296 (ex_tvs, 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 (zonkQuantifiedTyVar False) univ_tvs
302 ; ex_tvs' <- mapMaybeM (zonkQuantifiedTyVar False) ex_tvs
303 -- ToDo: The False means that we behave here as if
304 -- -XPolyKinds was always on, which isn't right.
305 ; prov_theta' <- zonkTcTypes prov_theta
306 ; req_theta' <- zonkTcTypes req_theta
307 ; pat_ty' <- zonkTcType pat_ty
308 ; arg_tys' <- zonkTcTypes arg_tys
309
310 ; let (env1, univ_tvs) = tidyTyCoVarBndrs emptyTidyEnv univ_tvs'
311 (env2, ex_tvs) = tidyTyCoVarBndrs env1 ex_tvs'
312 req_theta = tidyTypes env2 req_theta'
313 prov_theta = tidyTypes env2 prov_theta'
314 arg_tys = tidyTypes env2 arg_tys'
315 pat_ty = tidyType env2 pat_ty'
316
317 -- We need to update the univ and ex binders after zonking.
318 -- But zonking may have defaulted some erstwhile binders,
319 -- so we need to make sure the tyvars and tybinders remain
320 -- lined up
321 ; let update_binders :: [TyVar] -> [TcTyBinder] -> [TyBinder]
322 update_binders [] _ = []
323 update_binders all_tvs@(tv:tvs) (bndr:bndrs)
324 | tv == bndr_var
325 = mkNamedBinder (binderVisibility bndr) tv : update_binders tvs bndrs
326 | otherwise
327 = update_binders all_tvs bndrs
328 where
329 bndr_var = binderVar "tc_patsyn_finish" bndr
330 update_binders tvs _ = pprPanic "tc_patsyn_finish" (ppr lname $$ ppr tvs)
331
332 univ_bndrs' = update_binders univ_tvs univ_bndrs
333 ex_bndrs' = update_binders ex_tvs ex_bndrs
334
335 ; traceTc "tc_patsyn_finish {" $
336 ppr (unLoc lname) $$ ppr (unLoc lpat') $$
337 ppr (univ_tvs, univ_bndrs', req_theta, req_ev_binds, req_dicts) $$
338 ppr (ex_tvs, ex_bndrs', prov_theta, prov_dicts) $$
339 ppr args $$
340 ppr arg_tys $$
341 ppr pat_ty
342
343 -- Make the 'matcher'
344 ; (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat'
345 (univ_tvs, req_theta, req_ev_binds, req_dicts)
346 (ex_tvs, ex_tys, prov_theta, prov_dicts)
347 (args, arg_tys)
348 pat_ty
349
350
351 -- Make the 'builder'
352 ; builder_id <- mkPatSynBuilderId dir lname
353 univ_bndrs' req_theta
354 ex_bndrs' prov_theta
355 arg_tys pat_ty
356
357 -- TODO: Make this have the proper information
358 ; let mkFieldLabel name = FieldLabel { flLabel = occNameFS (nameOccName name)
359 , flIsOverloaded = False
360 , flSelector = name }
361 field_labels' = map mkFieldLabel field_labels
362
363
364 -- Make the PatSyn itself
365 ; let patSyn = mkPatSyn (unLoc lname) is_infix
366 (univ_tvs, univ_bndrs', req_theta)
367 (ex_tvs, ex_bndrs', prov_theta)
368 arg_tys
369 pat_ty
370 matcher_id builder_id
371 field_labels'
372
373 -- Selectors
374 ; let rn_rec_sel_binds = mkPatSynRecSelBinds patSyn (patSynFieldLabels patSyn)
375 tything = AConLike (PatSynCon patSyn)
376 ; tcg_env <- tcExtendGlobalEnv [tything] $
377 tcRecSelBinds rn_rec_sel_binds
378
379 ; traceTc "tc_patsyn_finish }" empty
380 ; return (matcher_bind, tcg_env) }
381
382 {-
383 ************************************************************************
384 * *
385 Constructing the "matcher" Id and its binding
386 * *
387 ************************************************************************
388 -}
389
390 tcPatSynMatcher :: Located Name
391 -> LPat Id
392 -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
393 -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
394 -> ([LHsExpr TcId], [TcType])
395 -> TcType
396 -> TcM ((Id, Bool), LHsBinds Id)
397 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
398 tcPatSynMatcher (L loc name) lpat
399 (univ_tvs, req_theta, req_ev_binds, req_dicts)
400 (ex_tvs, ex_tys, prov_theta, prov_dicts)
401 (args, arg_tys) pat_ty
402 = do { rr_name <- newNameAt (mkTyVarOcc "rep") loc
403 ; tv_name <- newNameAt (mkTyVarOcc "r") loc
404 ; let rr_tv = mkTcTyVar rr_name runtimeRepTy (SkolemTv False)
405 rr = mkTyVarTy rr_tv
406 res_tv = mkTcTyVar tv_name (tYPE rr) (SkolemTv False)
407 is_unlifted = null args && null prov_dicts
408 res_ty = mkTyVarTy res_tv
409 (cont_args, cont_arg_tys)
410 | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
411 | otherwise = (args, arg_tys)
412 cont_ty = mkInvSigmaTy ex_tvs prov_theta $
413 mkFunTys cont_arg_tys res_ty
414
415 fail_ty = mkFunTy voidPrimTy res_ty
416
417 ; matcher_name <- newImplicitBinder name mkMatcherOcc
418 ; scrutinee <- newSysLocalId (fsLit "scrut") pat_ty
419 ; cont <- newSysLocalId (fsLit "cont") cont_ty
420 ; fail <- newSysLocalId (fsLit "fail") fail_ty
421
422 ; let matcher_tau = mkFunTys [pat_ty, cont_ty, fail_ty] res_ty
423 matcher_sigma = mkInvSigmaTy (rr_tv:res_tv:univ_tvs) req_theta matcher_tau
424 matcher_id = mkExportedVanillaId matcher_name matcher_sigma
425 -- See Note [Exported LocalIds] in Id
426
427 inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys
428 cont' = foldl nlHsApp (mkLHsWrap inst_wrap (nlHsVar cont)) cont_args
429
430 fail' = nlHsApps fail [nlHsVar voidPrimId]
431
432 args = map nlVarPat [scrutinee, cont, fail]
433 lwpat = noLoc $ WildPat pat_ty
434 cases = if isIrrefutableHsPat lpat
435 then [mkHsCaseAlt lpat cont']
436 else [mkHsCaseAlt lpat cont',
437 mkHsCaseAlt lwpat fail']
438 body = mkLHsWrap (mkWpLet req_ev_binds) $
439 L (getLoc lpat) $
440 HsCase (nlHsVar scrutinee) $
441 MG{ mg_alts = L (getLoc lpat) cases
442 , mg_arg_tys = [pat_ty]
443 , mg_res_ty = res_ty
444 , mg_origin = Generated
445 }
446 body' = noLoc $
447 HsLam $
448 MG{ mg_alts = noLoc [mkSimpleMatch LambdaExpr
449 args body]
450 , mg_arg_tys = [pat_ty, cont_ty, res_ty]
451 , mg_res_ty = res_ty
452 , mg_origin = Generated
453 }
454 match = mkMatch (FunRhs (L loc name) Prefix) []
455 (mkHsLams (rr_tv:res_tv:univ_tvs)
456 req_dicts body')
457 (noLoc EmptyLocalBinds)
458 mg = MG{ mg_alts = L (getLoc match) [match]
459 , mg_arg_tys = []
460 , mg_res_ty = res_ty
461 , mg_origin = Generated
462 }
463
464 ; let bind = FunBind{ fun_id = L loc matcher_id
465 , fun_matches = mg
466 , fun_co_fn = idHsWrapper
467 , bind_fvs = emptyNameSet
468 , fun_tick = [] }
469 matcher_bind = unitBag (noLoc bind)
470
471 ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
472 ; traceTc "tcPatSynMatcher" (ppr matcher_bind)
473
474 ; return ((matcher_id, is_unlifted), matcher_bind) }
475
476 mkPatSynRecSelBinds :: PatSyn
477 -> [FieldLabel] -- ^ Visible field labels
478 -> HsValBinds Name
479 mkPatSynRecSelBinds ps fields
480 = ValBindsOut selector_binds sigs
481 where
482 (sigs, selector_binds) = unzip (map mkRecSel fields)
483 mkRecSel fld_lbl = mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl
484
485 isUnidirectional :: HsPatSynDir a -> Bool
486 isUnidirectional Unidirectional = True
487 isUnidirectional ImplicitBidirectional = False
488 isUnidirectional ExplicitBidirectional{} = False
489
490 {-
491 ************************************************************************
492 * *
493 Constructing the "builder" Id
494 * *
495 ************************************************************************
496 -}
497
498 mkPatSynBuilderId :: HsPatSynDir a -> Located Name
499 -> [TyBinder] -> ThetaType
500 -> [TyBinder] -> ThetaType
501 -> [Type] -> Type
502 -> TcM (Maybe (Id, Bool))
503 mkPatSynBuilderId dir (L _ name)
504 univ_bndrs req_theta ex_bndrs prov_theta
505 arg_tys pat_ty
506 | isUnidirectional dir
507 = return Nothing
508 | otherwise
509 = do { builder_name <- newImplicitBinder name mkBuilderOcc
510 ; let theta = req_theta ++ prov_theta
511 need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
512 builder_sigma = add_void need_dummy_arg $
513 mkForAllTys univ_bndrs $
514 mkForAllTys ex_bndrs $
515 mkFunTys theta $
516 mkFunTys arg_tys $
517 pat_ty
518 builder_id = mkExportedVanillaId builder_name builder_sigma
519 -- See Note [Exported LocalIds] in Id
520
521 ; return (Just (builder_id, need_dummy_arg)) }
522 where
523
524 tcPatSynBuilderBind :: PatSynBind Name Name
525 -> TcM (LHsBinds Id)
526 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
527 tcPatSynBuilderBind (PSB { psb_id = L loc name, psb_def = lpat
528 , psb_dir = dir, psb_args = details })
529 | isUnidirectional dir
530 = return emptyBag
531
532 | Left why <- mb_match_group -- Can't invert the pattern
533 = setSrcSpan (getLoc lpat) $ failWithTc $
534 vcat [ hang (text "Invalid right-hand side of bidirectional pattern synonym"
535 <+> quotes (ppr name) <> colon)
536 2 why
537 , text "RHS pattern:" <+> ppr lpat ]
538
539 | Right match_group <- mb_match_group -- Bidirectional
540 = do { patsyn <- tcLookupPatSyn name
541 ; traceTc "tcPatSynBuilderBind {" $ ppr patsyn
542 ; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn
543 -- Bidirectional, so patSynBuilder returns Just
544
545 match_group' | need_dummy_arg = add_dummy_arg match_group
546 | otherwise = match_group
547
548 bind = FunBind { fun_id = L loc (idName builder_id)
549 , fun_matches = match_group'
550 , fun_co_fn = idHsWrapper
551 , bind_fvs = placeHolderNamesTc
552 , fun_tick = [] }
553
554 sig = completeSigFromId (PatSynCtxt name) builder_id
555
556 ; (builder_binds, _) <- tcPolyCheck emptyPragEnv sig (noLoc bind)
557 ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
558 ; return builder_binds }
559
560 | otherwise = panic "tcPatSynBuilderBind" -- Both cases dealt with
561 where
562 mb_match_group
563 = case dir of
564 ExplicitBidirectional explicit_mg -> Right explicit_mg
565 ImplicitBidirectional -> fmap mk_mg (tcPatToExpr args lpat)
566 Unidirectional -> panic "tcPatSynBuilderBind"
567
568 mk_mg :: LHsExpr Name -> MatchGroup Name (LHsExpr Name)
569 mk_mg body = mkMatchGroupName Generated [builder_match]
570 where
571 builder_args = [L loc (VarPat (L loc n)) | L loc n <- args]
572 builder_match = mkMatch (FunRhs (L loc name) Prefix)
573 builder_args body
574 (noLoc EmptyLocalBinds)
575
576 args = case details of
577 PrefixPatSyn args -> args
578 InfixPatSyn arg1 arg2 -> [arg1, arg2]
579 RecordPatSyn args -> map recordPatSynPatVar args
580
581 add_dummy_arg :: MatchGroup Name (LHsExpr Name)
582 -> MatchGroup Name (LHsExpr Name)
583 add_dummy_arg mg@(MG { mg_alts = L l [L loc match@(Match { m_pats = pats })] })
584 = mg { mg_alts = L l [L loc (match { m_pats = nlWildPatName : pats })] }
585 add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
586 pprMatches other_mg
587
588 tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr TcId, TcSigmaType)
589 -- monadic only for failure
590 tcPatSynBuilderOcc ps
591 | Just (builder_id, add_void_arg) <- builder
592 , let builder_expr = HsVar (noLoc builder_id)
593 builder_ty = idType builder_id
594 = return $
595 if add_void_arg
596 then ( HsApp (noLoc $ builder_expr) (nlHsVar voidPrimId)
597 , tcFunResultTy builder_ty )
598 else (builder_expr, builder_ty)
599
600 | otherwise -- Unidirectional
601 = nonBidirectionalErr name
602 where
603 name = patSynName ps
604 builder = patSynBuilder ps
605
606 add_void :: Bool -> Type -> Type
607 add_void need_dummy_arg ty
608 | need_dummy_arg = mkFunTy voidPrimTy ty
609 | otherwise = ty
610
611 tcPatToExpr :: [Located Name] -> LPat Name -> Either MsgDoc (LHsExpr Name)
612 -- Given a /pattern/, return an /expression/ that builds a value
613 -- that matches the pattern. E.g. if the pattern is (Just [x]),
614 -- the expression is (Just [x]). They look the same, but the
615 -- input uses constructors from HsPat and the output uses constructors
616 -- from HsExpr.
617 --
618 -- Returns (Left r) if the pattern is not invertible, for reason r.
619 -- See Note [Builder for a bidirectional pattern synonym]
620 tcPatToExpr args pat = go pat
621 where
622 lhsVars = mkNameSet (map unLoc args)
623
624 -- Make a prefix con for prefix and infix patterns for simplicity
625 mkPrefixConExpr :: Located Name -> [LPat Name] -> Either MsgDoc (HsExpr Name)
626 mkPrefixConExpr lcon@(L loc _) pats
627 = do { exprs <- mapM go pats
628 ; return (foldl (\x y -> HsApp (L loc x) y)
629 (HsVar lcon) exprs) }
630
631 mkRecordConExpr :: Located Name -> HsRecFields Name (LPat Name)
632 -> Either MsgDoc (HsExpr Name)
633 mkRecordConExpr con fields
634 = do { exprFields <- mapM go fields
635 ; return (RecordCon con PlaceHolder noPostTcExpr exprFields) }
636
637 go :: LPat Name -> Either MsgDoc (LHsExpr Name)
638 go (L loc p) = L loc <$> go1 p
639
640 go1 :: Pat Name -> Either MsgDoc (HsExpr Name)
641 go1 (ConPatIn con info)
642 = case info of
643 PrefixCon ps -> mkPrefixConExpr con ps
644 InfixCon l r -> mkPrefixConExpr con [l,r]
645 RecCon fields -> mkRecordConExpr con fields
646
647 go1 (SigPatIn pat _) = go1 (unLoc pat)
648 -- See Note [Type signatures and the builder expression]
649
650 go1 (VarPat (L l var))
651 | var `elemNameSet` lhsVars
652 = return $ HsVar (L l var)
653 | otherwise
654 = Left (quotes (ppr var) <+> text "is not bound by the LHS of the pattern synonym")
655 go1 (ParPat pat) = fmap HsPar $ go pat
656 go1 (LazyPat pat) = go1 (unLoc pat)
657 go1 (BangPat pat) = go1 (unLoc pat)
658 go1 (PArrPat pats ptt) = do { exprs <- mapM go pats
659 ; return $ ExplicitPArr ptt exprs }
660 go1 (ListPat pats ptt reb) = do { exprs <- mapM go pats
661 ; return $ ExplicitList ptt (fmap snd reb) exprs }
662 go1 (TuplePat pats box _) = do { exprs <- mapM go pats
663 ; return $ ExplicitTuple
664 (map (noLoc . Present) exprs) box }
665 go1 (LitPat lit) = return $ HsLit lit
666 go1 (NPat (L _ n) mb_neg _ _)
667 | Just neg <- mb_neg = return $ unLoc $ nlHsSyntaxApps neg [noLoc (HsOverLit n)]
668 | otherwise = return $ HsOverLit n
669 go1 (ConPatOut{}) = panic "ConPatOut in output of renamer"
670 go1 (SigPatOut{}) = panic "SigPatOut in output of renamer"
671 go1 (CoPat{}) = panic "CoPat in output of renamer"
672 go1 p = Left (text "pattern" <+> quotes (ppr p) <+> text "is not invertible")
673
674 {- Note [Builder for a bidirectional pattern synonym]
675 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
676 For a bidirectional pattern synonym we need to produce an /expression/
677 that matches the supplied /pattern/, given values for the arguments
678 of the pattern synoymy. For example
679 pattern F x y = (Just x, [y])
680 The 'builder' for F looks like
681 $builderF x y = (Just x, [y])
682
683 We can't always do this:
684 * Some patterns aren't invertible; e.g. view patterns
685 pattern F x = (reverse -> x:_)
686
687 * The RHS pattern might bind more variables than the pattern
688 synonym, so again we can't invert it
689 pattern F x = (x,y)
690
691 * Ditto wildcards
692 pattern F x = (x,_)
693
694
695 Note [Redundant constraints for builder]
696 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
697 The builder can have redundant constraints, which are awkard to eliminate.
698 Consider
699 pattern P = Just 34
700 To match against this pattern we need (Eq a, Num a). But to build
701 (Just 34) we need only (Num a). Fortunately instTcSigFromId sets
702 sig_warn_redundant to False.
703
704 ************************************************************************
705 * *
706 Helper functions
707 * *
708 ************************************************************************
709
710 Note [As-patterns in pattern synonym definitions]
711 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
712 The rationale for rejecting as-patterns in pattern synonym definitions
713 is that an as-pattern would introduce nonindependent pattern synonym
714 arguments, e.g. given a pattern synonym like:
715
716 pattern K x y = x@(Just y)
717
718 one could write a nonsensical function like
719
720 f (K Nothing x) = ...
721
722 or
723 g (K (Just True) False) = ...
724
725 Note [Type signatures and the builder expression]
726 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
727 Consider
728 pattern L x = Left x :: Either [a] [b]
729
730 In tc{Infer/Check}PatSynDecl we will check that the pattern has the
731 specified type. We check the pattern *as a pattern*, so the type
732 signature is a pattern signature, and so brings 'a' and 'b' into
733 scope. But we don't have a way to bind 'a, b' in the LHS, as we do
734 'x', say. Nevertheless, the sigature may be useful to constrain
735 the type.
736
737 When making the binding for the *builder*, though, we don't want
738 $buildL x = Left x :: Either [a] [b]
739 because that wil either mean (forall a b. Either [a] [b]), or we'll
740 get a complaint that 'a' and 'b' are out of scope. (Actually the
741 latter; Trac #9867.) No, the job of the signature is done, so when
742 converting the pattern to an expression (for the builder RHS) we
743 simply discard the signature.
744
745 Note [Record PatSyn Desugaring]
746 -------------------------------
747 It is important that prov_theta comes before req_theta as this ordering is used
748 when desugaring record pattern synonym updates.
749
750 Any change to this ordering should make sure to change deSugar/DsExpr.hs if you
751 want to avoid difficult to decipher core lint errors!
752 -}
753
754 tcCheckPatSynPat :: LPat Name -> TcM ()
755 tcCheckPatSynPat = go
756 where
757 go :: LPat Name -> TcM ()
758 go = addLocM go1
759
760 go1 :: Pat Name -> TcM ()
761 go1 (ConPatIn _ info) = mapM_ go (hsConPatArgs info)
762 go1 VarPat{} = return ()
763 go1 WildPat{} = return ()
764 go1 p@(AsPat _ _) = asPatInPatSynErr p
765 go1 (LazyPat pat) = go pat
766 go1 (ParPat pat) = go pat
767 go1 (BangPat pat) = go pat
768 go1 (PArrPat pats _) = mapM_ go pats
769 go1 (ListPat pats _ _) = mapM_ go pats
770 go1 (TuplePat pats _ _) = mapM_ go pats
771 go1 LitPat{} = return ()
772 go1 NPat{} = return ()
773 go1 (SigPatIn pat _) = go pat
774 go1 (ViewPat _ pat _) = go pat
775 go1 p@SplicePat{} = thInPatSynErr p
776 go1 p@NPlusKPat{} = nPlusKPatInPatSynErr p
777 go1 ConPatOut{} = panic "ConPatOut in output of renamer"
778 go1 SigPatOut{} = panic "SigPatOut in output of renamer"
779 go1 CoPat{} = panic "CoPat in output of renamer"
780
781 asPatInPatSynErr :: (OutputableBndrId name) => Pat name -> TcM a
782 asPatInPatSynErr pat
783 = failWithTc $
784 hang (text "Pattern synonym definition cannot contain as-patterns (@):")
785 2 (ppr pat)
786
787 thInPatSynErr :: (OutputableBndrId name) => Pat name -> TcM a
788 thInPatSynErr pat
789 = failWithTc $
790 hang (text "Pattern synonym definition cannot contain Template Haskell:")
791 2 (ppr pat)
792
793 nPlusKPatInPatSynErr :: (OutputableBndrId name) => Pat name -> TcM a
794 nPlusKPatInPatSynErr pat
795 = failWithTc $
796 hang (text "Pattern synonym definition cannot contain n+k-pattern:")
797 2 (ppr pat)
798
799 nonBidirectionalErr :: Outputable name => name -> TcM a
800 nonBidirectionalErr name = failWithTc $
801 text "non-bidirectional pattern synonym"
802 <+> quotes (ppr name) <+> text "used in an expression"
803
804 -- Walk the whole pattern and for all ConPatOuts, collect the
805 -- existentially-bound type variables and evidence binding variables.
806 --
807 -- These are used in computing the type of a pattern synonym and also
808 -- in generating matcher functions, since success continuations need
809 -- to be passed these pattern-bound evidences.
810 tcCollectEx
811 :: LPat Id
812 -> ( ([Var], VarSet) -- Existentially-bound type variables as a
813 -- deterministically ordered list and a set.
814 -- See Note [Deterministic FV] in FV
815 , [EvVar]
816 )
817 tcCollectEx pat = let (fv, evs) = go pat in (fvVarListVarSet fv, evs)
818 where
819 go :: LPat Id -> (FV, [EvVar])
820 go = go1 . unLoc
821
822 go1 :: Pat Id -> (FV, [EvVar])
823 go1 (LazyPat p) = go p
824 go1 (AsPat _ p) = go p
825 go1 (ParPat p) = go p
826 go1 (BangPat p) = go p
827 go1 (ListPat ps _ _) = mergeMany . map go $ ps
828 go1 (TuplePat ps _ _) = mergeMany . map go $ ps
829 go1 (PArrPat ps _) = mergeMany . map go $ ps
830 go1 (ViewPat _ p _) = go p
831 go1 con@ConPatOut{} = merge (FV.mkFVs (pat_tvs con), pat_dicts con) $
832 goConDetails $ pat_args con
833 go1 (SigPatOut p _) = go p
834 go1 (CoPat _ p _) = go1 p
835 go1 (NPlusKPat n k _ geq subtract _)
836 = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract
837 go1 _ = empty
838
839 goConDetails :: HsConPatDetails Id -> (FV, [EvVar])
840 goConDetails (PrefixCon ps) = mergeMany . map go $ ps
841 goConDetails (InfixCon p1 p2) = go p1 `merge` go p2
842 goConDetails (RecCon HsRecFields{ rec_flds = flds })
843 = mergeMany . map goRecFd $ flds
844
845 goRecFd :: LHsRecField Id (LPat Id) -> (FV, [EvVar])
846 goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p
847
848 merge (vs1, evs1) (vs2, evs2) = (vs1 `unionFV` vs2, evs1 ++ evs2)
849 mergeMany = foldr merge empty
850 empty = (emptyFV, [])