87637748758d8d1505b1fc032373911e68bac667
[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
10 module TcPatSyn ( tcPatSynSig, tcInferPatSynDecl, tcCheckPatSynDecl
11 , tcPatSynBuilderBind, tcPatSynBuilderOcc, nonBidirectionalErr
12 ) where
13
14 import HsSyn
15 import TcPat
16 import TcHsType( tcImplicitTKBndrs, tcExplicitTKBndrs
17 , tcHsContext, tcHsLiftedType, tcHsOpenType, kindGeneralize )
18 import Type( binderVar, mkNamedBinders, binderVisibility
19 , tidyTyCoVarBndrs, tidyTypes, tidyType )
20 import TcRnMonad
21 import TcEnv
22 import TcMType
23 import TysPrim
24 import TysWiredIn ( runtimeRepTy )
25 import Name
26 import SrcLoc
27 import PatSyn
28 import NameSet
29 import Panic
30 import Outputable
31 import FastString
32 import Var
33 import VarEnv( emptyTidyEnv )
34 import Id
35 import IdInfo( RecSelParent(..))
36 import TcBinds
37 import BasicTypes
38 import TcSimplify
39 import TcUnify
40 import TcType
41 import TcEvidence
42 import BuildTyCl
43 import VarSet
44 import MkId
45 import TcTyDecls
46 import ConLike
47 import FieldLabel
48 import Bag
49 import Util
50 import ErrUtils
51 import FV
52 import Control.Monad ( unless, zipWithM )
53 import Data.List( partition )
54
55 #include "HsVersions.h"
56
57 {- *********************************************************************
58 * *
59 Type checking a pattern synonym signature
60 * *
61 ************************************************************************
62
63 Note [Pattern synonym signatures]
64 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
65 Pattern synonym signatures are surprisingly tricky (see Trac #11224 for example).
66 In general they look like this:
67
68 pattern P :: forall univ_tvs. req
69 => forall ex_tvs. prov
70 => arg1 -> .. -> argn -> body_ty
71
72 For parsing and renaming we treat the signature as an ordinary LHsSigType.
73
74 Once we get to type checking, we decompose it into its parts, in tcPatSynSig.
75
76 * Note that 'forall univ_tvs' and 'req =>'
77 and 'forall ex_tvs' and 'prov =>'
78 are all optional. We gather the pieces at the the top of tcPatSynSig
79
80 * Initially the implicitly-bound tyvars (added by the renamer) include both
81 universal and existential vars.
82
83 * After we kind-check the pieces and convert to Types, we do kind generalisation.
84
85 * Note [Splitting the implicit tyvars in a pattern synonym]
86 Now the tricky bit: we must split
87 the implicitly-bound variables, and
88 the kind-generalised variables
89 into universal and existential. We do so as follows:
90
91 Note [The pattern-synonym signature splitting rule]
92 the universals are the ones mentioned in
93 - univ_tvs (and the kinds thereof)
94 - req
95 - body_ty
96 the existentials are the rest
97
98 * Moreover see Note
99 -}
100
101 tcPatSynSig :: Name -> LHsSigType Name -> TcM TcPatSynInfo
102 tcPatSynSig name sig_ty
103 | HsIB { hsib_vars = implicit_hs_tvs
104 , hsib_body = hs_ty } <- sig_ty
105 , (univ_hs_tvs, hs_req, hs_ty1) <- splitLHsSigmaTy hs_ty
106 , (ex_hs_tvs, hs_prov, hs_ty2) <- splitLHsSigmaTy hs_ty1
107 , (hs_arg_tys, hs_body_ty) <- splitHsFunType hs_ty2
108 = do { (implicit_tvs, (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty))
109 <- solveEqualities $
110 tcImplicitTKBndrs implicit_hs_tvs $
111 tcExplicitTKBndrs univ_hs_tvs $ \ univ_tvs ->
112 tcExplicitTKBndrs ex_hs_tvs $ \ ex_tvs ->
113 do { req <- tcHsContext hs_req
114 ; prov <- tcHsContext hs_prov
115 ; arg_tys <- mapM tcHsOpenType (hs_arg_tys :: [LHsType Name])
116 -- A (literal) pattern can be unlifted;
117 -- -- e.g. pattern Zero <- 0# (Trac #12094)
118 ; body_ty <- tcHsOpenType hs_body_ty
119 ; let bound_tvs
120 = unionVarSets [ allBoundVariabless req
121 , allBoundVariabless prov
122 , allBoundVariabless (body_ty : arg_tys)
123 ]
124 ; return ( (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty)
125 , bound_tvs) }
126
127 -- Kind generalisation
128 ; kvs <- kindGeneralize $
129 mkSpecForAllTys (implicit_tvs ++ univ_tvs) $
130 mkFunTys req $
131 mkSpecForAllTys ex_tvs $
132 mkFunTys prov $
133 mkFunTys arg_tys $
134 body_ty
135
136 -- These are /signatures/ so we zonk to squeeze out any kind
137 -- unification variables. Do this after quantifyTyVars which may
138 -- default kind variables to *.
139 -- ToDo: checkValidType?
140 ; traceTc "about zonk" empty
141 ; implicit_tvs <- mapM zonkTcTyCoVarBndr implicit_tvs
142 ; univ_tvs <- mapM zonkTcTyCoVarBndr univ_tvs
143 ; ex_tvs <- mapM zonkTcTyCoVarBndr ex_tvs
144 ; req <- zonkTcTypes req
145 ; prov <- zonkTcTypes prov
146 ; arg_tys <- zonkTcTypes arg_tys
147 ; body_ty <- zonkTcType body_ty
148
149 -- Complain about: pattern P :: () => forall x. x -> P x
150 -- The renamer thought it was fine, but the existential 'x'
151 -- should not appear in the result type
152 ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType body_ty) ex_tvs
153 ; unless (null bad_tvs) $ addErr $
154 hang (text "The result type" <+> quotes (ppr body_ty))
155 2 (text "mentions existential type variable" <> plural bad_tvs
156 <+> pprQuotedList bad_tvs)
157
158 -- Split [Splitting the implicit tyvars in a pattern synonym]
159 ; let univ_fvs = closeOverKinds $
160 (tyCoVarsOfTypes (body_ty : req) `extendVarSetList` univ_tvs)
161 (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) .
162 binderVar "tcPatSynSig") $
163 mkNamedBinders Invisible kvs ++
164 mkNamedBinders Specified implicit_tvs
165 ; traceTc "tcTySig }" $
166 vcat [ text "implicit_tvs" <+> ppr_tvs implicit_tvs
167 , text "kvs" <+> ppr_tvs kvs
168 , text "extra_univ" <+> ppr extra_univ
169 , text "univ_tvs" <+> ppr_tvs univ_tvs
170 , text "req" <+> ppr req
171 , text "extra_ex" <+> ppr extra_ex
172 , text "ex_tvs" <+> ppr_tvs ex_tvs
173 , text "prov" <+> ppr prov
174 , text "arg_tys" <+> ppr arg_tys
175 , text "body_ty" <+> ppr body_ty ]
176 ; return (TPSI { patsig_name = name
177 , patsig_univ_bndrs = extra_univ ++
178 mkNamedBinders Specified univ_tvs
179 , patsig_req = req
180 , patsig_ex_bndrs = extra_ex ++
181 mkNamedBinders Specified ex_tvs
182 , patsig_prov = prov
183 , patsig_arg_tys = arg_tys
184 , patsig_body_ty = body_ty }) }
185 where
186
187 ppr_tvs :: [TyVar] -> SDoc
188 ppr_tvs tvs = braces (vcat [ ppr tv <+> dcolon <+> ppr (tyVarKind tv)
189 | tv <- tvs])
190
191
192 {-
193 ************************************************************************
194 * *
195 Type checking a pattern synonym
196 * *
197 ************************************************************************
198 -}
199
200 tcInferPatSynDecl :: PatSynBind Name Name
201 -> TcM (LHsBinds Id, TcGblEnv)
202 tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
203 psb_def = lpat, psb_dir = dir }
204 = addPatSynCtxt lname $
205 do { traceTc "tcInferPatSynDecl {" $ ppr name
206 ; tcCheckPatSynPat lpat
207
208 ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
209 ; (tclvl, wanted, ((lpat', args), pat_ty))
210 <- pushLevelAndCaptureConstraints $
211 do { pat_ty <- newOpenInferExpType
212 ; stuff <- tcPat PatSyn lpat pat_ty $
213 mapM tcLookupId arg_names
214 ; pat_ty <- readExpType pat_ty
215 ; return (stuff, pat_ty) }
216
217 ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
218
219 ; (qtvs, req_dicts, ev_binds) <- simplifyInfer tclvl False [] named_taus wanted
220
221 ; let ((ex_tvs, ex_vars), prov_dicts) = tcCollectEx lpat'
222 univ_tvs = filter (not . (`elemVarSet` ex_vars)) qtvs
223 prov_theta = map evVarPred prov_dicts
224 req_theta = map evVarPred req_dicts
225
226 ; traceTc "tcInferPatSynDecl }" $ ppr name
227 ; tc_patsyn_finish lname dir is_infix lpat'
228 (univ_tvs, mkNamedBinders Invisible univ_tvs
229 , req_theta, ev_binds, req_dicts)
230 (ex_tvs, mkNamedBinders Invisible ex_tvs
231 , mkTyVarTys ex_tvs, prov_theta, map EvId prov_dicts)
232 (map nlHsVar args, map idType args)
233 pat_ty rec_fields }
234
235
236 tcCheckPatSynDecl :: PatSynBind Name Name
237 -> TcPatSynInfo
238 -> TcM (LHsBinds Id, TcGblEnv)
239 tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
240 , psb_def = lpat, psb_dir = dir }
241 TPSI{ patsig_univ_bndrs = univ_bndrs, patsig_prov = prov_theta
242 , patsig_ex_bndrs = ex_bndrs, patsig_req = req_theta
243 , patsig_arg_tys = arg_tys, patsig_body_ty = pat_ty }
244 = addPatSynCtxt lname $
245 do { let decl_arity = length arg_names
246 ty_arity = length arg_tys
247 (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
248
249 univ_tvs = map (binderVar "tcCheckPatSynDecl 1") univ_bndrs
250 ex_tvs = map (binderVar "tcCheckPatSynDecl 2") ex_bndrs
251
252 ; traceTc "tcCheckPatSynDecl" $
253 vcat [ ppr univ_bndrs, ppr req_theta, ppr ex_bndrs
254 , ppr prov_theta, ppr arg_tys, ppr pat_ty ]
255
256 ; checkTc (decl_arity == ty_arity)
257 (wrongNumberOfParmsErr name decl_arity ty_arity)
258
259 ; tcCheckPatSynPat lpat
260
261 -- Right! Let's check the pattern against the signature
262 -- See Note [Checking against a pattern signature]
263 ; req_dicts <- newEvVars req_theta
264 ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
265 ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
266 pushLevelAndCaptureConstraints $
267 tcExtendTyVarEnv univ_tvs $
268 tcPat PatSyn lpat (mkCheckExpType pat_ty) $
269 do { (subst, ex_tvs') <- if isUnidirectional dir
270 then newMetaTyVars ex_tvs
271 else newMetaSigTyVars ex_tvs
272 -- See the "Existential type variables" part of
273 -- Note [Checking against a pattern signature]
274 ; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs])
275 ; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs'])
276 ; let prov_theta' = substTheta (extendTCvInScopeList subst univ_tvs) prov_theta
277 -- Add univ_tvs to the in_scope set to
278 -- satisfy the substition invariant. There's no need to
279 -- add 'ex_tvs' as they are already in the domain of the
280 -- substitution.
281 -- See also Note [The substitution invariant] in TyCoRep.
282 ; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta'
283 ; args' <- zipWithM (tc_arg subst) arg_names arg_tys
284 ; return (ex_tvs', prov_dicts, args') }
285
286 ; let skol_info = SigSkol (PatSynCtxt name) (mkPhiTy req_theta pat_ty)
287 -- The type here is a bit bogus, but we do not print
288 -- the type for PatSynCtxt, so it doesn't matter
289 -- See TcRnTypes Note [Skolem info for pattern synonyms]
290 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted
291
292 -- Solve the constraints now, because we are about to make a PatSyn,
293 -- which should not contain unification variables and the like (Trac #10997)
294 -- Since all the inputs are implications the returned bindings will be empty
295 ; _ <- simplifyTop (mkImplicWC implics)
296
297 -- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct
298 -- Otherwise we may get a type error when typechecking the builder,
299 -- when that should be impossible
300
301 ; traceTc "tcCheckPatSynDecl }" $ ppr name
302 ; tc_patsyn_finish lname dir is_infix lpat'
303 (univ_tvs, univ_bndrs, req_theta, ev_binds, req_dicts)
304 (ex_tvs, ex_bndrs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
305 (args', arg_tys)
306 pat_ty rec_fields }
307 where
308 tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr TcId)
309 tc_arg subst arg_name arg_ty
310 = do { -- Look up the variable actually bound by lpat
311 -- and check that it has the expected type
312 arg_id <- tcLookupId arg_name
313 ; coi <- unifyType (Just arg_id)
314 (idType arg_id)
315 (substTyUnchecked subst arg_ty)
316 ; return (mkLHsWrapCo coi $ nlHsVar arg_id) }
317
318 {- Note [Checking against a pattern signature]
319 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
320 When checking the actual supplied pattern against the pattern synonym
321 signature, we need to be quite careful.
322
323 ----- Provided constraints
324 Example
325
326 data T a where
327 MkT :: Ord a => a -> T a
328
329 pattern P :: () => Eq a => a -> [T a]
330 pattern P x = [MkT x]
331
332 We must check that the (Eq a) that P claims to bind (and to
333 make available to matches against P), is derivable from the
334 actual pattern. For example:
335 f (P (x::a)) = ...here (Eq a) should be available...
336 And yes, (Eq a) is derivable from the (Ord a) bound by P's rhs.
337
338 ----- Existential type variables
339 Unusually, we instantiate the existential tyvars of the pattern with
340 *meta* type variables. For example
341
342 data S where
343 MkS :: Eq a => [a] -> S
344
345 pattern P :: () => Eq x => x -> S
346 pattern P x <- MkS x
347
348 The pattern synonym conceals from its client the fact that MkS has a
349 list inside it. The client just thinks it's a type 'x'. So we must
350 unify x := [a] during type checking, and then use the instantiating type
351 [a] (called ex_tys) when building the matcher. In this case we'll get
352
353 $mP :: S -> (forall x. Ex x => x -> r) -> r -> r
354 $mP x k = case x of
355 MkS a (d:Eq a) (ys:[a]) -> let dl :: Eq [a]
356 dl = $dfunEqList d
357 in k [a] dl ys
358
359 This "concealing" story works for /uni-directional/ pattern synonmys,
360 but obviously not for bidirectional ones. So in the bidirectional case
361 we use SigTv, rather than a generic TauTv, meta-tyvar so that. And
362 we should really check that those SigTvs don't get unified with each
363 other.
364
365 -}
366
367 collectPatSynArgInfo :: HsPatSynDetails (Located Name) -> ([Name], [Name], Bool)
368 collectPatSynArgInfo details =
369 case details of
370 PrefixPatSyn names -> (map unLoc names, [], False)
371 InfixPatSyn name1 name2 -> (map unLoc [name1, name2], [], True)
372 RecordPatSyn names ->
373 let (vars, sels) = unzip (map splitRecordPatSyn names)
374 in (vars, sels, False)
375
376 where
377 splitRecordPatSyn :: RecordPatSynField (Located Name) -> (Name, Name)
378 splitRecordPatSyn (RecordPatSynField { recordPatSynPatVar = L _ patVar
379 , recordPatSynSelectorId = L _ selId })
380 = (patVar, selId)
381
382 addPatSynCtxt :: Located Name -> TcM a -> TcM a
383 addPatSynCtxt (L loc name) thing_inside
384 = setSrcSpan loc $
385 addErrCtxt (text "In the declaration for pattern synonym"
386 <+> quotes (ppr name)) $
387 thing_inside
388
389 wrongNumberOfParmsErr :: Name -> Arity -> Arity -> SDoc
390 wrongNumberOfParmsErr name decl_arity ty_arity
391 = hang (text "Pattern synonym" <+> quotes (ppr name) <+> ptext (sLit "has")
392 <+> speakNOf decl_arity (text "argument"))
393 2 (text "but its type signature has" <+> speakN ty_arity)
394
395 -------------------------
396 -- Shared by both tcInferPatSyn and tcCheckPatSyn
397 tc_patsyn_finish :: Located Name -- ^ PatSyn Name
398 -> HsPatSynDir Name -- ^ PatSyn type (Uni/Bidir/ExplicitBidir)
399 -> Bool -- ^ Whether infix
400 -> LPat Id -- ^ Pattern of the PatSyn
401 -> ([TcTyVar], [TcTyBinder], [PredType], TcEvBinds, [EvVar])
402 -> ([TcTyVar], [TcTyBinder], [TcType], [PredType], [EvTerm])
403 -> ([LHsExpr TcId], [TcType]) -- ^ Pattern arguments and types
404 -> TcType -- ^ Pattern type
405 -> [Name] -- ^ Selector names
406 -- ^ Whether fields, empty if not record PatSyn
407 -> TcM (LHsBinds Id, TcGblEnv)
408 tc_patsyn_finish lname dir is_infix lpat'
409 (univ_tvs, univ_bndrs, req_theta, req_ev_binds, req_dicts)
410 (ex_tvs, ex_bndrs, ex_tys, prov_theta, prov_dicts)
411 (args, arg_tys)
412 pat_ty field_labels
413 = do { -- Zonk everything. We are about to build a final PatSyn
414 -- so there had better be no unification variables in there
415 univ_tvs' <- mapMaybeM (zonkQuantifiedTyVar False) univ_tvs
416 ; ex_tvs' <- mapMaybeM (zonkQuantifiedTyVar False) ex_tvs
417 -- ToDo: The False means that we behave here as if
418 -- -XPolyKinds was always on, which isn't right.
419 ; prov_theta' <- zonkTcTypes prov_theta
420 ; req_theta' <- zonkTcTypes req_theta
421 ; pat_ty' <- zonkTcType pat_ty
422 ; arg_tys' <- zonkTcTypes arg_tys
423
424 ; let (env1, univ_tvs) = tidyTyCoVarBndrs emptyTidyEnv univ_tvs'
425 (env2, ex_tvs) = tidyTyCoVarBndrs env1 ex_tvs'
426 req_theta = tidyTypes env2 req_theta'
427 prov_theta = tidyTypes env2 prov_theta'
428 arg_tys = tidyTypes env2 arg_tys'
429 pat_ty = tidyType env2 pat_ty'
430
431 -- We need to update the univ and ex binders after zonking.
432 -- But zonking may have defaulted some erstwhile binders,
433 -- so we need to make sure the tyvars and tybinders remain
434 -- lined up
435 ; let update_binders :: [TyVar] -> [TcTyBinder] -> [TyBinder]
436 update_binders [] _ = []
437 update_binders all_tvs@(tv:tvs) (bndr:bndrs)
438 | tv == bndr_var
439 = mkNamedBinder (binderVisibility bndr) tv : update_binders tvs bndrs
440 | otherwise
441 = update_binders all_tvs bndrs
442 where
443 bndr_var = binderVar "tc_patsyn_finish" bndr
444 update_binders tvs _ = pprPanic "tc_patsyn_finish" (ppr lname $$ ppr tvs)
445
446 univ_bndrs' = update_binders univ_tvs univ_bndrs
447 ex_bndrs' = update_binders ex_tvs ex_bndrs
448
449 ; traceTc "tc_patsyn_finish {" $
450 ppr (unLoc lname) $$ ppr (unLoc lpat') $$
451 ppr (univ_tvs, univ_bndrs', req_theta, req_ev_binds, req_dicts) $$
452 ppr (ex_tvs, ex_bndrs', prov_theta, prov_dicts) $$
453 ppr args $$
454 ppr arg_tys $$
455 ppr pat_ty
456
457 -- Make the 'matcher'
458 ; (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat'
459 (univ_tvs, req_theta, req_ev_binds, req_dicts)
460 (ex_tvs, ex_tys, prov_theta, prov_dicts)
461 (args, arg_tys)
462 pat_ty
463
464
465 -- Make the 'builder'
466 ; builder_id <- mkPatSynBuilderId dir lname
467 univ_bndrs' req_theta
468 ex_bndrs' prov_theta
469 arg_tys pat_ty
470
471 -- TODO: Make this have the proper information
472 ; let mkFieldLabel name = FieldLabel { flLabel = occNameFS (nameOccName name)
473 , flIsOverloaded = False
474 , flSelector = name }
475 field_labels' = map mkFieldLabel field_labels
476
477
478 -- Make the PatSyn itself
479 ; let patSyn = mkPatSyn (unLoc lname) is_infix
480 (univ_tvs, univ_bndrs', req_theta)
481 (ex_tvs, ex_bndrs', prov_theta)
482 arg_tys
483 pat_ty
484 matcher_id builder_id
485 field_labels'
486
487 -- Selectors
488 ; let rn_rec_sel_binds = mkPatSynRecSelBinds patSyn (patSynFieldLabels patSyn)
489 tything = AConLike (PatSynCon patSyn)
490 ; tcg_env <- tcExtendGlobalEnv [tything] $
491 tcRecSelBinds rn_rec_sel_binds
492
493 ; traceTc "tc_patsyn_finish }" empty
494 ; return (matcher_bind, tcg_env) }
495
496 {-
497 ************************************************************************
498 * *
499 Constructing the "matcher" Id and its binding
500 * *
501 ************************************************************************
502 -}
503
504 tcPatSynMatcher :: Located Name
505 -> LPat Id
506 -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
507 -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
508 -> ([LHsExpr TcId], [TcType])
509 -> TcType
510 -> TcM ((Id, Bool), LHsBinds Id)
511 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
512 tcPatSynMatcher (L loc name) lpat
513 (univ_tvs, req_theta, req_ev_binds, req_dicts)
514 (ex_tvs, ex_tys, prov_theta, prov_dicts)
515 (args, arg_tys) pat_ty
516 = do { rr_uniq <- newUnique
517 ; tv_uniq <- newUnique
518 ; let rr_name = mkInternalName rr_uniq (mkTyVarOcc "rep") loc
519 tv_name = mkInternalName tv_uniq (mkTyVarOcc "r") loc
520 rr_tv = mkTcTyVar rr_name runtimeRepTy (SkolemTv False)
521 rr = mkTyVarTy rr_tv
522 res_tv = mkTcTyVar tv_name (tYPE rr) (SkolemTv False)
523 is_unlifted = null args && null prov_dicts
524 res_ty = mkTyVarTy res_tv
525 (cont_args, cont_arg_tys)
526 | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
527 | otherwise = (args, arg_tys)
528 cont_ty = mkInvSigmaTy ex_tvs prov_theta $
529 mkFunTys cont_arg_tys res_ty
530
531 fail_ty = mkFunTy voidPrimTy res_ty
532
533 ; matcher_name <- newImplicitBinder name mkMatcherOcc
534 ; scrutinee <- newSysLocalId (fsLit "scrut") pat_ty
535 ; cont <- newSysLocalId (fsLit "cont") cont_ty
536 ; fail <- newSysLocalId (fsLit "fail") fail_ty
537
538 ; let matcher_tau = mkFunTys [pat_ty, cont_ty, fail_ty] res_ty
539 matcher_sigma = mkInvSigmaTy (rr_tv:res_tv:univ_tvs) req_theta matcher_tau
540 matcher_id = mkExportedVanillaId matcher_name matcher_sigma
541 -- See Note [Exported LocalIds] in Id
542
543 inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys
544 cont' = foldl nlHsApp (mkLHsWrap inst_wrap (nlHsVar cont)) cont_args
545
546 fail' = nlHsApps fail [nlHsVar voidPrimId]
547
548 args = map nlVarPat [scrutinee, cont, fail]
549 lwpat = noLoc $ WildPat pat_ty
550 cases = if isIrrefutableHsPat lpat
551 then [mkSimpleHsAlt lpat cont']
552 else [mkSimpleHsAlt lpat cont',
553 mkSimpleHsAlt lwpat fail']
554 body = mkLHsWrap (mkWpLet req_ev_binds) $
555 L (getLoc lpat) $
556 HsCase (nlHsVar scrutinee) $
557 MG{ mg_alts = L (getLoc lpat) cases
558 , mg_arg_tys = [pat_ty]
559 , mg_res_ty = res_ty
560 , mg_origin = Generated
561 }
562 body' = noLoc $
563 HsLam $
564 MG{ mg_alts = noLoc [mkSimpleMatch args body]
565 , mg_arg_tys = [pat_ty, cont_ty, res_ty]
566 , mg_res_ty = res_ty
567 , mg_origin = Generated
568 }
569 match = mkMatch [] (mkHsLams (rr_tv:res_tv:univ_tvs) req_dicts body')
570 (noLoc EmptyLocalBinds)
571 mg = MG{ mg_alts = L (getLoc match) [match]
572 , mg_arg_tys = []
573 , mg_res_ty = res_ty
574 , mg_origin = Generated
575 }
576
577 ; let bind = FunBind{ fun_id = L loc matcher_id
578 , fun_matches = mg
579 , fun_co_fn = idHsWrapper
580 , bind_fvs = emptyNameSet
581 , fun_tick = [] }
582 matcher_bind = unitBag (noLoc bind)
583
584 ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
585 ; traceTc "tcPatSynMatcher" (ppr matcher_bind)
586
587 ; return ((matcher_id, is_unlifted), matcher_bind) }
588
589 mkPatSynRecSelBinds :: PatSyn
590 -> [FieldLabel] -- ^ Visible field labels
591 -> HsValBinds Name
592 mkPatSynRecSelBinds ps fields
593 = ValBindsOut selector_binds sigs
594 where
595 (sigs, selector_binds) = unzip (map mkRecSel fields)
596 mkRecSel fld_lbl = mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl
597
598 isUnidirectional :: HsPatSynDir a -> Bool
599 isUnidirectional Unidirectional = True
600 isUnidirectional ImplicitBidirectional = False
601 isUnidirectional ExplicitBidirectional{} = False
602
603 {-
604 ************************************************************************
605 * *
606 Constructing the "builder" Id
607 * *
608 ************************************************************************
609 -}
610
611 mkPatSynBuilderId :: HsPatSynDir a -> Located Name
612 -> [TyBinder] -> ThetaType
613 -> [TyBinder] -> ThetaType
614 -> [Type] -> Type
615 -> TcM (Maybe (Id, Bool))
616 mkPatSynBuilderId dir (L _ name)
617 univ_bndrs req_theta ex_bndrs prov_theta
618 arg_tys pat_ty
619 | isUnidirectional dir
620 = return Nothing
621 | otherwise
622 = do { builder_name <- newImplicitBinder name mkBuilderOcc
623 ; let theta = req_theta ++ prov_theta
624 need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
625 builder_sigma = add_void need_dummy_arg $
626 mkForAllTys univ_bndrs $
627 mkForAllTys ex_bndrs $
628 mkFunTys theta $
629 mkFunTys arg_tys $
630 pat_ty
631 builder_id = mkExportedVanillaId builder_name builder_sigma
632 -- See Note [Exported LocalIds] in Id
633
634 ; return (Just (builder_id, need_dummy_arg)) }
635 where
636
637 tcPatSynBuilderBind :: TcSigFun
638 -> PatSynBind Name Name
639 -> TcM (LHsBinds Id)
640 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
641 tcPatSynBuilderBind sig_fun PSB{ psb_id = L loc name, psb_def = lpat
642 , psb_dir = dir, psb_args = details }
643 | isUnidirectional dir
644 = return emptyBag
645
646 | Left why <- mb_match_group -- Can't invert the pattern
647 = setSrcSpan (getLoc lpat) $ failWithTc $
648 vcat [ hang (text "Invalid right-hand side of bidirectional pattern synonym"
649 <+> quotes (ppr name) <> colon)
650 2 why
651 , text "RHS pattern:" <+> ppr lpat ]
652
653 | Right match_group <- mb_match_group -- Bidirectional
654 = do { patsyn <- tcLookupPatSyn name
655 ; traceTc "tcPatSynBuilderBind {" $ ppr patsyn
656 ; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn
657 -- Bidirectional, so patSynBuilder returns Just
658
659 match_group' | need_dummy_arg = add_dummy_arg match_group
660 | otherwise = match_group
661
662 bind = FunBind { fun_id = L loc (idName builder_id)
663 , fun_matches = match_group'
664 , fun_co_fn = idHsWrapper
665 , bind_fvs = placeHolderNamesTc
666 , fun_tick = [] }
667
668 ; sig <- get_builder_sig sig_fun name builder_id need_dummy_arg
669
670 ; (builder_binds, _) <- tcPolyCheck NonRecursive emptyPragEnv sig (noLoc bind)
671 ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
672 ; return builder_binds }
673
674 | otherwise = panic "tcPatSynBuilderBind" -- Both cases dealt with
675 where
676 mb_match_group
677 = case dir of
678 ExplicitBidirectional explicit_mg -> Right explicit_mg
679 ImplicitBidirectional -> fmap mk_mg (tcPatToExpr args lpat)
680 Unidirectional -> panic "tcPatSynBuilderBind"
681
682 mk_mg :: LHsExpr Name -> MatchGroup Name (LHsExpr Name)
683 mk_mg body = mkMatchGroupName Generated [builder_match]
684 where
685 builder_args = [L loc (VarPat (L loc n)) | L loc n <- args]
686 builder_match = mkMatch builder_args body (noLoc EmptyLocalBinds)
687
688 args = case details of
689 PrefixPatSyn args -> args
690 InfixPatSyn arg1 arg2 -> [arg1, arg2]
691 RecordPatSyn args -> map recordPatSynPatVar args
692
693 add_dummy_arg :: MatchGroup Name (LHsExpr Name)
694 -> MatchGroup Name (LHsExpr Name)
695 add_dummy_arg mg@(MG { mg_alts = L l [L loc match@(Match { m_pats = pats })] })
696 = mg { mg_alts = L l [L loc (match { m_pats = nlWildPatName : pats })] }
697 add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
698 pprMatches (PatSyn :: HsMatchContext Name) other_mg
699
700 get_builder_sig :: TcSigFun -> Name -> Id -> Bool -> TcM TcIdSigInfo
701 get_builder_sig sig_fun name builder_id need_dummy_arg
702 | Just (TcPatSynSig sig) <- sig_fun name
703 , TPSI { patsig_univ_bndrs = univ_bndrs
704 , patsig_req = req
705 , patsig_ex_bndrs = ex_bndrs
706 , patsig_prov = prov
707 , patsig_arg_tys = arg_tys
708 , patsig_body_ty = body_ty } <- sig
709 = -- Constuct a TcIdSigInfo from a TcPatSynInfo
710 -- This does unfortunately mean that we have to know how to
711 -- make the builder Id's type from the TcPatSynInfo, which
712 -- duplicates the construction in mkPatSynBuilderId
713 -- But we really want to use the scoped type variables from
714 -- the actual sigature, so this is really the Right Thing
715 return (TISI { sig_bndr = CompleteSig builder_id
716 , sig_skols = [ (tyVarName tv, tv)
717 | bndr <- univ_bndrs ++ ex_bndrs
718 , let tv = binderVar "get_builder_sig" bndr ]
719 , sig_theta = req ++ prov
720 , sig_tau = add_void need_dummy_arg $
721 mkFunTys arg_tys body_ty
722 , sig_ctxt = PatSynCtxt name
723 , sig_loc = getSrcSpan name })
724 | otherwise
725 = -- No signature, so fake up a TcIdSigInfo from the builder Id
726 instTcTySigFromId builder_id
727 -- See Note [Redundant constraints for builder]
728
729 tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr TcId, TcSigmaType)
730 -- monadic only for failure
731 tcPatSynBuilderOcc ps
732 | Just (builder_id, add_void_arg) <- builder
733 , let builder_expr = HsVar (noLoc builder_id)
734 builder_ty = idType builder_id
735 = return $
736 if add_void_arg
737 then ( HsApp (noLoc $ builder_expr) (nlHsVar voidPrimId)
738 , tcFunResultTy builder_ty )
739 else (builder_expr, builder_ty)
740
741 | otherwise -- Unidirectional
742 = nonBidirectionalErr name
743 where
744 name = patSynName ps
745 builder = patSynBuilder ps
746
747 add_void :: Bool -> Type -> Type
748 add_void need_dummy_arg ty
749 | need_dummy_arg = mkFunTy voidPrimTy ty
750 | otherwise = ty
751
752 tcPatToExpr :: [Located Name] -> LPat Name -> Either MsgDoc (LHsExpr Name)
753 -- Given a /pattern/, return an /expression/ that builds a value
754 -- that matches the pattern. E.g. if the pattern is (Just [x]),
755 -- the expression is (Just [x]). They look the same, but the
756 -- input uses constructors from HsPat and the output uses constructors
757 -- from HsExpr.
758 --
759 -- Returns (Left r) if the pattern is not invertible, for reason r.
760 -- See Note [Builder for a bidirectional pattern synonym]
761 tcPatToExpr args pat = go pat
762 where
763 lhsVars = mkNameSet (map unLoc args)
764
765 -- Make a prefix con for prefix and infix patterns for simplicity
766 mkPrefixConExpr :: Located Name -> [LPat Name] -> Either MsgDoc (HsExpr Name)
767 mkPrefixConExpr lcon@(L loc _) pats
768 = do { exprs <- mapM go pats
769 ; return (foldl (\x y -> HsApp (L loc x) y)
770 (HsVar lcon) exprs) }
771
772 mkRecordConExpr :: Located Name -> HsRecFields Name (LPat Name)
773 -> Either MsgDoc (HsExpr Name)
774 mkRecordConExpr con fields
775 = do { exprFields <- mapM go fields
776 ; return (RecordCon con PlaceHolder noPostTcExpr exprFields) }
777
778 go :: LPat Name -> Either MsgDoc (LHsExpr Name)
779 go (L loc p) = L loc <$> go1 p
780
781 go1 :: Pat Name -> Either MsgDoc (HsExpr Name)
782 go1 (ConPatIn con info)
783 = case info of
784 PrefixCon ps -> mkPrefixConExpr con ps
785 InfixCon l r -> mkPrefixConExpr con [l,r]
786 RecCon fields -> mkRecordConExpr con fields
787
788 go1 (SigPatIn pat _) = go1 (unLoc pat)
789 -- See Note [Type signatures and the builder expression]
790
791 go1 (VarPat (L l var))
792 | var `elemNameSet` lhsVars
793 = return $ HsVar (L l var)
794 | otherwise
795 = Left (quotes (ppr var) <+> text "is not bound by the LHS of the pattern synonym")
796 go1 (ParPat pat) = fmap HsPar $ go pat
797 go1 (LazyPat pat) = go1 (unLoc pat)
798 go1 (BangPat pat) = go1 (unLoc pat)
799 go1 (PArrPat pats ptt) = do { exprs <- mapM go pats
800 ; return $ ExplicitPArr ptt exprs }
801 go1 (ListPat pats ptt reb) = do { exprs <- mapM go pats
802 ; return $ ExplicitList ptt (fmap snd reb) exprs }
803 go1 (TuplePat pats box _) = do { exprs <- mapM go pats
804 ; return $ ExplicitTuple
805 (map (noLoc . Present) exprs) box }
806 go1 (LitPat lit) = return $ HsLit lit
807 go1 (NPat (L _ n) mb_neg _ _)
808 | Just neg <- mb_neg = return $ unLoc $ nlHsSyntaxApps neg [noLoc (HsOverLit n)]
809 | otherwise = return $ HsOverLit n
810 go1 (ConPatOut{}) = panic "ConPatOut in output of renamer"
811 go1 (SigPatOut{}) = panic "SigPatOut in output of renamer"
812 go1 (CoPat{}) = panic "CoPat in output of renamer"
813 go1 p = Left (text "pattern" <+> quotes (ppr p) <+> text "is not invertible")
814
815 {- Note [Builder for a bidirectional pattern synonym]
816 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
817 For a bidirectional pattern synonym we need to produce an /expression/
818 that matches the supplied /pattern/, given values for the arguments
819 of the pattern synoymy. For example
820 pattern F x y = (Just x, [y])
821 The 'builder' for F looks like
822 $builderF x y = (Just x, [y])
823
824 We can't always do this:
825 * Some patterns aren't invertible; e.g. view patterns
826 pattern F x = (reverse -> x:_)
827
828 * The RHS pattern might bind more variables than the pattern
829 synonym, so again we can't invert it
830 pattern F x = (x,y)
831
832 * Ditto wildcards
833 pattern F x = (x,_)
834
835
836 Note [Redundant constraints for builder]
837 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
838 The builder can have redundant constraints, which are awkard to eliminate.
839 Consider
840 pattern P = Just 34
841 To match against this pattern we need (Eq a, Num a). But to build
842 (Just 34) we need only (Num a). Fortunately instTcSigFromId sets
843 sig_warn_redundant to False.
844
845 ************************************************************************
846 * *
847 Helper functions
848 * *
849 ************************************************************************
850
851 Note [As-patterns in pattern synonym definitions]
852 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
853 The rationale for rejecting as-patterns in pattern synonym definitions
854 is that an as-pattern would introduce nonindependent pattern synonym
855 arguments, e.g. given a pattern synonym like:
856
857 pattern K x y = x@(Just y)
858
859 one could write a nonsensical function like
860
861 f (K Nothing x) = ...
862
863 or
864 g (K (Just True) False) = ...
865
866 Note [Type signatures and the builder expression]
867 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
868 Consider
869 pattern L x = Left x :: Either [a] [b]
870
871 In tc{Infer/Check}PatSynDecl we will check that the pattern has the
872 specified type. We check the pattern *as a pattern*, so the type
873 signature is a pattern signature, and so brings 'a' and 'b' into
874 scope. But we don't have a way to bind 'a, b' in the LHS, as we do
875 'x', say. Nevertheless, the sigature may be useful to constrain
876 the type.
877
878 When making the binding for the *builder*, though, we don't want
879 $buildL x = Left x :: Either [a] [b]
880 because that wil either mean (forall a b. Either [a] [b]), or we'll
881 get a complaint that 'a' and 'b' are out of scope. (Actually the
882 latter; Trac #9867.) No, the job of the signature is done, so when
883 converting the pattern to an expression (for the builder RHS) we
884 simply discard the signature.
885
886 Note [Record PatSyn Desugaring]
887 -------------------------------
888 It is important that prov_theta comes before req_theta as this ordering is used
889 when desugaring record pattern synonym updates.
890
891 Any change to this ordering should make sure to change deSugar/DsExpr.hs if you
892 want to avoid difficult to decipher core lint errors!
893 -}
894
895 tcCheckPatSynPat :: LPat Name -> TcM ()
896 tcCheckPatSynPat = go
897 where
898 go :: LPat Name -> TcM ()
899 go = addLocM go1
900
901 go1 :: Pat Name -> TcM ()
902 go1 (ConPatIn _ info) = mapM_ go (hsConPatArgs info)
903 go1 VarPat{} = return ()
904 go1 WildPat{} = return ()
905 go1 p@(AsPat _ _) = asPatInPatSynErr p
906 go1 (LazyPat pat) = go pat
907 go1 (ParPat pat) = go pat
908 go1 (BangPat pat) = go pat
909 go1 (PArrPat pats _) = mapM_ go pats
910 go1 (ListPat pats _ _) = mapM_ go pats
911 go1 (TuplePat pats _ _) = mapM_ go pats
912 go1 LitPat{} = return ()
913 go1 NPat{} = return ()
914 go1 (SigPatIn pat _) = go pat
915 go1 (ViewPat _ pat _) = go pat
916 go1 p@SplicePat{} = thInPatSynErr p
917 go1 p@NPlusKPat{} = nPlusKPatInPatSynErr p
918 go1 ConPatOut{} = panic "ConPatOut in output of renamer"
919 go1 SigPatOut{} = panic "SigPatOut in output of renamer"
920 go1 CoPat{} = panic "CoPat in output of renamer"
921
922 asPatInPatSynErr :: OutputableBndr name => Pat name -> TcM a
923 asPatInPatSynErr pat
924 = failWithTc $
925 hang (text "Pattern synonym definition cannot contain as-patterns (@):")
926 2 (ppr pat)
927
928 thInPatSynErr :: OutputableBndr name => Pat name -> TcM a
929 thInPatSynErr pat
930 = failWithTc $
931 hang (text "Pattern synonym definition cannot contain Template Haskell:")
932 2 (ppr pat)
933
934 nPlusKPatInPatSynErr :: OutputableBndr name => Pat name -> TcM a
935 nPlusKPatInPatSynErr pat
936 = failWithTc $
937 hang (text "Pattern synonym definition cannot contain n+k-pattern:")
938 2 (ppr pat)
939
940 nonBidirectionalErr :: Outputable name => name -> TcM a
941 nonBidirectionalErr name = failWithTc $
942 text "non-bidirectional pattern synonym"
943 <+> quotes (ppr name) <+> text "used in an expression"
944
945 -- Walk the whole pattern and for all ConPatOuts, collect the
946 -- existentially-bound type variables and evidence binding variables.
947 --
948 -- These are used in computing the type of a pattern synonym and also
949 -- in generating matcher functions, since success continuations need
950 -- to be passed these pattern-bound evidences.
951 tcCollectEx
952 :: LPat Id
953 -> ( ([Var], VarSet) -- Existentially-bound type variables as a
954 -- deterministically ordered list and a set.
955 -- See Note [Deterministic FV] in FV
956 , [EvVar]
957 )
958 tcCollectEx pat = let (fv, evs) = go pat in (fvVarListVarSet fv, evs)
959 where
960 go :: LPat Id -> (FV, [EvVar])
961 go = go1 . unLoc
962
963 go1 :: Pat Id -> (FV, [EvVar])
964 go1 (LazyPat p) = go p
965 go1 (AsPat _ p) = go p
966 go1 (ParPat p) = go p
967 go1 (BangPat p) = go p
968 go1 (ListPat ps _ _) = mergeMany . map go $ ps
969 go1 (TuplePat ps _ _) = mergeMany . map go $ ps
970 go1 (PArrPat ps _) = mergeMany . map go $ ps
971 go1 (ViewPat _ p _) = go p
972 go1 con@ConPatOut{} = merge (FV.mkFVs (pat_tvs con), pat_dicts con) $
973 goConDetails $ pat_args con
974 go1 (SigPatOut p _) = go p
975 go1 (CoPat _ p _) = go1 p
976 go1 (NPlusKPat n k _ geq subtract _)
977 = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract
978 go1 _ = empty
979
980 goConDetails :: HsConPatDetails Id -> (FV, [EvVar])
981 goConDetails (PrefixCon ps) = mergeMany . map go $ ps
982 goConDetails (InfixCon p1 p2) = go p1 `merge` go p2
983 goConDetails (RecCon HsRecFields{ rec_flds = flds })
984 = mergeMany . map goRecFd $ flds
985
986 goRecFd :: LHsRecField Id (LPat Id) -> (FV, [EvVar])
987 goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p
988
989 merge (vs1, evs1) (vs2, evs2) = (vs1 `unionFV` vs2, evs1 ++ evs2)
990 mergeMany = foldr merge empty
991 empty = (emptyFV, [])