c998853b2ae911eb130a7bb9c90718963481fb6a
[ghc.git] / compiler / typecheck / TcTyDecls.lhs
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 \begin{code}
12 {-# LANGUAGE CPP #-}
13
14 module TcTyDecls(
15         calcRecFlags, RecTyInfo(..),
16         calcSynCycles, calcClassCycles,
17         RoleAnnots, extractRoleAnnots, emptyRoleAnnots, lookupRoleAnnots
18     ) where
19
20 #include "HsVersions.h"
21
22 import TypeRep
23 import HsSyn
24 import Class
25 import Type
26 import Kind
27 import HscTypes
28 import TyCon
29 import DataCon
30 import Var
31 import Name
32 import NameEnv
33 import VarEnv
34 import VarSet
35 import NameSet
36 import Coercion ( ltRole )
37 import Avail
38 import Digraph
39 import BasicTypes
40 import SrcLoc
41 import Outputable
42 import UniqSet
43 import Util
44 import Maybes
45 import Data.List
46
47 #if __GLASGOW_HASKELL__ < 709
48 import Control.Applicative (Applicative(..))
49 #endif
50
51 import Control.Monad
52 \end{code}
53
54
55 %************************************************************************
56 %*                                                                      *
57         Cycles in class and type synonym declarations
58 %*                                                                      *
59 %************************************************************************
60
61 Checking for class-decl loops is easy, because we don't allow class decls
62 in interface files.
63
64 We allow type synonyms in hi-boot files, but we *trust* hi-boot files,
65 so we don't check for loops that involve them.  So we only look for synonym
66 loops in the module being compiled.
67
68 We check for type synonym and class cycles on the *source* code.
69 Main reasons:
70
71   a) Otherwise we'd need a special function to extract type-synonym tycons
72      from a type, whereas we already have the free vars pinned on the decl
73
74   b) If we checked for type synonym loops after building the TyCon, we
75         can't do a hoistForAllTys on the type synonym rhs, (else we fall into
76         a black hole) which seems unclean.  Apart from anything else, it'd mean
77         that a type-synonym rhs could have for-alls to the right of an arrow,
78         which means adding new cases to the validity checker
79
80         Indeed, in general, checking for cycles beforehand means we need to
81         be less careful about black holes through synonym cycles.
82
83 The main disadvantage is that a cycle that goes via a type synonym in an
84 .hi-boot file can lead the compiler into a loop, because it assumes that cycles
85 only occur entirely within the source code of the module being compiled.
86 But hi-boot files are trusted anyway, so this isn't much worse than (say)
87 a kind error.
88
89 [  NOTE ----------------------------------------------
90 If we reverse this decision, this comment came from tcTyDecl1, and should
91  go back there
92         -- dsHsType, not tcHsKindedType, to avoid a loop.  tcHsKindedType does hoisting,
93         -- which requires looking through synonyms... and therefore goes into a loop
94         -- on (erroneously) recursive synonyms.
95         -- Solution: do not hoist synonyms, because they'll be hoisted soon enough
96         --           when they are substituted
97
98 We'd also need to add back in this definition
99
100 synTyConsOfType :: Type -> [TyCon]
101 -- Does not look through type synonyms at all
102 -- Return a list of synonym tycons
103 synTyConsOfType ty
104   = nameEnvElts (go ty)
105   where
106      go :: Type -> NameEnv TyCon  -- The NameEnv does duplicate elim
107      go (TyVarTy v)               = emptyNameEnv
108      go (TyConApp tc tys)         = go_tc tc tys
109      go (AppTy a b)               = go a `plusNameEnv` go b
110      go (FunTy a b)               = go a `plusNameEnv` go b
111      go (ForAllTy _ ty)           = go ty
112
113      go_tc tc tys | isSynTyCon tc = extendNameEnv (go_s tys) (tyConName tc) tc
114                   | otherwise     = go_s tys
115      go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
116 ---------------------------------------- END NOTE ]
117
118 \begin{code}
119 mkSynEdges :: [LTyClDecl Name] -> [(LTyClDecl Name, Name, [Name])]
120 mkSynEdges syn_decls = [ (ldecl, name, nameSetElems fvs)
121                        | ldecl@(L _ (SynDecl { tcdLName = L _ name
122                                              , tcdFVs = fvs })) <- syn_decls ]
123
124 calcSynCycles :: [LTyClDecl Name] -> [SCC (LTyClDecl Name)]
125 calcSynCycles = stronglyConnCompFromEdgedVertices . mkSynEdges
126 \end{code}
127
128 Note [Superclass cycle check]
129 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
130 We can't allow cycles via superclasses because it would result in the
131 type checker looping when it canonicalises a class constraint (superclasses
132 are added during canonicalisation).  More precisely, given a constraint
133     C ty1 .. tyn
134 we want to instantiate all of C's superclasses, transitively, and
135 that set must be finite.  So if
136      class (D b, E b a) => C a b
137 then when we encounter the constraint
138      C ty1 ty2
139 we'll instantiate the superclasses
140      (D ty2, E ty2 ty1)
141 and then *their* superclasses, and so on.  This set must be finite!
142
143 It is OK for superclasses to be type synonyms for other classes, so
144 must "look through" type synonyms. Eg
145      type X a = C [a]
146      class X a => C a   -- No!  Recursive superclass!
147
148 We want definitions such as:
149
150   class C cls a where cls a => a -> a
151   class C D a => D a where
152
153 to be accepted, even though a naive acyclicity check would reject the
154 program as having a cycle between D and its superclass.  Why? Because
155 when we instantiate
156      D ty1
157 we get the superclas
158      C D ty1
159 and C has no superclasses, so we have terminated with a finite set.
160
161 More precisely, the rule is this: the superclasses sup_C of a class C
162 are rejected iff:
163
164   C \elem expand(sup_C)
165
166 Where expand is defined as follows:
167
168 (1)  expand(a ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
169
170 (2)  expand(D ty1 ... tyN) = {D}
171                              \union sup_D[ty1/x1, ..., tyP/xP]
172                              \union expand(ty(P+1)) ... \union expand(tyN)
173            where (D x1 ... xM) is a class, P = min(M,N)
174
175 (3)  expand(T ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
176         where T is not a class
177
178 Eqn (1) is conservative; when there's a type variable at the head,
179 look in all the argument types.  Eqn (2) expands superclasses; the
180 third component of the union is like Eqn (1).  Eqn (3) happens mainly
181 when the context is a (constraint) tuple, such as (Eq a, Show a).
182
183 Furthermore, expand always looks through type synonyms.
184
185 \begin{code}
186 calcClassCycles :: Class -> [[TyCon]]
187 calcClassCycles cls
188   = nubBy eqAsCycle $
189     expandTheta (unitUniqSet cls) [classTyCon cls] (classSCTheta cls) []
190   where
191     -- The last TyCon in the cycle is always the same as the first
192     eqAsCycle xs ys = any (xs ==) (cycles (tail ys))
193     cycles xs = take n . map (take n) . tails . cycle $ xs
194       where n = length xs
195
196     -- No more superclasses to expand ==> no problems with cycles
197     -- See Note [Superclass cycle check]
198     expandTheta :: UniqSet Class -- Path of Classes to here in set form
199                 -> [TyCon]       -- Path to here
200                 -> ThetaType     -- Superclass work list
201                 -> [[TyCon]]     -- Input error paths
202                 -> [[TyCon]]     -- Final error paths
203     expandTheta _    _    []           = id
204     expandTheta seen path (pred:theta) = expandType seen path pred . expandTheta seen path theta
205
206     expandType seen path (TyConApp tc tys)
207       -- Expand unsaturated classes to their superclass theta if they are yet unseen.
208       -- If they have already been seen then we have detected an error!
209       | Just cls <- tyConClass_maybe tc
210       , let (env, remainder) = papp (classTyVars cls) tys
211             rest_tys = either (const []) id remainder
212       = if cls `elementOfUniqSet` seen
213          then (reverse (classTyCon cls:path):)
214               . flip (foldr (expandType seen path)) tys
215          else expandTheta (addOneToUniqSet seen cls) (tc:path)
216                           (substTys (mkTopTvSubst env) (classSCTheta cls))
217               . flip (foldr (expandType seen path)) rest_tys
218
219       -- For synonyms, try to expand them: some arguments might be
220       -- phantoms, after all. We can expand with impunity because at
221       -- this point the type synonym cycle check has already happened.
222       | Just (tvs, rhs) <- synTyConDefn_maybe tc
223       , let (env, remainder) = papp tvs tys
224             rest_tys = either (const []) id remainder
225       = expandType seen (tc:path) (substTy (mkTopTvSubst env) rhs)
226         . flip (foldr (expandType seen path)) rest_tys
227
228       -- For non-class, non-synonyms, just check the arguments
229       | otherwise
230       = flip (foldr (expandType seen path)) tys
231
232     expandType _    _    (TyVarTy {})     = id
233     expandType _    _    (LitTy {})       = id
234     expandType seen path (AppTy t1 t2)    = expandType seen path t1 . expandType seen path t2
235     expandType seen path (FunTy t1 t2)    = expandType seen path t1 . expandType seen path t2
236     expandType seen path (ForAllTy _tv t) = expandType seen path t
237
238     papp :: [TyVar] -> [Type] -> ([(TyVar, Type)], Either [TyVar] [Type])
239     papp []       tys      = ([], Right tys)
240     papp tvs      []       = ([], Left tvs)
241     papp (tv:tvs) (ty:tys) = ((tv, ty):env, remainder)
242       where (env, remainder) = papp tvs tys
243 \end{code}
244
245
246 %************************************************************************
247 %*                                                                      *
248         Deciding which type constructors are recursive
249 %*                                                                      *
250 %************************************************************************
251
252 Identification of recursive TyCons
253 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
254 The knot-tying parameters: @rec_details_list@ is an alist mapping @Name@s to
255 @TyThing@s.
256
257 Identifying a TyCon as recursive serves two purposes
258
259 1.  Avoid infinite types.  Non-recursive newtypes are treated as
260 "transparent", like type synonyms, after the type checker.  If we did
261 this for all newtypes, we'd get infinite types.  So we figure out for
262 each newtype whether it is "recursive", and add a coercion if so.  In
263 effect, we are trying to "cut the loops" by identifying a loop-breaker.
264
265 2.  Avoid infinite unboxing.  This has nothing to do with newtypes.
266 Suppose we have
267         data T = MkT Int T
268         f (MkT x t) = f t
269 Well, this function diverges, but we don't want the strictness analyser
270 to diverge.  But the strictness analyser will diverge because it looks
271 deeper and deeper into the structure of T.   (I believe there are
272 examples where the function does something sane, and the strictness
273 analyser still diverges, but I can't see one now.)
274
275 Now, concerning (1), the FC2 branch currently adds a coercion for ALL
276 newtypes.  I did this as an experiment, to try to expose cases in which
277 the coercions got in the way of optimisations.  If it turns out that we
278 can indeed always use a coercion, then we don't risk recursive types,
279 and don't need to figure out what the loop breakers are.
280
281 For newtype *families* though, we will always have a coercion, so they
282 are always loop breakers!  So you can easily adjust the current
283 algorithm by simply treating all newtype families as loop breakers (and
284 indeed type families).  I think.
285
286
287
288 For newtypes, we label some as "recursive" such that
289
290     INVARIANT: there is no cycle of non-recursive newtypes
291
292 In any loop, only one newtype need be marked as recursive; it is
293 a "loop breaker".  Labelling more than necessary as recursive is OK,
294 provided the invariant is maintained.
295
296 A newtype M.T is defined to be "recursive" iff
297         (a) it is declared in an hi-boot file (see RdrHsSyn.hsIfaceDecl)
298         (b) it is declared in a source file, but that source file has a
299             companion hi-boot file which declares the type
300    or   (c) one can get from T's rhs to T via type
301             synonyms, or non-recursive newtypes *in M*
302              e.g.  newtype T = MkT (T -> Int)
303
304 (a) is conservative; declarations in hi-boot files are always
305         made loop breakers. That's why in (b) we can restrict attention
306         to tycons in M, because any loops through newtypes outside M
307         will be broken by those newtypes
308 (b) ensures that a newtype is not treated as a loop breaker in one place
309 and later as a non-loop-breaker.  This matters in GHCi particularly, when
310 a newtype T might be embedded in many types in the environment, and then
311 T's source module is compiled.  We don't want T's recursiveness to change.
312
313 The "recursive" flag for algebraic data types is irrelevant (never consulted)
314 for types with more than one constructor.
315
316
317 An algebraic data type M.T is "recursive" iff
318         it has just one constructor, and
319         (a) it is declared in an hi-boot file (see RdrHsSyn.hsIfaceDecl)
320         (b) it is declared in a source file, but that source file has a
321             companion hi-boot file which declares the type
322  or     (c) one can get from its arg types to T via type synonyms,
323             or by non-recursive newtypes or non-recursive product types in M
324              e.g.  data T = MkT (T -> Int) Bool
325 Just like newtype in fact
326
327 A type synonym is recursive if one can get from its
328 right hand side back to it via type synonyms.  (This is
329 reported as an error.)
330
331 A class is recursive if one can get from its superclasses
332 back to it.  (This is an error too.)
333
334 Hi-boot types
335 ~~~~~~~~~~~~~
336 A data type read from an hi-boot file will have an AbstractTyCon as its AlgTyConRhs
337 and will respond True to isAbstractTyCon. The idea is that we treat these as if one
338 could get from these types to anywhere.  So when we see
339
340         module Baz where
341         import {-# SOURCE #-} Foo( T )
342         newtype S = MkS T
343
344 then we mark S as recursive, just in case. What that means is that if we see
345
346         import Baz( S )
347         newtype R = MkR S
348
349 then we don't need to look inside S to compute R's recursiveness.  Since S is imported
350 (not from an hi-boot file), one cannot get from R back to S except via an hi-boot file,
351 and that means that some data type will be marked recursive along the way.  So R is
352 unconditionly non-recursive (i.e. there'll be a loop breaker elsewhere if necessary)
353
354 This in turn means that we grovel through fewer interface files when computing
355 recursiveness, because we need only look at the type decls in the module being
356 compiled, plus the outer structure of directly-mentioned types.
357
358 \begin{code}
359 data RecTyInfo = RTI { rti_promotable :: Bool
360                      , rti_roles      :: Name -> [Role]
361                      , rti_is_rec     :: Name -> RecFlag }
362
363 calcRecFlags :: ModDetails -> Bool  -- hs-boot file?
364              -> RoleAnnots -> [TyThing] -> RecTyInfo
365 -- The 'boot_names' are the things declared in M.hi-boot, if M is the current module.
366 -- Any type constructors in boot_names are automatically considered loop breakers
367 calcRecFlags boot_details is_boot mrole_env tyclss
368   = RTI { rti_promotable = is_promotable
369         , rti_roles      = roles
370         , rti_is_rec     = is_rec }
371   where
372     rec_tycon_names = mkNameSet (map tyConName all_tycons)
373     all_tycons = mapMaybe getTyCon tyclss
374                    -- Recursion of newtypes/data types can happen via
375                    -- the class TyCon, so tyclss includes the class tycons
376
377     is_promotable = all (isPromotableTyCon rec_tycon_names) all_tycons
378
379     roles = inferRoles is_boot mrole_env all_tycons
380
381     ----------------- Recursion calculation ----------------
382     is_rec n | n `elemNameSet` rec_names = Recursive
383              | otherwise                 = NonRecursive
384
385     boot_name_set = availsToNameSet (md_exports boot_details)
386     rec_names = boot_name_set     `unionNameSet`
387                 nt_loop_breakers  `unionNameSet`
388                 prod_loop_breakers
389
390
391         -------------------------------------------------
392         --                      NOTE
393         -- These edge-construction loops rely on
394         -- every loop going via tyclss, the types and classes
395         -- in the module being compiled.  Stuff in interface
396         -- files should be correctly marked.  If not (e.g. a
397         -- type synonym in a hi-boot file) we can get an infinite
398         -- loop.  We could program round this, but it'd make the code
399         -- rather less nice, so I'm not going to do that yet.
400
401     single_con_tycons = [ tc | tc <- all_tycons
402                              , not (tyConName tc `elemNameSet` boot_name_set)
403                                  -- Remove the boot_name_set because they are
404                                  -- going to be loop breakers regardless.
405                              , isSingleton (tyConDataCons tc) ]
406         -- Both newtypes and data types, with exactly one data constructor
407
408     (new_tycons, prod_tycons) = partition isNewTyCon single_con_tycons
409         -- NB: we do *not* call isProductTyCon because that checks
410         --     for vanilla-ness of data constructors; and that depends
411         --     on empty existential type variables; and that is figured
412         --     out by tcResultType; which uses tcMatchTy; which uses
413         --     coreView; which calls coreExpandTyCon_maybe; which uses
414         --     the recursiveness of the TyCon.  Result... a black hole.
415         -- YUK YUK YUK
416
417         --------------- Newtypes ----------------------
418     nt_loop_breakers = mkNameSet (findLoopBreakers nt_edges)
419     is_rec_nt tc = tyConName tc  `elemNameSet` nt_loop_breakers
420         -- is_rec_nt is a locally-used helper function
421
422     nt_edges = [(t, mk_nt_edges t) | t <- new_tycons]
423
424     mk_nt_edges nt      -- Invariant: nt is a newtype
425         = [ tc | tc <- nameEnvElts (tyConsOfType (new_tc_rhs nt))
426                         -- tyConsOfType looks through synonyms
427                , tc `elem` new_tycons ]
428            -- If not (tc `elem` new_tycons) we know that either it's a local *data* type,
429            -- or it's imported.  Either way, it can't form part of a newtype cycle
430
431         --------------- Product types ----------------------
432     prod_loop_breakers = mkNameSet (findLoopBreakers prod_edges)
433
434     prod_edges = [(tc, mk_prod_edges tc) | tc <- prod_tycons]
435
436     mk_prod_edges tc    -- Invariant: tc is a product tycon
437         = concatMap (mk_prod_edges1 tc) (dataConOrigArgTys (head (tyConDataCons tc)))
438
439     mk_prod_edges1 ptc ty = concatMap (mk_prod_edges2 ptc) (nameEnvElts (tyConsOfType ty))
440
441     mk_prod_edges2 ptc tc
442         | tc `elem` prod_tycons   = [tc]                -- Local product
443         | tc `elem` new_tycons    = if is_rec_nt tc     -- Local newtype
444                                     then []
445                                     else mk_prod_edges1 ptc (new_tc_rhs tc)
446                 -- At this point we know that either it's a local non-product data type,
447                 -- or it's imported.  Either way, it can't form part of a cycle
448         | otherwise = []
449
450 new_tc_rhs :: TyCon -> Type
451 new_tc_rhs tc = snd (newTyConRhs tc)    -- Ignore the type variables
452
453 getTyCon :: TyThing -> Maybe TyCon
454 getTyCon (ATyCon tc) = Just tc
455 getTyCon _           = Nothing
456
457 findLoopBreakers :: [(TyCon, [TyCon])] -> [Name]
458 -- Finds a set of tycons that cut all loops
459 findLoopBreakers deps
460   = go [(tc,tc,ds) | (tc,ds) <- deps]
461   where
462     go edges = [ name
463                | CyclicSCC ((tc,_,_) : edges') <- stronglyConnCompFromEdgedVerticesR edges,
464                  name <- tyConName tc : go edges']
465 \end{code}
466
467
468 %************************************************************************
469 %*                                                                      *
470                   Promotion calculation
471 %*                                                                      *
472 %************************************************************************
473
474 See Note [Checking whether a group is promotable]
475 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
476 We only want to promote a TyCon if all its data constructors
477 are promotable; it'd be very odd to promote some but not others.
478
479 But the data constructors may mention this or other TyCons.
480
481 So we treat the recursive uses as all OK (ie promotable) and
482 do one pass to check that each TyCon is promotable.
483
484 Currently type synonyms are not promotable, though that
485 could change.
486
487 \begin{code}
488 isPromotableTyCon :: NameSet -> TyCon -> Bool
489 isPromotableTyCon rec_tycons tc
490   =  isAlgTyCon tc    -- Only algebraic; not even synonyms
491                      -- (we could reconsider the latter)
492   && ok_kind (tyConKind tc)
493   && case algTyConRhs tc of
494        DataTyCon { data_cons = cs } -> all ok_con cs
495        NewTyCon { data_con = c }    -> ok_con c
496        AbstractTyCon {}             -> False
497        DataFamilyTyCon {}           -> False
498
499   where
500     ok_kind kind = all isLiftedTypeKind args && isLiftedTypeKind res
501             where  -- Checks for * -> ... -> * -> *
502               (args, res) = splitKindFunTys kind
503
504     -- See Note [Promoted data constructors] in TyCon
505     ok_con con = all (isLiftedTypeKind . tyVarKind) ex_tvs
506               && null eq_spec   -- No constraints
507               && null theta
508               && all (isPromotableType rec_tycons) orig_arg_tys
509        where
510          (_, ex_tvs, eq_spec, theta, orig_arg_tys, _) = dataConFullSig con
511
512
513 isPromotableType :: NameSet -> Type -> Bool
514 -- Must line up with DataCon.promoteType
515 -- But the function lives here because we must treat the
516 -- *recursive* tycons as promotable
517 isPromotableType rec_tcs con_arg_ty
518   = go con_arg_ty
519   where
520     go (TyConApp tc tys) =  tys `lengthIs` tyConArity tc
521                          && (tyConName tc `elemNameSet` rec_tcs
522                              || isJust (promotableTyCon_maybe tc))
523                          && all go tys
524     go (FunTy arg res)   = go arg && go res
525     go (TyVarTy {})      = True
526     go _                 = False
527 \end{code}
528
529 %************************************************************************
530 %*                                                                      *
531         Role annotations
532 %*                                                                      *
533 %************************************************************************
534
535 \begin{code}
536 type RoleAnnots = NameEnv (LRoleAnnotDecl Name)
537
538 extractRoleAnnots :: TyClGroup Name -> RoleAnnots
539 extractRoleAnnots (TyClGroup { group_roles = roles })
540   = mkNameEnv [ (tycon, role_annot)
541               | role_annot@(L _ (RoleAnnotDecl (L _ tycon) _)) <- roles ]
542
543 emptyRoleAnnots :: RoleAnnots
544 emptyRoleAnnots = emptyNameEnv
545
546 lookupRoleAnnots :: RoleAnnots -> Name -> Maybe (LRoleAnnotDecl Name)
547 lookupRoleAnnots = lookupNameEnv
548
549 \end{code}
550
551 %************************************************************************
552 %*                                                                      *
553         Role inference
554 %*                                                                      *
555 %************************************************************************
556
557 Note [Role inference]
558 ~~~~~~~~~~~~~~~~~~~~~
559 The role inference algorithm datatype definitions to infer the roles on the
560 parameters. Although these roles are stored in the tycons, we can perform this
561 algorithm on the built tycons, as long as we don't peek at an as-yet-unknown
562 roles field! Ah, the magic of laziness.
563
564 First, we choose appropriate initial roles. For families and classes, roles
565 (including initial roles) are N. For datatypes, we start with the role in the
566 role annotation (if any), or otherwise use Phantom. This is done in
567 initialRoleEnv1.
568
569 The function irGroup then propagates role information until it reaches a
570 fixpoint, preferring N over (R or P) and R over P. To aid in this, we have a
571 monad RoleM, which is a combination reader and state monad. In its state are
572 the current RoleEnv, which gets updated by role propagation, and an update
573 bit, which we use to know whether or not we've reached the fixpoint. The
574 environment of RoleM contains the tycon whose parameters we are inferring, and
575 a VarEnv from parameters to their positions, so we can update the RoleEnv.
576 Between tycons, this reader information is missing; it is added by
577 addRoleInferenceInfo.
578
579 There are two kinds of tycons to consider: algebraic ones (excluding classes)
580 and type synonyms. (Remember, families don't participate -- all their parameters
581 are N.) An algebraic tycon processes each of its datacons, in turn. Note that
582 a datacon's universally quantified parameters might be different from the parent
583 tycon's parameters, so we use the datacon's univ parameters in the mapping from
584 vars to positions. Note also that we don't want to infer roles for existentials
585 (they're all at N, too), so we put them in the set of local variables. As an
586 optimisation, we skip any tycons whose roles are already all Nominal, as there
587 nowhere else for them to go. For synonyms, we just analyse their right-hand sides.
588
589 irType walks through a type, looking for uses of a variable of interest and
590 propagating role information. Because anything used under a phantom position
591 is at phantom and anything used under a nominal position is at nominal, the
592 irType function can assume that anything it sees is at representational. (The
593 other possibilities are pruned when they're encountered.)
594
595 The rest of the code is just plumbing.
596
597 How do we know that this algorithm is correct? It should meet the following
598 specification:
599
600 Let Z be a role context -- a mapping from variables to roles. The following
601 rules define the property (Z |- t : r), where t is a type and r is a role:
602
603 Z(a) = r'        r' <= r
604 ------------------------- RCVar
605 Z |- a : r
606
607 ---------- RCConst
608 Z |- T : r               -- T is a type constructor
609
610 Z |- t1 : r
611 Z |- t2 : N
612 -------------- RCApp
613 Z |- t1 t2 : r
614
615 forall i<=n. (r_i is R or N) implies Z |- t_i : r_i
616 roles(T) = r_1 .. r_n
617 ---------------------------------------------------- RCDApp
618 Z |- T t_1 .. t_n : R
619
620 Z, a:N |- t : r
621 ---------------------- RCAll
622 Z |- forall a:k.t : r
623
624
625 We also have the following rules:
626
627 For all datacon_i in type T, where a_1 .. a_n are universally quantified
628 and b_1 .. b_m are existentially quantified, and the arguments are t_1 .. t_p,
629 then if forall j<=p, a_1 : r_1 .. a_n : r_n, b_1 : N .. b_m : N |- t_j : R,
630 then roles(T) = r_1 .. r_n
631
632 roles(->) = R, R
633 roles(~#) = N, N
634
635 With -dcore-lint on, the output of this algorithm is checked in checkValidRoles,
636 called from checkValidTycon.
637
638 Note [Role-checking data constructor arguments]
639 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
640 Consider
641   data T a where
642     MkT :: Eq b => F a -> (a->a) -> T (G a)
643
644 Then we want to check the roles at which 'a' is used
645 in MkT's type.  We want to work on the user-written type,
646 so we need to take into account
647   * the arguments:   (F a) and (a->a)
648   * the context:     C a b
649   * the result type: (G a)   -- this is in the eq_spec
650
651 \begin{code}
652 type RoleEnv    = NameEnv [Role]        -- from tycon names to roles
653
654 -- This, and any of the functions it calls, must *not* look at the roles
655 -- field of a tycon we are inferring roles about!
656 -- See Note [Role inference]
657 inferRoles :: Bool -> RoleAnnots -> [TyCon] -> Name -> [Role]
658 inferRoles is_boot annots tycons
659   = let role_env  = initialRoleEnv is_boot annots tycons
660         role_env' = irGroup role_env tycons in
661     \name -> case lookupNameEnv role_env' name of
662       Just roles -> roles
663       Nothing    -> pprPanic "inferRoles" (ppr name)
664
665 initialRoleEnv :: Bool -> RoleAnnots -> [TyCon] -> RoleEnv
666 initialRoleEnv is_boot annots = extendNameEnvList emptyNameEnv .
667                                 map (initialRoleEnv1 is_boot annots)
668
669 initialRoleEnv1 :: Bool -> RoleAnnots -> TyCon -> (Name, [Role])
670 initialRoleEnv1 is_boot annots_env tc
671   | isFamilyTyCon tc      = (name, map (const Nominal) tyvars)
672   | isAlgTyCon tc         = (name, default_roles)
673   | isTypeSynonymTyCon tc = (name, default_roles)
674   | otherwise             = pprPanic "initialRoleEnv1" (ppr tc)
675   where name         = tyConName tc
676         tyvars       = tyConTyVars tc
677         (kvs, tvs)   = span isKindVar tyvars
678
679           -- if the number of annotations in the role annotation decl
680           -- is wrong, just ignore it. We check this in the validity check.
681         role_annots
682           = case lookupNameEnv annots_env name of
683               Just (L _ (RoleAnnotDecl _ annots))
684                 | annots `equalLength` tvs -> map unLoc annots
685               _                            -> map (const Nothing) tvs
686         default_roles = map (const Nominal) kvs ++
687                         zipWith orElse role_annots (repeat default_role)
688
689         default_role
690           | isClassTyCon tc = Nominal
691           | is_boot         = Representational
692           | otherwise       = Phantom
693
694 irGroup :: RoleEnv -> [TyCon] -> RoleEnv
695 irGroup env tcs
696   = let (env', update) = runRoleM env $ mapM_ irTyCon tcs in
697     if update
698     then irGroup env' tcs
699     else env'
700
701 irTyCon :: TyCon -> RoleM ()
702 irTyCon tc
703   | isAlgTyCon tc
704   = do { old_roles <- lookupRoles tc
705        ; unless (all (== Nominal) old_roles) $  -- also catches data families,
706                                                 -- which don't want or need role inference
707     do { whenIsJust (tyConClass_maybe tc) (irClass tc_name)
708        ; addRoleInferenceInfo tc_name (tyConTyVars tc) $
709          mapM_ (irType emptyVarSet) (tyConStupidTheta tc)  -- See #8958
710        ; mapM_ (irDataCon tc_name) (visibleDataCons $ algTyConRhs tc) }}
711
712   | Just ty <- synTyConRhs_maybe tc
713   = addRoleInferenceInfo tc_name (tyConTyVars tc) $
714     irType emptyVarSet ty
715
716   | otherwise
717   = return ()
718
719   where
720     tc_name = tyConName tc
721
722 -- any type variable used in an associated type must be Nominal
723 irClass :: Name -> Class -> RoleM ()
724 irClass tc_name cls
725   = addRoleInferenceInfo tc_name cls_tvs $
726     mapM_ ir_at (classATs cls)
727   where
728     cls_tvs    = classTyVars cls
729     cls_tv_set = mkVarSet cls_tvs
730
731     ir_at at_tc
732       = mapM_ (updateRole Nominal) (varSetElems nvars)
733       where nvars = (mkVarSet $ tyConTyVars at_tc) `intersectVarSet` cls_tv_set
734
735 -- See Note [Role inference]
736 irDataCon :: Name -> DataCon -> RoleM ()
737 irDataCon tc_name datacon
738   = addRoleInferenceInfo tc_name univ_tvs $
739     mapM_ (irType ex_var_set) (eqSpecPreds eq_spec ++ theta ++ arg_tys)
740       -- See Note [Role-checking data constructor arguments]
741   where
742     (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig datacon
743     ex_var_set = mkVarSet ex_tvs
744
745 irType :: VarSet -> Type -> RoleM ()
746 irType = go
747   where
748     go lcls (TyVarTy tv) = unless (tv `elemVarSet` lcls) $
749                            updateRole Representational tv
750     go lcls (AppTy t1 t2) = go lcls t1 >> mark_nominal lcls t2
751     go lcls (TyConApp tc tys)
752       = do { roles <- lookupRolesX tc
753            ; zipWithM_ (go_app lcls) roles tys }
754     go lcls (FunTy t1 t2) = go lcls t1 >> go lcls t2
755     go lcls (ForAllTy tv ty) = go (extendVarSet lcls tv) ty
756     go _    (LitTy {}) = return ()
757
758     go_app _ Phantom _ = return ()                 -- nothing to do here
759     go_app lcls Nominal ty = mark_nominal lcls ty  -- all vars below here are N
760     go_app lcls Representational ty = go lcls ty
761
762     mark_nominal lcls ty = let nvars = tyVarsOfType ty `minusVarSet` lcls in
763                            mapM_ (updateRole Nominal) (varSetElems nvars)
764
765 -- like lookupRoles, but with Nominal tags at the end for oversaturated TyConApps
766 lookupRolesX :: TyCon -> RoleM [Role]
767 lookupRolesX tc
768   = do { roles <- lookupRoles tc
769        ; return $ roles ++ repeat Nominal }
770
771 -- gets the roles either from the environment or the tycon
772 lookupRoles :: TyCon -> RoleM [Role]
773 lookupRoles tc
774   = do { env <- getRoleEnv
775        ; case lookupNameEnv env (tyConName tc) of
776            Just roles -> return roles
777            Nothing    -> return $ tyConRoles tc }
778
779 -- tries to update a role; won't ever update a role "downwards"
780 updateRole :: Role -> TyVar -> RoleM ()
781 updateRole role tv
782   = do { var_ns <- getVarNs
783        ; case lookupVarEnv var_ns tv of
784        { Nothing -> pprPanic "updateRole" (ppr tv)
785        ; Just n  -> do
786        { name <- getTyConName
787        ; updateRoleEnv name n role }}}
788
789 -- the state in the RoleM monad
790 data RoleInferenceState = RIS { role_env  :: RoleEnv
791                               , update    :: Bool }
792
793 -- the environment in the RoleM monad
794 type VarPositions = VarEnv Int
795 data RoleInferenceInfo = RII { var_ns :: VarPositions
796                              , name   :: Name }
797
798 -- See [Role inference]
799 newtype RoleM a = RM { unRM :: Maybe RoleInferenceInfo
800                             -> RoleInferenceState
801                             -> (a, RoleInferenceState) }
802
803 instance Functor RoleM where
804     fmap = liftM
805
806 instance Applicative RoleM where
807     pure = return
808     (<*>) = ap
809
810 instance Monad RoleM where
811   return x = RM $ \_ state -> (x, state)
812   a >>= f  = RM $ \m_info state -> let (a', state') = unRM a m_info state in
813                                    unRM (f a') m_info state'
814
815 runRoleM :: RoleEnv -> RoleM () -> (RoleEnv, Bool)
816 runRoleM env thing = (env', update)
817   where RIS { role_env = env', update = update } = snd $ unRM thing Nothing state
818         state = RIS { role_env  = env, update    = False }
819
820 addRoleInferenceInfo :: Name -> [TyVar] -> RoleM a -> RoleM a
821 addRoleInferenceInfo name tvs thing
822   = RM $ \_nothing state -> ASSERT( isNothing _nothing )
823                             unRM thing (Just info) state
824   where info = RII { var_ns = mkVarEnv (zip tvs [0..]), name = name }
825
826 getRoleEnv :: RoleM RoleEnv
827 getRoleEnv = RM $ \_ state@(RIS { role_env = env }) -> (env, state)
828
829 getVarNs :: RoleM VarPositions
830 getVarNs = RM $ \m_info state ->
831                 case m_info of
832                   Nothing -> panic "getVarNs"
833                   Just (RII { var_ns = var_ns }) -> (var_ns, state)
834
835 getTyConName :: RoleM Name
836 getTyConName = RM $ \m_info state ->
837                     case m_info of
838                       Nothing -> panic "getTyConName"
839                       Just (RII { name = name }) -> (name, state)
840
841
842 updateRoleEnv :: Name -> Int -> Role -> RoleM ()
843 updateRoleEnv name n role
844   = RM $ \_ state@(RIS { role_env = role_env }) -> ((),
845          case lookupNameEnv role_env name of
846            Nothing -> pprPanic "updateRoleEnv" (ppr name)
847            Just roles -> let (before, old_role : after) = splitAt n roles in
848                          if role `ltRole` old_role
849                          then let roles' = before ++ role : after
850                                   role_env' = extendNameEnv role_env name roles' in
851                               RIS { role_env = role_env', update = True }
852                          else state )
853
854 \end{code}