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