Improve printing of pattern synonym types
[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 VarEnv( emptyTidyEnv )
32 import Type( tidyTyCoVarBndrs, tidyTypes, tidyType )
33 import Id
34 import IdInfo( RecSelParent(..))
35 import TcBinds
36 import BasicTypes
37 import TcSimplify
38 import TcUnify
39 import TcType
40 import Type
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 Control.Monad ( unless, zipWithM )
52 import Data.List( partition )
53 import Pair( Pair(..) )
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 ; body_ty <- tcHsLiftedType hs_body_ty
117 ; let bound_tvs
118 = unionVarSets [ allBoundVariabless req
119 , allBoundVariabless prov
120 , allBoundVariabless (body_ty : arg_tys)
121 ]
122 ; return ( (univ_tvs, req, ex_tvs, prov, arg_tys, body_ty)
123 , bound_tvs) }
124
125 -- Kind generalisation; c.f. kindGeneralise
126 ; free_kvs <- zonkTcTypeAndFV $
127 mkSpecForAllTys (implicit_tvs ++ univ_tvs) $
128 mkFunTys req $
129 mkSpecForAllTys ex_tvs $
130 mkFunTys prov $
131 mkFunTys arg_tys $
132 body_ty
133
134 ; kvs <- quantifyZonkedTyVars emptyVarSet (Pair free_kvs emptyVarSet)
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_vars, prov_dicts) = tcCollectEx lpat'
222 univ_tvs = filter (not . (`elemVarSet` ex_vars)) qtvs
223 ex_tvs = varSetElems ex_vars
224 prov_theta = map evVarPred prov_dicts
225 req_theta = map evVarPred req_dicts
226
227 ; traceTc "tcInferPatSynDecl }" $ ppr name
228 ; tc_patsyn_finish lname dir is_infix lpat'
229 (univ_tvs, mkNamedBinders Invisible univ_tvs
230 , req_theta, ev_binds, req_dicts)
231 (ex_tvs, mkNamedBinders Invisible ex_tvs
232 , mkTyVarTys ex_tvs, prov_theta, map EvId prov_dicts)
233 (map nlHsVar args, map idType args)
234 pat_ty rec_fields }
235
236
237 tcCheckPatSynDecl :: PatSynBind Name Name
238 -> TcPatSynInfo
239 -> TcM (LHsBinds Id, TcGblEnv)
240 tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
241 , psb_def = lpat, psb_dir = dir }
242 TPSI{ patsig_univ_bndrs = univ_bndrs, patsig_prov = prov_theta
243 , patsig_ex_bndrs = ex_bndrs, patsig_req = req_theta
244 , patsig_arg_tys = arg_tys, patsig_body_ty = pat_ty }
245 = addPatSynCtxt lname $
246 do { let decl_arity = length arg_names
247 ty_arity = length arg_tys
248 (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
249
250 univ_tvs = map (binderVar "tcCheckPatSynDecl 1") univ_bndrs
251 ex_tvs = map (binderVar "tcCheckPatSynDecl 2") ex_bndrs
252
253 ; traceTc "tcCheckPatSynDecl" $
254 vcat [ ppr univ_bndrs, ppr req_theta, ppr ex_bndrs
255 , ppr prov_theta, ppr arg_tys, ppr pat_ty ]
256
257 ; checkTc (decl_arity == ty_arity)
258 (wrongNumberOfParmsErr name decl_arity ty_arity)
259
260 ; tcCheckPatSynPat lpat
261
262 -- Right! Let's check the pattern against the signature
263 -- See Note [Checking against a pattern signature]
264 ; req_dicts <- newEvVars req_theta
265 ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
266 ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
267 pushLevelAndCaptureConstraints $
268 tcExtendTyVarEnv univ_tvs $
269 tcPat PatSyn lpat (mkCheckExpType pat_ty) $
270 do { (subst, ex_tvs') <- if isUnidirectional dir
271 then newMetaTyVars ex_tvs
272 else newMetaSigTyVars ex_tvs
273 -- See the "Existential type variables" part of
274 -- Note [Checking against a pattern signature]
275 ; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs])
276 ; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs'])
277 ; let prov_theta' = substTheta (extendTCvInScopeList subst univ_tvs) prov_theta
278 -- Add univ_tvs to the in_scope set to
279 -- satisfy the substition invariant. There's no need to
280 -- add 'ex_tvs' as they are already in the domain of the
281 -- substitution.
282 -- See also Note [The substitution invariant] in TyCoRep.
283 ; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta'
284 ; args' <- zipWithM (tc_arg subst) arg_names arg_tys
285 ; return (ex_tvs', prov_dicts, args') }
286
287 ; let skol_info = SigSkol (PatSynCtxt name) (mkPhiTy req_theta pat_ty)
288 -- The type here is a bit bogus, but we do not print
289 -- the type for PatSynCtxt, so it doesn't matter
290 -- See TcRnTypes Note [Skolem info for pattern synonyms]
291 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted
292
293 -- Solve the constraints now, because we are about to make a PatSyn,
294 -- which should not contain unification variables and the like (Trac #10997)
295 -- Since all the inputs are implications the returned bindings will be empty
296 ; _ <- simplifyTop (mkImplicWC implics)
297
298 -- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct
299 -- Otherwise we may get a type error when typechecking the builder,
300 -- when that should be impossible
301
302 ; traceTc "tcCheckPatSynDecl }" $ ppr name
303 ; tc_patsyn_finish lname dir is_infix lpat'
304 (univ_tvs, univ_bndrs, req_theta, ev_binds, req_dicts)
305 (ex_tvs, ex_bndrs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
306 (args', arg_tys)
307 pat_ty rec_fields }
308 where
309 tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr TcId)
310 tc_arg subst arg_name arg_ty
311 = do { -- Look up the variable actually bound by lpat
312 -- and check that it has the expected type
313 arg_id <- tcLookupId arg_name
314 ; coi <- unifyType (Just arg_id)
315 (idType arg_id)
316 (substTyUnchecked subst arg_ty)
317 ; return (mkLHsWrapCo coi $ nlHsVar arg_id) }
318
319 {- Note [Checking against a pattern signature]
320 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
321 When checking the actual supplied pattern against the pattern synonym
322 signature, we need to be quite careful.
323
324 ----- Provided constraints
325 Example
326
327 data T a where
328 MkT :: Ord a => a -> T a
329
330 pattern P :: () => Eq a => a -> [T a]
331 pattern P x = [MkT x]
332
333 We must check that the (Eq a) that P claims to bind (and to
334 make available to matches against P), is derivable from the
335 actual pattern. For example:
336 f (P (x::a)) = ...here (Eq a) should be available...
337 And yes, (Eq a) is derivable from the (Ord a) bound by P's rhs.
338
339 ----- Existential type variables
340 Unusually, we instantiate the existential tyvars of the pattern with
341 *meta* type variables. For example
342
343 data S where
344 MkS :: Eq a => [a] -> S
345
346 pattern P :: () => Eq x => x -> S
347 pattern P x <- MkS x
348
349 The pattern synonym conceals from its client the fact that MkS has a
350 list inside it. The client just thinks it's a type 'x'. So we must
351 unify x := [a] during type checking, and then use the instantiating type
352 [a] (called ex_tys) when building the matcher. In this case we'll get
353
354 $mP :: S -> (forall x. Ex x => x -> r) -> r -> r
355 $mP x k = case x of
356 MkS a (d:Eq a) (ys:[a]) -> let dl :: Eq [a]
357 dl = $dfunEqList d
358 in k [a] dl ys
359
360 This "concealing" story works for /uni-directional/ pattern synonmys,
361 but obviously not for bidirectional ones. So in the bidirectional case
362 we use SigTv, rather than a generic TauTv, meta-tyvar so that. And
363 we should really check that those SigTvs don't get unified with each
364 other.
365
366 -}
367
368 collectPatSynArgInfo :: HsPatSynDetails (Located Name) -> ([Name], [Name], Bool)
369 collectPatSynArgInfo details =
370 case details of
371 PrefixPatSyn names -> (map unLoc names, [], False)
372 InfixPatSyn name1 name2 -> (map unLoc [name1, name2], [], True)
373 RecordPatSyn names ->
374 let (vars, sels) = unzip (map splitRecordPatSyn names)
375 in (vars, sels, False)
376
377 where
378 splitRecordPatSyn :: RecordPatSynField (Located Name) -> (Name, Name)
379 splitRecordPatSyn (RecordPatSynField { recordPatSynPatVar = L _ patVar
380 , recordPatSynSelectorId = L _ selId })
381 = (patVar, selId)
382
383 addPatSynCtxt :: Located Name -> TcM a -> TcM a
384 addPatSynCtxt (L loc name) thing_inside
385 = setSrcSpan loc $
386 addErrCtxt (text "In the declaration for pattern synonym"
387 <+> quotes (ppr name)) $
388 thing_inside
389
390 wrongNumberOfParmsErr :: Name -> Arity -> Arity -> SDoc
391 wrongNumberOfParmsErr name decl_arity ty_arity
392 = hang (text "Pattern synonym" <+> quotes (ppr name) <+> ptext (sLit "has")
393 <+> speakNOf decl_arity (text "argument"))
394 2 (text "but its type signature has" <+> speakN ty_arity)
395
396 -------------------------
397 -- Shared by both tcInferPatSyn and tcCheckPatSyn
398 tc_patsyn_finish :: Located Name -- ^ PatSyn Name
399 -> HsPatSynDir Name -- ^ PatSyn type (Uni/Bidir/ExplicitBidir)
400 -> Bool -- ^ Whether infix
401 -> LPat Id -- ^ Pattern of the PatSyn
402 -> ([TcTyVar], [TcTyBinder], [PredType], TcEvBinds, [EvVar])
403 -> ([TcTyVar], [TcTyBinder], [TcType], [PredType], [EvTerm])
404 -> ([LHsExpr TcId], [TcType]) -- ^ Pattern arguments and types
405 -> TcType -- ^ Pattern type
406 -> [Name] -- ^ Selector names
407 -- ^ Whether fields, empty if not record PatSyn
408 -> TcM (LHsBinds Id, TcGblEnv)
409 tc_patsyn_finish lname dir is_infix lpat'
410 (univ_tvs, univ_bndrs, req_theta, req_ev_binds, req_dicts)
411 (ex_tvs, ex_bndrs, ex_tys, prov_theta, prov_dicts)
412 (args, arg_tys)
413 pat_ty field_labels
414 = do { -- Zonk everything. We are about to build a final PatSyn
415 -- so there had better be no unification variables in there
416 univ_tvs' <- mapMaybeM zonkQuantifiedTyVar univ_tvs
417 ; ex_tvs' <- mapMaybeM zonkQuantifiedTyVar ex_tvs
418 ; prov_theta' <- zonkTcTypes prov_theta
419 ; req_theta' <- zonkTcTypes req_theta
420 ; pat_ty' <- zonkTcType pat_ty
421 ; arg_tys' <- zonkTcTypes arg_tys
422
423 ; let (env1, univ_tvs) = tidyTyCoVarBndrs emptyTidyEnv univ_tvs'
424 (env2, ex_tvs) = tidyTyCoVarBndrs env1 ex_tvs'
425 req_theta = tidyTypes env2 req_theta'
426 prov_theta = tidyTypes env2 prov_theta'
427 arg_tys = tidyTypes env2 arg_tys'
428 pat_ty = tidyType env2 pat_ty'
429
430 -- We need to update the univ and ex binders after zonking.
431 -- But zonking may have defaulted some erstwhile binders,
432 -- so we need to make sure the tyvars and tybinders remain
433 -- lined up
434 ; let update_binders :: [TyVar] -> [TcTyBinder] -> [TyBinder]
435 update_binders [] _ = []
436 update_binders all_tvs@(tv:tvs) (bndr:bndrs)
437 | tv == bndr_var
438 = mkNamedBinder (binderVisibility bndr) tv : update_binders tvs bndrs
439 | otherwise
440 = update_binders all_tvs bndrs
441 where
442 bndr_var = binderVar "tc_patsyn_finish" bndr
443 update_binders tvs _ = pprPanic "tc_patsyn_finish" (ppr lname $$ ppr tvs)
444
445 univ_bndrs' = update_binders univ_tvs univ_bndrs
446 ex_bndrs' = update_binders ex_tvs ex_bndrs
447
448 ; traceTc "tc_patsyn_finish {" $
449 ppr (unLoc lname) $$ ppr (unLoc lpat') $$
450 ppr (univ_tvs, univ_bndrs', req_theta, req_ev_binds, req_dicts) $$
451 ppr (ex_tvs, ex_bndrs', prov_theta, prov_dicts) $$
452 ppr args $$
453 ppr arg_tys $$
454 ppr pat_ty
455
456 -- Make the 'matcher'
457 ; (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat'
458 (univ_tvs, req_theta, req_ev_binds, req_dicts)
459 (ex_tvs, ex_tys, prov_theta, prov_dicts)
460 (args, arg_tys)
461 pat_ty
462
463
464 -- Make the 'builder'
465 ; builder_id <- mkPatSynBuilderId dir lname
466 univ_bndrs' req_theta
467 ex_bndrs' prov_theta
468 arg_tys pat_ty
469
470 -- TODO: Make this have the proper information
471 ; let mkFieldLabel name = FieldLabel (occNameFS (nameOccName name)) False name
472 field_labels' = (map mkFieldLabel field_labels)
473
474
475 -- Make the PatSyn itself
476 ; let patSyn = mkPatSyn (unLoc lname) is_infix
477 (univ_tvs, univ_bndrs', req_theta)
478 (ex_tvs, ex_bndrs', prov_theta)
479 arg_tys
480 pat_ty
481 matcher_id builder_id
482 field_labels'
483
484 -- Selectors
485 ; let (sigs, selector_binds) =
486 unzip (mkPatSynRecSelBinds patSyn (patSynFieldLabels patSyn))
487 ; let tything = AConLike (PatSynCon patSyn)
488 ; tcg_env <-
489 tcExtendGlobalEnv [tything] $
490 tcRecSelBinds
491 (ValBindsOut (zip (repeat NonRecursive) selector_binds) sigs)
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]
591 -- ^ Visible field labels
592 -> [(LSig Name, LHsBinds Name)]
593 mkPatSynRecSelBinds ps fields = map mkRecSel fields
594 where
595 mkRecSel fld_lbl =
596 case mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl of
597 (name, (_rec_flag, binds)) -> (name, binds)
598
599 isUnidirectional :: HsPatSynDir a -> Bool
600 isUnidirectional Unidirectional = True
601 isUnidirectional ImplicitBidirectional = False
602 isUnidirectional ExplicitBidirectional{} = False
603
604 {-
605 ************************************************************************
606 * *
607 Constructing the "builder" Id
608 * *
609 ************************************************************************
610 -}
611
612 mkPatSynBuilderId :: HsPatSynDir a -> Located Name
613 -> [TyBinder] -> ThetaType
614 -> [TyBinder] -> ThetaType
615 -> [Type] -> Type
616 -> TcM (Maybe (Id, Bool))
617 mkPatSynBuilderId dir (L _ name)
618 univ_bndrs req_theta ex_bndrs prov_theta
619 arg_tys pat_ty
620 | isUnidirectional dir
621 = return Nothing
622 | otherwise
623 = do { builder_name <- newImplicitBinder name mkBuilderOcc
624 ; let theta = req_theta ++ prov_theta
625 need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
626 builder_sigma = add_void need_dummy_arg $
627 mkForAllTys univ_bndrs $
628 mkForAllTys ex_bndrs $
629 mkFunTys theta $
630 mkFunTys arg_tys $
631 pat_ty
632 builder_id = mkExportedVanillaId builder_name builder_sigma
633 -- See Note [Exported LocalIds] in Id
634
635 ; return (Just (builder_id, need_dummy_arg)) }
636 where
637
638 tcPatSynBuilderBind :: TcSigFun
639 -> PatSynBind Name Name
640 -> TcM (LHsBinds Id)
641 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
642 tcPatSynBuilderBind sig_fun PSB{ psb_id = L loc name, psb_def = lpat
643 , psb_dir = dir, psb_args = details }
644 | isUnidirectional dir
645 = return emptyBag
646
647 | Left why <- mb_match_group -- Can't invert the pattern
648 = setSrcSpan (getLoc lpat) $ failWithTc $
649 vcat [ hang (text "Invalid right-hand side of bidirectional pattern synonym"
650 <+> quotes (ppr name) <> colon)
651 2 why
652 , text "RHS pattern:" <+> ppr lpat ]
653
654 | Right match_group <- mb_match_group -- Bidirectional
655 = do { patsyn <- tcLookupPatSyn name
656 ; traceTc "tcPatSynBuilderBind {" $ ppr patsyn
657 ; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn
658 -- Bidirectional, so patSynBuilder returns Just
659
660 match_group' | need_dummy_arg = add_dummy_arg match_group
661 | otherwise = match_group
662
663 bind = FunBind { fun_id = L loc (idName builder_id)
664 , fun_matches = match_group'
665 , fun_co_fn = idHsWrapper
666 , bind_fvs = placeHolderNamesTc
667 , fun_tick = [] }
668
669 ; sig <- get_builder_sig sig_fun name builder_id need_dummy_arg
670
671 ; (builder_binds, _) <- tcPolyCheck NonRecursive emptyPragEnv sig (noLoc bind)
672 ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
673 ; return builder_binds }
674
675 | otherwise = panic "tcPatSynBuilderBind" -- Both cases dealt with
676 where
677 mb_match_group
678 = case dir of
679 ExplicitBidirectional explicit_mg -> Right explicit_mg
680 ImplicitBidirectional -> fmap mk_mg (tcPatToExpr args lpat)
681 Unidirectional -> panic "tcPatSynBuilderBind"
682
683 mk_mg :: LHsExpr Name -> MatchGroup Name (LHsExpr Name)
684 mk_mg body = mkMatchGroupName Generated [builder_match]
685 where
686 builder_args = [L loc (VarPat (L loc n)) | L loc n <- args]
687 builder_match = mkMatch builder_args body (noLoc EmptyLocalBinds)
688
689 args = case details of
690 PrefixPatSyn args -> args
691 InfixPatSyn arg1 arg2 -> [arg1, arg2]
692 RecordPatSyn args -> map recordPatSynPatVar args
693
694 add_dummy_arg :: MatchGroup Name (LHsExpr Name)
695 -> MatchGroup Name (LHsExpr Name)
696 add_dummy_arg mg@(MG { mg_alts = L l [L loc match@(Match { m_pats = pats })] })
697 = mg { mg_alts = L l [L loc (match { m_pats = nlWildPatName : pats })] }
698 add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
699 pprMatches (PatSyn :: HsMatchContext Name) other_mg
700
701 get_builder_sig :: TcSigFun -> Name -> Id -> Bool -> TcM TcIdSigInfo
702 get_builder_sig sig_fun name builder_id need_dummy_arg
703 | Just (TcPatSynSig sig) <- sig_fun name
704 , TPSI { patsig_univ_bndrs = univ_bndrs
705 , patsig_req = req
706 , patsig_ex_bndrs = ex_bndrs
707 , patsig_prov = prov
708 , patsig_arg_tys = arg_tys
709 , patsig_body_ty = body_ty } <- sig
710 = -- Constuct a TcIdSigInfo from a TcPatSynInfo
711 -- This does unfortunately mean that we have to know how to
712 -- make the builder Id's type from the TcPatSynInfo, which
713 -- duplicates the construction in mkPatSynBuilderId
714 -- But we really want to use the scoped type variables from
715 -- the actual sigature, so this is really the Right Thing
716 return (TISI { sig_bndr = CompleteSig builder_id
717 , sig_skols = [ (tyVarName tv, tv)
718 | bndr <- univ_bndrs ++ ex_bndrs
719 , let tv = binderVar "get_builder_sig" bndr ]
720 , sig_theta = req ++ prov
721 , sig_tau = add_void need_dummy_arg $
722 mkFunTys arg_tys body_ty
723 , sig_ctxt = PatSynCtxt name
724 , sig_loc = getSrcSpan name })
725 | otherwise
726 = -- No signature, so fake up a TcIdSigInfo from the builder Id
727 instTcTySigFromId builder_id
728 -- See Note [Redundant constraints for builder]
729
730 tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr TcId, TcSigmaType)
731 -- monadic only for failure
732 tcPatSynBuilderOcc ps
733 | Just (builder_id, add_void_arg) <- builder
734 , let builder_expr = HsVar (noLoc builder_id)
735 builder_ty = idType builder_id
736 = return $
737 if add_void_arg
738 then ( HsApp (noLoc $ builder_expr) (nlHsVar voidPrimId)
739 , tcFunResultTy builder_ty )
740 else (builder_expr, builder_ty)
741
742 | otherwise -- Unidirectional
743 = nonBidirectionalErr name
744 where
745 name = patSynName ps
746 builder = patSynBuilder ps
747
748 add_void :: Bool -> Type -> Type
749 add_void need_dummy_arg ty
750 | need_dummy_arg = mkFunTy voidPrimTy ty
751 | otherwise = ty
752
753 tcPatToExpr :: [Located Name] -> LPat Name -> Either MsgDoc (LHsExpr Name)
754 -- Given a /pattern/, return an /expression/ that builds a value
755 -- that matches the pattern. E.g. if the pattern is (Just [x]),
756 -- the expression is (Just [x]). They look the same, but the
757 -- input uses constructors from HsPat and the output uses constructors
758 -- from HsExpr.
759 --
760 -- Returns (Left r) if the pattern is not invertible, for reason r.
761 -- See Note [Builder for a bidirectional pattern synonym]
762 tcPatToExpr args pat = go pat
763 where
764 lhsVars = mkNameSet (map unLoc args)
765
766 -- Make a prefix con for prefix and infix patterns for simplicity
767 mkPrefixConExpr :: Located Name -> [LPat Name] -> Either MsgDoc (HsExpr Name)
768 mkPrefixConExpr lcon@(L loc _) pats
769 = do { exprs <- mapM go pats
770 ; return (foldl (\x y -> HsApp (L loc x) y)
771 (HsVar lcon) exprs) }
772
773 mkRecordConExpr :: Located Name -> HsRecFields Name (LPat Name)
774 -> Either MsgDoc (HsExpr Name)
775 mkRecordConExpr con fields
776 = do { exprFields <- mapM go fields
777 ; return (RecordCon con PlaceHolder noPostTcExpr exprFields) }
778
779 go :: LPat Name -> Either MsgDoc (LHsExpr Name)
780 go (L loc p) = L loc <$> go1 p
781
782 go1 :: Pat Name -> Either MsgDoc (HsExpr Name)
783 go1 (ConPatIn con info)
784 = case info of
785 PrefixCon ps -> mkPrefixConExpr con ps
786 InfixCon l r -> mkPrefixConExpr con [l,r]
787 RecCon fields -> mkRecordConExpr con fields
788
789 go1 (SigPatIn pat _) = go1 (unLoc pat)
790 -- See Note [Type signatures and the builder expression]
791
792 go1 (VarPat (L l var))
793 | var `elemNameSet` lhsVars
794 = return $ HsVar (L l var)
795 | otherwise
796 = Left (quotes (ppr var) <+> text "is not bound by the LHS of the pattern synonym")
797 go1 (ParPat pat) = fmap HsPar $ go pat
798 go1 (LazyPat pat) = go1 (unLoc pat)
799 go1 (BangPat pat) = go1 (unLoc pat)
800 go1 (PArrPat pats ptt) = do { exprs <- mapM go pats
801 ; return $ ExplicitPArr ptt exprs }
802 go1 (ListPat pats ptt reb) = do { exprs <- mapM go pats
803 ; return $ ExplicitList ptt (fmap snd reb) exprs }
804 go1 (TuplePat pats box _) = do { exprs <- mapM go pats
805 ; return $ ExplicitTuple
806 (map (noLoc . Present) exprs) box }
807 go1 (LitPat lit) = return $ HsLit lit
808 go1 (NPat (L _ n) mb_neg _ _)
809 | Just neg <- mb_neg = return $ unLoc $ nlHsSyntaxApps neg [noLoc (HsOverLit n)]
810 | otherwise = return $ HsOverLit n
811 go1 (ConPatOut{}) = panic "ConPatOut in output of renamer"
812 go1 (SigPatOut{}) = panic "SigPatOut in output of renamer"
813 go1 (CoPat{}) = panic "CoPat in output of renamer"
814 go1 p = Left (text "pattern" <+> quotes (ppr p) <+> text "is not invertible")
815
816 {- Note [Builder for a bidirectional pattern synonym]
817 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
818 For a bidirectional pattern synonym we need to produce an /expression/
819 that matches the supplied /pattern/, given values for the arguments
820 of the pattern synoymy. For example
821 pattern F x y = (Just x, [y])
822 The 'builder' for F looks like
823 $builderF x y = (Just x, [y])
824
825 We can't always do this:
826 * Some patterns aren't invertible; e.g. view patterns
827 pattern F x = (reverse -> x:_)
828
829 * The RHS pattern might bind more variables than the pattern
830 synonym, so again we can't invert it
831 pattern F x = (x,y)
832
833 * Ditto wildcards
834 pattern F x = (x,_)
835
836
837 Note [Redundant constraints for builder]
838 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
839 The builder can have redundant constraints, which are awkard to eliminate.
840 Consider
841 pattern P = Just 34
842 To match against this pattern we need (Eq a, Num a). But to build
843 (Just 34) we need only (Num a). Fortunately instTcSigFromId sets
844 sig_warn_redundant to False.
845
846 ************************************************************************
847 * *
848 Helper functions
849 * *
850 ************************************************************************
851
852 Note [As-patterns in pattern synonym definitions]
853 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
854 The rationale for rejecting as-patterns in pattern synonym definitions
855 is that an as-pattern would introduce nonindependent pattern synonym
856 arguments, e.g. given a pattern synonym like:
857
858 pattern K x y = x@(Just y)
859
860 one could write a nonsensical function like
861
862 f (K Nothing x) = ...
863
864 or
865 g (K (Just True) False) = ...
866
867 Note [Type signatures and the builder expression]
868 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
869 Consider
870 pattern L x = Left x :: Either [a] [b]
871
872 In tc{Infer/Check}PatSynDecl we will check that the pattern has the
873 specified type. We check the pattern *as a pattern*, so the type
874 signature is a pattern signature, and so brings 'a' and 'b' into
875 scope. But we don't have a way to bind 'a, b' in the LHS, as we do
876 'x', say. Nevertheless, the sigature may be useful to constrain
877 the type.
878
879 When making the binding for the *builder*, though, we don't want
880 $buildL x = Left x :: Either [a] [b]
881 because that wil either mean (forall a b. Either [a] [b]), or we'll
882 get a complaint that 'a' and 'b' are out of scope. (Actually the
883 latter; Trac #9867.) No, the job of the signature is done, so when
884 converting the pattern to an expression (for the builder RHS) we
885 simply discard the signature.
886
887 Note [Record PatSyn Desugaring]
888 -------------------------------
889 It is important that prov_theta comes before req_theta as this ordering is used
890 when desugaring record pattern synonym updates.
891
892 Any change to this ordering should make sure to change deSugar/DsExpr.hs if you
893 want to avoid difficult to decipher core lint errors!
894 -}
895
896 tcCheckPatSynPat :: LPat Name -> TcM ()
897 tcCheckPatSynPat = go
898 where
899 go :: LPat Name -> TcM ()
900 go = addLocM go1
901
902 go1 :: Pat Name -> TcM ()
903 go1 (ConPatIn _ info) = mapM_ go (hsConPatArgs info)
904 go1 VarPat{} = return ()
905 go1 WildPat{} = return ()
906 go1 p@(AsPat _ _) = asPatInPatSynErr p
907 go1 (LazyPat pat) = go pat
908 go1 (ParPat pat) = go pat
909 go1 (BangPat pat) = go pat
910 go1 (PArrPat pats _) = mapM_ go pats
911 go1 (ListPat pats _ _) = mapM_ go pats
912 go1 (TuplePat pats _ _) = mapM_ go pats
913 go1 LitPat{} = return ()
914 go1 NPat{} = return ()
915 go1 (SigPatIn pat _) = go pat
916 go1 (ViewPat _ pat _) = go pat
917 go1 p@SplicePat{} = thInPatSynErr p
918 go1 p@NPlusKPat{} = nPlusKPatInPatSynErr p
919 go1 ConPatOut{} = panic "ConPatOut in output of renamer"
920 go1 SigPatOut{} = panic "SigPatOut in output of renamer"
921 go1 CoPat{} = panic "CoPat in output of renamer"
922
923 asPatInPatSynErr :: OutputableBndr name => Pat name -> TcM a
924 asPatInPatSynErr pat
925 = failWithTc $
926 hang (text "Pattern synonym definition cannot contain as-patterns (@):")
927 2 (ppr pat)
928
929 thInPatSynErr :: OutputableBndr name => Pat name -> TcM a
930 thInPatSynErr pat
931 = failWithTc $
932 hang (text "Pattern synonym definition cannot contain Template Haskell:")
933 2 (ppr pat)
934
935 nPlusKPatInPatSynErr :: OutputableBndr name => Pat name -> TcM a
936 nPlusKPatInPatSynErr pat
937 = failWithTc $
938 hang (text "Pattern synonym definition cannot contain n+k-pattern:")
939 2 (ppr pat)
940
941 nonBidirectionalErr :: Outputable name => name -> TcM a
942 nonBidirectionalErr name = failWithTc $
943 text "non-bidirectional pattern synonym"
944 <+> quotes (ppr name) <+> text "used in an expression"
945
946 -- Walk the whole pattern and for all ConPatOuts, collect the
947 -- existentially-bound type variables and evidence binding variables.
948 --
949 -- These are used in computing the type of a pattern synonym and also
950 -- in generating matcher functions, since success continuations need
951 -- to be passed these pattern-bound evidences.
952 tcCollectEx :: LPat Id -> (TyVarSet, [EvVar])
953 tcCollectEx pat = go pat
954 where
955 go :: LPat Id -> (TyVarSet, [EvVar])
956 go = go1 . unLoc
957
958 go1 :: Pat Id -> (TyVarSet, [EvVar])
959 go1 (LazyPat p) = go p
960 go1 (AsPat _ p) = go p
961 go1 (ParPat p) = go p
962 go1 (BangPat p) = go p
963 go1 (ListPat ps _ _) = mconcat . map go $ ps
964 go1 (TuplePat ps _ _) = mconcat . map go $ ps
965 go1 (PArrPat ps _) = mconcat . map go $ ps
966 go1 (ViewPat _ p _) = go p
967 go1 con@ConPatOut{} = mappend (mkVarSet (pat_tvs con), pat_dicts con) $
968 goConDetails $ pat_args con
969 go1 (SigPatOut p _) = go p
970 go1 (CoPat _ p _) = go1 p
971 go1 (NPlusKPat n k _ geq subtract _)
972 = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract
973 go1 _ = mempty
974
975 goConDetails :: HsConPatDetails Id -> (TyVarSet, [EvVar])
976 goConDetails (PrefixCon ps) = mconcat . map go $ ps
977 goConDetails (InfixCon p1 p2) = go p1 `mappend` go p2
978 goConDetails (RecCon HsRecFields{ rec_flds = flds })
979 = mconcat . map goRecFd $ flds
980
981 goRecFd :: LHsRecField Id (LPat Id) -> (TyVarSet, [EvVar])
982 goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p