0da0cb1382266ddd4d160a299d0332cccb05e77b
[ghc.git] / compiler / typecheck / TcTyDecls.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1999
4
5
6 Analysis functions over data types. Specficially, detecting recursive types.
7
8 This stuff is only used for source-code decls; it's recorded in interface
9 files for imported data types.
10 -}
11
12 {-# LANGUAGE CPP #-}
13
14 module TcTyDecls(
15 calcRecFlags, RecTyInfo(..),
16 calcSynCycles, calcClassCycles,
17 RoleAnnots, extractRoleAnnots, emptyRoleAnnots, lookupRoleAnnots,
18 mkDefaultMethodIds, mkRecSelBinds, mkOneRecordSelector
19 ) where
20
21 #include "HsVersions.h"
22
23 import TcRnMonad
24 import TcEnv
25 import TcType
26 import TysWiredIn( unitTy )
27 import MkCore( rEC_SEL_ERROR_ID )
28 import TypeRep
29 import HsSyn
30 import Class
31 import Type
32 import TyCon
33 import ConLike
34 import DataCon
35 import Name
36 import NameEnv
37 import RdrName ( mkVarUnqual )
38 import Var ( tyVarKind )
39 import Id
40 import IdInfo
41 import VarEnv
42 import VarSet
43 import NameSet
44 import Coercion ( ltRole )
45 import Digraph
46 import BasicTypes
47 import SrcLoc
48 import Unique ( mkBuiltinUnique )
49 import Outputable
50 import UniqSet
51 import Util
52 import Maybes
53 import Data.List
54 import Bag
55 import FastString ( fastStringToByteString )
56
57 import Control.Monad
58
59 {-
60 ************************************************************************
61 * *
62 Cycles in class and type synonym declarations
63 * *
64 ************************************************************************
65
66 Checking for class-decl loops is easy, because we don't allow class decls
67 in interface files.
68
69 We allow type synonyms in hi-boot files, but we *trust* hi-boot files,
70 so we don't check for loops that involve them. So we only look for synonym
71 loops in the module being compiled.
72
73 We check for type synonym and class cycles on the *source* code.
74 Main reasons:
75
76 a) Otherwise we'd need a special function to extract type-synonym tycons
77 from a type, whereas we already have the free vars pinned on the decl
78
79 b) If we checked for type synonym loops after building the TyCon, we
80 can't do a hoistForAllTys on the type synonym rhs, (else we fall into
81 a black hole) which seems unclean. Apart from anything else, it'd mean
82 that a type-synonym rhs could have for-alls to the right of an arrow,
83 which means adding new cases to the validity checker
84
85 Indeed, in general, checking for cycles beforehand means we need to
86 be less careful about black holes through synonym cycles.
87
88 The main disadvantage is that a cycle that goes via a type synonym in an
89 .hi-boot file can lead the compiler into a loop, because it assumes that cycles
90 only occur entirely within the source code of the module being compiled.
91 But hi-boot files are trusted anyway, so this isn't much worse than (say)
92 a kind error.
93
94 [ NOTE ----------------------------------------------
95 If we reverse this decision, this comment came from tcTyDecl1, and should
96 go back there
97 -- dsHsType, not tcHsKindedType, to avoid a loop. tcHsKindedType does hoisting,
98 -- which requires looking through synonyms... and therefore goes into a loop
99 -- on (erroneously) recursive synonyms.
100 -- Solution: do not hoist synonyms, because they'll be hoisted soon enough
101 -- when they are substituted
102
103 We'd also need to add back in this definition
104
105 synonymTyConsOfType :: Type -> [TyCon]
106 -- Does not look through type synonyms at all
107 -- Return a list of synonym tycons
108 synonymTyConsOfType ty
109 = nameEnvElts (go ty)
110 where
111 go :: Type -> NameEnv TyCon -- The NameEnv does duplicate elim
112 go (TyVarTy v) = emptyNameEnv
113 go (TyConApp tc tys) = go_tc tc tys
114 go (AppTy a b) = go a `plusNameEnv` go b
115 go (FunTy a b) = go a `plusNameEnv` go b
116 go (ForAllTy _ ty) = go ty
117
118 go_tc tc tys | isTypeSynonymTyCon tc = extendNameEnv (go_s tys)
119 (tyConName tc) tc
120 | otherwise = go_s tys
121 go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
122 ---------------------------------------- END NOTE ]
123 -}
124
125 mkSynEdges :: [LTyClDecl Name] -> [(LTyClDecl Name, Name, [Name])]
126 mkSynEdges syn_decls = [ (ldecl, name, nameSetElems fvs)
127 | ldecl@(L _ (SynDecl { tcdLName = L _ name
128 , tcdFVs = fvs })) <- syn_decls ]
129
130 calcSynCycles :: [LTyClDecl Name] -> [SCC (LTyClDecl Name)]
131 calcSynCycles = stronglyConnCompFromEdgedVertices . mkSynEdges
132
133 {-
134 Note [Superclass cycle check]
135 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
136 We can't allow cycles via superclasses because it would result in the
137 type checker looping when it canonicalises a class constraint (superclasses
138 are added during canonicalisation). More precisely, given a constraint
139 C ty1 .. tyn
140 we want to instantiate all of C's superclasses, transitively, and
141 that set must be finite. So if
142 class (D b, E b a) => C a b
143 then when we encounter the constraint
144 C ty1 ty2
145 we'll instantiate the superclasses
146 (D ty2, E ty2 ty1)
147 and then *their* superclasses, and so on. This set must be finite!
148
149 It is OK for superclasses to be type synonyms for other classes, so
150 must "look through" type synonyms. Eg
151 type X a = C [a]
152 class X a => C a -- No! Recursive superclass!
153
154 We want definitions such as:
155
156 class C cls a where cls a => a -> a
157 class C D a => D a where
158
159 to be accepted, even though a naive acyclicity check would reject the
160 program as having a cycle between D and its superclass. Why? Because
161 when we instantiate
162 D ty1
163 we get the superclas
164 C D ty1
165 and C has no superclasses, so we have terminated with a finite set.
166
167 More precisely, the rule is this: the superclasses sup_C of a class C
168 are rejected iff:
169
170 C \elem expand(sup_C)
171
172 Where expand is defined as follows:
173
174 (1) expand(a ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
175
176 (2) expand(D ty1 ... tyN) = {D}
177 \union sup_D[ty1/x1, ..., tyP/xP]
178 \union expand(ty(P+1)) ... \union expand(tyN)
179 where (D x1 ... xM) is a class, P = min(M,N)
180
181 (3) expand(T ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
182 where T is not a class
183
184 Eqn (1) is conservative; when there's a type variable at the head,
185 look in all the argument types. Eqn (2) expands superclasses; the
186 third component of the union is like Eqn (1). Eqn (3) happens mainly
187 when the context is a (constraint) tuple, such as (Eq a, Show a).
188
189 Furthermore, expand always looks through type synonyms.
190 -}
191
192 calcClassCycles :: Class -> [[TyCon]]
193 calcClassCycles cls
194 = nubBy eqAsCycle $
195 expandTheta (unitUniqSet cls) [classTyCon cls] (classSCTheta cls) []
196 where
197 -- The last TyCon in the cycle is always the same as the first
198 eqAsCycle xs ys = any (xs ==) (cycles (tail ys))
199 cycles xs = take n . map (take n) . tails . cycle $ xs
200 where n = length xs
201
202 -- No more superclasses to expand ==> no problems with cycles
203 -- See Note [Superclass cycle check]
204 expandTheta :: UniqSet Class -- Path of Classes to here in set form
205 -> [TyCon] -- Path to here
206 -> ThetaType -- Superclass work list
207 -> [[TyCon]] -- Input error paths
208 -> [[TyCon]] -- Final error paths
209 expandTheta _ _ [] = id
210 expandTheta seen path (pred:theta) = expandType seen path pred . expandTheta seen path theta
211
212 expandType seen path (TyConApp tc tys)
213 -- Expand unsaturated classes to their superclass theta if they are yet unseen.
214 -- If they have already been seen then we have detected an error!
215 | Just cls <- tyConClass_maybe tc
216 , let (env, remainder) = papp (classTyVars cls) tys
217 rest_tys = either (const []) id remainder
218 = if cls `elementOfUniqSet` seen
219 then (reverse (classTyCon cls:path):)
220 . flip (foldr (expandType seen path)) tys
221 else expandTheta (addOneToUniqSet seen cls) (tc:path)
222 (substTys (mkTopTvSubst env) (classSCTheta cls))
223 . flip (foldr (expandType seen path)) rest_tys
224
225 -- For synonyms, try to expand them: some arguments might be
226 -- phantoms, after all. We can expand with impunity because at
227 -- this point the type synonym cycle check has already happened.
228 | Just (tvs, rhs) <- synTyConDefn_maybe tc
229 , let (env, remainder) = papp tvs tys
230 rest_tys = either (const []) id remainder
231 = expandType seen (tc:path) (substTy (mkTopTvSubst env) rhs)
232 . flip (foldr (expandType seen path)) rest_tys
233
234 -- For non-class, non-synonyms, just check the arguments
235 | otherwise
236 = flip (foldr (expandType seen path)) tys
237
238 expandType _ _ (TyVarTy {}) = id
239 expandType _ _ (LitTy {}) = id
240 expandType seen path (AppTy t1 t2) = expandType seen path t1 . expandType seen path t2
241 expandType seen path (FunTy t1 t2) = expandType seen path t1 . expandType seen path t2
242 expandType seen path (ForAllTy _tv t) = expandType seen path t
243
244 papp :: [TyVar] -> [Type] -> ([(TyVar, Type)], Either [TyVar] [Type])
245 papp [] tys = ([], Right tys)
246 papp tvs [] = ([], Left tvs)
247 papp (tv:tvs) (ty:tys) = ((tv, ty):env, remainder)
248 where (env, remainder) = papp tvs tys
249
250 {-
251 ************************************************************************
252 * *
253 Deciding which type constructors are recursive
254 * *
255 ************************************************************************
256
257 Identification of recursive TyCons
258 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
259 The knot-tying parameters: @rec_details_list@ is an alist mapping @Name@s to
260 @TyThing@s.
261
262 Identifying a TyCon as recursive serves two purposes
263
264 1. Avoid infinite types. Non-recursive newtypes are treated as
265 "transparent", like type synonyms, after the type checker. If we did
266 this for all newtypes, we'd get infinite types. So we figure out for
267 each newtype whether it is "recursive", and add a coercion if so. In
268 effect, we are trying to "cut the loops" by identifying a loop-breaker.
269
270 2. Avoid infinite unboxing. This has nothing to do with newtypes.
271 Suppose we have
272 data T = MkT Int T
273 f (MkT x t) = f t
274 Well, this function diverges, but we don't want the strictness analyser
275 to diverge. But the strictness analyser will diverge because it looks
276 deeper and deeper into the structure of T. (I believe there are
277 examples where the function does something sane, and the strictness
278 analyser still diverges, but I can't see one now.)
279
280 Now, concerning (1), the FC2 branch currently adds a coercion for ALL
281 newtypes. I did this as an experiment, to try to expose cases in which
282 the coercions got in the way of optimisations. If it turns out that we
283 can indeed always use a coercion, then we don't risk recursive types,
284 and don't need to figure out what the loop breakers are.
285
286 For newtype *families* though, we will always have a coercion, so they
287 are always loop breakers! So you can easily adjust the current
288 algorithm by simply treating all newtype families as loop breakers (and
289 indeed type families). I think.
290
291
292
293 For newtypes, we label some as "recursive" such that
294
295 INVARIANT: there is no cycle of non-recursive newtypes
296
297 In any loop, only one newtype need be marked as recursive; it is
298 a "loop breaker". Labelling more than necessary as recursive is OK,
299 provided the invariant is maintained.
300
301 A newtype M.T is defined to be "recursive" iff
302 (a) it is declared in an hi-boot file (see RdrHsSyn.hsIfaceDecl)
303 (b) it is declared in a source file, but that source file has a
304 companion hi-boot file which declares the type
305 or (c) one can get from T's rhs to T via type
306 synonyms, or non-recursive newtypes *in M*
307 e.g. newtype T = MkT (T -> Int)
308
309 (a) is conservative; declarations in hi-boot files are always
310 made loop breakers. That's why in (b) we can restrict attention
311 to tycons in M, because any loops through newtypes outside M
312 will be broken by those newtypes
313 (b) ensures that a newtype is not treated as a loop breaker in one place
314 and later as a non-loop-breaker. This matters in GHCi particularly, when
315 a newtype T might be embedded in many types in the environment, and then
316 T's source module is compiled. We don't want T's recursiveness to change.
317
318 The "recursive" flag for algebraic data types is irrelevant (never consulted)
319 for types with more than one constructor.
320
321
322 An algebraic data type M.T is "recursive" iff
323 it has just one constructor, and
324 (a) it is declared in an hi-boot file (see RdrHsSyn.hsIfaceDecl)
325 (b) it is declared in a source file, but that source file has a
326 companion hi-boot file which declares the type
327 or (c) one can get from its arg types to T via type synonyms,
328 or by non-recursive newtypes or non-recursive product types in M
329 e.g. data T = MkT (T -> Int) Bool
330 Just like newtype in fact
331
332 A type synonym is recursive if one can get from its
333 right hand side back to it via type synonyms. (This is
334 reported as an error.)
335
336 A class is recursive if one can get from its superclasses
337 back to it. (This is an error too.)
338
339 Hi-boot types
340 ~~~~~~~~~~~~~
341 A data type read from an hi-boot file will have an AbstractTyCon as its AlgTyConRhs
342 and will respond True to isAbstractTyCon. The idea is that we treat these as if one
343 could get from these types to anywhere. So when we see
344
345 module Baz where
346 import {-# SOURCE #-} Foo( T )
347 newtype S = MkS T
348
349 then we mark S as recursive, just in case. What that means is that if we see
350
351 import Baz( S )
352 newtype R = MkR S
353
354 then we don't need to look inside S to compute R's recursiveness. Since S is imported
355 (not from an hi-boot file), one cannot get from R back to S except via an hi-boot file,
356 and that means that some data type will be marked recursive along the way. So R is
357 unconditionly non-recursive (i.e. there'll be a loop breaker elsewhere if necessary)
358
359 This in turn means that we grovel through fewer interface files when computing
360 recursiveness, because we need only look at the type decls in the module being
361 compiled, plus the outer structure of directly-mentioned types.
362 -}
363
364 data RecTyInfo = RTI { rti_promotable :: Bool
365 , rti_roles :: Name -> [Role]
366 , rti_is_rec :: Name -> RecFlag }
367
368 calcRecFlags :: SelfBootInfo -> Bool -- hs-boot file?
369 -> RoleAnnots -> [TyThing] -> RecTyInfo
370 -- The 'boot_names' are the things declared in M.hi-boot, if M is the current module.
371 -- Any type constructors in boot_names are automatically considered loop breakers
372 calcRecFlags boot_details is_boot mrole_env tyclss
373 = RTI { rti_promotable = is_promotable
374 , rti_roles = roles
375 , rti_is_rec = is_rec }
376 where
377 rec_tycon_names = mkNameSet (map tyConName all_tycons)
378 all_tycons = mapMaybe getTyCon tyclss
379 -- Recursion of newtypes/data types can happen via
380 -- the class TyCon, so tyclss includes the class tycons
381
382 is_promotable = all (isPromotableTyCon rec_tycon_names) all_tycons
383
384 roles = inferRoles is_boot mrole_env all_tycons
385
386 ----------------- Recursion calculation ----------------
387 is_rec n | n `elemNameSet` rec_names = Recursive
388 | otherwise = NonRecursive
389
390 boot_name_set = case boot_details of
391 NoSelfBoot -> emptyNameSet
392 SelfBoot { sb_tcs = tcs } -> tcs
393 rec_names = boot_name_set `unionNameSet`
394 nt_loop_breakers `unionNameSet`
395 prod_loop_breakers
396
397
398 -------------------------------------------------
399 -- NOTE
400 -- These edge-construction loops rely on
401 -- every loop going via tyclss, the types and classes
402 -- in the module being compiled. Stuff in interface
403 -- files should be correctly marked. If not (e.g. a
404 -- type synonym in a hi-boot file) we can get an infinite
405 -- loop. We could program round this, but it'd make the code
406 -- rather less nice, so I'm not going to do that yet.
407
408 single_con_tycons = [ tc | tc <- all_tycons
409 , not (tyConName tc `elemNameSet` boot_name_set)
410 -- Remove the boot_name_set because they are
411 -- going to be loop breakers regardless.
412 , isSingleton (tyConDataCons tc) ]
413 -- Both newtypes and data types, with exactly one data constructor
414
415 (new_tycons, prod_tycons) = partition isNewTyCon single_con_tycons
416 -- NB: we do *not* call isProductTyCon because that checks
417 -- for vanilla-ness of data constructors; and that depends
418 -- on empty existential type variables; and that is figured
419 -- out by tcResultType; which uses tcMatchTy; which uses
420 -- coreView; which calls expandSynTyCon_maybe; which uses
421 -- the recursiveness of the TyCon. Result... a black hole.
422 -- YUK YUK YUK
423
424 --------------- Newtypes ----------------------
425 nt_loop_breakers = mkNameSet (findLoopBreakers nt_edges)
426 is_rec_nt tc = tyConName tc `elemNameSet` nt_loop_breakers
427 -- is_rec_nt is a locally-used helper function
428
429 nt_edges = [(t, mk_nt_edges t) | t <- new_tycons]
430
431 mk_nt_edges nt -- Invariant: nt is a newtype
432 = [ tc | tc <- nameEnvElts (tyConsOfType (new_tc_rhs nt))
433 -- tyConsOfType looks through synonyms
434 , tc `elem` new_tycons ]
435 -- If not (tc `elem` new_tycons) we know that either it's a local *data* type,
436 -- or it's imported. Either way, it can't form part of a newtype cycle
437
438 --------------- Product types ----------------------
439 prod_loop_breakers = mkNameSet (findLoopBreakers prod_edges)
440
441 prod_edges = [(tc, mk_prod_edges tc) | tc <- prod_tycons]
442
443 mk_prod_edges tc -- Invariant: tc is a product tycon
444 = concatMap (mk_prod_edges1 tc) (dataConOrigArgTys (head (tyConDataCons tc)))
445
446 mk_prod_edges1 ptc ty = concatMap (mk_prod_edges2 ptc) (nameEnvElts (tyConsOfType ty))
447
448 mk_prod_edges2 ptc tc
449 | tc `elem` prod_tycons = [tc] -- Local product
450 | tc `elem` new_tycons = if is_rec_nt tc -- Local newtype
451 then []
452 else mk_prod_edges1 ptc (new_tc_rhs tc)
453 -- At this point we know that either it's a local non-product data type,
454 -- or it's imported. Either way, it can't form part of a cycle
455 | otherwise = []
456
457 new_tc_rhs :: TyCon -> Type
458 new_tc_rhs tc = snd (newTyConRhs tc) -- Ignore the type variables
459
460 getTyCon :: TyThing -> Maybe TyCon
461 getTyCon (ATyCon tc) = Just tc
462 getTyCon _ = Nothing
463
464 findLoopBreakers :: [(TyCon, [TyCon])] -> [Name]
465 -- Finds a set of tycons that cut all loops
466 findLoopBreakers deps
467 = go [(tc,tc,ds) | (tc,ds) <- deps]
468 where
469 go edges = [ name
470 | CyclicSCC ((tc,_,_) : edges') <- stronglyConnCompFromEdgedVerticesR edges,
471 name <- tyConName tc : go edges']
472
473 {-
474 ************************************************************************
475 * *
476 Promotion calculation
477 * *
478 ************************************************************************
479
480 See Note [Checking whether a group is promotable]
481 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
482 We only want to promote a TyCon if all its data constructors
483 are promotable; it'd be very odd to promote some but not others.
484
485 But the data constructors may mention this or other TyCons.
486
487 So we treat the recursive uses as all OK (ie promotable) and
488 do one pass to check that each TyCon is promotable.
489
490 Currently type synonyms are not promotable, though that
491 could change.
492 -}
493
494 isPromotableTyCon :: NameSet -> TyCon -> Bool
495 isPromotableTyCon rec_tycons tc
496 = isAlgTyCon tc -- Only algebraic; not even synonyms
497 -- (we could reconsider the latter)
498 && ok_kind (tyConKind tc)
499 && case algTyConRhs tc of
500 DataTyCon { data_cons = cs } -> all ok_con cs
501 NewTyCon { data_con = c } -> ok_con c
502 AbstractTyCon {} -> False
503 DataFamilyTyCon {} -> False
504 TupleTyCon { tup_sort = sort } -> case sort of
505 BoxedTuple -> True
506 UnboxedTuple -> False
507 ConstraintTuple -> False
508 where
509 ok_kind kind = all isLiftedTypeKind args && isLiftedTypeKind res
510 where -- Checks for * -> ... -> * -> *
511 (args, res) = splitKindFunTys kind
512
513 -- See Note [Promoted data constructors] in TyCon
514 ok_con con = all (isLiftedTypeKind . tyVarKind) ex_tvs
515 && null eq_spec -- No constraints
516 && null theta
517 && all (isPromotableType rec_tycons) orig_arg_tys
518 where
519 (_, ex_tvs, eq_spec, theta, orig_arg_tys, _) = dataConFullSig con
520
521
522 isPromotableType :: NameSet -> Type -> Bool
523 -- Must line up with DataCon.promoteType
524 -- But the function lives here because we must treat the
525 -- *recursive* tycons as promotable
526 isPromotableType rec_tcs con_arg_ty
527 = go con_arg_ty
528 where
529 go (TyConApp tc tys) = tys `lengthIs` tyConArity tc
530 && (tyConName tc `elemNameSet` rec_tcs
531 || isJust (promotableTyCon_maybe tc))
532 && all go tys
533 go (FunTy arg res) = go arg && go res
534 go (TyVarTy {}) = True
535 go _ = False
536
537 {-
538 ************************************************************************
539 * *
540 Role annotations
541 * *
542 ************************************************************************
543 -}
544
545 type RoleAnnots = NameEnv (LRoleAnnotDecl Name)
546
547 extractRoleAnnots :: TyClGroup Name -> RoleAnnots
548 extractRoleAnnots (TyClGroup { group_roles = roles })
549 = mkNameEnv [ (tycon, role_annot)
550 | role_annot@(L _ (RoleAnnotDecl (L _ tycon) _)) <- roles ]
551
552 emptyRoleAnnots :: RoleAnnots
553 emptyRoleAnnots = emptyNameEnv
554
555 lookupRoleAnnots :: RoleAnnots -> Name -> Maybe (LRoleAnnotDecl Name)
556 lookupRoleAnnots = lookupNameEnv
557
558 {-
559 ************************************************************************
560 * *
561 Role inference
562 * *
563 ************************************************************************
564
565 Note [Role inference]
566 ~~~~~~~~~~~~~~~~~~~~~
567 The role inference algorithm datatype definitions to infer the roles on the
568 parameters. Although these roles are stored in the tycons, we can perform this
569 algorithm on the built tycons, as long as we don't peek at an as-yet-unknown
570 roles field! Ah, the magic of laziness.
571
572 First, we choose appropriate initial roles. For families and classes, roles
573 (including initial roles) are N. For datatypes, we start with the role in the
574 role annotation (if any), or otherwise use Phantom. This is done in
575 initialRoleEnv1.
576
577 The function irGroup then propagates role information until it reaches a
578 fixpoint, preferring N over (R or P) and R over P. To aid in this, we have a
579 monad RoleM, which is a combination reader and state monad. In its state are
580 the current RoleEnv, which gets updated by role propagation, and an update
581 bit, which we use to know whether or not we've reached the fixpoint. The
582 environment of RoleM contains the tycon whose parameters we are inferring, and
583 a VarEnv from parameters to their positions, so we can update the RoleEnv.
584 Between tycons, this reader information is missing; it is added by
585 addRoleInferenceInfo.
586
587 There are two kinds of tycons to consider: algebraic ones (excluding classes)
588 and type synonyms. (Remember, families don't participate -- all their parameters
589 are N.) An algebraic tycon processes each of its datacons, in turn. Note that
590 a datacon's universally quantified parameters might be different from the parent
591 tycon's parameters, so we use the datacon's univ parameters in the mapping from
592 vars to positions. Note also that we don't want to infer roles for existentials
593 (they're all at N, too), so we put them in the set of local variables. As an
594 optimisation, we skip any tycons whose roles are already all Nominal, as there
595 nowhere else for them to go. For synonyms, we just analyse their right-hand sides.
596
597 irType walks through a type, looking for uses of a variable of interest and
598 propagating role information. Because anything used under a phantom position
599 is at phantom and anything used under a nominal position is at nominal, the
600 irType function can assume that anything it sees is at representational. (The
601 other possibilities are pruned when they're encountered.)
602
603 The rest of the code is just plumbing.
604
605 How do we know that this algorithm is correct? It should meet the following
606 specification:
607
608 Let Z be a role context -- a mapping from variables to roles. The following
609 rules define the property (Z |- t : r), where t is a type and r is a role:
610
611 Z(a) = r' r' <= r
612 ------------------------- RCVar
613 Z |- a : r
614
615 ---------- RCConst
616 Z |- T : r -- T is a type constructor
617
618 Z |- t1 : r
619 Z |- t2 : N
620 -------------- RCApp
621 Z |- t1 t2 : r
622
623 forall i<=n. (r_i is R or N) implies Z |- t_i : r_i
624 roles(T) = r_1 .. r_n
625 ---------------------------------------------------- RCDApp
626 Z |- T t_1 .. t_n : R
627
628 Z, a:N |- t : r
629 ---------------------- RCAll
630 Z |- forall a:k.t : r
631
632
633 We also have the following rules:
634
635 For all datacon_i in type T, where a_1 .. a_n are universally quantified
636 and b_1 .. b_m are existentially quantified, and the arguments are t_1 .. t_p,
637 then if forall j<=p, a_1 : r_1 .. a_n : r_n, b_1 : N .. b_m : N |- t_j : R,
638 then roles(T) = r_1 .. r_n
639
640 roles(->) = R, R
641 roles(~#) = N, N
642
643 With -dcore-lint on, the output of this algorithm is checked in checkValidRoles,
644 called from checkValidTycon.
645
646 Note [Role-checking data constructor arguments]
647 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
648 Consider
649 data T a where
650 MkT :: Eq b => F a -> (a->a) -> T (G a)
651
652 Then we want to check the roles at which 'a' is used
653 in MkT's type. We want to work on the user-written type,
654 so we need to take into account
655 * the arguments: (F a) and (a->a)
656 * the context: C a b
657 * the result type: (G a) -- this is in the eq_spec
658 -}
659
660 type RoleEnv = NameEnv [Role] -- from tycon names to roles
661
662 -- This, and any of the functions it calls, must *not* look at the roles
663 -- field of a tycon we are inferring roles about!
664 -- See Note [Role inference]
665 inferRoles :: Bool -> RoleAnnots -> [TyCon] -> Name -> [Role]
666 inferRoles is_boot annots tycons
667 = let role_env = initialRoleEnv is_boot annots tycons
668 role_env' = irGroup role_env tycons in
669 \name -> case lookupNameEnv role_env' name of
670 Just roles -> roles
671 Nothing -> pprPanic "inferRoles" (ppr name)
672
673 initialRoleEnv :: Bool -> RoleAnnots -> [TyCon] -> RoleEnv
674 initialRoleEnv is_boot annots = extendNameEnvList emptyNameEnv .
675 map (initialRoleEnv1 is_boot annots)
676
677 initialRoleEnv1 :: Bool -> RoleAnnots -> TyCon -> (Name, [Role])
678 initialRoleEnv1 is_boot annots_env tc
679 | isFamilyTyCon tc = (name, map (const Nominal) tyvars)
680 | isAlgTyCon tc = (name, default_roles)
681 | isTypeSynonymTyCon tc = (name, default_roles)
682 | otherwise = pprPanic "initialRoleEnv1" (ppr tc)
683 where name = tyConName tc
684 tyvars = tyConTyVars tc
685 (kvs, tvs) = span isKindVar tyvars
686
687 -- if the number of annotations in the role annotation decl
688 -- is wrong, just ignore it. We check this in the validity check.
689 role_annots
690 = case lookupNameEnv annots_env name of
691 Just (L _ (RoleAnnotDecl _ annots))
692 | annots `equalLength` tvs -> map unLoc annots
693 _ -> map (const Nothing) tvs
694 default_roles = map (const Nominal) kvs ++
695 zipWith orElse role_annots (repeat default_role)
696
697 default_role
698 | isClassTyCon tc = Nominal
699 | is_boot && isAbstractTyCon tc = Representational
700 | otherwise = Phantom
701
702 irGroup :: RoleEnv -> [TyCon] -> RoleEnv
703 irGroup env tcs
704 = let (env', update) = runRoleM env $ mapM_ irTyCon tcs in
705 if update
706 then irGroup env' tcs
707 else env'
708
709 irTyCon :: TyCon -> RoleM ()
710 irTyCon tc
711 | isAlgTyCon tc
712 = do { old_roles <- lookupRoles tc
713 ; unless (all (== Nominal) old_roles) $ -- also catches data families,
714 -- which don't want or need role inference
715 do { whenIsJust (tyConClass_maybe tc) (irClass tc_name)
716 ; addRoleInferenceInfo tc_name (tyConTyVars tc) $
717 mapM_ (irType emptyVarSet) (tyConStupidTheta tc) -- See #8958
718 ; mapM_ (irDataCon tc_name) (visibleDataCons $ algTyConRhs tc) }}
719
720 | Just ty <- synTyConRhs_maybe tc
721 = addRoleInferenceInfo tc_name (tyConTyVars tc) $
722 irType emptyVarSet ty
723
724 | otherwise
725 = return ()
726
727 where
728 tc_name = tyConName tc
729
730 -- any type variable used in an associated type must be Nominal
731 irClass :: Name -> Class -> RoleM ()
732 irClass tc_name cls
733 = addRoleInferenceInfo tc_name cls_tvs $
734 mapM_ ir_at (classATs cls)
735 where
736 cls_tvs = classTyVars cls
737 cls_tv_set = mkVarSet cls_tvs
738
739 ir_at at_tc
740 = mapM_ (updateRole Nominal) (varSetElems nvars)
741 where nvars = (mkVarSet $ tyConTyVars at_tc) `intersectVarSet` cls_tv_set
742
743 -- See Note [Role inference]
744 irDataCon :: Name -> DataCon -> RoleM ()
745 irDataCon tc_name datacon
746 = addRoleInferenceInfo tc_name univ_tvs $
747 mapM_ (irType ex_var_set) (eqSpecPreds eq_spec ++ theta ++ arg_tys)
748 -- See Note [Role-checking data constructor arguments]
749 where
750 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig datacon
751 ex_var_set = mkVarSet ex_tvs
752
753 irType :: VarSet -> Type -> RoleM ()
754 irType = go
755 where
756 go lcls (TyVarTy tv) = unless (tv `elemVarSet` lcls) $
757 updateRole Representational tv
758 go lcls (AppTy t1 t2) = go lcls t1 >> mark_nominal lcls t2
759 go lcls (TyConApp tc tys)
760 = do { roles <- lookupRolesX tc
761 ; zipWithM_ (go_app lcls) roles tys }
762 go lcls (FunTy t1 t2) = go lcls t1 >> go lcls t2
763 go lcls (ForAllTy tv ty) = go (extendVarSet lcls tv) ty
764 go _ (LitTy {}) = return ()
765
766 go_app _ Phantom _ = return () -- nothing to do here
767 go_app lcls Nominal ty = mark_nominal lcls ty -- all vars below here are N
768 go_app lcls Representational ty = go lcls ty
769
770 mark_nominal lcls ty = let nvars = tyVarsOfType ty `minusVarSet` lcls in
771 mapM_ (updateRole Nominal) (varSetElems nvars)
772
773 -- like lookupRoles, but with Nominal tags at the end for oversaturated TyConApps
774 lookupRolesX :: TyCon -> RoleM [Role]
775 lookupRolesX tc
776 = do { roles <- lookupRoles tc
777 ; return $ roles ++ repeat Nominal }
778
779 -- gets the roles either from the environment or the tycon
780 lookupRoles :: TyCon -> RoleM [Role]
781 lookupRoles tc
782 = do { env <- getRoleEnv
783 ; case lookupNameEnv env (tyConName tc) of
784 Just roles -> return roles
785 Nothing -> return $ tyConRoles tc }
786
787 -- tries to update a role; won't ever update a role "downwards"
788 updateRole :: Role -> TyVar -> RoleM ()
789 updateRole role tv
790 = do { var_ns <- getVarNs
791 ; case lookupVarEnv var_ns tv of
792 { Nothing -> pprPanic "updateRole" (ppr tv)
793 ; Just n -> do
794 { name <- getTyConName
795 ; updateRoleEnv name n role }}}
796
797 -- the state in the RoleM monad
798 data RoleInferenceState = RIS { role_env :: RoleEnv
799 , update :: Bool }
800
801 -- the environment in the RoleM monad
802 type VarPositions = VarEnv Int
803 data RoleInferenceInfo = RII { var_ns :: VarPositions
804 , name :: Name }
805
806 -- See [Role inference]
807 newtype RoleM a = RM { unRM :: Maybe RoleInferenceInfo
808 -> RoleInferenceState
809 -> (a, RoleInferenceState) }
810
811 instance Functor RoleM where
812 fmap = liftM
813
814 instance Applicative RoleM where
815 pure x = RM $ \_ state -> (x, state)
816 (<*>) = ap
817
818 instance Monad RoleM where
819 return = pure
820 a >>= f = RM $ \m_info state -> let (a', state') = unRM a m_info state in
821 unRM (f a') m_info state'
822
823 runRoleM :: RoleEnv -> RoleM () -> (RoleEnv, Bool)
824 runRoleM env thing = (env', update)
825 where RIS { role_env = env', update = update } = snd $ unRM thing Nothing state
826 state = RIS { role_env = env, update = False }
827
828 addRoleInferenceInfo :: Name -> [TyVar] -> RoleM a -> RoleM a
829 addRoleInferenceInfo name tvs thing
830 = RM $ \_nothing state -> ASSERT( isNothing _nothing )
831 unRM thing (Just info) state
832 where info = RII { var_ns = mkVarEnv (zip tvs [0..]), name = name }
833
834 getRoleEnv :: RoleM RoleEnv
835 getRoleEnv = RM $ \_ state@(RIS { role_env = env }) -> (env, state)
836
837 getVarNs :: RoleM VarPositions
838 getVarNs = RM $ \m_info state ->
839 case m_info of
840 Nothing -> panic "getVarNs"
841 Just (RII { var_ns = var_ns }) -> (var_ns, state)
842
843 getTyConName :: RoleM Name
844 getTyConName = RM $ \m_info state ->
845 case m_info of
846 Nothing -> panic "getTyConName"
847 Just (RII { name = name }) -> (name, state)
848
849
850 updateRoleEnv :: Name -> Int -> Role -> RoleM ()
851 updateRoleEnv name n role
852 = RM $ \_ state@(RIS { role_env = role_env }) -> ((),
853 case lookupNameEnv role_env name of
854 Nothing -> pprPanic "updateRoleEnv" (ppr name)
855 Just roles -> let (before, old_role : after) = splitAt n roles in
856 if role `ltRole` old_role
857 then let roles' = before ++ role : after
858 role_env' = extendNameEnv role_env name roles' in
859 RIS { role_env = role_env', update = True }
860 else state )
861
862 {-
863 ************************************************************************
864 * *
865 Building record selectors
866 * *
867 ************************************************************************
868 -}
869
870 mkDefaultMethodIds :: [TyThing] -> [Id]
871 -- See Note [Default method Ids and Template Haskell]
872 mkDefaultMethodIds things
873 = [ mkExportedLocalId VanillaId dm_name (idType sel_id)
874 | ATyCon tc <- things
875 , Just cls <- [tyConClass_maybe tc]
876 , (sel_id, DefMeth dm_name) <- classOpItems cls ]
877
878 {-
879 Note [Default method Ids and Template Haskell]
880 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
881 Consider this (Trac #4169):
882 class Numeric a where
883 fromIntegerNum :: a
884 fromIntegerNum = ...
885
886 ast :: Q [Dec]
887 ast = [d| instance Numeric Int |]
888
889 When we typecheck 'ast' we have done the first pass over the class decl
890 (in tcTyClDecls), but we have not yet typechecked the default-method
891 declarations (because they can mention value declarations). So we
892 must bring the default method Ids into scope first (so they can be seen
893 when typechecking the [d| .. |] quote, and typecheck them later.
894 -}
895
896 mkRecSelBinds :: [TyThing] -> HsValBinds Name
897 -- NB We produce *un-typechecked* bindings, rather like 'deriving'
898 -- This makes life easier, because the later type checking will add
899 -- all necessary type abstractions and applications
900 mkRecSelBinds tycons
901 = ValBindsOut [(NonRecursive, b) | b <- binds] sigs
902 where
903 (sigs, binds) = unzip rec_sels
904 rec_sels = map mkRecSelBind [ (tc,fld)
905 | ATyCon tc <- tycons
906 , fld <- tyConFieldLabels tc ]
907
908
909 mkRecSelBind :: (TyCon, FieldLabel) -> (LSig Name, LHsBinds Name)
910 mkRecSelBind (tycon, fl)
911 = mkOneRecordSelector all_cons (RecSelData tycon) fl
912 where
913 all_cons = map RealDataCon (tyConDataCons tycon)
914
915 mkOneRecordSelector :: [ConLike] -> RecSelParent -> FieldLabel
916 -> (LSig Name, LHsBinds Name)
917 mkOneRecordSelector all_cons idDetails fl =
918 (L loc (IdSig sel_id), unitBag (L loc sel_bind))
919 where
920 loc = getSrcSpan sel_name
921 lbl = flLabel fl
922 sel_name = flSelector fl
923
924 sel_id = mkExportedLocalId rec_details sel_name sel_ty
925 rec_details = RecSelId { sel_tycon = idDetails, sel_naughty = is_naughty }
926
927 -- Find a representative constructor, con1
928
929 cons_w_field = conLikesWithFields all_cons [lbl]
930 con1 = ASSERT( not (null cons_w_field) ) head cons_w_field
931 -- Selector type; Note [Polymorphic selectors]
932 field_ty = conLikeFieldType con1 lbl
933 data_tvs = tyVarsOfType data_ty
934 is_naughty = not (tyVarsOfType field_ty `subVarSet` data_tvs)
935 (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
936 sel_ty | is_naughty = unitTy -- See Note [Naughty record selectors]
937 | otherwise = mkForAllTys (varSetElemsKvsFirst $
938 data_tvs `extendVarSetList` field_tvs) $
939 mkPhiTy (conLikeStupidTheta con1) $ -- Urgh!
940 mkPhiTy field_theta $ -- Urgh!
941 -- req_theta is empty for normal DataCon
942 mkPhiTy req_theta $
943 mkFunTy data_ty field_tau
944
945 -- Make the binding: sel (C2 { fld = x }) = x
946 -- sel (C7 { fld = x }) = x
947 -- where cons_w_field = [C2,C7]
948 sel_bind = mkTopFunBind Generated sel_lname alts
949 where
950 alts | is_naughty = [mkSimpleMatch [] unit_rhs]
951 | otherwise = map mk_match cons_w_field ++ deflt
952 mk_match con = mkSimpleMatch [L loc (mk_sel_pat con)]
953 (L loc (HsVar field_var))
954 mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields)
955 rec_fields = HsRecFields { rec_flds = [rec_field], rec_dotdot = Nothing }
956 rec_field = noLoc (HsRecField { hsRecFieldLbl = L loc (FieldOcc (mkVarUnqual lbl) sel_name)
957 , hsRecFieldArg = L loc (VarPat field_var)
958 , hsRecPun = False })
959 sel_lname = L loc sel_name
960 field_var = mkInternalName (mkBuiltinUnique 1) (getOccName sel_name) loc
961
962 -- Add catch-all default case unless the case is exhaustive
963 -- We do this explicitly so that we get a nice error message that
964 -- mentions this particular record selector
965 deflt | all dealt_with all_cons = []
966 | otherwise = [mkSimpleMatch [L loc (WildPat placeHolderType)]
967 (mkHsApp (L loc (HsVar (getName rEC_SEL_ERROR_ID)))
968 (L loc (HsLit msg_lit)))]
969
970 -- Do not add a default case unless there are unmatched
971 -- constructors. We must take account of GADTs, else we
972 -- get overlap warning messages from the pattern-match checker
973 -- NB: we need to pass type args for the *representation* TyCon
974 -- to dataConCannotMatch, hence the calculation of inst_tys
975 -- This matters in data families
976 -- data instance T Int a where
977 -- A :: { fld :: Int } -> T Int Bool
978 -- B :: { fld :: Int } -> T Int Char
979 dealt_with :: ConLike -> Bool
980 dealt_with (PatSynCon _) = False -- We can't predict overlap
981 dealt_with con@(RealDataCon dc) =
982 con `elem` cons_w_field || dataConCannotMatch inst_tys dc
983
984 (univ_tvs, _, eq_spec, _, req_theta, _, data_ty) = conLikeFullSig con1
985
986 inst_tys = substTyVars (mkTopTvSubst eq_spec) univ_tvs
987
988 unit_rhs = mkLHsTupleExpr []
989 msg_lit = HsStringPrim "" (fastStringToByteString lbl)
990
991 {-
992 Note [Polymorphic selectors]
993 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
994 When a record has a polymorphic field, we pull the foralls out to the front.
995 data T = MkT { f :: forall a. [a] -> a }
996 Then f :: forall a. T -> [a] -> a
997 NOT f :: T -> forall a. [a] -> a
998
999 This is horrid. It's only needed in deeply obscure cases, which I hate.
1000 The only case I know is test tc163, which is worth looking at. It's far
1001 from clear that this test should succeed at all!
1002
1003 Note [Naughty record selectors]
1004 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1005 A "naughty" field is one for which we can't define a record
1006 selector, because an existential type variable would escape. For example:
1007 data T = forall a. MkT { x,y::a }
1008 We obviously can't define
1009 x (MkT v _) = v
1010 Nevertheless we *do* put a RecSelId into the type environment
1011 so that if the user tries to use 'x' as a selector we can bleat
1012 helpfully, rather than saying unhelpfully that 'x' is not in scope.
1013 Hence the sel_naughty flag, to identify record selectors that don't really exist.
1014
1015 In general, a field is "naughty" if its type mentions a type variable that
1016 isn't in the result type of the constructor. Note that this *allows*
1017 GADT record selectors (Note [GADT record selectors]) whose types may look
1018 like sel :: T [a] -> a
1019
1020 For naughty selectors we make a dummy binding
1021 sel = ()
1022 for naughty selectors, so that the later type-check will add them to the
1023 environment, and they'll be exported. The function is never called, because
1024 the tyepchecker spots the sel_naughty field.
1025
1026 Note [GADT record selectors]
1027 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1028 For GADTs, we require that all constructors with a common field 'f' have the same
1029 result type (modulo alpha conversion). [Checked in TcTyClsDecls.checkValidTyCon]
1030 E.g.
1031 data T where
1032 T1 { f :: Maybe a } :: T [a]
1033 T2 { f :: Maybe a, y :: b } :: T [a]
1034 T3 :: T Int
1035
1036 and now the selector takes that result type as its argument:
1037 f :: forall a. T [a] -> Maybe a
1038
1039 Details: the "real" types of T1,T2 are:
1040 T1 :: forall r a. (r~[a]) => a -> T r
1041 T2 :: forall r a b. (r~[a]) => a -> b -> T r
1042
1043 So the selector loooks like this:
1044 f :: forall a. T [a] -> Maybe a
1045 f (a:*) (t:T [a])
1046 = case t of
1047 T1 c (g:[a]~[c]) (v:Maybe c) -> v `cast` Maybe (right (sym g))
1048 T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
1049 T3 -> error "T3 does not have field f"
1050
1051 Note the forall'd tyvars of the selector are just the free tyvars
1052 of the result type; there may be other tyvars in the constructor's
1053 type (e.g. 'b' in T2).
1054
1055 Note the need for casts in the result!
1056
1057 Note [Selector running example]
1058 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1059 It's OK to combine GADTs and type families. Here's a running example:
1060
1061 data instance T [a] where
1062 T1 { fld :: b } :: T [Maybe b]
1063
1064 The representation type looks like this
1065 data :R7T a where
1066 T1 { fld :: b } :: :R7T (Maybe b)
1067
1068 and there's coercion from the family type to the representation type
1069 :CoR7T a :: T [a] ~ :R7T a
1070
1071 The selector we want for fld looks like this:
1072
1073 fld :: forall b. T [Maybe b] -> b
1074 fld = /\b. \(d::T [Maybe b]).
1075 case d `cast` :CoR7T (Maybe b) of
1076 T1 (x::b) -> x
1077
1078 The scrutinee of the case has type :R7T (Maybe b), which can be
1079 gotten by appying the eq_spec to the univ_tvs of the data con.
1080
1081 -}