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