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