Add kind equalities to GHC.
[ghc.git] / compiler / typecheck / TcTyDecls.hs
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
12 {-# LANGUAGE CPP #-}
13
14 module TcTyDecls(
15 calcRecFlags, RecTyInfo(..),
16 calcSynCycles, calcClassCycles,
17
18 -- * Roles
19 RoleAnnots, extractRoleAnnots, emptyRoleAnnots, lookupRoleAnnots,
20
21 -- * Implicits
22 tcAddImplicits,
23
24 -- * Record selectors
25 mkRecSelBinds, mkOneRecordSelector
26 ) where
27
28 #include "HsVersions.h"
29
30 import TcRnMonad
31 import TcEnv
32 import TcTypeable( mkTypeableBinds )
33 import TcBinds( tcRecSelBinds )
34 import TyCoRep( Type(..), TyBinder(..), delBinderVar )
35 import TcType
36 import TysWiredIn( unitTy )
37 import MkCore( rEC_SEL_ERROR_ID )
38 import HsSyn
39 import Class
40 import Type
41 import HscTypes
42 import TyCon
43 import ConLike
44 import DataCon
45 import Name
46 import NameEnv
47 import RdrName ( mkVarUnqual )
48 import Id
49 import IdInfo
50 import VarEnv
51 import VarSet
52 import NameSet
53 import Coercion ( ltRole )
54 import Digraph
55 import BasicTypes
56 import SrcLoc
57 import Unique ( mkBuiltinUnique )
58 import Outputable
59 import UniqSet
60 import Util
61 import Maybes
62 import Data.List
63 import Bag
64 import FastString ( fastStringToByteString )
65
66 import Control.Monad
67
68 {-
69 ************************************************************************
70 * *
71 Cycles in class and type synonym declarations
72 * *
73 ************************************************************************
74
75 Checking for class-decl loops is easy, because we don't allow class decls
76 in interface files.
77
78 We allow type synonyms in hi-boot files, but we *trust* hi-boot files,
79 so we don't check for loops that involve them. So we only look for synonym
80 loops in the module being compiled.
81
82 We check for type synonym and class cycles on the *source* code.
83 Main reasons:
84
85 a) Otherwise we'd need a special function to extract type-synonym tycons
86 from a type, whereas we already have the free vars pinned on the decl
87
88 b) If we checked for type synonym loops after building the TyCon, we
89 can't do a hoistForAllTys on the type synonym rhs, (else we fall into
90 a black hole) which seems unclean. Apart from anything else, it'd mean
91 that a type-synonym rhs could have for-alls to the right of an arrow,
92 which means adding new cases to the validity checker
93
94 Indeed, in general, checking for cycles beforehand means we need to
95 be less careful about black holes through synonym cycles.
96
97 The main disadvantage is that a cycle that goes via a type synonym in an
98 .hi-boot file can lead the compiler into a loop, because it assumes that cycles
99 only occur entirely within the source code of the module being compiled.
100 But hi-boot files are trusted anyway, so this isn't much worse than (say)
101 a kind error.
102
103 [ NOTE ----------------------------------------------
104 If we reverse this decision, this comment came from tcTyDecl1, and should
105 go back there
106 -- dsHsType, not tcHsKindedType, to avoid a loop. tcHsKindedType does hoisting,
107 -- which requires looking through synonyms... and therefore goes into a loop
108 -- on (erroneously) recursive synonyms.
109 -- Solution: do not hoist synonyms, because they'll be hoisted soon enough
110 -- when they are substituted
111
112 We'd also need to add back in this definition
113
114 synonymTyConsOfType :: Type -> [TyCon]
115 -- Does not look through type synonyms at all
116 -- Return a list of synonym tycons
117 synonymTyConsOfType ty
118 = nameEnvElts (go ty)
119 where
120 go :: Type -> NameEnv TyCon -- The NameEnv does duplicate elim
121 go (TyVarTy v) = emptyNameEnv
122 go (TyConApp tc tys) = go_tc tc tys
123 go (AppTy a b) = go a `plusNameEnv` go b
124 go (FunTy a b) = go a `plusNameEnv` go b
125 go (ForAllTy _ ty) = go ty
126
127 go_tc tc tys | isTypeSynonymTyCon tc = extendNameEnv (go_s tys)
128 (tyConName tc) tc
129 | otherwise = go_s tys
130 go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
131 ---------------------------------------- END NOTE ]
132 -}
133
134 mkSynEdges :: [LTyClDecl Name] -> [(LTyClDecl Name, Name, [Name])]
135 mkSynEdges syn_decls = [ (ldecl, name, nameSetElems fvs)
136 | ldecl@(L _ (SynDecl { tcdLName = L _ name
137 , tcdFVs = fvs })) <- syn_decls ]
138
139 calcSynCycles :: [LTyClDecl Name] -> [SCC (LTyClDecl Name)]
140 calcSynCycles = stronglyConnCompFromEdgedVertices . mkSynEdges
141
142 {-
143 Note [Superclass cycle check]
144 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
145 We can't allow cycles via superclasses because it would result in the
146 type checker looping when it canonicalises a class constraint (superclasses
147 are added during canonicalisation). More precisely, given a constraint
148 C ty1 .. tyn
149 we want to instantiate all of C's superclasses, transitively, and
150 that set must be finite. So if
151 class (D b, E b a) => C a b
152 then when we encounter the constraint
153 C ty1 ty2
154 we'll instantiate the superclasses
155 (D ty2, E ty2 ty1)
156 and then *their* superclasses, and so on. This set must be finite!
157
158 It is OK for superclasses to be type synonyms for other classes, so
159 must "look through" type synonyms. Eg
160 type X a = C [a]
161 class X a => C a -- No! Recursive superclass!
162
163 We want definitions such as:
164
165 class C cls a where cls a => a -> a
166 class C D a => D a where
167
168 to be accepted, even though a naive acyclicity check would reject the
169 program as having a cycle between D and its superclass. Why? Because
170 when we instantiate
171 D ty1
172 we get the superclas
173 C D ty1
174 and C has no superclasses, so we have terminated with a finite set.
175
176 More precisely, the rule is this: the superclasses sup_C of a class C
177 are rejected iff:
178
179 C \elem expand(sup_C)
180
181 Where expand is defined as follows:
182
183 (1) expand(a ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
184
185 (2) expand(D ty1 ... tyN) = {D}
186 \union sup_D[ty1/x1, ..., tyP/xP]
187 \union expand(ty(P+1)) ... \union expand(tyN)
188 where (D x1 ... xM) is a class, P = min(M,N)
189
190 (3) expand(T ty1 ... tyN) = expand(ty1) \union ... \union expand(tyN)
191 where T is not a class
192
193 Eqn (1) is conservative; when there's a type variable at the head,
194 look in all the argument types. Eqn (2) expands superclasses; the
195 third component of the union is like Eqn (1). Eqn (3) happens mainly
196 when the context is a (constraint) tuple, such as (Eq a, Show a).
197
198 Furthermore, expand always looks through type synonyms.
199 -}
200
201 calcClassCycles :: Class -> [[TyCon]]
202 calcClassCycles cls
203 = nubBy eqAsCycle $
204 expandTheta (unitUniqSet cls) [classTyCon cls] (classSCTheta cls) []
205 where
206 -- The last TyCon in the cycle is always the same as the first
207 eqAsCycle xs ys = any (xs ==) (cycles (tail ys))
208 cycles xs = take n . map (take n) . tails . cycle $ xs
209 where n = length xs
210
211 -- No more superclasses to expand ==> no problems with cycles
212 -- See Note [Superclass cycle check]
213 expandTheta :: UniqSet Class -- Path of Classes to here in set form
214 -> [TyCon] -- Path to here
215 -> ThetaType -- Superclass work list
216 -> [[TyCon]] -- Input error paths
217 -> [[TyCon]] -- Final error paths
218 expandTheta _ _ [] = id
219 expandTheta seen path (pred:theta) = expandType seen path pred . expandTheta seen path theta
220
221 expandType seen path (TyConApp tc tys)
222 -- Expand unsaturated classes to their superclass theta if they are yet unseen.
223 -- If they have already been seen then we have detected an error!
224 | Just cls <- tyConClass_maybe tc
225 , let (env, remainder) = papp (classTyVars cls) tys
226 rest_tys = either (const []) id remainder
227 = if cls `elementOfUniqSet` seen
228 then (reverse (classTyCon cls:path):)
229 . flip (foldr (expandType seen path)) tys
230 else expandTheta (addOneToUniqSet seen cls) (tc:path)
231 (substTys (mkTopTCvSubst env) (classSCTheta cls))
232 . flip (foldr (expandType seen path)) rest_tys
233
234 -- For synonyms, try to expand them: some arguments might be
235 -- phantoms, after all. We can expand with impunity because at
236 -- this point the type synonym cycle check has already happened.
237 | Just (tvs, rhs) <- synTyConDefn_maybe tc
238 , let (env, remainder) = papp tvs tys
239 rest_tys = either (const []) id remainder
240 = expandType seen (tc:path) (substTy (mkTopTCvSubst env) rhs)
241 . flip (foldr (expandType seen path)) rest_tys
242
243 -- For non-class, non-synonyms, just check the arguments
244 | otherwise
245 = flip (foldr (expandType seen path)) tys
246
247 expandType _ _ (TyVarTy {}) = id
248 expandType _ _ (LitTy {}) = id
249 expandType seen path (AppTy t1 t2) = expandType seen path t1 . expandType seen path t2
250 expandType seen path (ForAllTy b t) = expandType seen path (binderType b) . expandType seen path t
251 expandType seen path (CastTy ty _co) = expandType seen path ty
252 expandType _ _ (CoercionTy {}) = id
253
254 papp :: [TyVar] -> [Type] -> ([(TyVar, Type)], Either [TyVar] [Type])
255 papp [] tys = ([], Right tys)
256 papp tvs [] = ([], Left tvs)
257 papp (tv:tvs) (ty:tys) = ((tv, ty):env, remainder)
258 where (env, remainder) = papp tvs tys
259
260 {-
261 ************************************************************************
262 * *
263 Deciding which type constructors are recursive
264 * *
265 ************************************************************************
266
267 Identification of recursive TyCons
268 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
269 The knot-tying parameters: @rec_details_list@ is an alist mapping @Name@s to
270 @TyThing@s.
271
272 Identifying a TyCon as recursive serves two purposes
273
274 1. Avoid infinite types. Non-recursive newtypes are treated as
275 "transparent", like type synonyms, after the type checker. If we did
276 this for all newtypes, we'd get infinite types. So we figure out for
277 each newtype whether it is "recursive", and add a coercion if so. In
278 effect, we are trying to "cut the loops" by identifying a loop-breaker.
279
280 2. Avoid infinite unboxing. This has nothing to do with newtypes.
281 Suppose we have
282 data T = MkT Int T
283 f (MkT x t) = f t
284 Well, this function diverges, but we don't want the strictness analyser
285 to diverge. But the strictness analyser will diverge because it looks
286 deeper and deeper into the structure of T. (I believe there are
287 examples where the function does something sane, and the strictness
288 analyser still diverges, but I can't see one now.)
289
290 Now, concerning (1), the FC2 branch currently adds a coercion for ALL
291 newtypes. I did this as an experiment, to try to expose cases in which
292 the coercions got in the way of optimisations. If it turns out that we
293 can indeed always use a coercion, then we don't risk recursive types,
294 and don't need to figure out what the loop breakers are.
295
296 For newtype *families* though, we will always have a coercion, so they
297 are always loop breakers! So you can easily adjust the current
298 algorithm by simply treating all newtype families as loop breakers (and
299 indeed type families). I think.
300
301
302
303 For newtypes, we label some as "recursive" such that
304
305 INVARIANT: there is no cycle of non-recursive newtypes
306
307 In any loop, only one newtype need be marked as recursive; it is
308 a "loop breaker". Labelling more than necessary as recursive is OK,
309 provided the invariant is maintained.
310
311 A newtype M.T is defined to be "recursive" iff
312 (a) it is declared in an hi-boot file (see RdrHsSyn.hsIfaceDecl)
313 (b) it is declared in a source file, but that source file has a
314 companion hi-boot file which declares the type
315 or (c) one can get from T's rhs to T via type
316 synonyms, or non-recursive newtypes *in M*
317 e.g. newtype T = MkT (T -> Int)
318
319 (a) is conservative; declarations in hi-boot files are always
320 made loop breakers. That's why in (b) we can restrict attention
321 to tycons in M, because any loops through newtypes outside M
322 will be broken by those newtypes
323 (b) ensures that a newtype is not treated as a loop breaker in one place
324 and later as a non-loop-breaker. This matters in GHCi particularly, when
325 a newtype T might be embedded in many types in the environment, and then
326 T's source module is compiled. We don't want T's recursiveness to change.
327
328 The "recursive" flag for algebraic data types is irrelevant (never consulted)
329 for types with more than one constructor.
330
331
332 An algebraic data type M.T is "recursive" iff
333 it has just one constructor, and
334 (a) it is declared in an hi-boot file (see RdrHsSyn.hsIfaceDecl)
335 (b) it is declared in a source file, but that source file has a
336 companion hi-boot file which declares the type
337 or (c) one can get from its arg types to T via type synonyms,
338 or by non-recursive newtypes or non-recursive product types in M
339 e.g. data T = MkT (T -> Int) Bool
340 Just like newtype in fact
341
342 A type synonym is recursive if one can get from its
343 right hand side back to it via type synonyms. (This is
344 reported as an error.)
345
346 A class is recursive if one can get from its superclasses
347 back to it. (This is an error too.)
348
349 Hi-boot types
350 ~~~~~~~~~~~~~
351 A data type read from an hi-boot file will have an AbstractTyCon as its AlgTyConRhs
352 and will respond True to isAbstractTyCon. The idea is that we treat these as if one
353 could get from these types to anywhere. So when we see
354
355 module Baz where
356 import {-# SOURCE #-} Foo( T )
357 newtype S = MkS T
358
359 then we mark S as recursive, just in case. What that means is that if we see
360
361 import Baz( S )
362 newtype R = MkR S
363
364 then we don't need to look inside S to compute R's recursiveness. Since S is imported
365 (not from an hi-boot file), one cannot get from R back to S except via an hi-boot file,
366 and that means that some data type will be marked recursive along the way. So R is
367 unconditionly non-recursive (i.e. there'll be a loop breaker elsewhere if necessary)
368
369 This in turn means that we grovel through fewer interface files when computing
370 recursiveness, because we need only look at the type decls in the module being
371 compiled, plus the outer structure of directly-mentioned types.
372 -}
373
374 data RecTyInfo = RTI { rti_roles :: Name -> [Role]
375 , rti_is_rec :: Name -> RecFlag }
376
377 calcRecFlags :: SelfBootInfo -> Bool -- hs-boot file?
378 -> RoleAnnots -> [TyCon] -> RecTyInfo
379 -- The 'boot_names' are the things declared in M.hi-boot, if M is the current module.
380 -- Any type constructors in boot_names are automatically considered loop breakers
381 -- Recursion of newtypes/data types can happen via
382 -- the class TyCon, so all_tycons includes the class tycons
383 calcRecFlags boot_details is_boot mrole_env all_tycons
384 = RTI { rti_roles = roles
385 , rti_is_rec = is_rec }
386 where
387 roles = inferRoles is_boot mrole_env all_tycons
388
389 ----------------- Recursion calculation ----------------
390 is_rec n | n `elemNameSet` rec_names = Recursive
391 | otherwise = NonRecursive
392
393 boot_name_set = case boot_details of
394 NoSelfBoot -> emptyNameSet
395 SelfBoot { sb_tcs = tcs } -> tcs
396 rec_names = boot_name_set `unionNameSet`
397 nt_loop_breakers `unionNameSet`
398 prod_loop_breakers
399
400
401 -------------------------------------------------
402 -- NOTE
403 -- These edge-construction loops rely on
404 -- every loop going via tyclss, the types and classes
405 -- in the module being compiled. Stuff in interface
406 -- files should be correctly marked. If not (e.g. a
407 -- type synonym in a hi-boot file) we can get an infinite
408 -- loop. We could program round this, but it'd make the code
409 -- rather less nice, so I'm not going to do that yet.
410
411 single_con_tycons = [ tc | tc <- all_tycons
412 , not (tyConName tc `elemNameSet` boot_name_set)
413 -- Remove the boot_name_set because they are
414 -- going to be loop breakers regardless.
415 , isSingleton (tyConDataCons tc) ]
416 -- Both newtypes and data types, with exactly one data constructor
417
418 (new_tycons, prod_tycons) = partition isNewTyCon single_con_tycons
419 -- NB: we do *not* call isProductTyCon because that checks
420 -- for vanilla-ness of data constructors; and that depends
421 -- on empty existential type variables; and that is figured
422 -- out by tcResultType; which uses tcMatchTy; which uses
423 -- coreView; which calls expandSynTyCon_maybe; which uses
424 -- the recursiveness of the TyCon. Result... a black hole.
425 -- YUK YUK YUK
426
427 --------------- Newtypes ----------------------
428 nt_loop_breakers = mkNameSet (findLoopBreakers nt_edges)
429 is_rec_nt tc = tyConName tc `elemNameSet` nt_loop_breakers
430 -- is_rec_nt is a locally-used helper function
431
432 nt_edges = [(t, mk_nt_edges t) | t <- new_tycons]
433
434 mk_nt_edges nt -- Invariant: nt is a newtype
435 = [ tc | tc <- nameEnvElts (tyConsOfType (new_tc_rhs nt))
436 -- tyConsOfType looks through synonyms
437 , tc `elem` new_tycons ]
438 -- If not (tc `elem` new_tycons) we know that either it's a local *data* type,
439 -- or it's imported. Either way, it can't form part of a newtype cycle
440
441 --------------- Product types ----------------------
442 prod_loop_breakers = mkNameSet (findLoopBreakers prod_edges)
443
444 prod_edges = [(tc, mk_prod_edges tc) | tc <- prod_tycons]
445
446 mk_prod_edges tc -- Invariant: tc is a product tycon
447 = concatMap (mk_prod_edges1 tc) (dataConOrigArgTys (head (tyConDataCons tc)))
448
449 mk_prod_edges1 ptc ty = concatMap (mk_prod_edges2 ptc) (nameEnvElts (tyConsOfType ty))
450
451 mk_prod_edges2 ptc tc
452 | tc `elem` prod_tycons = [tc] -- Local product
453 | tc `elem` new_tycons = if is_rec_nt tc -- Local newtype
454 then []
455 else mk_prod_edges1 ptc (new_tc_rhs tc)
456 -- At this point we know that either it's a local non-product data type,
457 -- or it's imported. Either way, it can't form part of a cycle
458 | otherwise = []
459
460 new_tc_rhs :: TyCon -> Type
461 new_tc_rhs tc = snd (newTyConRhs tc) -- Ignore the type variables
462
463 findLoopBreakers :: [(TyCon, [TyCon])] -> [Name]
464 -- Finds a set of tycons that cut all loops
465 findLoopBreakers deps
466 = go [(tc,tc,ds) | (tc,ds) <- deps]
467 where
468 go edges = [ name
469 | CyclicSCC ((tc,_,_) : edges') <- stronglyConnCompFromEdgedVerticesR edges,
470 name <- tyConName tc : go edges']
471
472 {-
473 ************************************************************************
474 * *
475 Role annotations
476 * *
477 ************************************************************************
478 -}
479
480 type RoleAnnots = NameEnv (LRoleAnnotDecl Name)
481
482 extractRoleAnnots :: TyClGroup Name -> RoleAnnots
483 extractRoleAnnots (TyClGroup { group_roles = roles })
484 = mkNameEnv [ (tycon, role_annot)
485 | role_annot@(L _ (RoleAnnotDecl (L _ tycon) _)) <- roles ]
486
487 emptyRoleAnnots :: RoleAnnots
488 emptyRoleAnnots = emptyNameEnv
489
490 lookupRoleAnnots :: RoleAnnots -> Name -> Maybe (LRoleAnnotDecl Name)
491 lookupRoleAnnots = lookupNameEnv
492
493 {-
494 ************************************************************************
495 * *
496 Role inference
497 * *
498 ************************************************************************
499
500 Note [Role inference]
501 ~~~~~~~~~~~~~~~~~~~~~
502 The role inference algorithm datatype definitions to infer the roles on the
503 parameters. Although these roles are stored in the tycons, we can perform this
504 algorithm on the built tycons, as long as we don't peek at an as-yet-unknown
505 roles field! Ah, the magic of laziness.
506
507 First, we choose appropriate initial roles. For families and classes, roles
508 (including initial roles) are N. For datatypes, we start with the role in the
509 role annotation (if any), or otherwise use Phantom. This is done in
510 initialRoleEnv1.
511
512 The function irGroup then propagates role information until it reaches a
513 fixpoint, preferring N over (R or P) and R over P. To aid in this, we have a
514 monad RoleM, which is a combination reader and state monad. In its state are
515 the current RoleEnv, which gets updated by role propagation, and an update
516 bit, which we use to know whether or not we've reached the fixpoint. The
517 environment of RoleM contains the tycon whose parameters we are inferring, and
518 a VarEnv from parameters to their positions, so we can update the RoleEnv.
519 Between tycons, this reader information is missing; it is added by
520 addRoleInferenceInfo.
521
522 There are two kinds of tycons to consider: algebraic ones (excluding classes)
523 and type synonyms. (Remember, families don't participate -- all their parameters
524 are N.) An algebraic tycon processes each of its datacons, in turn. Note that
525 a datacon's universally quantified parameters might be different from the parent
526 tycon's parameters, so we use the datacon's univ parameters in the mapping from
527 vars to positions. Note also that we don't want to infer roles for existentials
528 (they're all at N, too), so we put them in the set of local variables. As an
529 optimisation, we skip any tycons whose roles are already all Nominal, as there
530 nowhere else for them to go. For synonyms, we just analyse their right-hand sides.
531
532 irType walks through a type, looking for uses of a variable of interest and
533 propagating role information. Because anything used under a phantom position
534 is at phantom and anything used under a nominal position is at nominal, the
535 irType function can assume that anything it sees is at representational. (The
536 other possibilities are pruned when they're encountered.)
537
538 The rest of the code is just plumbing.
539
540 How do we know that this algorithm is correct? It should meet the following
541 specification:
542
543 Let Z be a role context -- a mapping from variables to roles. The following
544 rules define the property (Z |- t : r), where t is a type and r is a role:
545
546 Z(a) = r' r' <= r
547 ------------------------- RCVar
548 Z |- a : r
549
550 ---------- RCConst
551 Z |- T : r -- T is a type constructor
552
553 Z |- t1 : r
554 Z |- t2 : N
555 -------------- RCApp
556 Z |- t1 t2 : r
557
558 forall i<=n. (r_i is R or N) implies Z |- t_i : r_i
559 roles(T) = r_1 .. r_n
560 ---------------------------------------------------- RCDApp
561 Z |- T t_1 .. t_n : R
562
563 Z, a:N |- t : r
564 ---------------------- RCAll
565 Z |- forall a:k.t : r
566
567
568 We also have the following rules:
569
570 For all datacon_i in type T, where a_1 .. a_n are universally quantified
571 and b_1 .. b_m are existentially quantified, and the arguments are t_1 .. t_p,
572 then if forall j<=p, a_1 : r_1 .. a_n : r_n, b_1 : N .. b_m : N |- t_j : R,
573 then roles(T) = r_1 .. r_n
574
575 roles(->) = R, R
576 roles(~#) = N, N
577
578 With -dcore-lint on, the output of this algorithm is checked in checkValidRoles,
579 called from checkValidTycon.
580
581 Note [Role-checking data constructor arguments]
582 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
583 Consider
584 data T a where
585 MkT :: Eq b => F a -> (a->a) -> T (G a)
586
587 Then we want to check the roles at which 'a' is used
588 in MkT's type. We want to work on the user-written type,
589 so we need to take into account
590 * the arguments: (F a) and (a->a)
591 * the context: C a b
592 * the result type: (G a) -- this is in the eq_spec
593
594
595 Note [Coercions in role inference]
596 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
597 Is (t |> co1) representationally equal to (t |> co2)? Of course they are! Changing
598 the kind of a type is totally irrelevant to the representation of that type. So,
599 we want to totally ignore coercions when doing role inference. This includes omitting
600 any type variables that appear in nominal positions but only within coercions.
601 -}
602
603 type RoleEnv = NameEnv [Role] -- from tycon names to roles
604
605 -- This, and any of the functions it calls, must *not* look at the roles
606 -- field of a tycon we are inferring roles about!
607 -- See Note [Role inference]
608 inferRoles :: Bool -> RoleAnnots -> [TyCon] -> Name -> [Role]
609 inferRoles is_boot annots tycons
610 = let role_env = initialRoleEnv is_boot annots tycons
611 role_env' = irGroup role_env tycons in
612 \name -> case lookupNameEnv role_env' name of
613 Just roles -> roles
614 Nothing -> pprPanic "inferRoles" (ppr name)
615
616 initialRoleEnv :: Bool -> RoleAnnots -> [TyCon] -> RoleEnv
617 initialRoleEnv is_boot annots = extendNameEnvList emptyNameEnv .
618 map (initialRoleEnv1 is_boot annots)
619
620 initialRoleEnv1 :: Bool -> RoleAnnots -> TyCon -> (Name, [Role])
621 initialRoleEnv1 is_boot annots_env tc
622 | isFamilyTyCon tc = (name, map (const Nominal) bndrs)
623 | isAlgTyCon tc = (name, default_roles)
624 | isTypeSynonymTyCon tc = (name, default_roles)
625 | otherwise = pprPanic "initialRoleEnv1" (ppr tc)
626 where name = tyConName tc
627 bndrs = tyConBinders tc
628 visflags = map binderVisibility $ take (tyConArity tc) bndrs
629 num_exps = count (== Visible) visflags
630
631 -- if the number of annotations in the role annotation decl
632 -- is wrong, just ignore it. We check this in the validity check.
633 role_annots
634 = case lookupNameEnv annots_env name of
635 Just (L _ (RoleAnnotDecl _ annots))
636 | annots `lengthIs` num_exps -> map unLoc annots
637 _ -> replicate num_exps Nothing
638 default_roles = build_default_roles visflags role_annots
639
640 build_default_roles (Invisible : viss) ras
641 = Nominal : build_default_roles viss ras
642 build_default_roles (Visible : viss) (m_annot : ras)
643 = (m_annot `orElse` default_role) : build_default_roles viss ras
644 build_default_roles [] [] = []
645 build_default_roles _ _ = pprPanic "initialRoleEnv1 (2)"
646 (vcat [ppr tc, ppr role_annots])
647
648 default_role
649 | isClassTyCon tc = Nominal
650 | is_boot && isAbstractTyCon tc = Representational
651 | otherwise = Phantom
652
653 irGroup :: RoleEnv -> [TyCon] -> RoleEnv
654 irGroup env tcs
655 = let (env', update) = runRoleM env $ mapM_ irTyCon tcs in
656 if update
657 then irGroup env' tcs
658 else env'
659
660 irTyCon :: TyCon -> RoleM ()
661 irTyCon tc
662 | isAlgTyCon tc
663 = do { old_roles <- lookupRoles tc
664 ; unless (all (== Nominal) old_roles) $ -- also catches data families,
665 -- which don't want or need role inference
666 irTcTyVars tc $
667 do { mapM_ (irType emptyVarSet) (tyConStupidTheta tc) -- See #8958
668 ; whenIsJust (tyConClass_maybe tc) irClass
669 ; mapM_ irDataCon (visibleDataCons $ algTyConRhs tc) }}
670
671 | Just ty <- synTyConRhs_maybe tc
672 = irTcTyVars tc $
673 irType emptyVarSet ty
674
675 | otherwise
676 = return ()
677
678 -- any type variable used in an associated type must be Nominal
679 irClass :: Class -> RoleM ()
680 irClass cls
681 = mapM_ ir_at (classATs cls)
682 where
683 cls_tvs = classTyVars cls
684 cls_tv_set = mkVarSet cls_tvs
685
686 ir_at at_tc
687 = mapM_ (updateRole Nominal) (varSetElems nvars)
688 where nvars = (mkVarSet $ tyConTyVars at_tc) `intersectVarSet` cls_tv_set
689
690 -- See Note [Role inference]
691 irDataCon :: DataCon -> RoleM ()
692 irDataCon datacon
693 = setRoleInferenceVars univ_tvs $
694 irExTyVars ex_tvs $ \ ex_var_set ->
695 mapM_ (irType ex_var_set)
696 (map tyVarKind ex_tvs ++ eqSpecPreds eq_spec ++ theta ++ arg_tys)
697 -- See Note [Role-checking data constructor arguments]
698 where
699 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
700 = dataConFullSig datacon
701
702 irType :: VarSet -> Type -> RoleM ()
703 irType = go
704 where
705 go lcls (TyVarTy tv) = unless (tv `elemVarSet` lcls) $
706 updateRole Representational tv
707 go lcls (AppTy t1 t2) = go lcls t1 >> markNominal lcls t2
708 go lcls (TyConApp tc tys) = do { roles <- lookupRolesX tc
709 ; zipWithM_ (go_app lcls) roles tys }
710 go lcls (ForAllTy (Named tv _) ty)
711 = let lcls' = extendVarSet lcls tv in
712 markNominal lcls (tyVarKind tv) >> go lcls' ty
713 go lcls (ForAllTy (Anon arg) res)
714 = go lcls arg >> go lcls res
715 go _ (LitTy {}) = return ()
716 -- See Note [Coercions in role inference]
717 go lcls (CastTy ty _) = go lcls ty
718 go _ (CoercionTy _) = return ()
719
720 go_app _ Phantom _ = return () -- nothing to do here
721 go_app lcls Nominal ty = markNominal lcls ty -- all vars below here are N
722 go_app lcls Representational ty = go lcls ty
723
724 irTcTyVars :: TyCon -> RoleM a -> RoleM a
725 irTcTyVars tc thing
726 = setRoleInferenceTc (tyConName tc) $ go (tyConTyVars tc)
727 where
728 go [] = thing
729 go (tv:tvs) = do { markNominal emptyVarSet (tyVarKind tv)
730 ; addRoleInferenceVar tv $ go tvs }
731
732 irExTyVars :: [TyVar] -> (TyVarSet -> RoleM a) -> RoleM a
733 irExTyVars orig_tvs thing = go emptyVarSet orig_tvs
734 where
735 go lcls [] = thing lcls
736 go lcls (tv:tvs) = do { markNominal lcls (tyVarKind tv)
737 ; go (extendVarSet lcls tv) tvs }
738
739 markNominal :: TyVarSet -- local variables
740 -> Type -> RoleM ()
741 markNominal lcls ty = let nvars = get_ty_vars ty `minusVarSet` lcls in
742 mapM_ (updateRole Nominal) (varSetElems nvars)
743 where
744 -- get_ty_vars gets all the tyvars (no covars!) from a type *without*
745 -- recurring into coercions. Recall: coercions are totally ignored during
746 -- role inference. See [Coercions in role inference]
747 get_ty_vars (TyVarTy tv) = unitVarSet tv
748 get_ty_vars (AppTy t1 t2) = get_ty_vars t1 `unionVarSet` get_ty_vars t2
749 get_ty_vars (TyConApp _ tys) = foldr (unionVarSet . get_ty_vars) emptyVarSet tys
750 get_ty_vars (ForAllTy bndr ty)
751 = get_ty_vars ty `delBinderVar` bndr
752 `unionVarSet` (tyCoVarsOfType $ binderType bndr)
753 get_ty_vars (LitTy {}) = emptyVarSet
754 get_ty_vars (CastTy ty _) = get_ty_vars ty
755 get_ty_vars (CoercionTy _) = emptyVarSet
756
757 -- like lookupRoles, but with Nominal tags at the end for oversaturated TyConApps
758 lookupRolesX :: TyCon -> RoleM [Role]
759 lookupRolesX tc
760 = do { roles <- lookupRoles tc
761 ; return $ roles ++ repeat Nominal }
762
763 -- gets the roles either from the environment or the tycon
764 lookupRoles :: TyCon -> RoleM [Role]
765 lookupRoles tc
766 = do { env <- getRoleEnv
767 ; case lookupNameEnv env (tyConName tc) of
768 Just roles -> return roles
769 Nothing -> return $ tyConRoles tc }
770
771 -- tries to update a role; won't ever update a role "downwards"
772 updateRole :: Role -> TyVar -> RoleM ()
773 updateRole role tv
774 = do { var_ns <- getVarNs
775 ; name <- getTyConName
776 ; case lookupVarEnv var_ns tv of
777 Nothing -> pprPanic "updateRole" (ppr name $$ ppr tv $$ ppr var_ns)
778 Just n -> updateRoleEnv name n role }
779
780 -- the state in the RoleM monad
781 data RoleInferenceState = RIS { role_env :: RoleEnv
782 , update :: Bool }
783
784 -- the environment in the RoleM monad
785 type VarPositions = VarEnv Int
786
787 -- See [Role inference]
788 newtype RoleM a = RM { unRM :: Maybe Name -- of the tycon
789 -> VarPositions
790 -> Int -- size of VarPositions
791 -> RoleInferenceState
792 -> (a, RoleInferenceState) }
793
794 instance Functor RoleM where
795 fmap = liftM
796
797 instance Applicative RoleM where
798 pure x = RM $ \_ _ _ state -> (x, state)
799 (<*>) = ap
800
801 instance Monad RoleM where
802 return = pure
803 a >>= f = RM $ \m_info vps nvps state ->
804 let (a', state') = unRM a m_info vps nvps state in
805 unRM (f a') m_info vps nvps state'
806
807 runRoleM :: RoleEnv -> RoleM () -> (RoleEnv, Bool)
808 runRoleM env thing = (env', update)
809 where RIS { role_env = env', update = update }
810 = snd $ unRM thing Nothing emptyVarEnv 0 state
811 state = RIS { role_env = env
812 , update = False }
813
814 setRoleInferenceTc :: Name -> RoleM a -> RoleM a
815 setRoleInferenceTc name thing = RM $ \m_name vps nvps state ->
816 ASSERT( isNothing m_name )
817 ASSERT( isEmptyVarEnv vps )
818 ASSERT( nvps == 0 )
819 unRM thing (Just name) vps nvps state
820
821 addRoleInferenceVar :: TyVar -> RoleM a -> RoleM a
822 addRoleInferenceVar tv thing
823 = RM $ \m_name vps nvps state ->
824 ASSERT( isJust m_name )
825 unRM thing m_name (extendVarEnv vps tv nvps) (nvps+1) state
826
827 setRoleInferenceVars :: [TyVar] -> RoleM a -> RoleM a
828 setRoleInferenceVars tvs thing
829 = RM $ \m_name _vps _nvps state ->
830 ASSERT( isJust m_name )
831 unRM thing m_name (mkVarEnv (zip tvs [0..])) (panic "setRoleInferenceVars")
832 state
833
834 getRoleEnv :: RoleM RoleEnv
835 getRoleEnv = RM $ \_ _ _ state@(RIS { role_env = env }) -> (env, state)
836
837 getVarNs :: RoleM VarPositions
838 getVarNs = RM $ \_ vps _ state -> (vps, state)
839
840 getTyConName :: RoleM Name
841 getTyConName = RM $ \m_name _ _ state ->
842 case m_name of
843 Nothing -> panic "getTyConName"
844 Just name -> (name, state)
845
846 updateRoleEnv :: Name -> Int -> Role -> RoleM ()
847 updateRoleEnv name n role
848 = RM $ \_ _ _ state@(RIS { role_env = role_env }) -> ((),
849 case lookupNameEnv role_env name of
850 Nothing -> pprPanic "updateRoleEnv" (ppr name)
851 Just roles -> let (before, old_role : after) = splitAt n roles in
852 if role `ltRole` old_role
853 then let roles' = before ++ role : after
854 role_env' = extendNameEnv role_env name roles' in
855 RIS { role_env = role_env', update = True }
856 else state )
857
858
859 {- *********************************************************************
860 * *
861 Building implicits
862 * *
863 ********************************************************************* -}
864
865 tcAddImplicits :: [TyCon] -> TcM TcGblEnv
866 -- Given a [TyCon], add to the TcGblEnv
867 -- * extend the TypeEnv with their implicitTyThings
868 -- * extend the TypeEnv with any default method Ids
869 -- * add bindings for record selectors
870 -- * add bindings for type representations for the TyThings
871 tcAddImplicits tycons
872 = discardWarnings $
873 tcExtendGlobalEnvImplicit implicit_things $
874 tcExtendGlobalValEnv def_meth_ids $
875 do { traceTc "tcAddImplicits" $ vcat
876 [ text "tycons" <+> ppr tycons
877 , text "implicits" <+> ppr implicit_things ]
878 ; gbl_env <- mkTypeableBinds tycons
879 ; gbl_env <- setGblEnv gbl_env $
880 tcRecSelBinds (mkRecSelBinds tycons)
881 ; return gbl_env }
882 where
883 implicit_things = concatMap implicitTyConThings tycons
884 def_meth_ids = mkDefaultMethodIds tycons
885
886 mkDefaultMethodIds :: [TyCon] -> [Id]
887 -- We want to put the default-method Ids (both vanilla and generic)
888 -- into the type environment so that they are found when we typecheck
889 -- the filled-in default methods of each instance declaration
890 -- See Note [Default method Ids and Template Haskell]
891 mkDefaultMethodIds tycons
892 = [ mkExportedLocalId VanillaId dm_name (mk_dm_ty cls sel_id dm_spec)
893 | tc <- tycons
894 , Just cls <- [tyConClass_maybe tc]
895 , (sel_id, Just (dm_name, dm_spec)) <- classOpItems cls ]
896 where
897 mk_dm_ty :: Class -> Id -> DefMethSpec Type -> Type
898 mk_dm_ty _ sel_id VanillaDM = idType sel_id
899 mk_dm_ty cls _ (GenericDM dm_ty) = mkInvSigmaTy cls_tvs [pred] dm_ty
900 where
901 cls_tvs = classTyVars cls
902 pred = mkClassPred cls (mkTyVarTys cls_tvs)
903
904 {-
905 ************************************************************************
906 * *
907 Building record selectors
908 * *
909 ************************************************************************
910 -}
911
912 {-
913 Note [Default method Ids and Template Haskell]
914 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
915 Consider this (Trac #4169):
916 class Numeric a where
917 fromIntegerNum :: a
918 fromIntegerNum = ...
919
920 ast :: Q [Dec]
921 ast = [d| instance Numeric Int |]
922
923 When we typecheck 'ast' we have done the first pass over the class decl
924 (in tcTyClDecls), but we have not yet typechecked the default-method
925 declarations (because they can mention value declarations). So we
926 must bring the default method Ids into scope first (so they can be seen
927 when typechecking the [d| .. |] quote, and typecheck them later.
928 -}
929
930 {-
931 ************************************************************************
932 * *
933 Building record selectors
934 * *
935 ************************************************************************
936 -}
937
938 mkRecSelBinds :: [TyCon] -> HsValBinds Name
939 -- NB We produce *un-typechecked* bindings, rather like 'deriving'
940 -- This makes life easier, because the later type checking will add
941 -- all necessary type abstractions and applications
942 mkRecSelBinds tycons
943 = ValBindsOut binds sigs
944 where
945 (sigs, binds) = unzip rec_sels
946 rec_sels = map mkRecSelBind [ (tc,fld)
947 | tc <- tycons
948 , fld <- tyConFieldLabels tc ]
949
950 mkRecSelBind :: (TyCon, FieldLabel) -> (LSig Name, (RecFlag, LHsBinds Name))
951 mkRecSelBind (tycon, fl)
952 = mkOneRecordSelector all_cons (RecSelData tycon) fl
953 where
954 all_cons = map RealDataCon (tyConDataCons tycon)
955
956 mkOneRecordSelector :: [ConLike] -> RecSelParent -> FieldLabel
957 -> (LSig Name, (RecFlag, LHsBinds Name))
958 mkOneRecordSelector all_cons idDetails fl
959 = (L loc (IdSig sel_id), (NonRecursive, unitBag (L loc sel_bind)))
960 where
961 loc = getSrcSpan sel_name
962 lbl = flLabel fl
963 sel_name = flSelector fl
964
965 sel_id = mkExportedLocalId rec_details sel_name sel_ty
966 rec_details = RecSelId { sel_tycon = idDetails, sel_naughty = is_naughty }
967
968 -- Find a representative constructor, con1
969 cons_w_field = conLikesWithFields all_cons [lbl]
970 con1 = ASSERT( not (null cons_w_field) ) head cons_w_field
971
972 -- Selector type; Note [Polymorphic selectors]
973 field_ty = conLikeFieldType con1 lbl
974 data_tvs = tyCoVarsOfType data_ty
975 is_naughty = not (tyCoVarsOfType field_ty `subVarSet` data_tvs)
976 (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
977 all_tvs = varSetElemsWellScoped $ data_tvs `extendVarSetList` field_tvs
978 sel_ty | is_naughty = unitTy -- See Note [Naughty record selectors]
979 | otherwise = ASSERT( all isTyVar all_tvs )
980 mkInvForAllTys all_tvs $
981 mkPhiTy (conLikeStupidTheta con1) $ -- Urgh!
982 mkPhiTy field_theta $ -- Urgh!
983 -- req_theta is empty for normal DataCon
984 mkPhiTy req_theta $
985 mkFunTy data_ty field_tau
986
987 -- Make the binding: sel (C2 { fld = x }) = x
988 -- sel (C7 { fld = x }) = x
989 -- where cons_w_field = [C2,C7]
990 sel_bind = mkTopFunBind Generated sel_lname alts
991 where
992 alts | is_naughty = [mkSimpleMatch [] unit_rhs]
993 | otherwise = map mk_match cons_w_field ++ deflt
994 mk_match con = mkSimpleMatch [L loc (mk_sel_pat con)]
995 (L loc (HsVar (L loc field_var)))
996 mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields)
997 rec_fields = HsRecFields { rec_flds = [rec_field], rec_dotdot = Nothing }
998 rec_field = noLoc (HsRecField
999 { hsRecFieldLbl = L loc (FieldOcc (mkVarUnqual lbl)
1000 sel_name)
1001 , hsRecFieldArg = L loc (VarPat (L loc field_var))
1002 , hsRecPun = False })
1003 sel_lname = L loc sel_name
1004 field_var = mkInternalName (mkBuiltinUnique 1) (getOccName sel_name) loc
1005
1006 -- Add catch-all default case unless the case is exhaustive
1007 -- We do this explicitly so that we get a nice error message that
1008 -- mentions this particular record selector
1009 deflt | all dealt_with all_cons = []
1010 | otherwise = [mkSimpleMatch [L loc (WildPat placeHolderType)]
1011 (mkHsApp (L loc (HsVar
1012 (L loc (getName rEC_SEL_ERROR_ID))))
1013 (L loc (HsLit msg_lit)))]
1014
1015 -- Do not add a default case unless there are unmatched
1016 -- constructors. We must take account of GADTs, else we
1017 -- get overlap warning messages from the pattern-match checker
1018 -- NB: we need to pass type args for the *representation* TyCon
1019 -- to dataConCannotMatch, hence the calculation of inst_tys
1020 -- This matters in data families
1021 -- data instance T Int a where
1022 -- A :: { fld :: Int } -> T Int Bool
1023 -- B :: { fld :: Int } -> T Int Char
1024 dealt_with :: ConLike -> Bool
1025 dealt_with (PatSynCon _) = False -- We can't predict overlap
1026 dealt_with con@(RealDataCon dc) =
1027 con `elem` cons_w_field || dataConCannotMatch inst_tys dc
1028
1029 (univ_tvs, _, eq_spec, _, req_theta, _, data_ty) = conLikeFullSig con1
1030
1031 inst_tys = substTyVars (mkTopTCvSubst (map eqSpecPair eq_spec)) univ_tvs
1032
1033 unit_rhs = mkLHsTupleExpr []
1034 msg_lit = HsStringPrim "" (fastStringToByteString lbl)
1035
1036 {-
1037 Note [Polymorphic selectors]
1038 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1039 When a record has a polymorphic field, we pull the foralls out to the front.
1040 data T = MkT { f :: forall a. [a] -> a }
1041 Then f :: forall a. T -> [a] -> a
1042 NOT f :: T -> forall a. [a] -> a
1043
1044 This is horrid. It's only needed in deeply obscure cases, which I hate.
1045 The only case I know is test tc163, which is worth looking at. It's far
1046 from clear that this test should succeed at all!
1047
1048 Note [Naughty record selectors]
1049 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1050 A "naughty" field is one for which we can't define a record
1051 selector, because an existential type variable would escape. For example:
1052 data T = forall a. MkT { x,y::a }
1053 We obviously can't define
1054 x (MkT v _) = v
1055 Nevertheless we *do* put a RecSelId into the type environment
1056 so that if the user tries to use 'x' as a selector we can bleat
1057 helpfully, rather than saying unhelpfully that 'x' is not in scope.
1058 Hence the sel_naughty flag, to identify record selectors that don't really exist.
1059
1060 In general, a field is "naughty" if its type mentions a type variable that
1061 isn't in the result type of the constructor. Note that this *allows*
1062 GADT record selectors (Note [GADT record selectors]) whose types may look
1063 like sel :: T [a] -> a
1064
1065 For naughty selectors we make a dummy binding
1066 sel = ()
1067 so that the later type-check will add them to the environment, and they'll be
1068 exported. The function is never called, because the typechecker spots the
1069 sel_naughty field.
1070
1071 Note [GADT record selectors]
1072 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1073 For GADTs, we require that all constructors with a common field 'f' have the same
1074 result type (modulo alpha conversion). [Checked in TcTyClsDecls.checkValidTyCon]
1075 E.g.
1076 data T where
1077 T1 { f :: Maybe a } :: T [a]
1078 T2 { f :: Maybe a, y :: b } :: T [a]
1079 T3 :: T Int
1080
1081 and now the selector takes that result type as its argument:
1082 f :: forall a. T [a] -> Maybe a
1083
1084 Details: the "real" types of T1,T2 are:
1085 T1 :: forall r a. (r~[a]) => a -> T r
1086 T2 :: forall r a b. (r~[a]) => a -> b -> T r
1087
1088 So the selector loooks like this:
1089 f :: forall a. T [a] -> Maybe a
1090 f (a:*) (t:T [a])
1091 = case t of
1092 T1 c (g:[a]~[c]) (v:Maybe c) -> v `cast` Maybe (right (sym g))
1093 T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
1094 T3 -> error "T3 does not have field f"
1095
1096 Note the forall'd tyvars of the selector are just the free tyvars
1097 of the result type; there may be other tyvars in the constructor's
1098 type (e.g. 'b' in T2).
1099
1100 Note the need for casts in the result!
1101
1102 Note [Selector running example]
1103 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1104 It's OK to combine GADTs and type families. Here's a running example:
1105
1106 data instance T [a] where
1107 T1 { fld :: b } :: T [Maybe b]
1108
1109 The representation type looks like this
1110 data :R7T a where
1111 T1 { fld :: b } :: :R7T (Maybe b)
1112
1113 and there's coercion from the family type to the representation type
1114 :CoR7T a :: T [a] ~ :R7T a
1115
1116 The selector we want for fld looks like this:
1117
1118 fld :: forall b. T [Maybe b] -> b
1119 fld = /\b. \(d::T [Maybe b]).
1120 case d `cast` :CoR7T (Maybe b) of
1121 T1 (x::b) -> x
1122
1123 The scrutinee of the case has type :R7T (Maybe b), which can be
1124 gotten by appying the eq_spec to the univ_tvs of the data con.
1125
1126 -}