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