Re-add FunTy (big patch)
[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 ( tcInferPatSynDecl, tcCheckPatSynDecl
12 , tcPatSynBuilderBind, tcPatSynBuilderOcc, nonBidirectionalErr
13 ) where
14
15 import HsSyn
16 import TcPat
17 import Type( binderVar, mkNamedBinders, binderVisibility, mkEmptyTCvSubst
18 , tidyTyCoVarBndrs, tidyTypes, tidyType )
19 , tcHsContext, tcHsLiftedType, tcHsOpenType, kindGeneralize )
20 import TcRnMonad
21 import TcSigs( emptyPragEnv, completeSigFromId )
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, mkInScopeSet )
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 * *
61 Type checking a pattern synonym
62 * *
63 ************************************************************************
64 -}
65
66 tcInferPatSynDecl :: PatSynBind Name Name
67 -> TcM (LHsBinds Id, TcGblEnv)
68 tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details,
69 psb_def = lpat, psb_dir = dir }
70 = addPatSynCtxt lname $
71 do { traceTc "tcInferPatSynDecl {" $ ppr name
72 ; tcCheckPatSynPat lpat
73
74 ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
75 ; (tclvl, wanted, ((lpat', args), pat_ty))
76 <- pushLevelAndCaptureConstraints $
77 do { pat_ty <- newOpenInferExpType
78 ; stuff <- tcPat PatSyn lpat pat_ty $
79 mapM tcLookupId arg_names
80 ; pat_ty <- readExpType pat_ty
81 ; return (stuff, pat_ty) }
82
83 ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
84
85 ; (qtvs, req_dicts, ev_binds) <- simplifyInfer tclvl False [] named_taus wanted
86
87 ; let ((ex_tvs, ex_vars), prov_dicts) = tcCollectEx lpat'
88 univ_tvs = filter (not . (`elemVarSet` ex_vars)) qtvs
89 prov_theta = map evVarPred prov_dicts
90 req_theta = map evVarPred req_dicts
91
92 ; traceTc "tcInferPatSynDecl }" $ ppr name
93 ; tc_patsyn_finish lname dir is_infix lpat'
94 (mkTyVarBinders Invisible univ_tvs
95 , req_theta, ev_binds, req_dicts)
96 (mkTyVarBinders Invisible ex_tvs
97 , mkTyVarTys ex_tvs, prov_theta, map EvId prov_dicts)
98 (map nlHsVar args, map idType args)
99 pat_ty rec_fields }
100
101
102 tcCheckPatSynDecl :: PatSynBind Name Name
103 -> TcPatSynInfo
104 -> TcM (LHsBinds Id, TcGblEnv)
105 tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
106 , psb_def = lpat, psb_dir = dir }
107 TPSI{ patsig_implicit_bndrs = implicit_tvs
108 , patsig_univ_bndrs = explicit_univ_tvs, patsig_prov = prov_theta
109 , patsig_ex_bndrs = explicit_ex_tvs, patsig_req = req_theta
110 , patsig_body_ty = sig_body_ty }
111 = addPatSynCtxt lname $
112 do { let decl_arity = length arg_names
113 (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
114
115 ; traceTc "tcCheckPatSynDecl" $
116 vcat [ ppr implicit_tvs, ppr explicit_univ_tvs, ppr req_theta
117 , ppr explicit_ex_tvs, ppr prov_theta, ppr sig_body_ty ]
118
119 ; tcCheckPatSynPat lpat
120
121 ; (arg_tys, pat_ty) <- case tcSplitFunTysN decl_arity sig_body_ty of
122 Right stuff -> return stuff
123 Left missing -> wrongNumberOfParmsErr name decl_arity missing
124
125 -- Complain about: pattern P :: () => forall x. x -> P x
126 -- The existential 'x' should not appear in the result type
127 -- Can't check this until we know P's arity
128 ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType pat_ty) explicit_ex_tvs
129 ; checkTc (null bad_tvs) $
130 hang (sep [ text "The result type of the signature for" <+> quotes (ppr name) <> comma
131 , text "namely" <+> quotes (ppr pat_ty) ])
132 2 (text "mentions existential type variable" <> plural bad_tvs
133 <+> pprQuotedList bad_tvs)
134
135 -- See Note [The pattern-synonym signature splitting rule]
136 ; let get_tv = binderVar "tcCheckPatSynDecl"
137 univ_fvs = closeOverKinds $
138 (tyCoVarsOfTypes (pat_ty : req_theta) `extendVarSetList` explicit_univ_tvs)
139 (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) . get_tv) implicit_tvs
140 univ_bndrs = extra_univ ++ mkNamedBinders Specified explicit_univ_tvs
141 ex_bndrs = extra_ex ++ mkNamedBinders Specified explicit_ex_tvs
142 univ_tvs = map get_tv univ_bndrs
143 ex_tvs = map get_tv ex_bndrs
144
145 -- Right! Let's check the pattern against the signature
146 -- See Note [Checking against a pattern signature]
147 ; req_dicts <- newEvVars req_theta
148 ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
149 ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
150 pushLevelAndCaptureConstraints $
151 tcExtendTyVarEnv univ_tvs $
152 tcPat PatSyn lpat (mkCheckExpType pat_ty) $
153 do { let new_tv | isUnidirectional dir = newMetaTyVarX
154 | otherwise = newMetaSigTyVarX
155 in_scope = mkInScopeSet (mkVarSet univ_tvs)
156 empty_subst = mkEmptyTCvSubst in_scope
157 ; (subst, ex_tvs') <- mapAccumLM new_tv empty_subst ex_tvs
158 -- See the "Existential type variables" part of
159 -- Note [Checking against a pattern signature]
160 ; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs])
161 ; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs'])
162 ; let prov_theta' = substTheta subst prov_theta
163 -- Add univ_tvs to the in_scope set to
164 -- satisfy the substition invariant. There's no need to
165 -- add 'ex_tvs' as they are already in the domain of the
166 -- substitution.
167 -- See also Note [The substitution invariant] in TyCoRep.
168 ; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta'
169 ; args' <- zipWithM (tc_arg subst) arg_names arg_tys
170 ; return (ex_tvs', prov_dicts, args') }
171
172 ; let skol_info = SigSkol (PatSynCtxt name) (mkPhiTy req_theta pat_ty)
173 -- The type here is a bit bogus, but we do not print
174 -- the type for PatSynCtxt, so it doesn't matter
175 -- See TcRnTypes Note [Skolem info for pattern synonyms]
176 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted
177
178 -- Solve the constraints now, because we are about to make a PatSyn,
179 -- which should not contain unification variables and the like (Trac #10997)
180 -- Since all the inputs are implications the returned bindings will be empty
181 ; _ <- simplifyTop (mkImplicWC implics)
182
183 -- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct
184 -- Otherwise we may get a type error when typechecking the builder,
185 -- when that should be impossible
186
187 ; traceTc "tcCheckPatSynDecl }" $ ppr name
188 ; tc_patsyn_finish lname dir is_infix lpat'
189 (univ_bndrs, req_theta, ev_binds, req_dicts)
190 (ex_bndrs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
191 (args', arg_tys)
192 pat_ty rec_fields }
193 where
194 tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr TcId)
195 tc_arg subst arg_name arg_ty
196 = do { -- Look up the variable actually bound by lpat
197 -- and check that it has the expected type
198 arg_id <- tcLookupId arg_name
199 ; coi <- unifyType (Just arg_id)
200 (idType arg_id)
201 (substTyUnchecked subst arg_ty)
202 ; return (mkLHsWrapCo coi $ nlHsVar arg_id) }
203
204 {- Note [Checking against a pattern signature]
205 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
206 When checking the actual supplied pattern against the pattern synonym
207 signature, we need to be quite careful.
208
209 ----- Provided constraints
210 Example
211
212 data T a where
213 MkT :: Ord a => a -> T a
214
215 pattern P :: () => Eq a => a -> [T a]
216 pattern P x = [MkT x]
217
218 We must check that the (Eq a) that P claims to bind (and to
219 make available to matches against P), is derivable from the
220 actual pattern. For example:
221 f (P (x::a)) = ...here (Eq a) should be available...
222 And yes, (Eq a) is derivable from the (Ord a) bound by P's rhs.
223
224 ----- Existential type variables
225 Unusually, we instantiate the existential tyvars of the pattern with
226 *meta* type variables. For example
227
228 data S where
229 MkS :: Eq a => [a] -> S
230
231 pattern P :: () => Eq x => x -> S
232 pattern P x <- MkS x
233
234 The pattern synonym conceals from its client the fact that MkS has a
235 list inside it. The client just thinks it's a type 'x'. So we must
236 unify x := [a] during type checking, and then use the instantiating type
237 [a] (called ex_tys) when building the matcher. In this case we'll get
238
239 $mP :: S -> (forall x. Ex x => x -> r) -> r -> r
240 $mP x k = case x of
241 MkS a (d:Eq a) (ys:[a]) -> let dl :: Eq [a]
242 dl = $dfunEqList d
243 in k [a] dl ys
244
245 This "concealing" story works for /uni-directional/ pattern synonmys,
246 but obviously not for bidirectional ones. So in the bidirectional case
247 we use SigTv, rather than a generic TauTv, meta-tyvar so that. And
248 we should really check that those SigTvs don't get unified with each
249 other.
250
251 -}
252
253 collectPatSynArgInfo :: HsPatSynDetails (Located Name) -> ([Name], [Name], Bool)
254 collectPatSynArgInfo details =
255 case details of
256 PrefixPatSyn names -> (map unLoc names, [], False)
257 InfixPatSyn name1 name2 -> (map unLoc [name1, name2], [], True)
258 RecordPatSyn names ->
259 let (vars, sels) = unzip (map splitRecordPatSyn names)
260 in (vars, sels, False)
261
262 where
263 splitRecordPatSyn :: RecordPatSynField (Located Name) -> (Name, Name)
264 splitRecordPatSyn (RecordPatSynField { recordPatSynPatVar = L _ patVar
265 , recordPatSynSelectorId = L _ selId })
266 = (patVar, selId)
267
268 addPatSynCtxt :: Located Name -> TcM a -> TcM a
269 addPatSynCtxt (L loc name) thing_inside
270 = setSrcSpan loc $
271 addErrCtxt (text "In the declaration for pattern synonym"
272 <+> quotes (ppr name)) $
273 thing_inside
274
275 wrongNumberOfParmsErr :: Name -> Arity -> Arity -> TcM a
276 wrongNumberOfParmsErr name decl_arity missing
277 = failWithTc $
278 hang (text "Pattern synonym" <+> quotes (ppr name) <+> ptext (sLit "has")
279 <+> speakNOf decl_arity (text "argument"))
280 2 (text "but its type signature has" <+> int missing <+> text "fewer arrows")
281
282 -------------------------
283 -- Shared by both tcInferPatSyn and tcCheckPatSyn
284 tc_patsyn_finish :: Located Name -- ^ PatSyn Name
285 -> HsPatSynDir Name -- ^ PatSyn type (Uni/Bidir/ExplicitBidir)
286 -> Bool -- ^ Whether infix
287 -> LPat Id -- ^ Pattern of the PatSyn
288 -> ([TcTyVarBinder], [PredType], TcEvBinds, [EvVar])
289 -> ([TcTyVarBinder], [TcType], [PredType], [EvTerm])
290 -> ([LHsExpr TcId], [TcType]) -- ^ Pattern arguments and types
291 -> TcType -- ^ Pattern type
292 -> [Name] -- ^ Selector names
293 -- ^ Whether fields, empty if not record PatSyn
294 -> TcM (LHsBinds Id, TcGblEnv)
295 tc_patsyn_finish lname dir is_infix lpat'
296 (univ_bndrs, req_theta, req_ev_binds, req_dicts)
297 (ex_bndrs, ex_tys, prov_theta, prov_dicts)
298 (args, arg_tys)
299 pat_ty field_labels
300 = do { -- Zonk everything. We are about to build a final PatSyn
301 -- so there had better be no unification variables in there
302 univ_tvs' <- mapMaybeM zonk_qtv univ_bndrs
303 ; ex_tvs' <- mapMaybeM zonk_qtv ex_bndrs
304 ; prov_theta' <- zonkTcTypes prov_theta
305 ; req_theta' <- zonkTcTypes req_theta
306 ; pat_ty' <- zonkTcType pat_ty
307 ; arg_tys' <- zonkTcTypes arg_tys
308
309 ; let (env1, univ_tvs) = tidyTyVarBinders emptyTidyEnv univ_tvs'
310 (env2, ex_tvs) = tidyTyVarBinders env1 ex_tvs'
311 req_theta = tidyTypes env2 req_theta'
312 prov_theta = tidyTypes env2 prov_theta'
313 arg_tys = tidyTypes env2 arg_tys'
314 pat_ty = tidyType env2 pat_ty'
315
316 ; traceTc "tc_patsyn_finish {" $
317 ppr (unLoc lname) $$ ppr (unLoc lpat') $$
318 ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
319 ppr (ex_tvs, prov_theta, prov_dicts) $$
320 ppr args $$
321 ppr arg_tys $$
322 ppr pat_ty
323
324 -- Make the 'matcher'
325 ; (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat'
326 (map binderVar univ_tvs, req_theta, req_ev_binds, req_dicts)
327 (map binderVar ex_tvs, ex_tys, prov_theta, prov_dicts)
328 (args, arg_tys)
329 pat_ty
330
331
332 -- Make the 'builder'
333 ; builder_id <- mkPatSynBuilderId dir lname
334 univ_tvs req_theta
335 ex_tvs prov_theta
336 arg_tys pat_ty
337
338 -- TODO: Make this have the proper information
339 ; let mkFieldLabel name = FieldLabel { flLabel = occNameFS (nameOccName name)
340 , flIsOverloaded = False
341 , flSelector = name }
342 field_labels' = map mkFieldLabel field_labels
343
344 -- Make the PatSyn itself
345 ; let patSyn = mkPatSyn (unLoc lname) is_infix
346 (univ_tvs, req_theta)
347 (ex_tvs, prov_theta)
348 arg_tys
349 pat_ty
350 matcher_id builder_id
351 field_labels'
352
353 -- Selectors
354 ; let rn_rec_sel_binds = mkPatSynRecSelBinds patSyn (patSynFieldLabels patSyn)
355 tything = AConLike (PatSynCon patSyn)
356 ; tcg_env <- tcExtendGlobalEnv [tything] $
357 tcRecSelBinds rn_rec_sel_binds
358
359 ; traceTc "tc_patsyn_finish }" empty
360 ; return (matcher_bind, tcg_env) }
361 where
362 -- This is a bit of an odd functions; why does it not occur elsewhere
363 zonk_qtv :: TcTyVarBinder -> TcM (Maybe TcTyVarBinder)
364 zonk_qtv (TvBndr tv vis)
365 = do { mb_tv' <- zonkQuantifiedTyVar False tv
366 -- ToDo: The False means that we behave here as if
367 -- -XPolyKinds was always on, which isn't right.
368 ; return (fmap (\tv' -> TvBndr tv' vis) mb_tv') }
369
370 {-
371 ************************************************************************
372 * *
373 Constructing the "matcher" Id and its binding
374 * *
375 ************************************************************************
376 -}
377
378 tcPatSynMatcher :: Located Name
379 -> LPat Id
380 -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
381 -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
382 -> ([LHsExpr TcId], [TcType])
383 -> TcType
384 -> TcM ((Id, Bool), LHsBinds Id)
385 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
386 tcPatSynMatcher (L loc name) lpat
387 (univ_tvs, req_theta, req_ev_binds, req_dicts)
388 (ex_tvs, ex_tys, prov_theta, prov_dicts)
389 (args, arg_tys) pat_ty
390 = do { rr_name <- newNameAt (mkTyVarOcc "rep") loc
391 ; tv_name <- newNameAt (mkTyVarOcc "r") loc
392 ; let rr_tv = mkTcTyVar rr_name runtimeRepTy (SkolemTv False)
393 rr = mkTyVarTy rr_tv
394 res_tv = mkTcTyVar tv_name (tYPE rr) (SkolemTv False)
395 is_unlifted = null args && null prov_dicts
396 res_ty = mkTyVarTy res_tv
397 (cont_args, cont_arg_tys)
398 | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
399 | otherwise = (args, arg_tys)
400 cont_ty = mkInvSigmaTy ex_tvs prov_theta $
401 mkFunTys cont_arg_tys res_ty
402
403 fail_ty = mkFunTy voidPrimTy res_ty
404
405 ; matcher_name <- newImplicitBinder name mkMatcherOcc
406 ; scrutinee <- newSysLocalId (fsLit "scrut") pat_ty
407 ; cont <- newSysLocalId (fsLit "cont") cont_ty
408 ; fail <- newSysLocalId (fsLit "fail") fail_ty
409
410 ; let matcher_tau = mkFunTys [pat_ty, cont_ty, fail_ty] res_ty
411 matcher_sigma = mkInvSigmaTy (rr_tv:res_tv:univ_tvs) req_theta matcher_tau
412 matcher_id = mkExportedVanillaId matcher_name matcher_sigma
413 -- See Note [Exported LocalIds] in Id
414
415 inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys
416 cont' = foldl nlHsApp (mkLHsWrap inst_wrap (nlHsVar cont)) cont_args
417
418 fail' = nlHsApps fail [nlHsVar voidPrimId]
419
420 args = map nlVarPat [scrutinee, cont, fail]
421 lwpat = noLoc $ WildPat pat_ty
422 cases = if isIrrefutableHsPat lpat
423 then [mkHsCaseAlt lpat cont']
424 else [mkHsCaseAlt lpat cont',
425 mkHsCaseAlt lwpat fail']
426 body = mkLHsWrap (mkWpLet req_ev_binds) $
427 L (getLoc lpat) $
428 HsCase (nlHsVar scrutinee) $
429 MG{ mg_alts = L (getLoc lpat) cases
430 , mg_arg_tys = [pat_ty]
431 , mg_res_ty = res_ty
432 , mg_origin = Generated
433 }
434 body' = noLoc $
435 HsLam $
436 MG{ mg_alts = noLoc [mkSimpleMatch LambdaExpr
437 args body]
438 , mg_arg_tys = [pat_ty, cont_ty, res_ty]
439 , mg_res_ty = res_ty
440 , mg_origin = Generated
441 }
442 match = mkMatch (FunRhs (L loc name) Prefix) []
443 (mkHsLams (rr_tv:res_tv:univ_tvs)
444 req_dicts body')
445 (noLoc EmptyLocalBinds)
446 mg = MG{ mg_alts = L (getLoc match) [match]
447 , mg_arg_tys = []
448 , mg_res_ty = res_ty
449 , mg_origin = Generated
450 }
451
452 ; let bind = FunBind{ fun_id = L loc matcher_id
453 , fun_matches = mg
454 , fun_co_fn = idHsWrapper
455 , bind_fvs = emptyNameSet
456 , fun_tick = [] }
457 matcher_bind = unitBag (noLoc bind)
458
459 ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
460 ; traceTc "tcPatSynMatcher" (ppr matcher_bind)
461
462 ; return ((matcher_id, is_unlifted), matcher_bind) }
463
464 mkPatSynRecSelBinds :: PatSyn
465 -> [FieldLabel] -- ^ Visible field labels
466 -> HsValBinds Name
467 mkPatSynRecSelBinds ps fields
468 = ValBindsOut selector_binds sigs
469 where
470 (sigs, selector_binds) = unzip (map mkRecSel fields)
471 mkRecSel fld_lbl = mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl
472
473 isUnidirectional :: HsPatSynDir a -> Bool
474 isUnidirectional Unidirectional = True
475 isUnidirectional ImplicitBidirectional = False
476 isUnidirectional ExplicitBidirectional{} = False
477
478 {-
479 ************************************************************************
480 * *
481 Constructing the "builder" Id
482 * *
483 ************************************************************************
484 -}
485
486 mkPatSynBuilderId :: HsPatSynDir a -> Located Name
487 -> [TyVarBinder] -> ThetaType
488 -> [TyVarBinder] -> ThetaType
489 -> [Type] -> Type
490 -> TcM (Maybe (Id, Bool))
491 mkPatSynBuilderId dir (L _ name)
492 univ_bndrs req_theta ex_bndrs prov_theta
493 arg_tys pat_ty
494 | isUnidirectional dir
495 = return Nothing
496 | otherwise
497 = do { builder_name <- newImplicitBinder name mkBuilderOcc
498 ; let theta = req_theta ++ prov_theta
499 need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
500 builder_sigma = add_void need_dummy_arg $
501 mkForAllTys univ_bndrs $
502 mkForAllTys ex_bndrs $
503 mkFunTys theta $
504 mkFunTys arg_tys $
505 pat_ty
506 builder_id = mkExportedVanillaId builder_name builder_sigma
507 -- See Note [Exported LocalIds] in Id
508
509 ; return (Just (builder_id, need_dummy_arg)) }
510 where
511
512 tcPatSynBuilderBind :: PatSynBind Name Name
513 -> TcM (LHsBinds Id)
514 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
515 tcPatSynBuilderBind (PSB { psb_id = L loc name, psb_def = lpat
516 , psb_dir = dir, psb_args = details })
517 | isUnidirectional dir
518 = return emptyBag
519
520 | Left why <- mb_match_group -- Can't invert the pattern
521 = setSrcSpan (getLoc lpat) $ failWithTc $
522 vcat [ hang (text "Invalid right-hand side of bidirectional pattern synonym"
523 <+> quotes (ppr name) <> colon)
524 2 why
525 , text "RHS pattern:" <+> ppr lpat ]
526
527 | Right match_group <- mb_match_group -- Bidirectional
528 = do { patsyn <- tcLookupPatSyn name
529 ; traceTc "tcPatSynBuilderBind {" $ ppr patsyn
530 ; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn
531 -- Bidirectional, so patSynBuilder returns Just
532
533 match_group' | need_dummy_arg = add_dummy_arg match_group
534 | otherwise = match_group
535
536 bind = FunBind { fun_id = L loc (idName builder_id)
537 , fun_matches = match_group'
538 , fun_co_fn = idHsWrapper
539 , bind_fvs = placeHolderNamesTc
540 , fun_tick = [] }
541
542 sig = completeSigFromId (PatSynCtxt name) builder_id
543
544 ; (builder_binds, _) <- tcPolyCheck emptyPragEnv sig (noLoc bind)
545 ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
546 ; return builder_binds }
547
548 | otherwise = panic "tcPatSynBuilderBind" -- Both cases dealt with
549 where
550 mb_match_group
551 = case dir of
552 ExplicitBidirectional explicit_mg -> Right explicit_mg
553 ImplicitBidirectional -> fmap mk_mg (tcPatToExpr args lpat)
554 Unidirectional -> panic "tcPatSynBuilderBind"
555
556 mk_mg :: LHsExpr Name -> MatchGroup Name (LHsExpr Name)
557 mk_mg body = mkMatchGroupName Generated [builder_match]
558 where
559 builder_args = [L loc (VarPat (L loc n)) | L loc n <- args]
560 builder_match = mkMatch (FunRhs (L loc name) Prefix)
561 builder_args body
562 (noLoc EmptyLocalBinds)
563
564 args = case details of
565 PrefixPatSyn args -> args
566 InfixPatSyn arg1 arg2 -> [arg1, arg2]
567 RecordPatSyn args -> map recordPatSynPatVar args
568
569 add_dummy_arg :: MatchGroup Name (LHsExpr Name)
570 -> MatchGroup Name (LHsExpr Name)
571 add_dummy_arg mg@(MG { mg_alts = L l [L loc match@(Match { m_pats = pats })] })
572 = mg { mg_alts = L l [L loc (match { m_pats = nlWildPatName : pats })] }
573 add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
574 pprMatches other_mg
575
576 tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr TcId, TcSigmaType)
577 -- monadic only for failure
578 tcPatSynBuilderOcc ps
579 | Just (builder_id, add_void_arg) <- builder
580 , let builder_expr = HsVar (noLoc builder_id)
581 builder_ty = idType builder_id
582 = return $
583 if add_void_arg
584 then ( HsApp (noLoc $ builder_expr) (nlHsVar voidPrimId)
585 , tcFunResultTy builder_ty )
586 else (builder_expr, builder_ty)
587
588 | otherwise -- Unidirectional
589 = nonBidirectionalErr name
590 where
591 name = patSynName ps
592 builder = patSynBuilder ps
593
594 add_void :: Bool -> Type -> Type
595 add_void need_dummy_arg ty
596 | need_dummy_arg = mkFunTy voidPrimTy ty
597 | otherwise = ty
598
599 tcPatToExpr :: [Located Name] -> LPat Name -> Either MsgDoc (LHsExpr Name)
600 -- Given a /pattern/, return an /expression/ that builds a value
601 -- that matches the pattern. E.g. if the pattern is (Just [x]),
602 -- the expression is (Just [x]). They look the same, but the
603 -- input uses constructors from HsPat and the output uses constructors
604 -- from HsExpr.
605 --
606 -- Returns (Left r) if the pattern is not invertible, for reason r.
607 -- See Note [Builder for a bidirectional pattern synonym]
608 tcPatToExpr args pat = go pat
609 where
610 lhsVars = mkNameSet (map unLoc args)
611
612 -- Make a prefix con for prefix and infix patterns for simplicity
613 mkPrefixConExpr :: Located Name -> [LPat Name] -> Either MsgDoc (HsExpr Name)
614 mkPrefixConExpr lcon@(L loc _) pats
615 = do { exprs <- mapM go pats
616 ; return (foldl (\x y -> HsApp (L loc x) y)
617 (HsVar lcon) exprs) }
618
619 mkRecordConExpr :: Located Name -> HsRecFields Name (LPat Name)
620 -> Either MsgDoc (HsExpr Name)
621 mkRecordConExpr con fields
622 = do { exprFields <- mapM go fields
623 ; return (RecordCon con PlaceHolder noPostTcExpr exprFields) }
624
625 go :: LPat Name -> Either MsgDoc (LHsExpr Name)
626 go (L loc p) = L loc <$> go1 p
627
628 go1 :: Pat Name -> Either MsgDoc (HsExpr Name)
629 go1 (ConPatIn con info)
630 = case info of
631 PrefixCon ps -> mkPrefixConExpr con ps
632 InfixCon l r -> mkPrefixConExpr con [l,r]
633 RecCon fields -> mkRecordConExpr con fields
634
635 go1 (SigPatIn pat _) = go1 (unLoc pat)
636 -- See Note [Type signatures and the builder expression]
637
638 go1 (VarPat (L l var))
639 | var `elemNameSet` lhsVars
640 = return $ HsVar (L l var)
641 | otherwise
642 = Left (quotes (ppr var) <+> text "is not bound by the LHS of the pattern synonym")
643 go1 (ParPat pat) = fmap HsPar $ go pat
644 go1 (LazyPat pat) = go1 (unLoc pat)
645 go1 (BangPat pat) = go1 (unLoc pat)
646 go1 (PArrPat pats ptt) = do { exprs <- mapM go pats
647 ; return $ ExplicitPArr ptt exprs }
648 go1 (ListPat pats ptt reb) = do { exprs <- mapM go pats
649 ; return $ ExplicitList ptt (fmap snd reb) exprs }
650 go1 (TuplePat pats box _) = do { exprs <- mapM go pats
651 ; return $ ExplicitTuple
652 (map (noLoc . Present) exprs) box }
653 go1 (LitPat lit) = return $ HsLit lit
654 go1 (NPat (L _ n) mb_neg _ _)
655 | Just neg <- mb_neg = return $ unLoc $ nlHsSyntaxApps neg [noLoc (HsOverLit n)]
656 | otherwise = return $ HsOverLit n
657 go1 (ConPatOut{}) = panic "ConPatOut in output of renamer"
658 go1 (SigPatOut{}) = panic "SigPatOut in output of renamer"
659 go1 (CoPat{}) = panic "CoPat in output of renamer"
660 go1 p = Left (text "pattern" <+> quotes (ppr p) <+> text "is not invertible")
661
662 {- Note [Builder for a bidirectional pattern synonym]
663 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
664 For a bidirectional pattern synonym we need to produce an /expression/
665 that matches the supplied /pattern/, given values for the arguments
666 of the pattern synoymy. For example
667 pattern F x y = (Just x, [y])
668 The 'builder' for F looks like
669 $builderF x y = (Just x, [y])
670
671 We can't always do this:
672 * Some patterns aren't invertible; e.g. view patterns
673 pattern F x = (reverse -> x:_)
674
675 * The RHS pattern might bind more variables than the pattern
676 synonym, so again we can't invert it
677 pattern F x = (x,y)
678
679 * Ditto wildcards
680 pattern F x = (x,_)
681
682
683 Note [Redundant constraints for builder]
684 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
685 The builder can have redundant constraints, which are awkard to eliminate.
686 Consider
687 pattern P = Just 34
688 To match against this pattern we need (Eq a, Num a). But to build
689 (Just 34) we need only (Num a). Fortunately instTcSigFromId sets
690 sig_warn_redundant to False.
691
692 ************************************************************************
693 * *
694 Helper functions
695 * *
696 ************************************************************************
697
698 Note [As-patterns in pattern synonym definitions]
699 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
700 The rationale for rejecting as-patterns in pattern synonym definitions
701 is that an as-pattern would introduce nonindependent pattern synonym
702 arguments, e.g. given a pattern synonym like:
703
704 pattern K x y = x@(Just y)
705
706 one could write a nonsensical function like
707
708 f (K Nothing x) = ...
709
710 or
711 g (K (Just True) False) = ...
712
713 Note [Type signatures and the builder expression]
714 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
715 Consider
716 pattern L x = Left x :: Either [a] [b]
717
718 In tc{Infer/Check}PatSynDecl we will check that the pattern has the
719 specified type. We check the pattern *as a pattern*, so the type
720 signature is a pattern signature, and so brings 'a' and 'b' into
721 scope. But we don't have a way to bind 'a, b' in the LHS, as we do
722 'x', say. Nevertheless, the sigature may be useful to constrain
723 the type.
724
725 When making the binding for the *builder*, though, we don't want
726 $buildL x = Left x :: Either [a] [b]
727 because that wil either mean (forall a b. Either [a] [b]), or we'll
728 get a complaint that 'a' and 'b' are out of scope. (Actually the
729 latter; Trac #9867.) No, the job of the signature is done, so when
730 converting the pattern to an expression (for the builder RHS) we
731 simply discard the signature.
732
733 Note [Record PatSyn Desugaring]
734 -------------------------------
735 It is important that prov_theta comes before req_theta as this ordering is used
736 when desugaring record pattern synonym updates.
737
738 Any change to this ordering should make sure to change deSugar/DsExpr.hs if you
739 want to avoid difficult to decipher core lint errors!
740 -}
741
742 tcCheckPatSynPat :: LPat Name -> TcM ()
743 tcCheckPatSynPat = go
744 where
745 go :: LPat Name -> TcM ()
746 go = addLocM go1
747
748 go1 :: Pat Name -> TcM ()
749 go1 (ConPatIn _ info) = mapM_ go (hsConPatArgs info)
750 go1 VarPat{} = return ()
751 go1 WildPat{} = return ()
752 go1 p@(AsPat _ _) = asPatInPatSynErr p
753 go1 (LazyPat pat) = go pat
754 go1 (ParPat pat) = go pat
755 go1 (BangPat pat) = go pat
756 go1 (PArrPat pats _) = mapM_ go pats
757 go1 (ListPat pats _ _) = mapM_ go pats
758 go1 (TuplePat pats _ _) = mapM_ go pats
759 go1 LitPat{} = return ()
760 go1 NPat{} = return ()
761 go1 (SigPatIn pat _) = go pat
762 go1 (ViewPat _ pat _) = go pat
763 go1 p@SplicePat{} = thInPatSynErr p
764 go1 p@NPlusKPat{} = nPlusKPatInPatSynErr p
765 go1 ConPatOut{} = panic "ConPatOut in output of renamer"
766 go1 SigPatOut{} = panic "SigPatOut in output of renamer"
767 go1 CoPat{} = panic "CoPat in output of renamer"
768
769 asPatInPatSynErr :: (OutputableBndrId name) => Pat name -> TcM a
770 asPatInPatSynErr pat
771 = failWithTc $
772 hang (text "Pattern synonym definition cannot contain as-patterns (@):")
773 2 (ppr pat)
774
775 thInPatSynErr :: (OutputableBndrId name) => Pat name -> TcM a
776 thInPatSynErr pat
777 = failWithTc $
778 hang (text "Pattern synonym definition cannot contain Template Haskell:")
779 2 (ppr pat)
780
781 nPlusKPatInPatSynErr :: (OutputableBndrId name) => Pat name -> TcM a
782 nPlusKPatInPatSynErr pat
783 = failWithTc $
784 hang (text "Pattern synonym definition cannot contain n+k-pattern:")
785 2 (ppr pat)
786
787 nonBidirectionalErr :: Outputable name => name -> TcM a
788 nonBidirectionalErr name = failWithTc $
789 text "non-bidirectional pattern synonym"
790 <+> quotes (ppr name) <+> text "used in an expression"
791
792 -- Walk the whole pattern and for all ConPatOuts, collect the
793 -- existentially-bound type variables and evidence binding variables.
794 --
795 -- These are used in computing the type of a pattern synonym and also
796 -- in generating matcher functions, since success continuations need
797 -- to be passed these pattern-bound evidences.
798 tcCollectEx
799 :: LPat Id
800 -> ( ([Var], VarSet) -- Existentially-bound type variables as a
801 -- deterministically ordered list and a set.
802 -- See Note [Deterministic FV] in FV
803 , [EvVar]
804 )
805 tcCollectEx pat = let (fv, evs) = go pat in (fvVarListVarSet fv, evs)
806 where
807 go :: LPat Id -> (FV, [EvVar])
808 go = go1 . unLoc
809
810 go1 :: Pat Id -> (FV, [EvVar])
811 go1 (LazyPat p) = go p
812 go1 (AsPat _ p) = go p
813 go1 (ParPat p) = go p
814 go1 (BangPat p) = go p
815 go1 (ListPat ps _ _) = mergeMany . map go $ ps
816 go1 (TuplePat ps _ _) = mergeMany . map go $ ps
817 go1 (PArrPat ps _) = mergeMany . map go $ ps
818 go1 (ViewPat _ p _) = go p
819 go1 con@ConPatOut{} = merge (FV.mkFVs (pat_tvs con), pat_dicts con) $
820 goConDetails $ pat_args con
821 go1 (SigPatOut p _) = go p
822 go1 (CoPat _ p _) = go1 p
823 go1 (NPlusKPat n k _ geq subtract _)
824 = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract
825 go1 _ = empty
826
827 goConDetails :: HsConPatDetails Id -> (FV, [EvVar])
828 goConDetails (PrefixCon ps) = mergeMany . map go $ ps
829 goConDetails (InfixCon p1 p2) = go p1 `merge` go p2
830 goConDetails (RecCon HsRecFields{ rec_flds = flds })
831 = mergeMany . map goRecFd $ flds
832
833 goRecFd :: LHsRecField Id (LPat Id) -> (FV, [EvVar])
834 goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p
835
836 merge (vs1, evs1) (vs2, evs2) = (vs1 `unionFV` vs2, evs1 ++ evs2)
837 mergeMany = foldr merge empty
838 empty = (emptyFV, [])