Track specified/invisible more carefully.
[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, DeriveDataTypeable #-}
9
10 module PatSyn (
11 -- * Main data types
12 PatSyn, mkPatSyn,
13
14 -- ** Type deconstruction
15 patSynName, patSynArity, patSynIsInfix,
16 patSynArgs, patSynType,
17 patSynMatcher, patSynBuilder,
18 patSynUnivTyBinders, patSynExTyVars, patSynExTyBinders, patSynSig,
19 patSynInstArgTys, patSynInstResTy, patSynFieldLabels,
20 patSynFieldType,
21
22 tidyPatSynIds
23 ) where
24
25 #include "HsVersions.h"
26
27 import Type
28 import TcType( mkSpecSigmaTy )
29 import Name
30 import Outputable
31 import Unique
32 import Util
33 import BasicTypes
34 import Var
35 import FieldLabel
36
37 import qualified Data.Data as Data
38 import qualified Data.Typeable
39 import Data.Function
40 import Data.List
41
42 {-
43 ************************************************************************
44 * *
45 \subsection{Pattern synonyms}
46 * *
47 ************************************************************************
48 -}
49
50 -- | A pattern synonym
51 -- See Note [Pattern synonym representation]
52 -- See Note [Pattern synonym signatures]
53 data PatSyn
54 = MkPatSyn {
55 psName :: Name,
56 psUnique :: Unique, -- Cached from Name
57
58 psArgs :: [Type],
59 psArity :: Arity, -- == length psArgs
60 psInfix :: Bool, -- True <=> declared infix
61 psFieldLabels :: [FieldLabel], -- List of fields for a
62 -- record pattern synonym
63 -- INVARIANT: either empty if no
64 -- record pat syn or same length as
65 -- psArgs
66
67 psUnivTyVars :: [TyVar], -- Universially-quantified type variables
68 psUnivTyBinders :: [TyBinder], -- same, with visibility info
69 psReqTheta :: ThetaType, -- Required dictionaries
70 -- these constraints are very much like
71 -- stupid thetas (which is a useful
72 -- guideline when implementing)
73 -- but are actually needed.
74 psExTyVars :: [TyVar], -- Existentially-quantified type vars
75 psExTyBinders :: [TyBinder], -- same, with visibility info
76 psProvTheta :: ThetaType, -- Provided dictionaries
77 psOrigResTy :: Type, -- Mentions only psUnivTyVars
78
79 -- See Note [Matchers and builders for pattern synonyms]
80 psMatcher :: (Id, Bool),
81 -- Matcher function.
82 -- If Bool is True then prov_theta and arg_tys are empty
83 -- and type is
84 -- forall (p :: RuntimeRep) (r :: TYPE p) univ_tvs.
85 -- req_theta
86 -- => res_ty
87 -- -> (forall ex_tvs. Void# -> r)
88 -- -> (Void# -> r)
89 -- -> r
90 --
91 -- Otherwise type is
92 -- forall (p :: RuntimeRep) (r :: TYPE r) univ_tvs.
93 -- req_theta
94 -- => res_ty
95 -- -> (forall ex_tvs. prov_theta => arg_tys -> r)
96 -- -> (Void# -> r)
97 -- -> r
98
99 psBuilder :: Maybe (Id, Bool)
100 -- Nothing => uni-directional pattern synonym
101 -- Just (builder, is_unlifted) => bi-directional
102 -- Builder function, of type
103 -- forall univ_tvs, ex_tvs. (req_theta, prov_theta)
104 -- => arg_tys -> res_ty
105 -- See Note [Builder for pattern synonyms with unboxed type]
106 }
107 deriving Data.Typeable.Typeable
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
245 ************************************************************************
246 * *
247 \subsection{Instances}
248 * *
249 ************************************************************************
250 -}
251
252 instance Eq PatSyn where
253 (==) = (==) `on` getUnique
254 (/=) = (/=) `on` getUnique
255
256 instance Ord PatSyn where
257 (<=) = (<=) `on` getUnique
258 (<) = (<) `on` getUnique
259 (>=) = (>=) `on` getUnique
260 (>) = (>) `on` getUnique
261 compare = compare `on` getUnique
262
263 instance Uniquable PatSyn where
264 getUnique = psUnique
265
266 instance NamedThing PatSyn where
267 getName = patSynName
268
269 instance Outputable PatSyn where
270 ppr = ppr . getName
271
272 instance OutputableBndr PatSyn where
273 pprInfixOcc = pprInfixName . getName
274 pprPrefixOcc = pprPrefixName . getName
275
276 instance Data.Data PatSyn where
277 -- don't traverse?
278 toConstr _ = abstractConstr "PatSyn"
279 gunfold _ _ = error "gunfold"
280 dataTypeOf _ = mkNoRepType "PatSyn"
281
282 {-
283 ************************************************************************
284 * *
285 \subsection{Construction}
286 * *
287 ************************************************************************
288 -}
289
290 -- | Build a new pattern synonym
291 mkPatSyn :: Name
292 -> Bool -- ^ Is the pattern synonym declared infix?
293 -> ([TyVar], [TyBinder], ThetaType)
294 -- ^ Universially-quantified type variables
295 -- and required dicts
296 -> ([TyVar], [TyBinder], ThetaType)
297 -- ^ Existentially-quantified type variables
298 -- and provided dicts
299 -> [Type] -- ^ Original arguments
300 -> Type -- ^ Original result type
301 -> (Id, Bool) -- ^ Name of matcher
302 -> Maybe (Id, Bool) -- ^ Name of builder
303 -> [FieldLabel] -- ^ Names of fields for
304 -- a record pattern synonym
305 -> PatSyn
306 -- NB: The univ and ex vars are both in TyBinder form and TyVar form for
307 -- convenience. All the TyBinders should be Named!
308 mkPatSyn name declared_infix
309 (univ_tvs, univ_bndrs, req_theta)
310 (ex_tvs, ex_bndrs, prov_theta)
311 orig_args
312 orig_res_ty
313 matcher builder field_labels
314 = MkPatSyn {psName = name, psUnique = getUnique name,
315 psUnivTyVars = univ_tvs, psUnivTyBinders = univ_bndrs,
316 psExTyVars = ex_tvs, psExTyBinders = ex_bndrs,
317 psProvTheta = prov_theta, psReqTheta = req_theta,
318 psInfix = declared_infix,
319 psArgs = orig_args,
320 psArity = length orig_args,
321 psOrigResTy = orig_res_ty,
322 psMatcher = matcher,
323 psBuilder = builder,
324 psFieldLabels = field_labels
325 }
326
327 -- | The 'Name' of the 'PatSyn', giving it a unique, rooted identification
328 patSynName :: PatSyn -> Name
329 patSynName = psName
330
331 patSynType :: PatSyn -> Type
332 -- The full pattern type, used only in error messages
333 -- See Note [Pattern synonym signatures]
334 patSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta
335 , psExTyVars = ex_tvs, psProvTheta = prov_theta
336 , psArgs = orig_args, psOrigResTy = orig_res_ty })
337 = mkSpecSigmaTy univ_tvs req_theta $ -- use mkSpecSigmaTy because it
338 mkSpecSigmaTy ex_tvs prov_theta $ -- prints better
339 mkFunTys orig_args orig_res_ty
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