Remove references to SynTyCon. Fixes #9812
[ghc.git] / compiler / typecheck / TcTyDecls.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1999
4 %
5
6 Analysis functions over data types.  Specficially, detecting recursive types.
7
8 This stuff is only used for source-code decls; it's recorded in interface
9 files for imported data types.
10
11 \begin{code}
12 {-# LANGUAGE CPP #-}
13
14 module TcTyDecls(
15         calcRecFlags, RecTyInfo(..),
16         calcSynCycles, calcClassCycles,
17         RoleAnnots, extractRoleAnnots, emptyRoleAnnots, lookupRoleAnnots
18     ) where
19
20 #include "HsVersions.h"
21
22 import TypeRep
23 import HsSyn
24 import Class
25 import Type
26 import Kind
27 import HscTypes
28 import TyCon
29 import DataCon
30 import Var
31 import Name
32 import NameEnv
33 import VarEnv
34 import VarSet
35 import NameSet
36 import Coercion ( ltRole )
37 import Avail
38 import Digraph
39 import BasicTypes
40 import SrcLoc
41 import Outputable
42 import UniqSet
43 import Util
44 import Maybes
45 import Data.List
46
47 #if __GLASGOW_HASKELL__ < 709
48 import Control.Applicative (Applicative(..))
49 #endif
50
51 import Control.Monad
52 \end{code}
53
54
55 %************************************************************************
56 %*                                                                      *
57         Cycles in class and type synonym declarations
58 %*                                                                      *
59 %************************************************************************
60
61 Checking for class-decl loops is easy, because we don't allow class decls
62 in interface files.
63
64 We allow type synonyms in hi-boot files, but we *trust* hi-boot files,
65 so we don't check for loops that involve them.  So we only look for synonym
66 loops in the module being compiled.
67
68 We check for type synonym and class cycles on the *source* code.
69 Main reasons:
70
71   a) Otherwise we'd need a special function to extract type-synonym tycons
72      from a type, whereas we already have the free vars pinned on the decl
73
74   b) If we checked for type synonym loops after building the TyCon, we
75         can't do a hoistForAllTys on the type synonym rhs, (else we fall into
76         a black hole) which seems unclean.  Apart from anything else, it'd mean
77         that a type-synonym rhs could have for-alls to the right of an arrow,
78         which means adding new cases to the validity checker
79
80         Indeed, in general, checking for cycles beforehand means we need to
81         be less careful about black holes through synonym cycles.
82
83 The main disadvantage is that a cycle that goes via a type synonym in an
84 .hi-boot file can lead the compiler into a loop, because it assumes that cycles
85 only occur entirely within the source code of the module being compiled.
86 But hi-boot files are trusted anyway, so this isn't much worse than (say)
87 a kind error.
88
89 [  NOTE ----------------------------------------------
90 If we reverse this decision, this comment came from tcTyDecl1, and should
91  go back there
92         -- dsHsType, not tcHsKindedType, to avoid a loop.  tcHsKindedType does hoisting,
93         -- which requires looking through synonyms... and therefore goes into a loop
94         -- on (erroneously) recursive synonyms.
95         -- Solution: do not hoist synonyms, because they'll be hoisted soon enough
96         --           when they are substituted
97
98 We'd also need to add back in this definition
99
100 synonymTyConsOfType :: Type -> [TyCon]
101 -- Does not look through type synonyms at all
102 -- Return a list of synonym tycons
103 synonymTyConsOfType ty
104   = nameEnvElts (go ty)
105   where
106      go :: Type -> NameEnv TyCon  -- The NameEnv does duplicate elim
107      go (TyVarTy v)               = emptyNameEnv
108      go (TyConApp tc tys)         = go_tc tc tys
109      go (AppTy a b)               = go a `plusNameEnv` go b
110      go (FunTy a b)               = go a `plusNameEnv` go b
111      go (ForAllTy _ ty)           = go ty
112
113      go_tc tc tys | isTypeSynonymTyCon tc = extendNameEnv (go_s tys)
114                                                           (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, nameSetElems 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 has 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 = mapMaybe 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     `unionNameSet`
388                 nt_loop_breakers  `unionNameSet`
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         = [ tc | tc <- nameEnvElts (tyConsOfType (new_tc_rhs nt))
427                         -- tyConsOfType looks through synonyms
428                , tc `elem` new_tycons ]
429            -- If not (tc `elem` new_tycons) we know that either it's a local *data* type,
430            -- or it's imported.  Either way, it can't form part of a newtype cycle
431
432         --------------- Product types ----------------------
433     prod_loop_breakers = mkNameSet (findLoopBreakers prod_edges)
434
435     prod_edges = [(tc, mk_prod_edges tc) | tc <- prod_tycons]
436
437     mk_prod_edges tc    -- Invariant: tc is a product tycon
438         = concatMap (mk_prod_edges1 tc) (dataConOrigArgTys (head (tyConDataCons tc)))
439
440     mk_prod_edges1 ptc ty = concatMap (mk_prod_edges2 ptc) (nameEnvElts (tyConsOfType ty))
441
442     mk_prod_edges2 ptc tc
443         | tc `elem` prod_tycons   = [tc]                -- Local product
444         | tc `elem` new_tycons    = if is_rec_nt tc     -- Local newtype
445                                     then []
446                                     else mk_prod_edges1 ptc (new_tc_rhs tc)
447                 -- At this point we know that either it's a local non-product data type,
448                 -- or it's imported.  Either way, it can't form part of a cycle
449         | otherwise = []
450
451 new_tc_rhs :: TyCon -> Type
452 new_tc_rhs tc = snd (newTyConRhs tc)    -- Ignore the type variables
453
454 getTyCon :: TyThing -> Maybe TyCon
455 getTyCon (ATyCon tc) = Just tc
456 getTyCon _           = Nothing
457
458 findLoopBreakers :: [(TyCon, [TyCon])] -> [Name]
459 -- Finds a set of tycons that cut all loops
460 findLoopBreakers deps
461   = go [(tc,tc,ds) | (tc,ds) <- deps]
462   where
463     go edges = [ name
464                | CyclicSCC ((tc,_,_) : edges') <- stronglyConnCompFromEdgedVerticesR edges,
465                  name <- tyConName tc : go edges']
466 \end{code}
467
468
469 %************************************************************************
470 %*                                                                      *
471                   Promotion calculation
472 %*                                                                      *
473 %************************************************************************
474
475 See Note [Checking whether a group is promotable]
476 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
477 We only want to promote a TyCon if all its data constructors
478 are promotable; it'd be very odd to promote some but not others.
479
480 But the data constructors may mention this or other TyCons.
481
482 So we treat the recursive uses as all OK (ie promotable) and
483 do one pass to check that each TyCon is promotable.
484
485 Currently type synonyms are not promotable, though that
486 could change.
487
488 \begin{code}
489 isPromotableTyCon :: NameSet -> TyCon -> Bool
490 isPromotableTyCon rec_tycons tc
491   =  isAlgTyCon tc    -- Only algebraic; not even synonyms
492                      -- (we could reconsider the latter)
493   && ok_kind (tyConKind tc)
494   && case algTyConRhs tc of
495        DataTyCon { data_cons = cs } -> all ok_con cs
496        NewTyCon { data_con = c }    -> ok_con c
497        AbstractTyCon {}             -> False
498        DataFamilyTyCon {}           -> False
499
500   where
501     ok_kind kind = all isLiftedTypeKind args && isLiftedTypeKind res
502             where  -- Checks for * -> ... -> * -> *
503               (args, res) = splitKindFunTys kind
504
505     -- See Note [Promoted data constructors] in TyCon
506     ok_con con = all (isLiftedTypeKind . tyVarKind) ex_tvs
507               && null eq_spec   -- No constraints
508               && null theta
509               && all (isPromotableType rec_tycons) orig_arg_tys
510        where
511          (_, ex_tvs, eq_spec, theta, orig_arg_tys, _) = dataConFullSig con
512
513
514 isPromotableType :: NameSet -> Type -> Bool
515 -- Must line up with DataCon.promoteType
516 -- But the function lives here because we must treat the
517 -- *recursive* tycons as promotable
518 isPromotableType rec_tcs con_arg_ty
519   = go con_arg_ty
520   where
521     go (TyConApp tc tys) =  tys `lengthIs` tyConArity tc
522                          && (tyConName tc `elemNameSet` rec_tcs
523                              || isJust (promotableTyCon_maybe tc))
524                          && all go tys
525     go (FunTy arg res)   = go arg && go res
526     go (TyVarTy {})      = True
527     go _                 = False
528 \end{code}
529
530 %************************************************************************
531 %*                                                                      *
532         Role annotations
533 %*                                                                      *
534 %************************************************************************
535
536 \begin{code}
537 type RoleAnnots = NameEnv (LRoleAnnotDecl Name)
538
539 extractRoleAnnots :: TyClGroup Name -> RoleAnnots
540 extractRoleAnnots (TyClGroup { group_roles = roles })
541   = mkNameEnv [ (tycon, role_annot)
542               | role_annot@(L _ (RoleAnnotDecl (L _ tycon) _)) <- roles ]
543
544 emptyRoleAnnots :: RoleAnnots
545 emptyRoleAnnots = emptyNameEnv
546
547 lookupRoleAnnots :: RoleAnnots -> Name -> Maybe (LRoleAnnotDecl Name)
548 lookupRoleAnnots = lookupNameEnv
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         = (name, default_roles)
674   | isTypeSynonymTyCon 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        ; addRoleInferenceInfo tc_name (tyConTyVars tc) $
710          mapM_ (irType emptyVarSet) (tyConStupidTheta tc)  -- See #8958
711        ; mapM_ (irDataCon tc_name) (visibleDataCons $ algTyConRhs tc) }}
712
713   | Just ty <- synTyConRhs_maybe tc
714   = addRoleInferenceInfo tc_name (tyConTyVars tc) $
715     irType emptyVarSet ty
716
717   | otherwise
718   = return ()
719
720   where
721     tc_name = tyConName tc
722
723 -- any type variable used in an associated type must be Nominal
724 irClass :: Name -> Class -> RoleM ()
725 irClass tc_name cls
726   = addRoleInferenceInfo tc_name cls_tvs $
727     mapM_ ir_at (classATs cls)
728   where
729     cls_tvs    = classTyVars cls
730     cls_tv_set = mkVarSet cls_tvs
731
732     ir_at at_tc
733       = mapM_ (updateRole Nominal) (varSetElems nvars)
734       where nvars = (mkVarSet $ tyConTyVars at_tc) `intersectVarSet` cls_tv_set
735
736 -- See Note [Role inference]
737 irDataCon :: Name -> DataCon -> RoleM ()
738 irDataCon tc_name datacon
739   = addRoleInferenceInfo tc_name univ_tvs $
740     mapM_ (irType ex_var_set) (eqSpecPreds eq_spec ++ theta ++ arg_tys)
741       -- See Note [Role-checking data constructor arguments]
742   where
743     (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig datacon
744     ex_var_set = mkVarSet ex_tvs
745
746 irType :: VarSet -> Type -> RoleM ()
747 irType = go
748   where
749     go lcls (TyVarTy tv) = unless (tv `elemVarSet` lcls) $
750                            updateRole Representational tv
751     go lcls (AppTy t1 t2) = go lcls t1 >> mark_nominal lcls t2
752     go lcls (TyConApp tc tys)
753       = do { roles <- lookupRolesX tc
754            ; zipWithM_ (go_app lcls) roles tys }
755     go lcls (FunTy t1 t2) = go lcls t1 >> go lcls t2
756     go lcls (ForAllTy tv ty) = go (extendVarSet lcls tv) ty
757     go _    (LitTy {}) = return ()
758
759     go_app _ Phantom _ = return ()                 -- nothing to do here
760     go_app lcls Nominal ty = mark_nominal lcls ty  -- all vars below here are N
761     go_app lcls Representational ty = go lcls ty
762
763     mark_nominal lcls ty = let nvars = tyVarsOfType ty `minusVarSet` lcls in
764                            mapM_ (updateRole Nominal) (varSetElems nvars)
765
766 -- like lookupRoles, but with Nominal tags at the end for oversaturated TyConApps
767 lookupRolesX :: TyCon -> RoleM [Role]
768 lookupRolesX tc
769   = do { roles <- lookupRoles tc
770        ; return $ roles ++ repeat Nominal }
771
772 -- gets the roles either from the environment or the tycon
773 lookupRoles :: TyCon -> RoleM [Role]
774 lookupRoles tc
775   = do { env <- getRoleEnv
776        ; case lookupNameEnv env (tyConName tc) of
777            Just roles -> return roles
778            Nothing    -> return $ tyConRoles tc }
779
780 -- tries to update a role; won't ever update a role "downwards"
781 updateRole :: Role -> TyVar -> RoleM ()
782 updateRole role tv
783   = do { var_ns <- getVarNs
784        ; case lookupVarEnv var_ns tv of
785        { Nothing -> pprPanic "updateRole" (ppr tv)
786        ; Just n  -> do
787        { name <- getTyConName
788        ; updateRoleEnv name n role }}}
789
790 -- the state in the RoleM monad
791 data RoleInferenceState = RIS { role_env  :: RoleEnv
792                               , update    :: Bool }
793
794 -- the environment in the RoleM monad
795 type VarPositions = VarEnv Int
796 data RoleInferenceInfo = RII { var_ns :: VarPositions
797                              , name   :: Name }
798
799 -- See [Role inference]
800 newtype RoleM a = RM { unRM :: Maybe RoleInferenceInfo
801                             -> RoleInferenceState
802                             -> (a, RoleInferenceState) }
803
804 instance Functor RoleM where
805     fmap = liftM
806
807 instance Applicative RoleM where
808     pure = return
809     (<*>) = ap
810
811 instance Monad RoleM where
812   return x = RM $ \_ state -> (x, state)
813   a >>= f  = RM $ \m_info state -> let (a', state') = unRM a m_info state in
814                                    unRM (f a') m_info state'
815
816 runRoleM :: RoleEnv -> RoleM () -> (RoleEnv, Bool)
817 runRoleM env thing = (env', update)
818   where RIS { role_env = env', update = update } = snd $ unRM thing Nothing state
819         state = RIS { role_env  = env, update    = False }
820
821 addRoleInferenceInfo :: Name -> [TyVar] -> RoleM a -> RoleM a
822 addRoleInferenceInfo name tvs thing
823   = RM $ \_nothing state -> ASSERT( isNothing _nothing )
824                             unRM thing (Just info) state
825   where info = RII { var_ns = mkVarEnv (zip tvs [0..]), name = name }
826
827 getRoleEnv :: RoleM RoleEnv
828 getRoleEnv = RM $ \_ state@(RIS { role_env = env }) -> (env, state)
829
830 getVarNs :: RoleM VarPositions
831 getVarNs = RM $ \m_info state ->
832                 case m_info of
833                   Nothing -> panic "getVarNs"
834                   Just (RII { var_ns = var_ns }) -> (var_ns, state)
835
836 getTyConName :: RoleM Name
837 getTyConName = RM $ \m_info state ->
838                     case m_info of
839                       Nothing -> panic "getTyConName"
840                       Just (RII { name = name }) -> (name, state)
841
842
843 updateRoleEnv :: Name -> Int -> Role -> RoleM ()
844 updateRoleEnv name n role
845   = RM $ \_ state@(RIS { role_env = role_env }) -> ((),
846          case lookupNameEnv role_env name of
847            Nothing -> pprPanic "updateRoleEnv" (ppr name)
848            Just roles -> let (before, old_role : after) = splitAt n roles in
849                          if role `ltRole` old_role
850                          then let roles' = before ++ role : after
851                                   role_env' = extendNameEnv role_env name roles' in
852                               RIS { role_env = role_env', update = True }
853                          else state )
854
855 \end{code}