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