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