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