0f64e9c2a5dcd9487b837fed4118ed048e56fdf3
[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 noExt (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 noExt $
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 = XValBindsLR (NValBinds 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 noExt (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 noExt (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 noExt (L loc x) y)
673 (HsVar noExt 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 noExt con 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 (SigPat _ 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 noExt (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 noExt) $ go pat
700 go1 (PArrPat _ pats) = do { exprs <- mapM go pats
701 ; return $ ExplicitPArr noExt exprs }
702 go1 p@(ListPat _ pats _ty reb)
703 | Nothing <- reb = do { exprs <- mapM go pats
704 ; return $ ExplicitList noExt Nothing exprs }
705 | otherwise = notInvertibleListPat p
706 go1 (TuplePat _ pats box) = do { exprs <- mapM go pats
707 ; return $ ExplicitTuple noExt
708 (map (noLoc . Present) exprs) box }
709 go1 (SumPat _ pat alt arity) = do { expr <- go1 (unLoc pat)
710 ; return $ ExplicitSum noExt alt arity
711 (noLoc expr)
712 }
713 go1 (LitPat _ lit) = return $ HsLit noExt lit
714 go1 (NPat _ (L _ n) mb_neg _)
715 | Just neg <- mb_neg = return $ unLoc $ nlHsSyntaxApps neg
716 [noLoc (HsOverLit noExt n)]
717 | otherwise = return $ HsOverLit noExt n
718 go1 (ConPatOut{}) = panic "ConPatOut in output of renamer"
719 go1 (CoPat{}) = panic "CoPat in output of renamer"
720 go1 (SplicePat _ (HsSpliced _ (HsSplicedPat pat)))
721 = go1 pat
722 go1 (SplicePat _ (HsSpliced{})) = panic "Invalid splice variety"
723
724 -- The following patterns are not invertible.
725 go1 p@(BangPat {}) = notInvertible p -- #14112
726 go1 p@(LazyPat {}) = notInvertible p
727 go1 p@(WildPat {}) = notInvertible p
728 go1 p@(AsPat {}) = notInvertible p
729 go1 p@(ViewPat {}) = notInvertible p
730 go1 p@(NPlusKPat {}) = notInvertible p
731 go1 p@(XPat {}) = notInvertible p
732 go1 p@(SplicePat _ (HsTypedSplice {})) = notInvertible p
733 go1 p@(SplicePat _ (HsUntypedSplice {})) = notInvertible p
734 go1 p@(SplicePat _ (HsQuasiQuote {})) = notInvertible p
735
736 notInvertible p = Left (not_invertible_msg p)
737
738 not_invertible_msg p
739 = text "Pattern" <+> quotes (ppr p) <+> text "is not invertible"
740 $+$ hang (text "Suggestion: instead use an explicitly bidirectional"
741 <+> text "pattern synonym, e.g.")
742 2 (hang (text "pattern" <+> pp_name <+> pp_args <+> larrow
743 <+> ppr pat <+> text "where")
744 2 (pp_name <+> pp_args <+> equals <+> text "..."))
745 where
746 pp_name = ppr name
747 pp_args = hsep (map ppr args)
748
749 -- We should really be able to invert list patterns, even when
750 -- rebindable syntax is on, but doing so involves a bit of
751 -- refactoring; see Trac #14380. Until then we reject with a
752 -- helpful error message.
753 notInvertibleListPat p
754 = Left (vcat [ not_invertible_msg p
755 , text "Reason: rebindable syntax is on."
756 , text "This is fixable: add use-case to Trac #14380" ])
757
758 {- Note [Builder for a bidirectional pattern synonym]
759 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
760 For a bidirectional pattern synonym we need to produce an /expression/
761 that matches the supplied /pattern/, given values for the arguments
762 of the pattern synoymy. For example
763 pattern F x y = (Just x, [y])
764 The 'builder' for F looks like
765 $builderF x y = (Just x, [y])
766
767 We can't always do this:
768 * Some patterns aren't invertible; e.g. view patterns
769 pattern F x = (reverse -> x:_)
770
771 * The RHS pattern might bind more variables than the pattern
772 synonym, so again we can't invert it
773 pattern F x = (x,y)
774
775 * Ditto wildcards
776 pattern F x = (x,_)
777
778
779 Note [Redundant constraints for builder]
780 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
781 The builder can have redundant constraints, which are awkard to eliminate.
782 Consider
783 pattern P = Just 34
784 To match against this pattern we need (Eq a, Num a). But to build
785 (Just 34) we need only (Num a). Fortunately instTcSigFromId sets
786 sig_warn_redundant to False.
787
788 ************************************************************************
789 * *
790 Helper functions
791 * *
792 ************************************************************************
793
794 Note [As-patterns in pattern synonym definitions]
795 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
796 The rationale for rejecting as-patterns in pattern synonym definitions
797 is that an as-pattern would introduce nonindependent pattern synonym
798 arguments, e.g. given a pattern synonym like:
799
800 pattern K x y = x@(Just y)
801
802 one could write a nonsensical function like
803
804 f (K Nothing x) = ...
805
806 or
807 g (K (Just True) False) = ...
808
809 Note [Type signatures and the builder expression]
810 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
811 Consider
812 pattern L x = Left x :: Either [a] [b]
813
814 In tc{Infer/Check}PatSynDecl we will check that the pattern has the
815 specified type. We check the pattern *as a pattern*, so the type
816 signature is a pattern signature, and so brings 'a' and 'b' into
817 scope. But we don't have a way to bind 'a, b' in the LHS, as we do
818 'x', say. Nevertheless, the sigature may be useful to constrain
819 the type.
820
821 When making the binding for the *builder*, though, we don't want
822 $buildL x = Left x :: Either [a] [b]
823 because that wil either mean (forall a b. Either [a] [b]), or we'll
824 get a complaint that 'a' and 'b' are out of scope. (Actually the
825 latter; Trac #9867.) No, the job of the signature is done, so when
826 converting the pattern to an expression (for the builder RHS) we
827 simply discard the signature.
828
829 Note [Record PatSyn Desugaring]
830 -------------------------------
831 It is important that prov_theta comes before req_theta as this ordering is used
832 when desugaring record pattern synonym updates.
833
834 Any change to this ordering should make sure to change deSugar/DsExpr.hs if you
835 want to avoid difficult to decipher core lint errors!
836 -}
837
838 tcCheckPatSynPat :: LPat GhcRn -> TcM ()
839 tcCheckPatSynPat = go
840 where
841 go :: LPat GhcRn -> TcM ()
842 go = addLocM go1
843
844 go1 :: Pat GhcRn -> TcM ()
845 -- See Note [Bad patterns]
846 go1 p@(AsPat _ _ _) = asPatInPatSynErr p
847 go1 p@NPlusKPat{} = nPlusKPatInPatSynErr p
848
849 go1 (ConPatIn _ info) = mapM_ go (hsConPatArgs info)
850 go1 VarPat{} = return ()
851 go1 WildPat{} = return ()
852 go1 (LazyPat _ pat) = go pat
853 go1 (ParPat _ pat) = go pat
854 go1 (BangPat _ pat) = go pat
855 go1 (PArrPat _ pats) = mapM_ go pats
856 go1 (ListPat _ pats _ _) = mapM_ go pats
857 go1 (TuplePat _ pats _) = mapM_ go pats
858 go1 (SumPat _ pat _ _) = go pat
859 go1 LitPat{} = return ()
860 go1 NPat{} = return ()
861 go1 (SigPat _ pat) = go pat
862 go1 (ViewPat _ _ pat) = go pat
863 go1 (SplicePat _ splice)
864 | HsSpliced mod_finalizers (HsSplicedPat pat) <- splice
865 = do addModFinalizersWithLclEnv mod_finalizers
866 go1 pat
867 | otherwise = panic "non-pattern from spliced thing"
868 go1 ConPatOut{} = panic "ConPatOut in output of renamer"
869 go1 CoPat{} = panic "CoPat in output of renamer"
870 go1 XPat{} = panic "XPat in output of renamer"
871
872 asPatInPatSynErr :: (SourceTextX (GhcPass p), OutputableBndrId (GhcPass p))
873 => Pat (GhcPass p) -> TcM a
874 asPatInPatSynErr pat
875 = failWithTc $
876 hang (text "Pattern synonym definition cannot contain as-patterns (@):")
877 2 (ppr pat)
878
879 nPlusKPatInPatSynErr :: (SourceTextX (GhcPass p), OutputableBndrId (GhcPass p))
880 => Pat (GhcPass p) -> TcM a
881 nPlusKPatInPatSynErr pat
882 = failWithTc $
883 hang (text "Pattern synonym definition cannot contain n+k-pattern:")
884 2 (ppr pat)
885
886 {- Note [Bad patterns]
887 ~~~~~~~~~~~~~~~~~~~~~~
888 We don't currently allow as-patterns or n+k patterns in a pattern synonym.
889 Reason: consider
890 pattern P x y = x@(Just y)
891
892 What would
893 f (P Nothing False) = e
894 mean? Presumably something like
895 f Nothing@(Just False) = e
896 But as-patterns don't allow a pattern before the @ sign! Perhaps they
897 should -- with p1@p2 meaning match both p1 and p2 -- but they don't
898 currently. Hence bannning them in pattern synonyms. Actually lifting
899 the restriction would be simple and well-defined. See Trac #9793.
900 -}
901
902
903 nonBidirectionalErr :: Outputable name => name -> TcM a
904 nonBidirectionalErr name = failWithTc $
905 text "non-bidirectional pattern synonym"
906 <+> quotes (ppr name) <+> text "used in an expression"
907
908 -- Walk the whole pattern and for all ConPatOuts, collect the
909 -- existentially-bound type variables and evidence binding variables.
910 --
911 -- These are used in computing the type of a pattern synonym and also
912 -- in generating matcher functions, since success continuations need
913 -- to be passed these pattern-bound evidences.
914 tcCollectEx
915 :: LPat GhcTc
916 -> ( [TyVar] -- Existentially-bound type variables
917 -- in correctly-scoped order; e.g. [ k:*, x:k ]
918 , [EvVar] ) -- and evidence variables
919
920 tcCollectEx pat = go pat
921 where
922 go :: LPat GhcTc -> ([TyVar], [EvVar])
923 go = go1 . unLoc
924
925 go1 :: Pat GhcTc -> ([TyVar], [EvVar])
926 go1 (LazyPat _ p) = go p
927 go1 (AsPat _ _ p) = go p
928 go1 (ParPat _ p) = go p
929 go1 (BangPat _ p) = go p
930 go1 (ListPat _ ps _ _) = mergeMany . map go $ ps
931 go1 (TuplePat _ ps _) = mergeMany . map go $ ps
932 go1 (SumPat _ p _ _) = go p
933 go1 (PArrPat _ ps) = mergeMany . map go $ ps
934 go1 (ViewPat _ _ p) = go p
935 go1 con@ConPatOut{} = merge (pat_tvs con, pat_dicts con) $
936 goConDetails $ pat_args con
937 go1 (SigPat _ p) = go p
938 go1 (CoPat _ _ p _) = go1 p
939 go1 (NPlusKPat _ n k _ geq subtract)
940 = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract
941 go1 _ = empty
942
943 goConDetails :: HsConPatDetails GhcTc -> ([TyVar], [EvVar])
944 goConDetails (PrefixCon ps) = mergeMany . map go $ ps
945 goConDetails (InfixCon p1 p2) = go p1 `merge` go p2
946 goConDetails (RecCon HsRecFields{ rec_flds = flds })
947 = mergeMany . map goRecFd $ flds
948
949 goRecFd :: LHsRecField GhcTc (LPat GhcTc) -> ([TyVar], [EvVar])
950 goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p
951
952 merge (vs1, evs1) (vs2, evs2) = (vs1 ++ vs2, evs1 ++ evs2)
953 mergeMany = foldr merge empty
954 empty = ([], [])