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