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