Refactor the treatment of predicate types
[ghc.git] / compiler / typecheck / TcPatSyn.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5 \section[TcPatSyn]{Typechecking pattern synonym declarations}
6 -}
7
8 {-# LANGUAGE CPP #-}
9 {-# LANGUAGE FlexibleContexts #-}
10 {-# LANGUAGE TypeFamilies #-}
11
12 module TcPatSyn ( tcPatSynDecl, tcPatSynBuilderBind
13 , tcPatSynBuilderOcc, nonBidirectionalErr
14 ) where
15
16 import GhcPrelude
17
18 import HsSyn
19 import TcPat
20 import Type( mkEmptyTCvSubst, tidyTyCoVarBinders, tidyTypes, tidyType )
21 import TcRnMonad
22 import TcSigs( emptyPragEnv, completeSigFromId )
23 import TcType( mkMinimalBySCs )
24 import TcEnv
25 import TcMType
26 import TcHsSyn
27 import TysPrim
28 import TysWiredIn ( runtimeRepTy )
29 import Name
30 import SrcLoc
31 import PatSyn
32 import NameSet
33 import Panic
34 import Outputable
35 import FastString
36 import Var
37 import VarEnv( emptyTidyEnv, mkInScopeSet )
38 import Id
39 import IdInfo( RecSelParent(..), setLevityInfoWithType )
40 import TcBinds
41 import BasicTypes
42 import TcSimplify
43 import TcUnify
44 import Type( PredTree(..), EqRel(..), classifyPredType )
45 import TysWiredIn
46 import TcType
47 import TcEvidence
48 import BuildTyCl
49 import VarSet
50 import MkId
51 import TcTyDecls
52 import ConLike
53 import FieldLabel
54 import Bag
55 import Util
56 import ErrUtils
57 import Data.Maybe( mapMaybe )
58 import Control.Monad ( zipWithM )
59 import Data.List( partition )
60
61 #include "HsVersions.h"
62
63 {-
64 ************************************************************************
65 * *
66 Type checking a pattern synonym
67 * *
68 ************************************************************************
69 -}
70
71 tcPatSynDecl :: PatSynBind GhcRn GhcRn
72 -> Maybe TcSigInfo
73 -> TcM (LHsBinds GhcTc, TcGblEnv)
74 tcPatSynDecl psb mb_sig
75 = recoverM (recoverPSB psb) $
76 case mb_sig of
77 Nothing -> tcInferPatSynDecl psb
78 Just (TcPatSynSig tpsi) -> tcCheckPatSynDecl psb tpsi
79 _ -> panic "tcPatSynDecl"
80
81 recoverPSB :: PatSynBind GhcRn GhcRn
82 -> TcM (LHsBinds GhcTc, TcGblEnv)
83 -- See Note [Pattern synonym error recovery]
84 recoverPSB (PSB { psb_id = L _ name, psb_args = details })
85 = do { matcher_name <- newImplicitBinder name mkMatcherOcc
86 ; let placeholder = AConLike $ PatSynCon $
87 mk_placeholder matcher_name
88 ; gbl_env <- tcExtendGlobalEnv [placeholder] getGblEnv
89 ; return (emptyBag, gbl_env) }
90 where
91 (_arg_names, _rec_fields, is_infix) = collectPatSynArgInfo details
92 mk_placeholder matcher_name
93 = mkPatSyn name is_infix
94 ([mkTyVarBinder Specified alphaTyVar], []) ([], [])
95 [] -- Arg tys
96 alphaTy
97 (matcher_id, True) Nothing
98 [] -- Field labels
99 where
100 -- The matcher_id is used only by the desugarer, so actually
101 -- and error-thunk would probably do just as well here.
102 matcher_id = mkLocalId matcher_name $
103 mkSpecForAllTys [alphaTyVar] alphaTy
104
105 recoverPSB (XPatSynBind {}) = panic "recoverPSB"
106
107 {- Note [Pattern synonym error recovery]
108 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
109 If type inference for a pattern synonym fails, we can't continue with
110 the rest of tc_patsyn_finish, because we may get knock-on errors, or
111 even a crash. E.g. from
112 pattern What = True :: Maybe
113 we get a kind error; and we must stop right away (Trac #15289).
114
115 We stop if there are /any/ unsolved constraints, not just insoluble
116 ones; because pattern synonyms are top-level things, we will never
117 solve them later if we can't solve them now. And if we were to carry
118 on, tc_patsyn_finish does zonkTcTypeToType, which defaults any
119 unsolved unificatdion variables to Any, which confuses the error
120 reporting no end (Trac #15685).
121
122 So we use simplifyTop to completely solve the constraint, report
123 any errors, throw an exception.
124
125 Even in the event of such an error we can recover and carry on, just
126 as we do for value bindings, provided we plug in placeholder for the
127 pattern synonym: see recoverPSB. The goal of the placeholder is not
128 to cause a raft of follow-on errors. I've used the simplest thing for
129 now, but we might need to elaborate it a bit later. (e.g. I've given
130 it zero args, which may cause knock-on errors if it is used in a
131 pattern.) But it'll do for now.
132
133 -}
134
135 tcInferPatSynDecl :: PatSynBind GhcRn GhcRn
136 -> TcM (LHsBinds GhcTc, TcGblEnv)
137 tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details
138 , psb_def = lpat, psb_dir = dir })
139 = addPatSynCtxt lname $
140 do { traceTc "tcInferPatSynDecl {" $ ppr name
141
142 ; let (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
143 ; (tclvl, wanted, ((lpat', args), pat_ty))
144 <- pushLevelAndCaptureConstraints $
145 tcInferNoInst $ \ exp_ty ->
146 tcPat PatSyn lpat exp_ty $
147 mapM tcLookupId arg_names
148
149 ; let named_taus = (name, pat_ty) : map (\arg -> (getName arg, varType arg)) args
150
151 ; (qtvs, req_dicts, ev_binds, residual, _)
152 <- simplifyInfer tclvl NoRestrictions [] named_taus wanted
153 ; top_ev_binds <- checkNoErrs (simplifyTop residual)
154 ; addTopEvBinds top_ev_binds $
155
156 do { let (ex_tvs, prov_dicts) = tcCollectEx lpat'
157 ex_tv_set = mkVarSet ex_tvs
158 univ_tvs = filterOut (`elemVarSet` ex_tv_set) qtvs
159 req_theta = map evVarPred req_dicts
160
161 ; prov_dicts <- mapM zonkId prov_dicts
162 ; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts
163 -- Filtering: see Note [Remove redundant provided dicts]
164 (prov_theta, prov_evs)
165 = unzip (mapMaybe mkProvEvidence filtered_prov_dicts)
166
167 -- Report bad universal type variables
168 -- See Note [Type variables whose kind is captured]
169 ; let bad_tvs = [ tv | tv <- univ_tvs
170 , tyCoVarsOfType (tyVarKind tv)
171 `intersectsVarSet` ex_tv_set ]
172 ; mapM_ (badUnivTvErr ex_tvs) bad_tvs
173
174 -- Report coercions that esacpe
175 -- See Note [Coercions that escape]
176 ; args <- mapM zonkId args
177 ; let bad_args = [ (arg, bad_cos) | arg <- args ++ prov_dicts
178 , let bad_cos = filterDVarSet isId $
179 (tyCoVarsOfTypeDSet (idType arg))
180 , not (isEmptyDVarSet bad_cos) ]
181 ; mapM_ dependentArgErr bad_args
182
183 ; traceTc "tcInferPatSynDecl }" $ (ppr name $$ ppr ex_tvs)
184 ; tc_patsyn_finish lname dir is_infix lpat'
185 (mkTyVarBinders Inferred univ_tvs
186 , req_theta, ev_binds, req_dicts)
187 (mkTyVarBinders Inferred ex_tvs
188 , mkTyVarTys ex_tvs, prov_theta, prov_evs)
189 (map nlHsVar args, map idType args)
190 pat_ty rec_fields } }
191 tcInferPatSynDecl (XPatSynBind _) = panic "tcInferPatSynDecl"
192
193 mkProvEvidence :: EvId -> Maybe (PredType, EvTerm)
194 -- See Note [Equality evidence in pattern synonyms]
195 mkProvEvidence ev_id
196 | EqPred r ty1 ty2 <- classifyPredType pred
197 , let k1 = typeKind ty1
198 k2 = typeKind ty2
199 is_homo = k1 `tcEqType` k2
200 homo_tys = [k1, ty1, ty2]
201 hetero_tys = [k1, k2, ty1, ty2]
202 = case r of
203 ReprEq | is_homo
204 -> Just ( mkClassPred coercibleClass homo_tys
205 , evDataConApp coercibleDataCon homo_tys eq_con_args )
206 | otherwise -> Nothing
207 NomEq | is_homo
208 -> Just ( mkClassPred eqClass homo_tys
209 , evDataConApp eqDataCon homo_tys eq_con_args )
210 | otherwise
211 -> Just ( mkClassPred heqClass hetero_tys
212 , evDataConApp heqDataCon hetero_tys eq_con_args )
213
214 | otherwise
215 = Just (pred, EvExpr (evId ev_id))
216 where
217 pred = evVarPred ev_id
218 eq_con_args = [evId ev_id]
219
220 badUnivTvErr :: [TyVar] -> TyVar -> TcM ()
221 -- See Note [Type variables whose kind is captured]
222 badUnivTvErr ex_tvs bad_tv
223 = addErrTc $
224 vcat [ text "Universal type variable" <+> quotes (ppr bad_tv)
225 <+> text "has existentially bound kind:"
226 , nest 2 (ppr_with_kind bad_tv)
227 , hang (text "Existentially-bound variables:")
228 2 (vcat (map ppr_with_kind ex_tvs))
229 , text "Probable fix: give the pattern synonym a type signature"
230 ]
231 where
232 ppr_with_kind tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
233
234 dependentArgErr :: (Id, DTyCoVarSet) -> TcM ()
235 -- See Note [Coercions that escape]
236 dependentArgErr (arg, bad_cos)
237 = addErrTc $
238 vcat [ text "Iceland Jack! Iceland Jack! Stop torturing me!"
239 , hang (text "Pattern-bound variable")
240 2 (ppr arg <+> dcolon <+> ppr (idType arg))
241 , nest 2 $
242 hang (text "has a type that mentions pattern-bound coercion"
243 <> plural bad_co_list <> colon)
244 2 (pprWithCommas ppr bad_co_list)
245 , text "Hint: use -fprint-explicit-coercions to see the coercions"
246 , text "Probable fix: add a pattern signature" ]
247 where
248 bad_co_list = dVarSetElems bad_cos
249
250 {- Note [Remove redundant provided dicts]
251 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
252 Recall that
253 HRefl :: forall k1 k2 (a1:k1) (a2:k2). (k1 ~ k2, a1 ~ a2)
254 => a1 :~~: a2
255 (NB: technically the (k1~k2) existential dictionary is not necessary,
256 but it's there at the moment.)
257
258 Now consider (Trac #14394):
259 pattern Foo = HRefl
260 in a non-poly-kinded module. We don't want to get
261 pattern Foo :: () => (* ~ *, b ~ a) => a :~~: b
262 with that redundant (* ~ *). We'd like to remove it; hence the call to
263 mkMinimalWithSCs.
264
265 Similarly consider
266 data S a where { MkS :: Ord a => a -> S a }
267 pattern Bam x y <- (MkS (x::a), MkS (y::a)))
268
269 The pattern (Bam x y) binds two (Ord a) dictionaries, but we only
270 need one. Agian mkMimimalWithSCs removes the redundant one.
271
272 Note [Equality evidence in pattern synonyms]
273 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
274 Consider
275 data X a where
276 MkX :: Eq a => [a] -> X (Maybe a)
277 pattern P x = MkG x
278
279 Then there is a danger that GHC will infer
280 P :: forall a. () =>
281 forall b. (a ~# Maybe b, Eq b) => [b] -> X a
282
283 The 'builder' for P, which is called in user-code, will then
284 have type
285 $bP :: forall a b. (a ~# Maybe b, Eq b) => [b] -> X a
286
287 and that is bad because (a ~# Maybe b) is not a predicate type
288 (see Note [Types for coercions, predicates, and evidence] in Type)
289 and is not implicitly instantiated.
290
291 So in mkProvEvidence we lift (a ~# b) to (a ~ b). Tiresome, and
292 marginally less efficient, if the builder/martcher are not inlined.
293
294 See also Note [Lift equality constaints when quantifying] in TcType
295
296 Note [Type variables whose kind is captured]
297 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
298 Consider
299 data AST a = Sym [a]
300 class Prj s where { prj :: [a] -> Maybe (s a)
301 pattern P x <= Sym (prj -> Just x)
302
303 Here we get a matcher with this type
304 $mP :: forall s a. Prj s => AST a -> (s a -> r) -> r -> r
305
306 No problem. But note that 's' is not fixed by the type of the
307 pattern (AST a), nor is it existentially bound. It's really only
308 fixed by the type of the continuation.
309
310 Trac #14552 showed that this can go wrong if the kind of 's' mentions
311 existentially bound variables. We obviously can't make a type like
312 $mP :: forall (s::k->*) a. Prj s => AST a -> (forall k. s a -> r)
313 -> r -> r
314 But neither is 's' itself existentially bound, so the forall (s::k->*)
315 can't go in the inner forall either. (What would the matcher apply
316 the continuation to?)
317
318 So we just fail in this case, with a pretty terrible error message.
319 Maybe we could do better, but I can't see how. (It'd be possible to
320 default 's' to (Any k), but that probably isn't what the user wanted,
321 and it not straightforward to implement, because by the time we see
322 the problem, simplifyInfer has already skolemised 's'.)
323
324 This stuff can only happen in the presence of view patterns, with
325 PolyKinds, so it's a bit of a corner case.
326
327 Note [Coercions that escape]
328 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
329 Trac #14507 showed an example where the inferred type of the matcher
330 for the pattern synonym was somethign like
331 $mSO :: forall (r :: TYPE rep) kk (a :: k).
332 TypeRep k a
333 -> ((Bool ~ k) => TypeRep Bool (a |> co_a2sv) -> r)
334 -> (Void# -> r)
335 -> r
336
337 What is that co_a2sv :: Bool ~# *?? It was bound (via a superclass
338 selection) by the pattern being matched; and indeed it is implicit in
339 the context (Bool ~ k). You could imagine trying to extract it like
340 this:
341 $mSO :: forall (r :: TYPE rep) kk (a :: k).
342 TypeRep k a
343 -> ( co :: ((Bool :: *) ~ (k :: *)) =>
344 let co_a2sv = sc_sel co
345 in TypeRep Bool (a |> co_a2sv) -> r)
346 -> (Void# -> r)
347 -> r
348
349 But we simply don't allow that in types. Maybe one day but not now.
350
351 How to detect this situation? We just look for free coercion variables
352 in the types of any of the arguments to the matcher. The error message
353 is not very helpful, but at least we don't get a Lint error.
354 -}
355
356 tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn
357 -> TcPatSynInfo
358 -> TcM (LHsBinds GhcTc, TcGblEnv)
359 tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
360 , psb_def = lpat, psb_dir = dir }
361 TPSI{ patsig_implicit_bndrs = implicit_tvs
362 , patsig_univ_bndrs = explicit_univ_tvs, patsig_prov = prov_theta
363 , patsig_ex_bndrs = explicit_ex_tvs, patsig_req = req_theta
364 , patsig_body_ty = sig_body_ty }
365 = addPatSynCtxt lname $
366 do { let decl_arity = length arg_names
367 (arg_names, rec_fields, is_infix) = collectPatSynArgInfo details
368
369 ; traceTc "tcCheckPatSynDecl" $
370 vcat [ ppr implicit_tvs, ppr explicit_univ_tvs, ppr req_theta
371 , ppr explicit_ex_tvs, ppr prov_theta, ppr sig_body_ty ]
372
373 ; (arg_tys, pat_ty) <- case tcSplitFunTysN decl_arity sig_body_ty of
374 Right stuff -> return stuff
375 Left missing -> wrongNumberOfParmsErr name decl_arity missing
376
377 -- Complain about: pattern P :: () => forall x. x -> P x
378 -- The existential 'x' should not appear in the result type
379 -- Can't check this until we know P's arity
380 ; let bad_tvs = filter (`elemVarSet` tyCoVarsOfType pat_ty) explicit_ex_tvs
381 ; checkTc (null bad_tvs) $
382 hang (sep [ text "The result type of the signature for" <+> quotes (ppr name) <> comma
383 , text "namely" <+> quotes (ppr pat_ty) ])
384 2 (text "mentions existential type variable" <> plural bad_tvs
385 <+> pprQuotedList bad_tvs)
386
387 -- See Note [The pattern-synonym signature splitting rule] in TcSigs
388 ; let univ_fvs = closeOverKinds $
389 (tyCoVarsOfTypes (pat_ty : req_theta) `extendVarSetList` explicit_univ_tvs)
390 (extra_univ, extra_ex) = partition ((`elemVarSet` univ_fvs) . binderVar) implicit_tvs
391 univ_bndrs = extra_univ ++ mkTyVarBinders Specified explicit_univ_tvs
392 ex_bndrs = extra_ex ++ mkTyVarBinders Specified explicit_ex_tvs
393 univ_tvs = binderVars univ_bndrs
394 ex_tvs = binderVars ex_bndrs
395
396 -- Right! Let's check the pattern against the signature
397 -- See Note [Checking against a pattern signature]
398 ; req_dicts <- newEvVars req_theta
399 ; (tclvl, wanted, (lpat', (ex_tvs', prov_dicts, args'))) <-
400 ASSERT2( equalLength arg_names arg_tys, ppr name $$ ppr arg_names $$ ppr arg_tys )
401 pushLevelAndCaptureConstraints $
402 tcExtendTyVarEnv univ_tvs $
403 tcExtendKindEnvList [(getName (binderVar ex_tv), APromotionErr PatSynExPE)
404 | ex_tv <- extra_ex] $
405 -- See Note [Pattern synonym existentials do not scope]
406 tcPat PatSyn lpat (mkCheckExpType pat_ty) $
407 do { let in_scope = mkInScopeSet (mkVarSet univ_tvs)
408 empty_subst = mkEmptyTCvSubst in_scope
409 ; (subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst ex_tvs
410 -- newMetaTyVarX: see the "Existential type variables"
411 -- part of Note [Checking against a pattern signature]
412 ; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs])
413 ; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs'])
414 ; let prov_theta' = substTheta subst prov_theta
415 -- Add univ_tvs to the in_scope set to
416 -- satisfy the substitution invariant. There's no need to
417 -- add 'ex_tvs' as they are already in the domain of the
418 -- substitution.
419 -- See also Note [The substitution invariant] in TyCoRep.
420 ; prov_dicts <- mapM (emitWanted (ProvCtxtOrigin psb)) prov_theta'
421 ; args' <- zipWithM (tc_arg subst) arg_names arg_tys
422 ; return (ex_tvs', prov_dicts, args') }
423
424 ; let skol_info = SigSkol (PatSynCtxt name) pat_ty []
425 -- The type here is a bit bogus, but we do not print
426 -- the type for PatSynCtxt, so it doesn't matter
427 -- See TcRnTypes Note [Skolem info for pattern synonyms]
428 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info univ_tvs req_dicts wanted
429
430 -- Solve the constraints now, because we are about to make a PatSyn,
431 -- which should not contain unification variables and the like (Trac #10997)
432 ; simplifyTopImplic implics
433
434 -- ToDo: in the bidirectional case, check that the ex_tvs' are all distinct
435 -- Otherwise we may get a type error when typechecking the builder,
436 -- when that should be impossible
437
438 ; traceTc "tcCheckPatSynDecl }" $ ppr name
439 ; tc_patsyn_finish lname dir is_infix lpat'
440 (univ_bndrs, req_theta, ev_binds, req_dicts)
441 (ex_bndrs, mkTyVarTys ex_tvs', prov_theta, prov_dicts)
442 (args', arg_tys)
443 pat_ty rec_fields }
444 where
445 tc_arg :: TCvSubst -> Name -> Type -> TcM (LHsExpr GhcTcId)
446 tc_arg subst arg_name arg_ty
447 = do { -- Look up the variable actually bound by lpat
448 -- and check that it has the expected type
449 arg_id <- tcLookupId arg_name
450 ; wrap <- tcSubType_NC GenSigCtxt
451 (idType arg_id)
452 (substTyUnchecked subst arg_ty)
453 -- Why do we need tcSubType here?
454 -- See Note [Pattern synonyms and higher rank types]
455 ; return (mkLHsWrap wrap $ nlHsVar arg_id) }
456 tcCheckPatSynDecl (XPatSynBind _) _ = panic "tcCheckPatSynDecl"
457
458 {- [Pattern synonyms and higher rank types]
459 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
460 Consider
461 data T = MkT (forall a. a->a)
462
463 pattern P :: (Int -> Int) -> T
464 pattern P x <- MkT x
465
466 This should work. But in the matcher we must match against MkT, and then
467 instantiate its argument 'x', to get a function of type (Int -> Int).
468 Equality is not enough! Trac #13752 was an example.
469
470 Note [Pattern synonym existentials do not scope]
471 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
472 Consider this (Trac #14498):
473 pattern SS :: forall (t :: k). () =>
474 => forall (a :: kk -> k) (n :: kk).
475 => TypeRep n -> TypeRep t
476 pattern SS n <- (App (Typeable :: TypeRep (a::kk -> k)) n)
477
478 Here 'k' is implicitly bound in the signature, but (with
479 -XScopedTypeVariables) it does still scope over the pattern-synonym
480 definition. But what about 'kk', which is oexistential? It too is
481 implicitly bound in the signature; should it too scope? And if so,
482 what type variable is it bound to?
483
484 The trouble is that the type variable to which it is bound is itself
485 only brought into scope in part the pattern, so it makes no sense for
486 'kk' to scope over the whole pattern. See the discussion on
487 Trac #14498, esp comment:16ff. Here is a simpler example:
488 data T where { MkT :: x -> (x->Int) -> T }
489 pattern P :: () => forall x. x -> (x->Int) -> T
490 pattern P a b = (MkT a b, True)
491
492 Here it would make no sense to mention 'x' in the True pattern,
493 like this:
494 pattern P a b = (MkT a b, True :: x)
495
496 The 'x' only makes sense "under" the MkT pattern. Conclusion: the
497 existential type variables of a pattern-synonym signature should not
498 scope.
499
500 But it's not that easy to implement, because we don't know
501 exactly what the existentials /are/ until we get to type checking.
502 (See Note [The pattern-synonym signature splitting rule], and
503 the partition of implicit_tvs in tcCheckPatSynDecl.)
504
505 So we do this:
506
507 - The reaner brings all the implicitly-bound kind variables into
508 scope, without trying to distinguish universal from existential
509
510 - tcCheckPatSynDecl uses tcExtendKindEnvList to bind the
511 implicitly-bound existentials to
512 APromotionErr PatSynExPE
513 It's not really a promotion error, but it's a way to bind the Name
514 (which the renamer has not complained about) to something that, when
515 looked up, will cause a complaint (in this case
516 TcHsType.promotionErr)
517
518
519 Note [The pattern-synonym signature splitting rule]
520 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
521 Given a pattern signature, we must split
522 the kind-generalised variables, and
523 the implicitly-bound variables
524 into universal and existential. The rule is this
525 (see discussion on Trac #11224):
526
527 The universal tyvars are the ones mentioned in
528 - univ_tvs: the user-specified (forall'd) universals
529 - req_theta
530 - res_ty
531 The existential tyvars are all the rest
532
533 For example
534
535 pattern P :: () => b -> T a
536 pattern P x = ...
537
538 Here 'a' is universal, and 'b' is existential. But there is a wrinkle:
539 how do we split the arg_tys from req_ty? Consider
540
541 pattern Q :: () => b -> S c -> T a
542 pattern Q x = ...
543
544 This is an odd example because Q has only one syntactic argument, and
545 so presumably is defined by a view pattern matching a function. But
546 it can happen (Trac #11977, #12108).
547
548 We don't know Q's arity from the pattern signature, so we have to wait
549 until we see the pattern declaration itself before deciding res_ty is,
550 and hence which variables are existential and which are universal.
551
552 And that in turn is why TcPatSynInfo has a separate field,
553 patsig_implicit_bndrs, to capture the implicitly bound type variables,
554 because we don't yet know how to split them up.
555
556 It's a slight compromise, because it means we don't really know the
557 pattern synonym's real signature until we see its declaration. So,
558 for example, in hs-boot file, we may need to think what to do...
559 (eg don't have any implicitly-bound variables).
560
561
562 Note [Checking against a pattern signature]
563 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
564 When checking the actual supplied pattern against the pattern synonym
565 signature, we need to be quite careful.
566
567 ----- Provided constraints
568 Example
569
570 data T a where
571 MkT :: Ord a => a -> T a
572
573 pattern P :: () => Eq a => a -> [T a]
574 pattern P x = [MkT x]
575
576 We must check that the (Eq a) that P claims to bind (and to
577 make available to matches against P), is derivable from the
578 actual pattern. For example:
579 f (P (x::a)) = ...here (Eq a) should be available...
580 And yes, (Eq a) is derivable from the (Ord a) bound by P's rhs.
581
582 ----- Existential type variables
583 Unusually, we instantiate the existential tyvars of the pattern with
584 *meta* type variables. For example
585
586 data S where
587 MkS :: Eq a => [a] -> S
588
589 pattern P :: () => Eq x => x -> S
590 pattern P x <- MkS x
591
592 The pattern synonym conceals from its client the fact that MkS has a
593 list inside it. The client just thinks it's a type 'x'. So we must
594 unify x := [a] during type checking, and then use the instantiating type
595 [a] (called ex_tys) when building the matcher. In this case we'll get
596
597 $mP :: S -> (forall x. Ex x => x -> r) -> r -> r
598 $mP x k = case x of
599 MkS a (d:Eq a) (ys:[a]) -> let dl :: Eq [a]
600 dl = $dfunEqList d
601 in k [a] dl ys
602
603 All this applies when type-checking the /matching/ side of
604 a pattern synonym. What about the /building/ side?
605
606 * For Unidirectional, there is no builder
607
608 * For ExplicitBidirectional, the builder is completely separate
609 code, typechecked in tcPatSynBuilderBind
610
611 * For ImplicitBidirectional, the builder is still typechecked in
612 tcPatSynBuilderBind, by converting the pattern to an expression and
613 typechecking it.
614
615 At one point, for ImplicitBidirectional I used TyVarTvs (instead of
616 TauTvs) in tcCheckPatSynDecl. But (a) strengthening the check here
617 is redundant since tcPatSynBuilderBind does the job, (b) it was
618 still incomplete (TyVarTvs can unify with each other), and (c) it
619 didn't even work (Trac #13441 was accepted with
620 ExplicitBidirectional, but rejected if expressed in
621 ImplicitBidirectional form. Conclusion: trying to be too clever is
622 a bad idea.
623 -}
624
625 collectPatSynArgInfo :: HsPatSynDetails (Located Name)
626 -> ([Name], [Name], Bool)
627 collectPatSynArgInfo details =
628 case details of
629 PrefixCon names -> (map unLoc names, [], False)
630 InfixCon name1 name2 -> (map unLoc [name1, name2], [], True)
631 RecCon names -> (vars, sels, False)
632 where
633 (vars, sels) = unzip (map splitRecordPatSyn names)
634 where
635 splitRecordPatSyn :: RecordPatSynField (Located Name)
636 -> (Name, Name)
637 splitRecordPatSyn (RecordPatSynField { recordPatSynPatVar = L _ patVar
638 , recordPatSynSelectorId = L _ selId })
639 = (patVar, selId)
640
641 addPatSynCtxt :: Located Name -> TcM a -> TcM a
642 addPatSynCtxt (L loc name) thing_inside
643 = setSrcSpan loc $
644 addErrCtxt (text "In the declaration for pattern synonym"
645 <+> quotes (ppr name)) $
646 thing_inside
647
648 wrongNumberOfParmsErr :: Name -> Arity -> Arity -> TcM a
649 wrongNumberOfParmsErr name decl_arity missing
650 = failWithTc $
651 hang (text "Pattern synonym" <+> quotes (ppr name) <+> ptext (sLit "has")
652 <+> speakNOf decl_arity (text "argument"))
653 2 (text "but its type signature has" <+> int missing <+> text "fewer arrows")
654
655 -------------------------
656 -- Shared by both tcInferPatSyn and tcCheckPatSyn
657 tc_patsyn_finish :: Located Name -- ^ PatSyn Name
658 -> HsPatSynDir GhcRn -- ^ PatSyn type (Uni/Bidir/ExplicitBidir)
659 -> Bool -- ^ Whether infix
660 -> LPat GhcTc -- ^ Pattern of the PatSyn
661 -> ([TcTyVarBinder], [PredType], TcEvBinds, [EvVar])
662 -> ([TcTyVarBinder], [TcType], [PredType], [EvTerm])
663 -> ([LHsExpr GhcTcId], [TcType]) -- ^ Pattern arguments and
664 -- types
665 -> TcType -- ^ Pattern type
666 -> [Name] -- ^ Selector names
667 -- ^ Whether fields, empty if not record PatSyn
668 -> TcM (LHsBinds GhcTc, TcGblEnv)
669 tc_patsyn_finish lname dir is_infix lpat'
670 (univ_tvs, req_theta, req_ev_binds, req_dicts)
671 (ex_tvs, ex_tys, prov_theta, prov_dicts)
672 (args, arg_tys)
673 pat_ty field_labels
674 = do { -- Zonk everything. We are about to build a final PatSyn
675 -- so there had better be no unification variables in there
676
677 (ze, univ_tvs') <- zonkTyVarBinders univ_tvs
678 ; req_theta' <- zonkTcTypesToTypesX ze req_theta
679 ; (ze, ex_tvs') <- zonkTyVarBindersX ze ex_tvs
680 ; prov_theta' <- zonkTcTypesToTypesX ze prov_theta
681 ; pat_ty' <- zonkTcTypeToTypeX ze pat_ty
682 ; arg_tys' <- zonkTcTypesToTypesX ze arg_tys
683
684 ; let (env1, univ_tvs) = tidyTyCoVarBinders emptyTidyEnv univ_tvs'
685 (env2, ex_tvs) = tidyTyCoVarBinders env1 ex_tvs'
686 req_theta = tidyTypes env2 req_theta'
687 prov_theta = tidyTypes env2 prov_theta'
688 arg_tys = tidyTypes env2 arg_tys'
689 pat_ty = tidyType env2 pat_ty'
690
691 ; traceTc "tc_patsyn_finish {" $
692 ppr (unLoc lname) $$ ppr (unLoc lpat') $$
693 ppr (univ_tvs, req_theta, req_ev_binds, req_dicts) $$
694 ppr (ex_tvs, prov_theta, prov_dicts) $$
695 ppr args $$
696 ppr arg_tys $$
697 ppr pat_ty
698
699 -- Make the 'matcher'
700 ; (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat'
701 (binderVars univ_tvs, req_theta, req_ev_binds, req_dicts)
702 (binderVars ex_tvs, ex_tys, prov_theta, prov_dicts)
703 (args, arg_tys)
704 pat_ty
705
706 -- Make the 'builder'
707 ; builder_id <- mkPatSynBuilderId dir lname
708 univ_tvs req_theta
709 ex_tvs prov_theta
710 arg_tys pat_ty
711
712 -- TODO: Make this have the proper information
713 ; let mkFieldLabel name = FieldLabel { flLabel = occNameFS (nameOccName name)
714 , flIsOverloaded = False
715 , flSelector = name }
716 field_labels' = map mkFieldLabel field_labels
717
718
719 -- Make the PatSyn itself
720 ; let patSyn = mkPatSyn (unLoc lname) is_infix
721 (univ_tvs, req_theta)
722 (ex_tvs, prov_theta)
723 arg_tys
724 pat_ty
725 matcher_id builder_id
726 field_labels'
727
728 -- Selectors
729 ; let rn_rec_sel_binds = mkPatSynRecSelBinds patSyn (patSynFieldLabels patSyn)
730 tything = AConLike (PatSynCon patSyn)
731 ; tcg_env <- tcExtendGlobalEnv [tything] $
732 tcRecSelBinds rn_rec_sel_binds
733
734 ; traceTc "tc_patsyn_finish }" empty
735 ; return (matcher_bind, tcg_env) }
736
737 {-
738 ************************************************************************
739 * *
740 Constructing the "matcher" Id and its binding
741 * *
742 ************************************************************************
743 -}
744
745 tcPatSynMatcher :: Located Name
746 -> LPat GhcTc
747 -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar])
748 -> ([TcTyVar], [TcType], ThetaType, [EvTerm])
749 -> ([LHsExpr GhcTcId], [TcType])
750 -> TcType
751 -> TcM ((Id, Bool), LHsBinds GhcTc)
752 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
753 tcPatSynMatcher (L loc name) lpat
754 (univ_tvs, req_theta, req_ev_binds, req_dicts)
755 (ex_tvs, ex_tys, prov_theta, prov_dicts)
756 (args, arg_tys) pat_ty
757 = do { rr_name <- newNameAt (mkTyVarOcc "rep") loc
758 ; tv_name <- newNameAt (mkTyVarOcc "r") loc
759 ; let rr_tv = mkTyVar rr_name runtimeRepTy
760 rr = mkTyVarTy rr_tv
761 res_tv = mkTyVar tv_name (tYPE rr)
762 res_ty = mkTyVarTy res_tv
763 is_unlifted = null args && null prov_dicts
764 (cont_args, cont_arg_tys)
765 | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy])
766 | otherwise = (args, arg_tys)
767 cont_ty = mkInfSigmaTy ex_tvs prov_theta $
768 mkFunTys cont_arg_tys res_ty
769
770 fail_ty = mkFunTy voidPrimTy res_ty
771
772 ; matcher_name <- newImplicitBinder name mkMatcherOcc
773 ; scrutinee <- newSysLocalId (fsLit "scrut") pat_ty
774 ; cont <- newSysLocalId (fsLit "cont") cont_ty
775 ; fail <- newSysLocalId (fsLit "fail") fail_ty
776
777 ; let matcher_tau = mkFunTys [pat_ty, cont_ty, fail_ty] res_ty
778 matcher_sigma = mkInfSigmaTy (rr_tv:res_tv:univ_tvs) req_theta matcher_tau
779 matcher_id = mkExportedVanillaId matcher_name matcher_sigma
780 -- See Note [Exported LocalIds] in Id
781
782 inst_wrap = mkWpEvApps prov_dicts <.> mkWpTyApps ex_tys
783 cont' = foldl' nlHsApp (mkLHsWrap inst_wrap (nlHsVar cont)) cont_args
784
785 fail' = nlHsApps fail [nlHsVar voidPrimId]
786
787 args = map nlVarPat [scrutinee, cont, fail]
788 lwpat = noLoc $ WildPat pat_ty
789 cases = if isIrrefutableHsPat lpat
790 then [mkHsCaseAlt lpat cont']
791 else [mkHsCaseAlt lpat cont',
792 mkHsCaseAlt lwpat fail']
793 body = mkLHsWrap (mkWpLet req_ev_binds) $
794 L (getLoc lpat) $
795 HsCase noExt (nlHsVar scrutinee) $
796 MG{ mg_alts = L (getLoc lpat) cases
797 , mg_ext = MatchGroupTc [pat_ty] res_ty
798 , mg_origin = Generated
799 }
800 body' = noLoc $
801 HsLam noExt $
802 MG{ mg_alts = noLoc [mkSimpleMatch LambdaExpr
803 args body]
804 , mg_ext = MatchGroupTc [pat_ty, cont_ty, fail_ty] res_ty
805 , mg_origin = Generated
806 }
807 match = mkMatch (mkPrefixFunRhs (L loc name)) []
808 (mkHsLams (rr_tv:res_tv:univ_tvs)
809 req_dicts body')
810 (noLoc (EmptyLocalBinds noExt))
811 mg :: MatchGroup GhcTc (LHsExpr GhcTc)
812 mg = MG{ mg_alts = L (getLoc match) [match]
813 , mg_ext = MatchGroupTc [] res_ty
814 , mg_origin = Generated
815 }
816
817 ; let bind = FunBind{ fun_ext = emptyNameSet
818 , fun_id = L loc matcher_id
819 , fun_matches = mg
820 , fun_co_fn = idHsWrapper
821 , fun_tick = [] }
822 matcher_bind = unitBag (noLoc bind)
823
824 ; traceTc "tcPatSynMatcher" (ppr name $$ ppr (idType matcher_id))
825 ; traceTc "tcPatSynMatcher" (ppr matcher_bind)
826
827 ; return ((matcher_id, is_unlifted), matcher_bind) }
828
829 mkPatSynRecSelBinds :: PatSyn
830 -> [FieldLabel] -- ^ Visible field labels
831 -> [(Id, LHsBind GhcRn)]
832 mkPatSynRecSelBinds ps fields
833 = [ mkOneRecordSelector [PatSynCon ps] (RecSelPatSyn ps) fld_lbl
834 | fld_lbl <- fields ]
835
836 isUnidirectional :: HsPatSynDir a -> Bool
837 isUnidirectional Unidirectional = True
838 isUnidirectional ImplicitBidirectional = False
839 isUnidirectional ExplicitBidirectional{} = False
840
841 {-
842 ************************************************************************
843 * *
844 Constructing the "builder" Id
845 * *
846 ************************************************************************
847 -}
848
849 mkPatSynBuilderId :: HsPatSynDir a -> Located Name
850 -> [TyVarBinder] -> ThetaType
851 -> [TyVarBinder] -> ThetaType
852 -> [Type] -> Type
853 -> TcM (Maybe (Id, Bool))
854 mkPatSynBuilderId dir (L _ name)
855 univ_bndrs req_theta ex_bndrs prov_theta
856 arg_tys pat_ty
857 | isUnidirectional dir
858 = return Nothing
859 | otherwise
860 = do { builder_name <- newImplicitBinder name mkBuilderOcc
861 ; let theta = req_theta ++ prov_theta
862 need_dummy_arg = isUnliftedType pat_ty && null arg_tys && null theta
863 builder_sigma = add_void need_dummy_arg $
864 mkForAllTys univ_bndrs $
865 mkForAllTys ex_bndrs $
866 mkFunTys theta $
867 mkFunTys arg_tys $
868 pat_ty
869 builder_id = mkExportedVanillaId builder_name builder_sigma
870 -- See Note [Exported LocalIds] in Id
871
872 builder_id' = modifyIdInfo (`setLevityInfoWithType` pat_ty) builder_id
873
874 ; return (Just (builder_id', need_dummy_arg)) }
875 where
876
877 tcPatSynBuilderBind :: PatSynBind GhcRn GhcRn
878 -> TcM (LHsBinds GhcTc)
879 -- See Note [Matchers and builders for pattern synonyms] in PatSyn
880 tcPatSynBuilderBind (PSB { psb_id = L loc name, psb_def = lpat
881 , psb_dir = dir, psb_args = details })
882 | isUnidirectional dir
883 = return emptyBag
884
885 | Left why <- mb_match_group -- Can't invert the pattern
886 = setSrcSpan (getLoc lpat) $ failWithTc $
887 vcat [ hang (text "Invalid right-hand side of bidirectional pattern synonym"
888 <+> quotes (ppr name) <> colon)
889 2 why
890 , text "RHS pattern:" <+> ppr lpat ]
891
892 | Right match_group <- mb_match_group -- Bidirectional
893 = do { patsyn <- tcLookupPatSyn name
894 ; case patSynBuilder patsyn of {
895 Nothing -> return emptyBag ;
896 -- This case happens if we found a type error in the
897 -- pattern synonym, recovered, and put a placeholder
898 -- with patSynBuilder=Nothing in the environment
899
900 Just (builder_id, need_dummy_arg) -> -- Normal case
901 do { -- Bidirectional, so patSynBuilder returns Just
902 let match_group' | need_dummy_arg = add_dummy_arg match_group
903 | otherwise = match_group
904
905 bind = FunBind { fun_ext = placeHolderNamesTc
906 , fun_id = L loc (idName builder_id)
907 , fun_matches = match_group'
908 , fun_co_fn = idHsWrapper
909 , fun_tick = [] }
910
911 sig = completeSigFromId (PatSynCtxt name) builder_id
912
913 ; traceTc "tcPatSynBuilderBind {" $
914 ppr patsyn $$ ppr builder_id <+> dcolon <+> ppr (idType builder_id)
915 ; (builder_binds, _) <- tcPolyCheck emptyPragEnv sig (noLoc bind)
916 ; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
917 ; return builder_binds } } }
918
919 | otherwise = panic "tcPatSynBuilderBind" -- Both cases dealt with
920 where
921 mb_match_group
922 = case dir of
923 ExplicitBidirectional explicit_mg -> Right explicit_mg
924 ImplicitBidirectional -> fmap mk_mg (tcPatToExpr name args lpat)
925 Unidirectional -> panic "tcPatSynBuilderBind"
926
927 mk_mg :: LHsExpr GhcRn -> MatchGroup GhcRn (LHsExpr GhcRn)
928 mk_mg body = mkMatchGroup Generated [builder_match]
929 where
930 builder_args = [L loc (VarPat noExt (L loc n)) | L loc n <- args]
931 builder_match = mkMatch (mkPrefixFunRhs (L loc name))
932 builder_args body
933 (noLoc (EmptyLocalBinds noExt))
934
935 args = case details of
936 PrefixCon args -> args
937 InfixCon arg1 arg2 -> [arg1, arg2]
938 RecCon args -> map recordPatSynPatVar args
939
940 add_dummy_arg :: MatchGroup GhcRn (LHsExpr GhcRn)
941 -> MatchGroup GhcRn (LHsExpr GhcRn)
942 add_dummy_arg mg@(MG { mg_alts = L l [L loc match@(Match { m_pats = pats })] })
943 = mg { mg_alts = L l [L loc (match { m_pats = nlWildPatName : pats })] }
944 add_dummy_arg other_mg = pprPanic "add_dummy_arg" $
945 pprMatches other_mg
946 tcPatSynBuilderBind (XPatSynBind _) = panic "tcPatSynBuilderBind"
947
948 tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr GhcTcId, TcSigmaType)
949 -- monadic only for failure
950 tcPatSynBuilderOcc ps
951 | Just (builder_id, add_void_arg) <- builder
952 , let builder_expr = HsConLikeOut noExt (PatSynCon ps)
953 builder_ty = idType builder_id
954 = return $
955 if add_void_arg
956 then ( builder_expr -- still just return builder_expr; the void# arg is added
957 -- by dsConLike in the desugarer
958 , tcFunResultTy builder_ty )
959 else (builder_expr, builder_ty)
960
961 | otherwise -- Unidirectional
962 = nonBidirectionalErr name
963 where
964 name = patSynName ps
965 builder = patSynBuilder ps
966
967 add_void :: Bool -> Type -> Type
968 add_void need_dummy_arg ty
969 | need_dummy_arg = mkFunTy voidPrimTy ty
970 | otherwise = ty
971
972 tcPatToExpr :: Name -> [Located Name] -> LPat GhcRn
973 -> Either MsgDoc (LHsExpr GhcRn)
974 -- Given a /pattern/, return an /expression/ that builds a value
975 -- that matches the pattern. E.g. if the pattern is (Just [x]),
976 -- the expression is (Just [x]). They look the same, but the
977 -- input uses constructors from HsPat and the output uses constructors
978 -- from HsExpr.
979 --
980 -- Returns (Left r) if the pattern is not invertible, for reason r.
981 -- See Note [Builder for a bidirectional pattern synonym]
982 tcPatToExpr name args pat = go pat
983 where
984 lhsVars = mkNameSet (map unLoc args)
985
986 -- Make a prefix con for prefix and infix patterns for simplicity
987 mkPrefixConExpr :: Located Name -> [LPat GhcRn]
988 -> Either MsgDoc (HsExpr GhcRn)
989 mkPrefixConExpr lcon@(L loc _) pats
990 = do { exprs <- mapM go pats
991 ; return (foldl' (\x y -> HsApp noExt (L loc x) y)
992 (HsVar noExt lcon) exprs) }
993
994 mkRecordConExpr :: Located Name -> HsRecFields GhcRn (LPat GhcRn)
995 -> Either MsgDoc (HsExpr GhcRn)
996 mkRecordConExpr con fields
997 = do { exprFields <- mapM go fields
998 ; return (RecordCon noExt con exprFields) }
999
1000 go :: LPat GhcRn -> Either MsgDoc (LHsExpr GhcRn)
1001 go (L loc p) = L loc <$> go1 p
1002
1003 go1 :: Pat GhcRn -> Either MsgDoc (HsExpr GhcRn)
1004 go1 (ConPatIn con info)
1005 = case info of
1006 PrefixCon ps -> mkPrefixConExpr con ps
1007 InfixCon l r -> mkPrefixConExpr con [l,r]
1008 RecCon fields -> mkRecordConExpr con fields
1009
1010 go1 (SigPat _ pat) = go1 (unLoc pat)
1011 -- See Note [Type signatures and the builder expression]
1012
1013 go1 (VarPat _ (L l var))
1014 | var `elemNameSet` lhsVars
1015 = return $ HsVar noExt (L l var)
1016 | otherwise
1017 = Left (quotes (ppr var) <+> text "is not bound by the LHS of the pattern synonym")
1018 go1 (ParPat _ pat) = fmap (HsPar noExt) $ go pat
1019 go1 p@(ListPat reb pats)
1020 | Nothing <- reb = do { exprs <- mapM go pats
1021 ; return $ ExplicitList noExt Nothing exprs }
1022 | otherwise = notInvertibleListPat p
1023 go1 (TuplePat _ pats box) = do { exprs <- mapM go pats
1024 ; return $ ExplicitTuple noExt
1025 (map (noLoc . (Present noExt)) exprs)
1026 box }
1027 go1 (SumPat _ pat alt arity) = do { expr <- go1 (unLoc pat)
1028 ; return $ ExplicitSum noExt alt arity
1029 (noLoc expr)
1030 }
1031 go1 (LitPat _ lit) = return $ HsLit noExt lit
1032 go1 (NPat _ (L _ n) mb_neg _)
1033 | Just neg <- mb_neg = return $ unLoc $ nlHsSyntaxApps neg
1034 [noLoc (HsOverLit noExt n)]
1035 | otherwise = return $ HsOverLit noExt n
1036 go1 (ConPatOut{}) = panic "ConPatOut in output of renamer"
1037 go1 (CoPat{}) = panic "CoPat in output of renamer"
1038 go1 (SplicePat _ (HsSpliced _ _ (HsSplicedPat pat)))
1039 = go1 pat
1040 go1 (SplicePat _ (HsSpliced{})) = panic "Invalid splice variety"
1041
1042 -- The following patterns are not invertible.
1043 go1 p@(BangPat {}) = notInvertible p -- #14112
1044 go1 p@(LazyPat {}) = notInvertible p
1045 go1 p@(WildPat {}) = notInvertible p
1046 go1 p@(AsPat {}) = notInvertible p
1047 go1 p@(ViewPat {}) = notInvertible p
1048 go1 p@(NPlusKPat {}) = notInvertible p
1049 go1 p@(XPat {}) = notInvertible p
1050 go1 p@(SplicePat _ (HsTypedSplice {})) = notInvertible p
1051 go1 p@(SplicePat _ (HsUntypedSplice {})) = notInvertible p
1052 go1 p@(SplicePat _ (HsQuasiQuote {})) = notInvertible p
1053 go1 p@(SplicePat _ (XSplice {})) = notInvertible p
1054
1055 notInvertible p = Left (not_invertible_msg p)
1056
1057 not_invertible_msg p
1058 = text "Pattern" <+> quotes (ppr p) <+> text "is not invertible"
1059 $+$ hang (text "Suggestion: instead use an explicitly bidirectional"
1060 <+> text "pattern synonym, e.g.")
1061 2 (hang (text "pattern" <+> pp_name <+> pp_args <+> larrow
1062 <+> ppr pat <+> text "where")
1063 2 (pp_name <+> pp_args <+> equals <+> text "..."))
1064 where
1065 pp_name = ppr name
1066 pp_args = hsep (map ppr args)
1067
1068 -- We should really be able to invert list patterns, even when
1069 -- rebindable syntax is on, but doing so involves a bit of
1070 -- refactoring; see Trac #14380. Until then we reject with a
1071 -- helpful error message.
1072 notInvertibleListPat p
1073 = Left (vcat [ not_invertible_msg p
1074 , text "Reason: rebindable syntax is on."
1075 , text "This is fixable: add use-case to Trac #14380" ])
1076
1077 {- Note [Builder for a bidirectional pattern synonym]
1078 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1079 For a bidirectional pattern synonym we need to produce an /expression/
1080 that matches the supplied /pattern/, given values for the arguments
1081 of the pattern synonym. For example
1082 pattern F x y = (Just x, [y])
1083 The 'builder' for F looks like
1084 $builderF x y = (Just x, [y])
1085
1086 We can't always do this:
1087 * Some patterns aren't invertible; e.g. view patterns
1088 pattern F x = (reverse -> x:_)
1089
1090 * The RHS pattern might bind more variables than the pattern
1091 synonym, so again we can't invert it
1092 pattern F x = (x,y)
1093
1094 * Ditto wildcards
1095 pattern F x = (x,_)
1096
1097
1098 Note [Redundant constraints for builder]
1099 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1100 The builder can have redundant constraints, which are awkard to eliminate.
1101 Consider
1102 pattern P = Just 34
1103 To match against this pattern we need (Eq a, Num a). But to build
1104 (Just 34) we need only (Num a). Fortunately instTcSigFromId sets
1105 sig_warn_redundant to False.
1106
1107 ************************************************************************
1108 * *
1109 Helper functions
1110 * *
1111 ************************************************************************
1112
1113 Note [As-patterns in pattern synonym definitions]
1114 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1115 The rationale for rejecting as-patterns in pattern synonym definitions
1116 is that an as-pattern would introduce nonindependent pattern synonym
1117 arguments, e.g. given a pattern synonym like:
1118
1119 pattern K x y = x@(Just y)
1120
1121 one could write a nonsensical function like
1122
1123 f (K Nothing x) = ...
1124
1125 or
1126 g (K (Just True) False) = ...
1127
1128 Note [Type signatures and the builder expression]
1129 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1130 Consider
1131 pattern L x = Left x :: Either [a] [b]
1132
1133 In tc{Infer/Check}PatSynDecl we will check that the pattern has the
1134 specified type. We check the pattern *as a pattern*, so the type
1135 signature is a pattern signature, and so brings 'a' and 'b' into
1136 scope. But we don't have a way to bind 'a, b' in the LHS, as we do
1137 'x', say. Nevertheless, the sigature may be useful to constrain
1138 the type.
1139
1140 When making the binding for the *builder*, though, we don't want
1141 $buildL x = Left x :: Either [a] [b]
1142 because that wil either mean (forall a b. Either [a] [b]), or we'll
1143 get a complaint that 'a' and 'b' are out of scope. (Actually the
1144 latter; Trac #9867.) No, the job of the signature is done, so when
1145 converting the pattern to an expression (for the builder RHS) we
1146 simply discard the signature.
1147
1148 Note [Record PatSyn Desugaring]
1149 -------------------------------
1150 It is important that prov_theta comes before req_theta as this ordering is used
1151 when desugaring record pattern synonym updates.
1152
1153 Any change to this ordering should make sure to change deSugar/DsExpr.hs if you
1154 want to avoid difficult to decipher core lint errors!
1155 -}
1156
1157
1158 nonBidirectionalErr :: Outputable name => name -> TcM a
1159 nonBidirectionalErr name = failWithTc $
1160 text "non-bidirectional pattern synonym"
1161 <+> quotes (ppr name) <+> text "used in an expression"
1162
1163 -- Walk the whole pattern and for all ConPatOuts, collect the
1164 -- existentially-bound type variables and evidence binding variables.
1165 --
1166 -- These are used in computing the type of a pattern synonym and also
1167 -- in generating matcher functions, since success continuations need
1168 -- to be passed these pattern-bound evidences.
1169 tcCollectEx
1170 :: LPat GhcTc
1171 -> ( [TyVar] -- Existentially-bound type variables
1172 -- in correctly-scoped order; e.g. [ k:*, x:k ]
1173 , [EvVar] ) -- and evidence variables
1174
1175 tcCollectEx pat = go pat
1176 where
1177 go :: LPat GhcTc -> ([TyVar], [EvVar])
1178 go = go1 . unLoc
1179
1180 go1 :: Pat GhcTc -> ([TyVar], [EvVar])
1181 go1 (LazyPat _ p) = go p
1182 go1 (AsPat _ _ p) = go p
1183 go1 (ParPat _ p) = go p
1184 go1 (BangPat _ p) = go p
1185 go1 (ListPat _ ps) = mergeMany . map go $ ps
1186 go1 (TuplePat _ ps _) = mergeMany . map go $ ps
1187 go1 (SumPat _ p _ _) = go p
1188 go1 (ViewPat _ _ p) = go p
1189 go1 con@ConPatOut{} = merge (pat_tvs con, pat_dicts con) $
1190 goConDetails $ pat_args con
1191 go1 (SigPat _ p) = go p
1192 go1 (CoPat _ _ p _) = go1 p
1193 go1 (NPlusKPat _ n k _ geq subtract)
1194 = pprPanic "TODO: NPlusKPat" $ ppr n $$ ppr k $$ ppr geq $$ ppr subtract
1195 go1 _ = empty
1196
1197 goConDetails :: HsConPatDetails GhcTc -> ([TyVar], [EvVar])
1198 goConDetails (PrefixCon ps) = mergeMany . map go $ ps
1199 goConDetails (InfixCon p1 p2) = go p1 `merge` go p2
1200 goConDetails (RecCon HsRecFields{ rec_flds = flds })
1201 = mergeMany . map goRecFd $ flds
1202
1203 goRecFd :: LHsRecField GhcTc (LPat GhcTc) -> ([TyVar], [EvVar])
1204 goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p
1205
1206 merge (vs1, evs1) (vs2, evs2) = (vs1 ++ vs2, evs1 ++ evs2)
1207 mergeMany = foldr merge empty
1208 empty = ([], [])