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