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