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