Change default roles for classes to be *nominal*.
[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://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
17 -- for details
18
19 module TcTyDecls(
20         calcRecFlags, RecTyInfo(..), 
21         calcSynCycles, calcClassCycles,
22         extractRoleAnnots, emptyRoleAnnots, 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 -> Bool  -- hs-boot file?
365              -> RoleAnnots -> [TyThing] -> RecTyInfo
366 -- The 'boot_names' are the things declared in M.hi-boot, if M is the current module.
367 -- Any type constructors in boot_names are automatically considered loop breakers
368 calcRecFlags boot_details is_boot mrole_env tyclss
369   = RTI { rti_promotable = is_promotable
370         , rti_roles      = roles
371         , rti_is_rec     = is_rec }
372   where
373     rec_tycon_names = mkNameSet (map tyConName all_tycons)
374     all_tycons = mapCatMaybes getTyCon tyclss
375                    -- Recursion of newtypes/data types can happen via
376                    -- the class TyCon, so tyclss includes the class tycons
377
378     is_promotable = all (isPromotableTyCon rec_tycon_names) all_tycons
379
380     roles = inferRoles is_boot mrole_env all_tycons
381
382     ----------------- Recursion calculation ----------------
383     is_rec n | n `elemNameSet` rec_names = Recursive
384              | otherwise                 = NonRecursive
385
386     boot_name_set = availsToNameSet (md_exports boot_details)
387     rec_names = boot_name_set     `unionNameSets`
388                 nt_loop_breakers  `unionNameSets`
389                 prod_loop_breakers
390
391
392         -------------------------------------------------
393         --                      NOTE
394         -- These edge-construction loops rely on
395         -- every loop going via tyclss, the types and classes
396         -- in the module being compiled.  Stuff in interface
397         -- files should be correctly marked.  If not (e.g. a
398         -- type synonym in a hi-boot file) we can get an infinite
399         -- loop.  We could program round this, but it'd make the code
400         -- rather less nice, so I'm not going to do that yet.
401
402     single_con_tycons = [ tc | tc <- all_tycons
403                              , not (tyConName tc `elemNameSet` boot_name_set)
404                                  -- Remove the boot_name_set because they are 
405                                  -- going to be loop breakers regardless.
406                              , isSingleton (tyConDataCons tc) ]
407         -- Both newtypes and data types, with exactly one data constructor
408
409     (new_tycons, prod_tycons) = partition isNewTyCon single_con_tycons
410         -- NB: we do *not* call isProductTyCon because that checks
411         --     for vanilla-ness of data constructors; and that depends
412         --     on empty existential type variables; and that is figured
413         --     out by tcResultType; which uses tcMatchTy; which uses
414         --     coreView; which calls coreExpandTyCon_maybe; which uses
415         --     the recursiveness of the TyCon.  Result... a black hole.
416         -- YUK YUK YUK
417
418         --------------- Newtypes ----------------------
419     nt_loop_breakers = mkNameSet (findLoopBreakers nt_edges)
420     is_rec_nt tc = tyConName tc  `elemNameSet` nt_loop_breakers
421         -- is_rec_nt is a locally-used helper function
422
423     nt_edges = [(t, mk_nt_edges t) | t <- new_tycons]
424
425     mk_nt_edges nt      -- Invariant: nt is a newtype
426         = concatMap (mk_nt_edges1 nt) (tyConsOfType (new_tc_rhs nt))
427                         -- tyConsOfType looks through synonyms
428
429     mk_nt_edges1 _ tc
430         | tc `elem` new_tycons = [tc]           -- Loop
431                 -- At this point we know that either it's a local *data* type,
432                 -- or it's imported.  Either way, it can't form part of a newtype cycle
433         | otherwise = []
434
435         --------------- Product types ----------------------
436     prod_loop_breakers = mkNameSet (findLoopBreakers prod_edges)
437
438     prod_edges = [(tc, mk_prod_edges tc) | tc <- prod_tycons]
439
440     mk_prod_edges tc    -- Invariant: tc is a product tycon
441         = concatMap (mk_prod_edges1 tc) (dataConOrigArgTys (head (tyConDataCons tc)))
442
443     mk_prod_edges1 ptc ty = concatMap (mk_prod_edges2 ptc) (tyConsOfType ty)
444
445     mk_prod_edges2 ptc tc
446         | tc `elem` prod_tycons   = [tc]                -- Local product
447         | tc `elem` new_tycons    = if is_rec_nt tc     -- Local newtype
448                                     then []
449                                     else mk_prod_edges1 ptc (new_tc_rhs tc)
450                 -- At this point we know that either it's a local non-product data type,
451                 -- or it's imported.  Either way, it can't form part of a cycle
452         | otherwise = []
453
454 new_tc_rhs :: TyCon -> Type
455 new_tc_rhs tc = snd (newTyConRhs tc)    -- Ignore the type variables
456
457 getTyCon :: TyThing -> Maybe TyCon
458 getTyCon (ATyCon tc) = Just tc
459 getTyCon _           = Nothing
460
461 findLoopBreakers :: [(TyCon, [TyCon])] -> [Name]
462 -- Finds a set of tycons that cut all loops
463 findLoopBreakers deps
464   = go [(tc,tc,ds) | (tc,ds) <- deps]
465   where
466     go edges = [ name
467                | CyclicSCC ((tc,_,_) : edges') <- stronglyConnCompFromEdgedVerticesR edges,
468                  name <- tyConName tc : go edges']
469 \end{code}
470
471
472 %************************************************************************
473 %*                                                                      *
474                   Promotion calculation
475 %*                                                                      *
476 %************************************************************************
477
478 See Note [Checking whether a group is promotable]
479 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
480 We only want to promote a TyCon if all its data constructors
481 are promotable; it'd be very odd to promote some but not others.
482
483 But the data constructors may mention this or other TyCons.
484
485 So we treat the recursive uses as all OK (ie promotable) and
486 do one pass to check that each TyCon is promotable.
487
488 Currently type synonyms are not promotable, though that
489 could change.
490
491 \begin{code}
492 isPromotableTyCon :: NameSet -> TyCon -> Bool
493 isPromotableTyCon rec_tycons tc
494   =  isAlgTyCon tc    -- Only algebraic; not even synonyms
495                      -- (we could reconsider the latter)
496   && ok_kind (tyConKind tc)
497   && case algTyConRhs tc of 
498        DataTyCon { data_cons = cs } -> all ok_con cs 
499        NewTyCon { data_con = c }    -> ok_con c
500        AbstractTyCon {}             -> False
501        DataFamilyTyCon {}           -> False
502
503   where
504     ok_kind kind = all isLiftedTypeKind args && isLiftedTypeKind res
505             where  -- Checks for * -> ... -> * -> *
506               (args, res) = splitKindFunTys kind
507
508     -- See Note [Promoted data constructors] in TyCon
509     ok_con con = all (isLiftedTypeKind . tyVarKind) ex_tvs
510               && null eq_spec   -- No constraints
511               && null theta
512               && all (isPromotableType rec_tycons) orig_arg_tys
513        where
514          (_, ex_tvs, eq_spec, theta, orig_arg_tys, _) = dataConFullSig con
515
516
517 isPromotableType :: NameSet -> Type -> Bool
518 -- Must line up with DataCon.promoteType
519 -- But the function lives here because we must treat the
520 -- *recursive* tycons as promotable
521 isPromotableType rec_tcs con_arg_ty
522   = go con_arg_ty
523   where
524     go (TyConApp tc tys) =  tys `lengthIs` tyConArity tc 
525                          && (tyConName tc `elemNameSet` rec_tcs 
526                              || isJust (promotableTyCon_maybe tc))
527                          && all go tys
528     go (FunTy arg res)   = go arg && go res
529     go (TyVarTy {})      = True
530     go _                 = False
531 \end{code}
532
533 %************************************************************************
534 %*                                                                      *
535         Role annotations
536 %*                                                                      *
537 %************************************************************************
538
539 \begin{code}
540 type RoleAnnots = NameEnv (LRoleAnnotDecl Name)
541
542 extractRoleAnnots :: TyClGroup Name -> RoleAnnots
543 extractRoleAnnots (TyClGroup { group_roles = roles })
544   = mkNameEnv [ (tycon, role_annot)
545               | role_annot@(L _ (RoleAnnotDecl (L _ tycon) _)) <- roles ]
546
547 emptyRoleAnnots :: RoleAnnots
548 emptyRoleAnnots = emptyNameEnv
549
550 \end{code}
551
552 %************************************************************************
553 %*                                                                      *
554         Role inference
555 %*                                                                      *
556 %************************************************************************
557
558 Note [Role inference]
559 ~~~~~~~~~~~~~~~~~~~~~
560 The role inference algorithm datatype definitions to infer the roles on the
561 parameters. Although these roles are stored in the tycons, we can perform this
562 algorithm on the built tycons, as long as we don't peek at an as-yet-unknown
563 roles field! Ah, the magic of laziness.
564
565 First, we choose appropriate initial roles. For families and classes, roles
566 (including initial roles) are N. For datatypes, we start with the role in the
567 role annotation (if any), or otherwise use Phantom. This is done in
568 initialRoleEnv1.
569
570 The function irGroup then propagates role information until it reaches a
571 fixpoint, preferring N over (R or P) and R over P. To aid in this, we have a
572 monad RoleM, which is a combination reader and state monad. In its state are
573 the current RoleEnv, which gets updated by role propagation, and an update
574 bit, which we use to know whether or not we've reached the fixpoint. The
575 environment of RoleM contains the tycon whose parameters we are inferring, and
576 a VarEnv from parameters to their positions, so we can update the RoleEnv.
577 Between tycons, this reader information is missing; it is added by
578 addRoleInferenceInfo.
579
580 There are two kinds of tycons to consider: algebraic ones (excluding classes)
581 and type synonyms. (Remember, families don't participate -- all their parameters
582 are N.) An algebraic tycon processes each of its datacons, in turn. Note that
583 a datacon's universally quantified parameters might be different from the parent
584 tycon's parameters, so we use the datacon's univ parameters in the mapping from
585 vars to positions. Note also that we don't want to infer roles for existentials
586 (they're all at N, too), so we put them in the set of local variables. As an
587 optimisation, we skip any tycons whose roles are already all Nominal, as there
588 nowhere else for them to go. For synonyms, we just analyse their right-hand sides.
589
590 irType walks through a type, looking for uses of a variable of interest and
591 propagating role information. Because anything used under a phantom position
592 is at phantom and anything used under a nominal position is at nominal, the
593 irType function can assume that anything it sees is at representational. (The
594 other possibilities are pruned when they're encountered.)
595
596 The rest of the code is just plumbing.
597
598 How do we know that this algorithm is correct? It should meet the following
599 specification:
600
601 Let Z be a role context -- a mapping from variables to roles. The following
602 rules define the property (Z |- t : r), where t is a type and r is a role:
603
604 Z(a) = r'        r' <= r
605 ------------------------- RCVar
606 Z |- a : r
607
608 ---------- RCConst
609 Z |- T : r               -- T is a type constructor
610
611 Z |- t1 : r
612 Z |- t2 : N
613 -------------- RCApp
614 Z |- t1 t2 : r
615
616 forall i<=n. (r_i is R or N) implies Z |- t_i : r_i
617 roles(T) = r_1 .. r_n
618 ---------------------------------------------------- RCDApp
619 Z |- T t_1 .. t_n : R
620
621 Z, a:N |- t : r
622 ---------------------- RCAll
623 Z |- forall a:k.t : r
624
625
626 We also have the following rules:
627
628 For all datacon_i in type T, where a_1 .. a_n are universally quantified
629 and b_1 .. b_m are existentially quantified, and the arguments are t_1 .. t_p,
630 then if forall j<=p, a_1 : r_1 .. a_n : r_n, b_1 : N .. b_m : N |- t_j : R,
631 then roles(T) = r_1 .. r_n
632
633 roles(->) = R, R
634 roles(~#) = N, N
635
636 With -dcore-lint on, the output of this algorithm is checked in checkValidRoles,
637 called from checkValidTycon.
638
639 Note [Role-checking data constructor arguments]
640 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
641 Consider
642   data T a where
643     MkT :: Eq b => F a -> (a->a) -> T (G a)
644
645 Then we want to check the roles at which 'a' is used
646 in MkT's type.  We want to work on the user-written type,
647 so we need to take into account
648   * the arguments:   (F a) and (a->a)
649   * the context:     C a b
650   * the result type: (G a)   -- this is in the eq_spec
651
652 \begin{code}
653 type RoleEnv    = NameEnv [Role]        -- from tycon names to roles
654
655 -- This, and any of the functions it calls, must *not* look at the roles
656 -- field of a tycon we are inferring roles about!
657 -- See Note [Role inference]
658 inferRoles :: Bool -> RoleAnnots -> [TyCon] -> Name -> [Role]
659 inferRoles is_boot annots tycons
660   = let role_env  = initialRoleEnv is_boot annots tycons
661         role_env' = irGroup role_env tycons in
662     \name -> case lookupNameEnv role_env' name of
663       Just roles -> roles
664       Nothing    -> pprPanic "inferRoles" (ppr name)
665
666 initialRoleEnv :: Bool -> RoleAnnots -> [TyCon] -> RoleEnv
667 initialRoleEnv is_boot annots = extendNameEnvList emptyNameEnv .
668                                 map (initialRoleEnv1 is_boot annots)
669
670 initialRoleEnv1 :: Bool -> RoleAnnots -> TyCon -> (Name, [Role])
671 initialRoleEnv1 is_boot annots_env tc
672   | isFamilyTyCon tc = (name, map (const Nominal) tyvars)
673   |  isAlgTyCon tc
674   || isSynTyCon tc   = (name, default_roles)
675   | otherwise        = pprPanic "initialRoleEnv1" (ppr tc)
676   where name         = tyConName tc
677         tyvars       = tyConTyVars tc
678         (kvs, tvs)   = span isKindVar tyvars
679
680           -- if the number of annotations in the role annotation decl
681           -- is wrong, just ignore it. We check this in the validity check.
682         role_annots
683           = case lookupNameEnv annots_env name of
684               Just (L _ (RoleAnnotDecl _ annots))
685                 | annots `equalLength` tvs -> map unLoc annots
686               _                            -> map (const Nothing) tvs
687         default_roles = map (const Nominal) kvs ++
688                         zipWith orElse role_annots (repeat default_role)
689
690         default_role
691           | isClassTyCon tc = Nominal
692           | is_boot         = Representational
693           | otherwise       = Phantom
694
695 irGroup :: RoleEnv -> [TyCon] -> RoleEnv
696 irGroup env tcs
697   = let (env', update) = runRoleM env $ mapM_ irTyCon tcs in
698     if update
699     then irGroup env' tcs
700     else env'
701
702 irTyCon :: TyCon -> RoleM ()
703 irTyCon tc
704   | isAlgTyCon tc
705   = do { old_roles <- lookupRoles tc
706        ; unless (all (== Nominal) old_roles) $  -- also catches data families,
707                                                 -- which don't want or need role inference
708     do { whenIsJust (tyConClass_maybe tc) (irClass tc_name)
709        ; mapM_ (irDataCon tc_name) (visibleDataCons $ algTyConRhs tc) }}
710
711   | Just (SynonymTyCon ty) <- synTyConRhs_maybe tc
712   = addRoleInferenceInfo tc_name (tyConTyVars tc) $
713     irType emptyVarSet ty
714
715   | otherwise
716   = return ()
717
718   where
719     tc_name = tyConName tc
720
721 -- any type variable used in an associated type must be Nominal
722 irClass :: Name -> Class -> RoleM ()
723 irClass tc_name cls
724   = addRoleInferenceInfo tc_name cls_tvs $
725     mapM_ ir_at (classATs cls)
726   where
727     cls_tvs    = classTyVars cls
728     cls_tv_set = mkVarSet cls_tvs
729
730     ir_at at_tc
731       = mapM_ (updateRole Nominal) (varSetElems nvars)
732       where nvars = (mkVarSet $ tyConTyVars at_tc) `intersectVarSet` cls_tv_set
733
734 -- See Note [Role inference]
735 irDataCon :: Name -> DataCon -> RoleM ()
736 irDataCon tc_name datacon
737   = addRoleInferenceInfo tc_name univ_tvs $
738     mapM_ (irType ex_var_set) (eqSpecPreds eq_spec ++ theta ++ arg_tys)
739       -- See Note [Role-checking data constructor arguments] 
740   where
741     (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig datacon
742     ex_var_set = mkVarSet ex_tvs
743
744 irType :: VarSet -> Type -> RoleM ()
745 irType = go
746   where
747     go lcls (TyVarTy tv) = unless (tv `elemVarSet` lcls) $
748                            updateRole Representational tv
749     go lcls (AppTy t1 t2) = go lcls t1 >> mark_nominal lcls t2
750     go lcls (TyConApp tc tys)
751       = do { roles <- lookupRolesX tc
752            ; zipWithM_ (go_app lcls) roles tys }
753     go lcls (FunTy t1 t2) = go lcls t1 >> go lcls t2
754     go lcls (ForAllTy tv ty) = go (extendVarSet lcls tv) ty
755     go _    (LitTy {}) = return ()
756
757     go_app _ Phantom _ = return ()                 -- nothing to do here
758     go_app lcls Nominal ty = mark_nominal lcls ty  -- all vars below here are N
759     go_app lcls Representational ty = go lcls ty
760
761     mark_nominal lcls ty = let nvars = tyVarsOfType ty `minusVarSet` lcls in
762                            mapM_ (updateRole Nominal) (varSetElems nvars)
763
764 -- like lookupRoles, but with Nominal tags at the end for oversaturated TyConApps
765 lookupRolesX :: TyCon -> RoleM [Role]
766 lookupRolesX tc
767   = do { roles <- lookupRoles tc
768        ; return $ roles ++ repeat Nominal }
769
770 -- gets the roles either from the environment or the tycon
771 lookupRoles :: TyCon -> RoleM [Role]
772 lookupRoles tc
773   = do { env <- getRoleEnv
774        ; case lookupNameEnv env (tyConName tc) of
775            Just roles -> return roles
776            Nothing    -> return $ tyConRoles tc }
777
778 -- tries to update a role; won't even update a role "downwards"
779 updateRole :: Role -> TyVar -> RoleM ()
780 updateRole role tv
781   = do { var_ns <- getVarNs
782        ; case lookupVarEnv var_ns tv of
783        { Nothing -> pprPanic "updateRole" (ppr tv)
784        ; Just n  -> do
785        { name <- getTyConName
786        ; updateRoleEnv name n role }}}
787
788 -- the state in the RoleM monad
789 data RoleInferenceState = RIS { role_env  :: RoleEnv
790                               , update    :: Bool }
791
792 -- the environment in the RoleM monad
793 type VarPositions = VarEnv Int
794 data RoleInferenceInfo = RII { var_ns :: VarPositions
795                              , name   :: Name }
796
797 -- See [Role inference]
798 newtype RoleM a = RM { unRM :: Maybe RoleInferenceInfo
799                             -> RoleInferenceState
800                             -> (a, RoleInferenceState) }
801
802 instance Functor RoleM where
803     fmap = liftM
804
805 instance Applicative RoleM where
806     pure = return
807     (<*>) = ap
808
809 instance Monad RoleM where
810   return x = RM $ \_ state -> (x, state)
811   a >>= f  = RM $ \m_info state -> let (a', state') = unRM a m_info state in
812                                    unRM (f a') m_info state'
813
814 runRoleM :: RoleEnv -> RoleM () -> (RoleEnv, Bool)
815 runRoleM env thing = (env', update)
816   where RIS { role_env = env', update = update } = snd $ unRM thing Nothing state 
817         state = RIS { role_env  = env, update    = False }
818
819 addRoleInferenceInfo :: Name -> [TyVar] -> RoleM a -> RoleM a
820 addRoleInferenceInfo name tvs thing
821   = RM $ \_nothing state -> ASSERT( isNothing _nothing )
822                             unRM thing (Just info) state
823   where info = RII { var_ns = mkVarEnv (zip tvs [0..]), name = name }
824
825 getRoleEnv :: RoleM RoleEnv
826 getRoleEnv = RM $ \_ state@(RIS { role_env = env }) -> (env, state)
827
828 getVarNs :: RoleM VarPositions
829 getVarNs = RM $ \m_info state ->
830                 case m_info of
831                   Nothing -> panic "getVarNs"
832                   Just (RII { var_ns = var_ns }) -> (var_ns, state)
833
834 getTyConName :: RoleM Name
835 getTyConName = RM $ \m_info state ->
836                     case m_info of
837                       Nothing -> panic "getTyConName"
838                       Just (RII { name = name }) -> (name, state)
839
840
841 updateRoleEnv :: Name -> Int -> Role -> RoleM ()
842 updateRoleEnv name n role
843   = RM $ \_ state@(RIS { role_env = role_env }) -> ((),
844          case lookupNameEnv role_env name of
845            Nothing -> pprPanic "updateRoleEnv" (ppr name)
846            Just roles -> let (before, old_role : after) = splitAt n roles in
847                          if role `ltRole` old_role
848                          then let roles' = before ++ role : after
849                                   role_env' = extendNameEnv role_env name roles' in
850                               RIS { role_env = role_env', update = True }
851                          else state )
852
853 \end{code}