3c5e709f471420e942e878580e12b3383dbd6d11
[ghc.git] / compiler / basicTypes / PatSyn.hs
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 {-# LANGUAGE CPP #-}
9
10 module PatSyn (
11 -- * Main data types
12 PatSyn, mkPatSyn,
13
14 -- ** Type deconstruction
15 patSynName, patSynArity, patSynIsInfix,
16 patSynArgs,
17 patSynMatcher, patSynBuilder,
18 patSynUnivTyBinders, patSynExTyVars, patSynExTyBinders, patSynSig,
19 patSynInstArgTys, patSynInstResTy, patSynFieldLabels,
20 patSynFieldType,
21
22 tidyPatSynIds, pprPatSynType
23 ) where
24
25 #include "HsVersions.h"
26
27 import Type
28 import Name
29 import Outputable
30 import Unique
31 import Util
32 import BasicTypes
33 import Var
34 import FieldLabel
35
36 import qualified Data.Data as Data
37 import Data.Function
38 import Data.List
39
40 {-
41 ************************************************************************
42 * *
43 \subsection{Pattern synonyms}
44 * *
45 ************************************************************************
46 -}
47
48 -- | A pattern synonym
49 -- See Note [Pattern synonym representation]
50 -- See Note [Pattern synonym signatures]
51 data PatSyn
52 = MkPatSyn {
53 psName :: Name,
54 psUnique :: Unique, -- Cached from Name
55
56 psArgs :: [Type],
57 psArity :: Arity, -- == length psArgs
58 psInfix :: Bool, -- True <=> declared infix
59 psFieldLabels :: [FieldLabel], -- List of fields for a
60 -- record pattern synonym
61 -- INVARIANT: either empty if no
62 -- record pat syn or same length as
63 -- psArgs
64
65 -- Universially-quantified type variables
66 psUnivTyVars :: [TyVar], -- Two linked fields; see DataCon
67 psUnivTyBinders :: [TyBinder], -- Note [TyBinders in DataCons]
68
69 -- Required dictionaries (may mention psUnivTyVars)
70 psReqTheta :: ThetaType,
71
72 -- Existentially-quantified type vars
73 psExTyVars :: [TyVar], -- Two linked fields; see DataCon
74 psExTyBinders :: [TyBinder], -- Note [TyBinders in DataCons]
75
76 -- Provided dictionaries (may mention psUnivTyVars or psExTyVars)
77 psProvTheta :: ThetaType,
78
79 -- Result type
80 psOrigResTy :: Type, -- Mentions only psUnivTyVars
81
82 -- See Note [Matchers and builders for pattern synonyms]
83 psMatcher :: (Id, Bool),
84 -- Matcher function.
85 -- If Bool is True then prov_theta and arg_tys are empty
86 -- and type is
87 -- forall (p :: RuntimeRep) (r :: TYPE p) univ_tvs.
88 -- req_theta
89 -- => res_ty
90 -- -> (forall ex_tvs. Void# -> r)
91 -- -> (Void# -> r)
92 -- -> r
93 --
94 -- Otherwise type is
95 -- forall (p :: RuntimeRep) (r :: TYPE r) univ_tvs.
96 -- req_theta
97 -- => res_ty
98 -- -> (forall ex_tvs. prov_theta => arg_tys -> r)
99 -- -> (Void# -> r)
100 -- -> r
101
102 psBuilder :: Maybe (Id, Bool)
103 -- Nothing => uni-directional pattern synonym
104 -- Just (builder, is_unlifted) => bi-directional
105 -- Builder function, of type
106 -- forall univ_tvs, ex_tvs. (req_theta, prov_theta)
107 -- => arg_tys -> res_ty
108 -- See Note [Builder for pattern synonyms with unboxed type]
109 }
110
111 {- Note [Pattern synonym signatures]
112 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
113 In a pattern synonym signature we write
114 pattern P :: req => prov => t1 -> ... tn -> res_ty
115
116 Note that the "required" context comes first, then the "provided"
117 context. Moreover, the "required" context must not mention
118 existentially-bound type variables; that is, ones not mentioned in
119 res_ty. See lots of discussion in Trac #10928.
120
121 If there is no "provided" context, you can omit it; but you
122 can't omit the "required" part (unless you omit both).
123
124 Example 1:
125 pattern P1 :: (Num a, Eq a) => b -> Maybe (a,b)
126 pattern P1 x = Just (3,x)
127
128 We require (Num a, Eq a) to match the 3; there is no provided
129 context.
130
131 Example 2:
132 data T2 where
133 MkT2 :: (Num a, Eq a) => a -> a -> T2
134
135 pattern P2 :: () => (Num a, Eq a) => a -> T2
136 pattern P2 x = MkT2 3 x
137
138 When we match against P2 we get a Num dictionary provided.
139 We can use that to check the match against 3.
140
141 Example 3:
142 pattern P3 :: Eq a => a -> b -> T3 b
143
144 This signature is illegal because the (Eq a) is a required
145 constraint, but it mentions the existentially-bound variable 'a'.
146 You can see it's existential because it doesn't appear in the
147 result type (T3 b).
148
149 Note [Pattern synonym representation]
150 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
151 Consider the following pattern synonym declaration
152
153 pattern P x = MkT [x] (Just 42)
154
155 where
156 data T a where
157 MkT :: (Show a, Ord b) => [b] -> a -> T a
158
159 so pattern P has type
160
161 b -> T (Maybe t)
162
163 with the following typeclass constraints:
164
165 requires: (Eq t, Num t)
166 provides: (Show (Maybe t), Ord b)
167
168 In this case, the fields of MkPatSyn will be set as follows:
169
170 psArgs = [b]
171 psArity = 1
172 psInfix = False
173
174 psUnivTyVars = [t]
175 psExTyVars = [b]
176 psProvTheta = (Show (Maybe t), Ord b)
177 psReqTheta = (Eq t, Num t)
178 psOrigResTy = T (Maybe t)
179
180 Note [Matchers and builders for pattern synonyms]
181 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
182 For each pattern synonym P, we generate
183
184 * a "matcher" function, used to desugar uses of P in patterns,
185 which implements pattern matching
186
187 * A "builder" function (for bidirectional pattern synonyms only),
188 used to desugar uses of P in expressions, which constructs P-values.
189
190 For the above example, the matcher function has type:
191
192 $mP :: forall (r :: ?) t. (Eq t, Num t)
193 => T (Maybe t)
194 -> (forall b. (Show (Maybe t), Ord b) => b -> r)
195 -> (Void# -> r)
196 -> r
197
198 with the following implementation:
199
200 $mP @r @t $dEq $dNum scrut cont fail
201 = case scrut of
202 MkT @b $dShow $dOrd [x] (Just 42) -> cont @b $dShow $dOrd x
203 _ -> fail Void#
204
205 Notice that the return type 'r' has an open kind, so that it can
206 be instantiated by an unboxed type; for example where we see
207 f (P x) = 3#
208
209 The extra Void# argument for the failure continuation is needed so that
210 it is lazy even when the result type is unboxed.
211
212 For the same reason, if the pattern has no arguments, an extra Void#
213 argument is added to the success continuation as well.
214
215 For *bidirectional* pattern synonyms, we also generate a "builder"
216 function which implements the pattern synonym in an expression
217 context. For our running example, it will be:
218
219 $bP :: forall t b. (Eq t, Num t, Show (Maybe t), Ord b)
220 => b -> T (Maybe t)
221 $bP x = MkT [x] (Just 42)
222
223 NB: the existential/universal and required/provided split does not
224 apply to the builder since you are only putting stuff in, not getting
225 stuff out.
226
227 Injectivity of bidirectional pattern synonyms is checked in
228 tcPatToExpr which walks the pattern and returns its corresponding
229 expression when available.
230
231 Note [Builder for pattern synonyms with unboxed type]
232 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
233 For bidirectional pattern synonyms that have no arguments and have an
234 unboxed type, we add an extra Void# argument to the builder, else it
235 would be a top-level declaration with an unboxed type.
236
237 pattern P = 0#
238
239 $bP :: Void# -> Int#
240 $bP _ = 0#
241
242 This means that when typechecking an occurrence of P in an expression,
243 we must remember that the builder has this void argument. This is
244 done by TcPatSyn.patSynBuilderOcc.
245
246 Note [Pattern synonyms and the data type Type]
247 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
248 The type of a pattern synonym is of the form (See Note
249 [Pattern synonym signatures]):
250
251 forall univ_tvs. req => forall ex_tvs. prov => ...
252
253 We cannot in general represent this by a value of type Type:
254
255 - if ex_tvs is empty, then req and prov cannot be distinguished from
256 each other
257 - if req is empty, then univ_tvs and ex_tvs cannot be distinguished
258 from each other, and moreover, prov is seen as the "required" context
259 (as it is the only context)
260
261
262 ************************************************************************
263 * *
264 \subsection{Instances}
265 * *
266 ************************************************************************
267 -}
268
269 instance Eq PatSyn where
270 (==) = (==) `on` getUnique
271 (/=) = (/=) `on` getUnique
272
273 instance Uniquable PatSyn where
274 getUnique = psUnique
275
276 instance NamedThing PatSyn where
277 getName = patSynName
278
279 instance Outputable PatSyn where
280 ppr = ppr . getName
281
282 instance OutputableBndr PatSyn where
283 pprInfixOcc = pprInfixName . getName
284 pprPrefixOcc = pprPrefixName . getName
285
286 instance Data.Data PatSyn where
287 -- don't traverse?
288 toConstr _ = abstractConstr "PatSyn"
289 gunfold _ _ = error "gunfold"
290 dataTypeOf _ = mkNoRepType "PatSyn"
291
292 {-
293 ************************************************************************
294 * *
295 \subsection{Construction}
296 * *
297 ************************************************************************
298 -}
299
300 -- | Build a new pattern synonym
301 mkPatSyn :: Name
302 -> Bool -- ^ Is the pattern synonym declared infix?
303 -> ([TyVar], [TyBinder], ThetaType)
304 -- ^ Universially-quantified type variables
305 -- and required dicts
306 -> ([TyVar], [TyBinder], ThetaType)
307 -- ^ Existentially-quantified type variables
308 -- and provided dicts
309 -> [Type] -- ^ Original arguments
310 -> Type -- ^ Original result type
311 -> (Id, Bool) -- ^ Name of matcher
312 -> Maybe (Id, Bool) -- ^ Name of builder
313 -> [FieldLabel] -- ^ Names of fields for
314 -- a record pattern synonym
315 -> PatSyn
316 -- NB: The univ and ex vars are both in TyBinder form and TyVar form for
317 -- convenience. All the TyBinders should be Named!
318 mkPatSyn name declared_infix
319 (univ_tvs, univ_bndrs, req_theta)
320 (ex_tvs, ex_bndrs, prov_theta)
321 orig_args
322 orig_res_ty
323 matcher builder field_labels
324 = MkPatSyn {psName = name, psUnique = getUnique name,
325 psUnivTyVars = univ_tvs, psUnivTyBinders = univ_bndrs,
326 psExTyVars = ex_tvs, psExTyBinders = ex_bndrs,
327 psProvTheta = prov_theta, psReqTheta = req_theta,
328 psInfix = declared_infix,
329 psArgs = orig_args,
330 psArity = length orig_args,
331 psOrigResTy = orig_res_ty,
332 psMatcher = matcher,
333 psBuilder = builder,
334 psFieldLabels = field_labels
335 }
336
337 -- | The 'Name' of the 'PatSyn', giving it a unique, rooted identification
338 patSynName :: PatSyn -> Name
339 patSynName = psName
340
341 -- | Should the 'PatSyn' be presented infix?
342 patSynIsInfix :: PatSyn -> Bool
343 patSynIsInfix = psInfix
344
345 -- | Arity of the pattern synonym
346 patSynArity :: PatSyn -> Arity
347 patSynArity = psArity
348
349 patSynArgs :: PatSyn -> [Type]
350 patSynArgs = psArgs
351
352 patSynFieldLabels :: PatSyn -> [FieldLabel]
353 patSynFieldLabels = psFieldLabels
354
355 -- | Extract the type for any given labelled field of the 'DataCon'
356 patSynFieldType :: PatSyn -> FieldLabelString -> Type
357 patSynFieldType ps label
358 = case find ((== label) . flLabel . fst) (psFieldLabels ps `zip` psArgs ps) of
359 Just (_, ty) -> ty
360 Nothing -> pprPanic "dataConFieldType" (ppr ps <+> ppr label)
361
362 patSynUnivTyBinders :: PatSyn -> [TyBinder]
363 patSynUnivTyBinders = psUnivTyBinders
364
365 patSynExTyVars :: PatSyn -> [TyVar]
366 patSynExTyVars = psExTyVars
367
368 patSynExTyBinders :: PatSyn -> [TyBinder]
369 patSynExTyBinders = psExTyBinders
370
371 patSynSig :: PatSyn -> ([TyVar], ThetaType, [TyVar], ThetaType, [Type], Type)
372 patSynSig (MkPatSyn { psUnivTyVars = univ_tvs, psExTyVars = ex_tvs
373 , psProvTheta = prov, psReqTheta = req
374 , psArgs = arg_tys, psOrigResTy = res_ty })
375 = (univ_tvs, req, ex_tvs, prov, arg_tys, res_ty)
376
377 patSynMatcher :: PatSyn -> (Id,Bool)
378 patSynMatcher = psMatcher
379
380 patSynBuilder :: PatSyn -> Maybe (Id, Bool)
381 patSynBuilder = psBuilder
382
383 tidyPatSynIds :: (Id -> Id) -> PatSyn -> PatSyn
384 tidyPatSynIds tidy_fn ps@(MkPatSyn { psMatcher = matcher, psBuilder = builder })
385 = ps { psMatcher = tidy_pr matcher, psBuilder = fmap tidy_pr builder }
386 where
387 tidy_pr (id, dummy) = (tidy_fn id, dummy)
388
389 patSynInstArgTys :: PatSyn -> [Type] -> [Type]
390 -- Return the types of the argument patterns
391 -- e.g. data D a = forall b. MkD a b (b->a)
392 -- pattern P f x y = MkD (x,True) y f
393 -- D :: forall a. forall b. a -> b -> (b->a) -> D a
394 -- P :: forall c. forall b. (b->(c,Bool)) -> c -> b -> P c
395 -- patSynInstArgTys P [Int,bb] = [bb->(Int,Bool), Int, bb]
396 -- NB: the inst_tys should be both universal and existential
397 patSynInstArgTys (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
398 , psExTyVars = ex_tvs, psArgs = arg_tys })
399 inst_tys
400 = ASSERT2( length tyvars == length inst_tys
401 , text "patSynInstArgTys" <+> ppr name $$ ppr tyvars $$ ppr inst_tys )
402 map (substTyWith tyvars inst_tys) arg_tys
403 where
404 tyvars = univ_tvs ++ ex_tvs
405
406 patSynInstResTy :: PatSyn -> [Type] -> Type
407 -- Return the type of whole pattern
408 -- E.g. pattern P x y = Just (x,x,y)
409 -- P :: a -> b -> Just (a,a,b)
410 -- (patSynInstResTy P [Int,Bool] = Maybe (Int,Int,Bool)
411 -- NB: unlikepatSynInstArgTys, the inst_tys should be just the *universal* tyvars
412 patSynInstResTy (MkPatSyn { psName = name, psUnivTyVars = univ_tvs
413 , psOrigResTy = res_ty })
414 inst_tys
415 = ASSERT2( length univ_tvs == length inst_tys
416 , text "patSynInstResTy" <+> ppr name $$ ppr univ_tvs $$ ppr inst_tys )
417 substTyWith univ_tvs inst_tys res_ty
418
419 -- | Print the type of a pattern synonym. The foralls are printed explicitly
420 pprPatSynType :: PatSyn -> SDoc
421 pprPatSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta
422 , psExTyVars = ex_tvs, psProvTheta = prov_theta
423 , psArgs = orig_args, psOrigResTy = orig_res_ty })
424 = sep [ pprForAllImplicit univ_tvs
425 , pprThetaArrowTy req_theta
426 , ppWhen insert_empty_ctxt $ parens empty <+> darrow
427 , pprType sigma_ty ]
428 where
429 sigma_ty = mkForAllTys (mkNamedBinders Specified ex_tvs) $
430 mkFunTys prov_theta $
431 mkFunTys orig_args orig_res_ty
432 insert_empty_ctxt = null req_theta && not (null prov_theta && null ex_tvs)