never executed always true always false
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1998
4
5 \section[PatSyn]{@PatSyn@: Pattern synonyms}
6 -}
7
8
9
10 module GHC.Core.PatSyn (
11 -- * Main data types
12 PatSyn, PatSynMatcher, PatSynBuilder, mkPatSyn,
13
14 -- ** Type deconstruction
15 patSynName, patSynArity, patSynIsInfix, patSynResultType,
16 isVanillaPatSyn,
17 patSynArgs,
18 patSynMatcher, patSynBuilder,
19 patSynUnivTyVarBinders, patSynExTyVars, patSynExTyVarBinders,
20 patSynSig, patSynSigBndr,
21 patSynInstArgTys, patSynInstResTy, patSynFieldLabels,
22 patSynFieldType,
23
24 pprPatSynType
25 ) where
26
27 import GHC.Prelude
28
29 import GHC.Core.Type
30 import GHC.Core.TyCo.Ppr
31 import GHC.Types.Name
32 import GHC.Types.Unique
33 import GHC.Types.Basic
34 import GHC.Types.Var
35 import GHC.Types.FieldLabel
36
37 import GHC.Utils.Misc
38 import GHC.Utils.Outputable
39 import GHC.Utils.Panic
40
41 import qualified Data.Data as Data
42 import Data.Function
43 import Data.List (find)
44
45 {-
46 ************************************************************************
47 * *
48 \subsection{Pattern synonyms}
49 * *
50 ************************************************************************
51 -}
52
53 -- | Pattern Synonym
54 --
55 -- See Note [Pattern synonym representation]
56 -- See Note [Pattern synonym signature contexts]
57 data PatSyn
58 = MkPatSyn {
59 psName :: Name,
60 psUnique :: Unique, -- Cached from Name
61
62 psArgs :: [Type],
63 psArity :: Arity, -- == length psArgs
64 psInfix :: Bool, -- True <=> declared infix
65 psFieldLabels :: [FieldLabel], -- List of fields for a
66 -- record pattern synonym
67 -- INVARIANT: either empty if no
68 -- record pat syn or same length as
69 -- psArgs
70
71 -- Universally-quantified type variables
72 psUnivTyVars :: [InvisTVBinder],
73
74 -- Required dictionaries (may mention psUnivTyVars)
75 psReqTheta :: ThetaType,
76
77 -- Existentially-quantified type vars
78 psExTyVars :: [InvisTVBinder],
79
80 -- Provided dictionaries (may mention psUnivTyVars or psExTyVars)
81 psProvTheta :: ThetaType,
82
83 -- Result type
84 psResultTy :: Type, -- Mentions only psUnivTyVars
85 -- See Note [Pattern synonym result type]
86
87 -- See Note [Matchers and builders for pattern synonyms]
88 -- See Note [Keep Ids out of PatSyn]
89 psMatcher :: PatSynMatcher,
90 psBuilder :: PatSynBuilder
91 }
92
93 type PatSynMatcher = (Name, Type, Bool)
94 -- Matcher function.
95 -- If Bool is True then prov_theta and arg_tys are empty
96 -- and type is
97 -- forall (p :: RuntimeRep) (r :: TYPE p) univ_tvs.
98 -- req_theta
99 -- => res_ty
100 -- -> (forall ex_tvs. Void# -> r)
101 -- -> (Void# -> r)
102 -- -> r
103 --
104 -- Otherwise type is
105 -- forall (p :: RuntimeRep) (r :: TYPE r) univ_tvs.
106 -- req_theta
107 -- => res_ty
108 -- -> (forall ex_tvs. prov_theta => arg_tys -> r)
109 -- -> (Void# -> r)
110 -- -> r
111
112 type PatSynBuilder = Maybe (Name, Type, Bool)
113 -- Nothing => uni-directional pattern synonym
114 -- Just (builder, is_unlifted) => bi-directional
115 -- Builder function, of type
116 -- forall univ_tvs, ex_tvs. (req_theta, prov_theta)
117 -- => arg_tys -> res_ty
118 -- See Note [Builder for pattern synonyms with unboxed type]
119
120 {- Note [Pattern synonym signature contexts]
121 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
122 In a pattern synonym signature we write
123 pattern P :: req => prov => t1 -> ... tn -> res_ty
124
125 Note that the "required" context comes first, then the "provided"
126 context. Moreover, the "required" context must not mention
127 existentially-bound type variables; that is, ones not mentioned in
128 res_ty. See lots of discussion in #10928.
129
130 If there is no "provided" context, you can omit it; but you
131 can't omit the "required" part (unless you omit both).
132
133 Example 1:
134 pattern P1 :: (Num a, Eq a) => b -> Maybe (a,b)
135 pattern P1 x = Just (3,x)
136
137 We require (Num a, Eq a) to match the 3; there is no provided
138 context.
139
140 Example 2:
141 data T2 where
142 MkT2 :: (Num a, Eq a) => a -> a -> T2
143
144 pattern P2 :: () => (Num a, Eq a) => a -> T2
145 pattern P2 x = MkT2 3 x
146
147 When we match against P2 we get a Num dictionary provided.
148 We can use that to check the match against 3.
149
150 Example 3:
151 pattern P3 :: Eq a => a -> b -> T3 b
152
153 This signature is illegal because the (Eq a) is a required
154 constraint, but it mentions the existentially-bound variable 'a'.
155 You can see it's existential because it doesn't appear in the
156 result type (T3 b).
157
158 Note [Pattern synonym result type]
159 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
160 Consider
161 data T a b = MkT b a
162
163 pattern P :: a -> T [a] Bool
164 pattern P x = MkT True [x]
165
166 P's psResultTy is (T a Bool), and it really only matches values of
167 type (T [a] Bool). For example, this is ill-typed
168
169 f :: T p q -> String
170 f (P x) = "urk"
171
172 This is different to the situation with GADTs:
173
174 data S a where
175 MkS :: Int -> S Bool
176
177 Now MkS (and pattern synonyms coming from MkS) can match a
178 value of type (S a), not just (S Bool); we get type refinement.
179
180 That in turn means that if you have a pattern
181
182 P x :: T [ty] Bool
183
184 it's not entirely straightforward to work out the instantiation of
185 P's universal tyvars. You have to /match/
186 the type of the pattern, (T [ty] Bool)
187 against
188 the psResultTy for the pattern synonym, T [a] Bool
189 to get the instantiation a := ty.
190
191 This is very unlike DataCons, where univ tyvars match 1-1 the
192 arguments of the TyCon.
193
194 Side note: I (SG) get the impression that instantiated return types should
195 generate a *required* constraint for pattern synonyms, rather than a *provided*
196 constraint like it's the case for GADTs. For example, I'd expect these
197 declarations to have identical semantics:
198
199 pattern Just42 :: Maybe Int
200 pattern Just42 = Just 42
201
202 pattern Just'42 :: (a ~ Int) => Maybe a
203 pattern Just'42 = Just 42
204
205 The latter generates the proper required constraint, the former does not.
206 Also rather different to GADTs is the fact that Just42 doesn't have any
207 universally quantified type variables, whereas Just'42 or MkS above has.
208
209 Note [Keep Ids out of PatSyn]
210 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
211 We carefully arrange that PatSyn does not contain the Ids for the matcher
212 and builder. We want PatSyn, like TyCon and DataCon, to be completely
213 immutable. But, the matcher and builder are relatively sophisticated
214 functions, and we want to get their final IdInfo in the same way as
215 any other Id, so we'd have to update the Ids in the PatSyn too.
216
217 Rather than try to tidy PatSyns (which is easy to forget and is a bit
218 tricky, see #19074), it seems cleaner to make them entirely immutable,
219 like TyCons and Classes. To that end PatSynBuilder and PatSynMatcher
220 contain Names not Ids. Which, it turns out, is absolutely fine.
221
222 c.f. DefMethInfo in Class, which contains the Name, but not the Id,
223 of the default method.
224
225 Note [Pattern synonym representation]
226 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
227 Consider the following pattern synonym declaration
228
229 pattern P x = MkT [x] (Just 42)
230
231 where
232 data T a where
233 MkT :: (Show a, Ord b) => [b] -> a -> T a
234
235 so pattern P has type
236
237 b -> T (Maybe t)
238
239 with the following typeclass constraints:
240
241 requires: (Eq t, Num t)
242 provides: (Show (Maybe t), Ord b)
243
244 In this case, the fields of MkPatSyn will be set as follows:
245
246 psArgs = [b]
247 psArity = 1
248 psInfix = False
249
250 psUnivTyVars = [t]
251 psExTyVars = [b]
252 psProvTheta = (Show (Maybe t), Ord b)
253 psReqTheta = (Eq t, Num t)
254 psResultTy = T (Maybe t)
255
256 Note [Matchers and builders for pattern synonyms]
257 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
258 For each pattern synonym P, we generate
259
260 * a "matcher" function, used to desugar uses of P in patterns,
261 which implements pattern matching
262
263 * A "builder" function (for bidirectional pattern synonyms only),
264 used to desugar uses of P in expressions, which constructs P-values.
265
266 For the above example, the matcher function has type:
267
268 $mP :: forall (r :: ?) t. (Eq t, Num t)
269 => T (Maybe t)
270 -> (forall b. (Show (Maybe t), Ord b) => b -> r)
271 -> (Void# -> r)
272 -> r
273
274 with the following implementation:
275
276 $mP @r @t $dEq $dNum scrut cont fail
277 = case scrut of
278 MkT @b $dShow $dOrd [x] (Just 42) -> cont @b $dShow $dOrd x
279 _ -> fail Void#
280
281 Notice that the return type 'r' has an open kind, so that it can
282 be instantiated by an unboxed type; for example where we see
283 f (P x) = 3#
284
285 The extra Void# argument for the failure continuation is needed so that
286 it is lazy even when the result type is unboxed.
287
288 For the same reason, if the pattern has no arguments, an extra Void#
289 argument is added to the success continuation as well.
290
291 For *bidirectional* pattern synonyms, we also generate a "builder"
292 function which implements the pattern synonym in an expression
293 context. For our running example, it will be:
294
295 $bP :: forall t b. (Eq t, Num t, Show (Maybe t), Ord b)
296 => b -> T (Maybe t)
297 $bP x = MkT [x] (Just 42)
298
299 NB: the existential/universal and required/provided split does not
300 apply to the builder since you are only putting stuff in, not getting
301 stuff out.
302
303 Injectivity of bidirectional pattern synonyms is checked in
304 tcPatToExpr which walks the pattern and returns its corresponding
305 expression when available.
306
307 Note [Builder for pattern synonyms with unboxed type]
308 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
309 For bidirectional pattern synonyms that have no arguments and have an
310 unboxed type, we add an extra Void# argument to the builder, else it
311 would be a top-level declaration with an unboxed type.
312
313 pattern P = 0#
314
315 $bP :: Void# -> Int#
316 $bP _ = 0#
317
318 This means that when typechecking an occurrence of P in an expression,
319 we must remember that the builder has this void argument. This is
320 done by GHC.Tc.TyCl.PatSyn.patSynBuilderOcc.
321
322 Note [Pattern synonyms and the data type Type]
323 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
324 The type of a pattern synonym is of the form (See Note
325 [Pattern synonym signatures] in GHC.Tc.Gen.Sig):
326
327 forall univ_tvs. req => forall ex_tvs. prov => ...
328
329 We cannot in general represent this by a value of type Type:
330
331 - if ex_tvs is empty, then req and prov cannot be distinguished from
332 each other
333 - if req is empty, then univ_tvs and ex_tvs cannot be distinguished
334 from each other, and moreover, prov is seen as the "required" context
335 (as it is the only context)
336
337
338 ************************************************************************
339 * *
340 \subsection{Instances}
341 * *
342 ************************************************************************
343 -}
344
345 instance Eq PatSyn where
346 (==) = (==) `on` getUnique
347 (/=) = (/=) `on` getUnique
348
349 instance Uniquable PatSyn where
350 getUnique = psUnique
351
352 instance NamedThing PatSyn where
353 getName = patSynName
354
355 instance Outputable PatSyn where
356 ppr = ppr . getName
357
358 instance OutputableBndr PatSyn where
359 pprInfixOcc = pprInfixName . getName
360 pprPrefixOcc = pprPrefixName . getName
361
362 instance Data.Data PatSyn where
363 -- don't traverse?
364 toConstr _ = abstractConstr "PatSyn"
365 gunfold _ _ = error "gunfold"
366 dataTypeOf _ = mkNoRepType "PatSyn"
367
368 {-
369 ************************************************************************
370 * *
371 \subsection{Construction}
372 * *
373 ************************************************************************
374 -}
375
376 -- | Build a new pattern synonym
377 mkPatSyn :: Name
378 -> Bool -- ^ Is the pattern synonym declared infix?
379 -> ([InvisTVBinder], ThetaType) -- ^ Universially-quantified type
380 -- variables and required dicts
381 -> ([InvisTVBinder], ThetaType) -- ^ Existentially-quantified type
382 -- variables and provided dicts
383 -> [Type] -- ^ Original arguments
384 -> Type -- ^ Original result type
385 -> PatSynMatcher -- ^ Matcher
386 -> PatSynBuilder -- ^ Builder
387 -> [FieldLabel] -- ^ Names of fields for
388 -- a record pattern synonym
389 -> PatSyn
390 -- NB: The univ and ex vars are both in TyBinder form and TyVar form for
391 -- convenience. All the TyBinders should be Named!
392 mkPatSyn name declared_infix
393 (univ_tvs, req_theta)
394 (ex_tvs, prov_theta)
395 orig_args
396 orig_res_ty
397 matcher builder field_labels
398 = MkPatSyn {psName = name, psUnique = getUnique name,
399 psUnivTyVars = univ_tvs,
400 psExTyVars = ex_tvs,
401 psProvTheta = prov_theta, psReqTheta = req_theta,
402 psInfix = declared_infix,
403 psArgs = orig_args,
404 psArity = length orig_args,
405 psResultTy = orig_res_ty,
406 psMatcher = matcher,
407 psBuilder = builder,
408 psFieldLabels = field_labels
409 }
410
411 -- | The 'Name' of the 'PatSyn', giving it a unique, rooted identification
412 patSynName :: PatSyn -> Name
413 patSynName = psName
414
415 -- | Should the 'PatSyn' be presented infix?
416 patSynIsInfix :: PatSyn -> Bool
417 patSynIsInfix = psInfix
418
419 -- | Arity of the pattern synonym
420 patSynArity :: PatSyn -> Arity
421 patSynArity = psArity
422
423 -- | Is this a \'vanilla\' pattern synonym (no existentials, no provided constraints)?
424 isVanillaPatSyn :: PatSyn -> Bool
425 isVanillaPatSyn ps = null (psExTyVars ps) && null (psProvTheta ps)
426
427 patSynArgs :: PatSyn -> [Type]
428 patSynArgs = psArgs
429
430 patSynFieldLabels :: PatSyn -> [FieldLabel]
431 patSynFieldLabels = psFieldLabels
432
433 -- | Extract the type for any given labelled field of the 'DataCon'
434 patSynFieldType :: PatSyn -> FieldLabelString -> Type
435 patSynFieldType ps label
436 = case find ((== label) . flLabel . fst) (psFieldLabels ps `zip` psArgs ps) of
437 Just (_, ty) -> ty
438 Nothing -> pprPanic "dataConFieldType" (ppr ps <+> ppr label)
439
440 patSynUnivTyVarBinders :: PatSyn -> [InvisTVBinder]
441 patSynUnivTyVarBinders = psUnivTyVars
442
443 patSynExTyVars :: PatSyn -> [TyVar]
444 patSynExTyVars ps = binderVars (psExTyVars ps)
445
446 patSynExTyVarBinders :: PatSyn -> [InvisTVBinder]
447 patSynExTyVarBinders = psExTyVars
448
449 patSynSigBndr :: PatSyn -> ([InvisTVBinder], ThetaType, [InvisTVBinder], ThetaType, [Scaled Type], Type)
450 patSynSigBndr (MkPatSyn { psUnivTyVars = univ_tvs, psExTyVars = ex_tvs
451 , psProvTheta = prov, psReqTheta = req
452 , psArgs = arg_tys, psResultTy = res_ty })
453 = (univ_tvs, req, ex_tvs, prov, map unrestricted arg_tys, res_ty)
454
455 patSynSig :: PatSyn -> ([TyVar], ThetaType, [TyVar], ThetaType, [Scaled Type], Type)
456 patSynSig ps = let (u_tvs, req, e_tvs, prov, arg_tys, res_ty) = patSynSigBndr ps
457 in (binderVars u_tvs, req, binderVars e_tvs, prov, arg_tys, res_ty)
458
459 patSynMatcher :: PatSyn -> PatSynMatcher
460 patSynMatcher = psMatcher
461
462 patSynBuilder :: PatSyn -> PatSynBuilder
463 patSynBuilder = psBuilder
464
465 patSynResultType :: PatSyn -> Type
466 patSynResultType = psResultTy
467
468 patSynInstArgTys :: PatSyn -> [Type] -> [Type]
469 -- Return the types of the argument patterns
470 -- e.g. data D a = forall b. MkD a b (b->a)
471 -- pattern P f x y = MkD (x,True) y f
472 -- D :: forall a. forall b. a -> b -> (b->a) -> D a
473 -- P :: forall c. forall b. (b->(c,Bool)) -> c -> b -> P c
474 -- patSynInstArgTys P [Int,bb] = [bb->(Int,Bool), Int, bb]
475 -- NB: the inst_tys should be both universal and existential
476 patSynInstArgTys (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
477 , psExTyVars = ex_tvs, psArgs = arg_tys })
478 inst_tys
479 = assertPpr (tyvars `equalLength` inst_tys)
480 (text "patSynInstArgTys" <+> ppr name $$ ppr tyvars $$ ppr inst_tys) $
481 map (substTyWith tyvars inst_tys) arg_tys
482 where
483 tyvars = binderVars (univ_tvs ++ ex_tvs)
484
485 patSynInstResTy :: PatSyn -> [Type] -> Type
486 -- Return the type of whole pattern
487 -- E.g. pattern P x y = Just (x,x,y)
488 -- P :: a -> b -> Just (a,a,b)
489 -- (patSynInstResTy P [Int,Bool] = Maybe (Int,Int,Bool)
490 -- NB: unlike patSynInstArgTys, the inst_tys should be just the *universal* tyvars
491 patSynInstResTy (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
492 , psResultTy = res_ty })
493 inst_tys
494 = assertPpr (univ_tvs `equalLength` inst_tys)
495 (text "patSynInstResTy" <+> ppr name $$ ppr univ_tvs $$ ppr inst_tys) $
496 substTyWith (binderVars univ_tvs) inst_tys res_ty
497
498 -- | Print the type of a pattern synonym. The foralls are printed explicitly
499 pprPatSynType :: PatSyn -> SDoc
500 pprPatSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta
501 , psExTyVars = ex_tvs, psProvTheta = prov_theta
502 , psArgs = orig_args, psResultTy = orig_res_ty })
503 = sep [ pprForAll $ tyVarSpecToBinders univ_tvs
504 , pprThetaArrowTy req_theta
505 , ppWhen insert_empty_ctxt $ parens empty <+> darrow
506 , pprType sigma_ty ]
507 where
508 sigma_ty = mkInvisForAllTys ex_tvs $
509 mkInvisFunTysMany prov_theta $
510 mkVisFunTysMany orig_args orig_res_ty
511 insert_empty_ctxt = null req_theta && not (null prov_theta && null ex_tvs)