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