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