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