[TTG: Handling Source Locations] Foundation and Pat
[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. Specifically, 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 {-# LANGUAGE TypeFamilies #-}
14 {-# LANGUAGE ViewPatterns #-}
15
16 module TcTyDecls(
17 RolesInfo,
18 inferRoles,
19 checkSynCycles,
20 checkClassCycles,
21
22 -- * Implicits
23 addTyConsToGblEnv, mkDefaultMethodType,
24
25 -- * Record selectors
26 tcRecSelBinds, mkRecSelBinds, mkOneRecordSelector
27 ) where
28
29 #include "HsVersions.h"
30
31 import GhcPrelude
32
33 import TcRnMonad
34 import TcEnv
35 import TcBinds( tcValBinds, addTypecheckedBinds )
36 import TyCoRep( Type(..), Coercion(..), MCoercion(..), UnivCoProvenance(..) )
37 import TcType
38 import TysWiredIn( unitTy )
39 import MkCore( rEC_SEL_ERROR_ID )
40 import HsSyn
41 import Class
42 import Type
43 import HscTypes
44 import TyCon
45 import ConLike
46 import DataCon
47 import Name
48 import NameEnv
49 import NameSet hiding (unitFV)
50 import RdrName ( mkVarUnqual )
51 import Id
52 import IdInfo
53 import VarEnv
54 import VarSet
55 import Coercion ( ltRole )
56 import BasicTypes
57 import SrcLoc
58 import Unique ( mkBuiltinUnique )
59 import Outputable
60 import Util
61 import Maybes
62 import Bag
63 import FastString
64 import FV
65 import Module
66
67 import Control.Monad
68
69 {-
70 ************************************************************************
71 * *
72 Cycles in type synonym declarations
73 * *
74 ************************************************************************
75 -}
76
77 synonymTyConsOfType :: Type -> [TyCon]
78 -- Does not look through type synonyms at all
79 -- Return a list of synonym tycons
80 -- Keep this synchronized with 'expandTypeSynonyms'
81 synonymTyConsOfType ty
82 = nameEnvElts (go ty)
83 where
84 go :: Type -> NameEnv TyCon -- The NameEnv does duplicate elim
85 go (TyConApp tc tys) = go_tc tc `plusNameEnv` go_s tys
86 go (LitTy _) = emptyNameEnv
87 go (TyVarTy _) = emptyNameEnv
88 go (AppTy a b) = go a `plusNameEnv` go b
89 go (FunTy a b) = go a `plusNameEnv` go b
90 go (ForAllTy _ ty) = go ty
91 go (CastTy ty co) = go ty `plusNameEnv` go_co co
92 go (CoercionTy co) = go_co co
93
94 -- Note [TyCon cycles through coercions?!]
95 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
96 -- Although, in principle, it's possible for a type synonym loop
97 -- could go through a coercion (since a coercion can refer to
98 -- a TyCon or Type), it doesn't seem possible to actually construct
99 -- a Haskell program which tickles this case. Here is an example
100 -- program which causes a coercion:
101 --
102 -- type family Star where
103 -- Star = Type
104 --
105 -- data T :: Star -> Type
106 -- data S :: forall (a :: Type). T a -> Type
107 --
108 -- Here, the application 'T a' must first coerce a :: Type to a :: Star,
109 -- witnessed by the type family. But if we now try to make Type refer
110 -- to a type synonym which in turn refers to Star, we'll run into
111 -- trouble: we're trying to define and use the type constructor
112 -- in the same recursive group. Possibly this restriction will be
113 -- lifted in the future but for now, this code is "just for completeness
114 -- sake".
115 go_mco MRefl = emptyNameEnv
116 go_mco (MCo co) = go_co co
117
118 go_co (Refl ty) = go ty
119 go_co (GRefl _ ty mco) = go ty `plusNameEnv` go_mco mco
120 go_co (TyConAppCo _ tc cs) = go_tc tc `plusNameEnv` go_co_s cs
121 go_co (AppCo co co') = go_co co `plusNameEnv` go_co co'
122 go_co (ForAllCo _ co co') = go_co co `plusNameEnv` go_co co'
123 go_co (FunCo _ co co') = go_co co `plusNameEnv` go_co co'
124 go_co (CoVarCo _) = emptyNameEnv
125 go_co (HoleCo {}) = emptyNameEnv
126 go_co (AxiomInstCo _ _ cs) = go_co_s cs
127 go_co (UnivCo p _ ty ty') = go_prov p `plusNameEnv` go ty `plusNameEnv` go ty'
128 go_co (SymCo co) = go_co co
129 go_co (TransCo co co') = go_co co `plusNameEnv` go_co co'
130 go_co (NthCo _ _ co) = go_co co
131 go_co (LRCo _ co) = go_co co
132 go_co (InstCo co co') = go_co co `plusNameEnv` go_co co'
133 go_co (KindCo co) = go_co co
134 go_co (SubCo co) = go_co co
135 go_co (AxiomRuleCo _ cs) = go_co_s cs
136
137 go_prov UnsafeCoerceProv = emptyNameEnv
138 go_prov (PhantomProv co) = go_co co
139 go_prov (ProofIrrelProv co) = go_co co
140 go_prov (PluginProv _) = emptyNameEnv
141
142 go_tc tc | isTypeSynonymTyCon tc = unitNameEnv (tyConName tc) tc
143 | otherwise = emptyNameEnv
144 go_s tys = foldr (plusNameEnv . go) emptyNameEnv tys
145 go_co_s cos = foldr (plusNameEnv . go_co) emptyNameEnv cos
146
147 -- | A monad for type synonym cycle checking, which keeps
148 -- track of the TyCons which are known to be acyclic, or
149 -- a failure message reporting that a cycle was found.
150 newtype SynCycleM a = SynCycleM {
151 runSynCycleM :: SynCycleState -> Either (SrcSpan, SDoc) (a, SynCycleState) }
152
153 type SynCycleState = NameSet
154
155 instance Functor SynCycleM where
156 fmap = liftM
157
158 instance Applicative SynCycleM where
159 pure x = SynCycleM $ \state -> Right (x, state)
160 (<*>) = ap
161
162 instance Monad SynCycleM where
163 m >>= f = SynCycleM $ \state ->
164 case runSynCycleM m state of
165 Right (x, state') ->
166 runSynCycleM (f x) state'
167 Left err -> Left err
168
169 failSynCycleM :: SrcSpan -> SDoc -> SynCycleM ()
170 failSynCycleM loc err = SynCycleM $ \_ -> Left (loc, err)
171
172 -- | Test if a 'Name' is acyclic, short-circuiting if we've
173 -- seen it already.
174 checkNameIsAcyclic :: Name -> SynCycleM () -> SynCycleM ()
175 checkNameIsAcyclic n m = SynCycleM $ \s ->
176 if n `elemNameSet` s
177 then Right ((), s) -- short circuit
178 else case runSynCycleM m s of
179 Right ((), s') -> Right ((), extendNameSet s' n)
180 Left err -> Left err
181
182 -- | Checks if any of the passed in 'TyCon's have cycles.
183 -- Takes the 'UnitId' of the home package (as we can avoid
184 -- checking those TyCons: cycles never go through foreign packages) and
185 -- the corresponding @LTyClDecl Name@ for each 'TyCon', so we
186 -- can give better error messages.
187 checkSynCycles :: UnitId -> [TyCon] -> [LTyClDecl GhcRn] -> TcM ()
188 checkSynCycles this_uid tcs tyclds = do
189 case runSynCycleM (mapM_ (go emptyNameSet []) tcs) emptyNameSet of
190 Left (loc, err) -> setSrcSpan loc $ failWithTc err
191 Right _ -> return ()
192 where
193 -- Try our best to print the LTyClDecl for locally defined things
194 lcl_decls = mkNameEnv (zip (map tyConName tcs) tyclds)
195
196 -- Short circuit if we've already seen this Name and concluded
197 -- it was acyclic.
198 go :: NameSet -> [TyCon] -> TyCon -> SynCycleM ()
199 go so_far seen_tcs tc =
200 checkNameIsAcyclic (tyConName tc) $ go' so_far seen_tcs tc
201
202 -- Expand type synonyms, complaining if you find the same
203 -- type synonym a second time.
204 go' :: NameSet -> [TyCon] -> TyCon -> SynCycleM ()
205 go' so_far seen_tcs tc
206 | n `elemNameSet` so_far
207 = failSynCycleM (getSrcSpan (head seen_tcs)) $
208 sep [ text "Cycle in type synonym declarations:"
209 , nest 2 (vcat (map ppr_decl seen_tcs)) ]
210 -- Optimization: we don't allow cycles through external packages,
211 -- so once we find a non-local name we are guaranteed to not
212 -- have a cycle.
213 --
214 -- This won't hold once we get recursive packages with Backpack,
215 -- but for now it's fine.
216 | not (isHoleModule mod ||
217 moduleUnitId mod == this_uid ||
218 isInteractiveModule mod)
219 = return ()
220 | Just ty <- synTyConRhs_maybe tc =
221 go_ty (extendNameSet so_far (tyConName tc)) (tc:seen_tcs) ty
222 | otherwise = return ()
223 where
224 n = tyConName tc
225 mod = nameModule n
226 ppr_decl tc =
227 case lookupNameEnv lcl_decls n of
228 Just (dL->L loc decl) -> ppr loc <> colon <+> ppr decl
229 Nothing -> ppr (getSrcSpan n) <> colon <+> ppr n
230 <+> text "from external module"
231 where
232 n = tyConName tc
233
234 go_ty :: NameSet -> [TyCon] -> Type -> SynCycleM ()
235 go_ty so_far seen_tcs ty =
236 mapM_ (go so_far seen_tcs) (synonymTyConsOfType ty)
237
238 {- Note [Superclass cycle check]
239 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
240 The superclass cycle check for C decides if we can statically
241 guarantee that expanding C's superclass cycles transitively is
242 guaranteed to terminate. This is a Haskell98 requirement,
243 but one that we lift with -XUndecidableSuperClasses.
244
245 The worry is that a superclass cycle could make the type checker loop.
246 More precisely, with a constraint (Given or Wanted)
247 C ty1 .. tyn
248 one approach is to instantiate all of C's superclasses, transitively.
249 We can only do so if that set is finite.
250
251 This potential loop occurs only through superclasses. This, for
252 example, is fine
253 class C a where
254 op :: C b => a -> b -> b
255 even though C's full definition uses C.
256
257 Making the check static also makes it conservative. Eg
258 type family F a
259 class F a => C a
260 Here an instance of (F a) might mention C:
261 type instance F [a] = C a
262 and now we'd have a loop.
263
264 The static check works like this, starting with C
265 * Look at C's superclass predicates
266 * If any is a type-function application,
267 or is headed by a type variable, fail
268 * If any has C at the head, fail
269 * If any has a type class D at the head,
270 make the same test with D
271
272 A tricky point is: what if there is a type variable at the head?
273 Consider this:
274 class f (C f) => C f
275 class c => Id c
276 and now expand superclasses for constraint (C Id):
277 C Id
278 --> Id (C Id)
279 --> C Id
280 --> ....
281 Each step expands superclasses one layer, and clearly does not terminate.
282 -}
283
284 checkClassCycles :: Class -> Maybe SDoc
285 -- Nothing <=> ok
286 -- Just err <=> possible cycle error
287 checkClassCycles cls
288 = do { (definite_cycle, err) <- go (unitNameSet (getName cls))
289 cls (mkTyVarTys (classTyVars cls))
290 ; let herald | definite_cycle = text "Superclass cycle for"
291 | otherwise = text "Potential superclass cycle for"
292 ; return (vcat [ herald <+> quotes (ppr cls)
293 , nest 2 err, hint]) }
294 where
295 hint = text "Use UndecidableSuperClasses to accept this"
296
297 -- Expand superclasses starting with (C a b), complaining
298 -- if you find the same class a second time, or a type function
299 -- or predicate headed by a type variable
300 --
301 -- NB: this code duplicates TcType.transSuperClasses, but
302 -- with more error message generation clobber
303 -- Make sure the two stay in sync.
304 go :: NameSet -> Class -> [Type] -> Maybe (Bool, SDoc)
305 go so_far cls tys = firstJusts $
306 map (go_pred so_far) $
307 immSuperClasses cls tys
308
309 go_pred :: NameSet -> PredType -> Maybe (Bool, SDoc)
310 -- Nothing <=> ok
311 -- Just (True, err) <=> definite cycle
312 -- Just (False, err) <=> possible cycle
313 go_pred so_far pred -- NB: tcSplitTyConApp looks through synonyms
314 | Just (tc, tys) <- tcSplitTyConApp_maybe pred
315 = go_tc so_far pred tc tys
316 | hasTyVarHead pred
317 = Just (False, hang (text "one of whose superclass constraints is headed by a type variable:")
318 2 (quotes (ppr pred)))
319 | otherwise
320 = Nothing
321
322 go_tc :: NameSet -> PredType -> TyCon -> [Type] -> Maybe (Bool, SDoc)
323 go_tc so_far pred tc tys
324 | isFamilyTyCon tc
325 = Just (False, hang (text "one of whose superclass constraints is headed by a type family:")
326 2 (quotes (ppr pred)))
327 | Just cls <- tyConClass_maybe tc
328 = go_cls so_far cls tys
329 | otherwise -- Equality predicate, for example
330 = Nothing
331
332 go_cls :: NameSet -> Class -> [Type] -> Maybe (Bool, SDoc)
333 go_cls so_far cls tys
334 | cls_nm `elemNameSet` so_far
335 = Just (True, text "one of whose superclasses is" <+> quotes (ppr cls))
336 | isCTupleClass cls
337 = go so_far cls tys
338 | otherwise
339 = do { (b,err) <- go (so_far `extendNameSet` cls_nm) cls tys
340 ; return (b, text "one of whose superclasses is" <+> quotes (ppr cls)
341 $$ err) }
342 where
343 cls_nm = getName cls
344
345 {-
346 ************************************************************************
347 * *
348 Role inference
349 * *
350 ************************************************************************
351
352 Note [Role inference]
353 ~~~~~~~~~~~~~~~~~~~~~
354 The role inference algorithm datatype definitions to infer the roles on the
355 parameters. Although these roles are stored in the tycons, we can perform this
356 algorithm on the built tycons, as long as we don't peek at an as-yet-unknown
357 roles field! Ah, the magic of laziness.
358
359 First, we choose appropriate initial roles. For families and classes, roles
360 (including initial roles) are N. For datatypes, we start with the role in the
361 role annotation (if any), or otherwise use Phantom. This is done in
362 initialRoleEnv1.
363
364 The function irGroup then propagates role information until it reaches a
365 fixpoint, preferring N over (R or P) and R over P. To aid in this, we have a
366 monad RoleM, which is a combination reader and state monad. In its state are
367 the current RoleEnv, which gets updated by role propagation, and an update
368 bit, which we use to know whether or not we've reached the fixpoint. The
369 environment of RoleM contains the tycon whose parameters we are inferring, and
370 a VarEnv from parameters to their positions, so we can update the RoleEnv.
371 Between tycons, this reader information is missing; it is added by
372 addRoleInferenceInfo.
373
374 There are two kinds of tycons to consider: algebraic ones (excluding classes)
375 and type synonyms. (Remember, families don't participate -- all their parameters
376 are N.) An algebraic tycon processes each of its datacons, in turn. Note that
377 a datacon's universally quantified parameters might be different from the parent
378 tycon's parameters, so we use the datacon's univ parameters in the mapping from
379 vars to positions. Note also that we don't want to infer roles for existentials
380 (they're all at N, too), so we put them in the set of local variables. As an
381 optimisation, we skip any tycons whose roles are already all Nominal, as there
382 nowhere else for them to go. For synonyms, we just analyse their right-hand sides.
383
384 irType walks through a type, looking for uses of a variable of interest and
385 propagating role information. Because anything used under a phantom position
386 is at phantom and anything used under a nominal position is at nominal, the
387 irType function can assume that anything it sees is at representational. (The
388 other possibilities are pruned when they're encountered.)
389
390 The rest of the code is just plumbing.
391
392 How do we know that this algorithm is correct? It should meet the following
393 specification:
394
395 Let Z be a role context -- a mapping from variables to roles. The following
396 rules define the property (Z |- t : r), where t is a type and r is a role:
397
398 Z(a) = r' r' <= r
399 ------------------------- RCVar
400 Z |- a : r
401
402 ---------- RCConst
403 Z |- T : r -- T is a type constructor
404
405 Z |- t1 : r
406 Z |- t2 : N
407 -------------- RCApp
408 Z |- t1 t2 : r
409
410 forall i<=n. (r_i is R or N) implies Z |- t_i : r_i
411 roles(T) = r_1 .. r_n
412 ---------------------------------------------------- RCDApp
413 Z |- T t_1 .. t_n : R
414
415 Z, a:N |- t : r
416 ---------------------- RCAll
417 Z |- forall a:k.t : r
418
419
420 We also have the following rules:
421
422 For all datacon_i in type T, where a_1 .. a_n are universally quantified
423 and b_1 .. b_m are existentially quantified, and the arguments are t_1 .. t_p,
424 then if forall j<=p, a_1 : r_1 .. a_n : r_n, b_1 : N .. b_m : N |- t_j : R,
425 then roles(T) = r_1 .. r_n
426
427 roles(->) = R, R
428 roles(~#) = N, N
429
430 With -dcore-lint on, the output of this algorithm is checked in checkValidRoles,
431 called from checkValidTycon.
432
433 Note [Role-checking data constructor arguments]
434 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
435 Consider
436 data T a where
437 MkT :: Eq b => F a -> (a->a) -> T (G a)
438
439 Then we want to check the roles at which 'a' is used
440 in MkT's type. We want to work on the user-written type,
441 so we need to take into account
442 * the arguments: (F a) and (a->a)
443 * the context: C a b
444 * the result type: (G a) -- this is in the eq_spec
445
446
447 Note [Coercions in role inference]
448 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
449 Is (t |> co1) representationally equal to (t |> co2)? Of course they are! Changing
450 the kind of a type is totally irrelevant to the representation of that type. So,
451 we want to totally ignore coercions when doing role inference. This includes omitting
452 any type variables that appear in nominal positions but only within coercions.
453 -}
454
455 type RolesInfo = Name -> [Role]
456
457 type RoleEnv = NameEnv [Role] -- from tycon names to roles
458
459 -- This, and any of the functions it calls, must *not* look at the roles
460 -- field of a tycon we are inferring roles about!
461 -- See Note [Role inference]
462 inferRoles :: HscSource -> RoleAnnotEnv -> [TyCon] -> Name -> [Role]
463 inferRoles hsc_src annots tycons
464 = let role_env = initialRoleEnv hsc_src annots tycons
465 role_env' = irGroup role_env tycons in
466 \name -> case lookupNameEnv role_env' name of
467 Just roles -> roles
468 Nothing -> pprPanic "inferRoles" (ppr name)
469
470 initialRoleEnv :: HscSource -> RoleAnnotEnv -> [TyCon] -> RoleEnv
471 initialRoleEnv hsc_src annots = extendNameEnvList emptyNameEnv .
472 map (initialRoleEnv1 hsc_src annots)
473
474 initialRoleEnv1 :: HscSource -> RoleAnnotEnv -> TyCon -> (Name, [Role])
475 initialRoleEnv1 hsc_src annots_env tc
476 | isFamilyTyCon tc = (name, map (const Nominal) bndrs)
477 | isAlgTyCon tc = (name, default_roles)
478 | isTypeSynonymTyCon tc = (name, default_roles)
479 | otherwise = pprPanic "initialRoleEnv1" (ppr tc)
480 where name = tyConName tc
481 bndrs = tyConBinders tc
482 argflags = map tyConBinderArgFlag bndrs
483 num_exps = count isVisibleArgFlag argflags
484
485 -- if the number of annotations in the role annotation decl
486 -- is wrong, just ignore it. We check this in the validity check.
487 role_annots
488 = case lookupRoleAnnot annots_env name of
489 Just (dL->L _ (RoleAnnotDecl _ _ annots))
490 | annots `lengthIs` num_exps -> map unLoc annots
491 _ -> replicate num_exps Nothing
492 default_roles = build_default_roles argflags role_annots
493
494 build_default_roles (argf : argfs) (m_annot : ras)
495 | isVisibleArgFlag argf
496 = (m_annot `orElse` default_role) : build_default_roles argfs ras
497 build_default_roles (_argf : argfs) ras
498 = Nominal : build_default_roles argfs ras
499 build_default_roles [] [] = []
500 build_default_roles _ _ = pprPanic "initialRoleEnv1 (2)"
501 (vcat [ppr tc, ppr role_annots])
502
503 default_role
504 | isClassTyCon tc = Nominal
505 -- Note [Default roles for abstract TyCons in hs-boot/hsig]
506 | HsBootFile <- hsc_src
507 , isAbstractTyCon tc = Representational
508 | HsigFile <- hsc_src
509 , isAbstractTyCon tc = Nominal
510 | otherwise = Phantom
511
512 -- Note [Default roles for abstract TyCons in hs-boot/hsig]
513 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
514 -- What should the default role for an abstract TyCon be?
515 --
516 -- Originally, we inferred phantom role for abstract TyCons
517 -- in hs-boot files, because the type variables were never used.
518 --
519 -- This was silly, because the role of the abstract TyCon
520 -- was required to match the implementation, and the roles of
521 -- data types are almost never phantom. Thus, in ticket #9204,
522 -- the default was changed so be representational (the most common case). If
523 -- the implementing data type was actually nominal, you'd get an easy
524 -- to understand error, and add the role annotation yourself.
525 --
526 -- Then Backpack was added, and with it we added role *subtyping*
527 -- the matching judgment: if an abstract TyCon has a nominal
528 -- parameter, it's OK to implement it with a representational
529 -- parameter. But now, the representational default is not a good
530 -- one, because you should *only* request representational if
531 -- you're planning to do coercions. To be maximally flexible
532 -- with what data types you will accept, you want the default
533 -- for hsig files is nominal. We don't allow role subtyping
534 -- with hs-boot files (it's good practice to give an exactly
535 -- accurate role here, because any types that use the abstract
536 -- type will propagate the role information.)
537
538 irGroup :: RoleEnv -> [TyCon] -> RoleEnv
539 irGroup env tcs
540 = let (env', update) = runRoleM env $ mapM_ irTyCon tcs in
541 if update
542 then irGroup env' tcs
543 else env'
544
545 irTyCon :: TyCon -> RoleM ()
546 irTyCon tc
547 | isAlgTyCon tc
548 = do { old_roles <- lookupRoles tc
549 ; unless (all (== Nominal) old_roles) $ -- also catches data families,
550 -- which don't want or need role inference
551 irTcTyVars tc $
552 do { mapM_ (irType emptyVarSet) (tyConStupidTheta tc) -- See #8958
553 ; whenIsJust (tyConClass_maybe tc) irClass
554 ; mapM_ irDataCon (visibleDataCons $ algTyConRhs tc) }}
555
556 | Just ty <- synTyConRhs_maybe tc
557 = irTcTyVars tc $
558 irType emptyVarSet ty
559
560 | otherwise
561 = return ()
562
563 -- any type variable used in an associated type must be Nominal
564 irClass :: Class -> RoleM ()
565 irClass cls
566 = mapM_ ir_at (classATs cls)
567 where
568 cls_tvs = classTyVars cls
569 cls_tv_set = mkVarSet cls_tvs
570
571 ir_at at_tc
572 = mapM_ (updateRole Nominal) nvars
573 where nvars = filter (`elemVarSet` cls_tv_set) $ tyConTyVars at_tc
574
575 -- See Note [Role inference]
576 irDataCon :: DataCon -> RoleM ()
577 irDataCon datacon
578 = setRoleInferenceVars univ_tvs $
579 irExTyVars ex_tvs $ \ ex_var_set ->
580 mapM_ (irType ex_var_set)
581 (map tyVarKind ex_tvs ++ eqSpecPreds eq_spec ++ theta ++ arg_tys)
582 -- See Note [Role-checking data constructor arguments]
583 where
584 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
585 = dataConFullSig datacon
586
587 irType :: VarSet -> Type -> RoleM ()
588 irType = go
589 where
590 go lcls ty | Just ty' <- coreView ty -- #14101
591 = go lcls ty'
592 go lcls (TyVarTy tv) = unless (tv `elemVarSet` lcls) $
593 updateRole Representational tv
594 go lcls (AppTy t1 t2) = go lcls t1 >> markNominal lcls t2
595 go lcls (TyConApp tc tys) = do { roles <- lookupRolesX tc
596 ; zipWithM_ (go_app lcls) roles tys }
597 go lcls (ForAllTy tvb ty) = do { let tv = binderVar tvb
598 lcls' = extendVarSet lcls tv
599 ; markNominal lcls (tyVarKind tv)
600 ; go lcls' ty }
601 go lcls (FunTy arg res) = go lcls arg >> go lcls res
602 go _ (LitTy {}) = return ()
603 -- See Note [Coercions in role inference]
604 go lcls (CastTy ty _) = go lcls ty
605 go _ (CoercionTy _) = return ()
606
607 go_app _ Phantom _ = return () -- nothing to do here
608 go_app lcls Nominal ty = markNominal lcls ty -- all vars below here are N
609 go_app lcls Representational ty = go lcls ty
610
611 irTcTyVars :: TyCon -> RoleM a -> RoleM a
612 irTcTyVars tc thing
613 = setRoleInferenceTc (tyConName tc) $ go (tyConTyVars tc)
614 where
615 go [] = thing
616 go (tv:tvs) = do { markNominal emptyVarSet (tyVarKind tv)
617 ; addRoleInferenceVar tv $ go tvs }
618
619 irExTyVars :: [TyVar] -> (TyVarSet -> RoleM a) -> RoleM a
620 irExTyVars orig_tvs thing = go emptyVarSet orig_tvs
621 where
622 go lcls [] = thing lcls
623 go lcls (tv:tvs) = do { markNominal lcls (tyVarKind tv)
624 ; go (extendVarSet lcls tv) tvs }
625
626 markNominal :: TyVarSet -- local variables
627 -> Type -> RoleM ()
628 markNominal lcls ty = let nvars = fvVarList (FV.delFVs lcls $ get_ty_vars ty) in
629 mapM_ (updateRole Nominal) nvars
630 where
631 -- get_ty_vars gets all the tyvars (no covars!) from a type *without*
632 -- recurring into coercions. Recall: coercions are totally ignored during
633 -- role inference. See [Coercions in role inference]
634 get_ty_vars :: Type -> FV
635 get_ty_vars (TyVarTy tv) = unitFV tv
636 get_ty_vars (AppTy t1 t2) = get_ty_vars t1 `unionFV` get_ty_vars t2
637 get_ty_vars (FunTy t1 t2) = get_ty_vars t1 `unionFV` get_ty_vars t2
638 get_ty_vars (TyConApp _ tys) = mapUnionFV get_ty_vars tys
639 get_ty_vars (ForAllTy tvb ty) = tyCoFVsBndr tvb (get_ty_vars ty)
640 get_ty_vars (LitTy {}) = emptyFV
641 get_ty_vars (CastTy ty _) = get_ty_vars ty
642 get_ty_vars (CoercionTy _) = emptyFV
643
644 -- like lookupRoles, but with Nominal tags at the end for oversaturated TyConApps
645 lookupRolesX :: TyCon -> RoleM [Role]
646 lookupRolesX tc
647 = do { roles <- lookupRoles tc
648 ; return $ roles ++ repeat Nominal }
649
650 -- gets the roles either from the environment or the tycon
651 lookupRoles :: TyCon -> RoleM [Role]
652 lookupRoles tc
653 = do { env <- getRoleEnv
654 ; case lookupNameEnv env (tyConName tc) of
655 Just roles -> return roles
656 Nothing -> return $ tyConRoles tc }
657
658 -- tries to update a role; won't ever update a role "downwards"
659 updateRole :: Role -> TyVar -> RoleM ()
660 updateRole role tv
661 = do { var_ns <- getVarNs
662 ; name <- getTyConName
663 ; case lookupVarEnv var_ns tv of
664 Nothing -> pprPanic "updateRole" (ppr name $$ ppr tv $$ ppr var_ns)
665 Just n -> updateRoleEnv name n role }
666
667 -- the state in the RoleM monad
668 data RoleInferenceState = RIS { role_env :: RoleEnv
669 , update :: Bool }
670
671 -- the environment in the RoleM monad
672 type VarPositions = VarEnv Int
673
674 -- See [Role inference]
675 newtype RoleM a = RM { unRM :: Maybe Name -- of the tycon
676 -> VarPositions
677 -> Int -- size of VarPositions
678 -> RoleInferenceState
679 -> (a, RoleInferenceState) }
680
681 instance Functor RoleM where
682 fmap = liftM
683
684 instance Applicative RoleM where
685 pure x = RM $ \_ _ _ state -> (x, state)
686 (<*>) = ap
687
688 instance Monad RoleM where
689 a >>= f = RM $ \m_info vps nvps state ->
690 let (a', state') = unRM a m_info vps nvps state in
691 unRM (f a') m_info vps nvps state'
692
693 runRoleM :: RoleEnv -> RoleM () -> (RoleEnv, Bool)
694 runRoleM env thing = (env', update)
695 where RIS { role_env = env', update = update }
696 = snd $ unRM thing Nothing emptyVarEnv 0 state
697 state = RIS { role_env = env
698 , update = False }
699
700 setRoleInferenceTc :: Name -> RoleM a -> RoleM a
701 setRoleInferenceTc name thing = RM $ \m_name vps nvps state ->
702 ASSERT( isNothing m_name )
703 ASSERT( isEmptyVarEnv vps )
704 ASSERT( nvps == 0 )
705 unRM thing (Just name) vps nvps state
706
707 addRoleInferenceVar :: TyVar -> RoleM a -> RoleM a
708 addRoleInferenceVar tv thing
709 = RM $ \m_name vps nvps state ->
710 ASSERT( isJust m_name )
711 unRM thing m_name (extendVarEnv vps tv nvps) (nvps+1) state
712
713 setRoleInferenceVars :: [TyVar] -> RoleM a -> RoleM a
714 setRoleInferenceVars tvs thing
715 = RM $ \m_name _vps _nvps state ->
716 ASSERT( isJust m_name )
717 unRM thing m_name (mkVarEnv (zip tvs [0..])) (panic "setRoleInferenceVars")
718 state
719
720 getRoleEnv :: RoleM RoleEnv
721 getRoleEnv = RM $ \_ _ _ state@(RIS { role_env = env }) -> (env, state)
722
723 getVarNs :: RoleM VarPositions
724 getVarNs = RM $ \_ vps _ state -> (vps, state)
725
726 getTyConName :: RoleM Name
727 getTyConName = RM $ \m_name _ _ state ->
728 case m_name of
729 Nothing -> panic "getTyConName"
730 Just name -> (name, state)
731
732 updateRoleEnv :: Name -> Int -> Role -> RoleM ()
733 updateRoleEnv name n role
734 = RM $ \_ _ _ state@(RIS { role_env = role_env }) -> ((),
735 case lookupNameEnv role_env name of
736 Nothing -> pprPanic "updateRoleEnv" (ppr name)
737 Just roles -> let (before, old_role : after) = splitAt n roles in
738 if role `ltRole` old_role
739 then let roles' = before ++ role : after
740 role_env' = extendNameEnv role_env name roles' in
741 RIS { role_env = role_env', update = True }
742 else state )
743
744
745 {- *********************************************************************
746 * *
747 Building implicits
748 * *
749 ********************************************************************* -}
750
751 addTyConsToGblEnv :: [TyCon] -> TcM TcGblEnv
752 -- Given a [TyCon], add to the TcGblEnv
753 -- * extend the TypeEnv with the tycons
754 -- * extend the TypeEnv with their implicitTyThings
755 -- * extend the TypeEnv with any default method Ids
756 -- * add bindings for record selectors
757 addTyConsToGblEnv tyclss
758 = tcExtendTyConEnv tyclss $
759 tcExtendGlobalEnvImplicit implicit_things $
760 tcExtendGlobalValEnv def_meth_ids $
761 do { traceTc "tcAddTyCons" $ vcat
762 [ text "tycons" <+> ppr tyclss
763 , text "implicits" <+> ppr implicit_things ]
764 ; gbl_env <- tcRecSelBinds (mkRecSelBinds tyclss)
765 ; return gbl_env }
766 where
767 implicit_things = concatMap implicitTyConThings tyclss
768 def_meth_ids = mkDefaultMethodIds tyclss
769
770 mkDefaultMethodIds :: [TyCon] -> [Id]
771 -- We want to put the default-method Ids (both vanilla and generic)
772 -- into the type environment so that they are found when we typecheck
773 -- the filled-in default methods of each instance declaration
774 -- See Note [Default method Ids and Template Haskell]
775 mkDefaultMethodIds tycons
776 = [ mkExportedVanillaId dm_name (mkDefaultMethodType cls sel_id dm_spec)
777 | tc <- tycons
778 , Just cls <- [tyConClass_maybe tc]
779 , (sel_id, Just (dm_name, dm_spec)) <- classOpItems cls ]
780
781 mkDefaultMethodType :: Class -> Id -> DefMethSpec Type -> Type
782 -- Returns the top-level type of the default method
783 mkDefaultMethodType _ sel_id VanillaDM = idType sel_id
784 mkDefaultMethodType cls _ (GenericDM dm_ty) = mkSigmaTy tv_bndrs [pred] dm_ty
785 where
786 pred = mkClassPred cls (mkTyVarTys (binderVars cls_bndrs))
787 cls_bndrs = tyConBinders (classTyCon cls)
788 tv_bndrs = tyConTyVarBinders cls_bndrs
789 -- NB: the Class doesn't have TyConBinders; we reach into its
790 -- TyCon to get those. We /do/ need the TyConBinders because
791 -- we need the correct visibility: these default methods are
792 -- used in code generated by the fill-in for missing
793 -- methods in instances (TcInstDcls.mkDefMethBind), and
794 -- then typechecked. So we need the right visibilty info
795 -- (Trac #13998)
796
797 {-
798 ************************************************************************
799 * *
800 Building record selectors
801 * *
802 ************************************************************************
803 -}
804
805 {-
806 Note [Default method Ids and Template Haskell]
807 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
808 Consider this (Trac #4169):
809 class Numeric a where
810 fromIntegerNum :: a
811 fromIntegerNum = ...
812
813 ast :: Q [Dec]
814 ast = [d| instance Numeric Int |]
815
816 When we typecheck 'ast' we have done the first pass over the class decl
817 (in tcTyClDecls), but we have not yet typechecked the default-method
818 declarations (because they can mention value declarations). So we
819 must bring the default method Ids into scope first (so they can be seen
820 when typechecking the [d| .. |] quote, and typecheck them later.
821 -}
822
823 {-
824 ************************************************************************
825 * *
826 Building record selectors
827 * *
828 ************************************************************************
829 -}
830
831 tcRecSelBinds :: [(Id, LHsBind GhcRn)] -> TcM TcGblEnv
832 tcRecSelBinds sel_bind_prs
833 = tcExtendGlobalValEnv [sel_id | (dL->L _ (IdSig _ sel_id)) <- sigs] $
834 do { (rec_sel_binds, tcg_env) <- discardWarnings $
835 tcValBinds TopLevel binds sigs getGblEnv
836 ; return (tcg_env `addTypecheckedBinds` map snd rec_sel_binds) }
837 where
838 sigs = [ cL loc (IdSig noExt sel_id) | (sel_id, _) <- sel_bind_prs
839 , let loc = getSrcSpan sel_id ]
840 binds = [(NonRecursive, unitBag bind) | (_, bind) <- sel_bind_prs]
841
842 mkRecSelBinds :: [TyCon] -> [(Id, LHsBind GhcRn)]
843 -- NB We produce *un-typechecked* bindings, rather like 'deriving'
844 -- This makes life easier, because the later type checking will add
845 -- all necessary type abstractions and applications
846 mkRecSelBinds tycons
847 = map mkRecSelBind [ (tc,fld) | tc <- tycons
848 , fld <- tyConFieldLabels tc ]
849
850 mkRecSelBind :: (TyCon, FieldLabel) -> (Id, LHsBind GhcRn)
851 mkRecSelBind (tycon, fl)
852 = mkOneRecordSelector all_cons (RecSelData tycon) fl
853 where
854 all_cons = map RealDataCon (tyConDataCons tycon)
855
856 mkOneRecordSelector :: [ConLike] -> RecSelParent -> FieldLabel
857 -> (Id, LHsBind GhcRn)
858 mkOneRecordSelector all_cons idDetails fl
859 = (sel_id, cL loc sel_bind)
860 where
861 loc = getSrcSpan sel_name
862 lbl = flLabel fl
863 sel_name = flSelector fl
864
865 sel_id = mkExportedLocalId rec_details sel_name sel_ty
866 rec_details = RecSelId { sel_tycon = idDetails, sel_naughty = is_naughty }
867
868 -- Find a representative constructor, con1
869 cons_w_field = conLikesWithFields all_cons [lbl]
870 con1 = ASSERT( not (null cons_w_field) ) head cons_w_field
871
872 -- Selector type; Note [Polymorphic selectors]
873 field_ty = conLikeFieldType con1 lbl
874 data_tvs = tyCoVarsOfTypesWellScoped inst_tys
875 data_tv_set= mkVarSet data_tvs
876 is_naughty = not (tyCoVarsOfType field_ty `subVarSet` data_tv_set)
877 (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
878 sel_ty | is_naughty = unitTy -- See Note [Naughty record selectors]
879 | otherwise = mkSpecForAllTys data_tvs $
880 mkPhiTy (conLikeStupidTheta con1) $ -- Urgh!
881 mkFunTy data_ty $
882 mkSpecForAllTys field_tvs $
883 mkPhiTy field_theta $
884 -- req_theta is empty for normal DataCon
885 mkPhiTy req_theta $
886 field_tau
887
888 -- Make the binding: sel (C2 { fld = x }) = x
889 -- sel (C7 { fld = x }) = x
890 -- where cons_w_field = [C2,C7]
891 sel_bind = mkTopFunBind Generated sel_lname alts
892 where
893 alts | is_naughty = [mkSimpleMatch (mkPrefixFunRhs sel_lname)
894 [] unit_rhs]
895 | otherwise = map mk_match cons_w_field ++ deflt
896 mk_match con = mkSimpleMatch (mkPrefixFunRhs sel_lname)
897 [cL loc (mk_sel_pat con)]
898 (cL loc (HsVar noExt (cL loc field_var)))
899 mk_sel_pat con = ConPatIn (cL loc (getName con)) (RecCon rec_fields)
900 rec_fields = HsRecFields { rec_flds = [rec_field], rec_dotdot = Nothing }
901 rec_field = noLoc (HsRecField
902 { hsRecFieldLbl
903 = cL loc (FieldOcc sel_name
904 (cL loc $ mkVarUnqual lbl))
905 , hsRecFieldArg
906 = cL loc (VarPat noExt (cL loc field_var))
907 , hsRecPun = False })
908 sel_lname = cL loc sel_name
909 field_var = mkInternalName (mkBuiltinUnique 1) (getOccName sel_name) loc
910
911 -- Add catch-all default case unless the case is exhaustive
912 -- We do this explicitly so that we get a nice error message that
913 -- mentions this particular record selector
914 deflt | all dealt_with all_cons = []
915 | otherwise = [mkSimpleMatch CaseAlt
916 [cL loc (WildPat noExt)]
917 (mkHsApp (cL loc (HsVar noExt
918 (cL loc (getName rEC_SEL_ERROR_ID))))
919 (cL loc (HsLit noExt msg_lit)))]
920
921 -- Do not add a default case unless there are unmatched
922 -- constructors. We must take account of GADTs, else we
923 -- get overlap warning messages from the pattern-match checker
924 -- NB: we need to pass type args for the *representation* TyCon
925 -- to dataConCannotMatch, hence the calculation of inst_tys
926 -- This matters in data families
927 -- data instance T Int a where
928 -- A :: { fld :: Int } -> T Int Bool
929 -- B :: { fld :: Int } -> T Int Char
930 dealt_with :: ConLike -> Bool
931 dealt_with (PatSynCon _) = False -- We can't predict overlap
932 dealt_with con@(RealDataCon dc) =
933 con `elem` cons_w_field || dataConCannotMatch inst_tys dc
934
935 (univ_tvs, _, eq_spec, _, req_theta, _, data_ty) = conLikeFullSig con1
936
937 eq_subst = mkTvSubstPrs (map eqSpecPair eq_spec)
938 inst_tys = substTyVars eq_subst univ_tvs
939
940 unit_rhs = mkLHsTupleExpr []
941 msg_lit = HsStringPrim NoSourceText (fastStringToByteString lbl)
942
943 {-
944 Note [Polymorphic selectors]
945 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
946 We take care to build the type of a polymorphic selector in the right
947 order, so that visible type application works.
948
949 data Ord a => T a = MkT { field :: forall b. (Num a, Show b) => (a, b) }
950
951 We want
952
953 field :: forall a. Ord a => T a -> forall b. (Num a, Show b) => (a, b)
954
955 Note [Naughty record selectors]
956 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
957 A "naughty" field is one for which we can't define a record
958 selector, because an existential type variable would escape. For example:
959 data T = forall a. MkT { x,y::a }
960 We obviously can't define
961 x (MkT v _) = v
962 Nevertheless we *do* put a RecSelId into the type environment
963 so that if the user tries to use 'x' as a selector we can bleat
964 helpfully, rather than saying unhelpfully that 'x' is not in scope.
965 Hence the sel_naughty flag, to identify record selectors that don't really exist.
966
967 In general, a field is "naughty" if its type mentions a type variable that
968 isn't in the result type of the constructor. Note that this *allows*
969 GADT record selectors (Note [GADT record selectors]) whose types may look
970 like sel :: T [a] -> a
971
972 For naughty selectors we make a dummy binding
973 sel = ()
974 so that the later type-check will add them to the environment, and they'll be
975 exported. The function is never called, because the typechecker spots the
976 sel_naughty field.
977
978 Note [GADT record selectors]
979 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
980 For GADTs, we require that all constructors with a common field 'f' have the same
981 result type (modulo alpha conversion). [Checked in TcTyClsDecls.checkValidTyCon]
982 E.g.
983 data T where
984 T1 { f :: Maybe a } :: T [a]
985 T2 { f :: Maybe a, y :: b } :: T [a]
986 T3 :: T Int
987
988 and now the selector takes that result type as its argument:
989 f :: forall a. T [a] -> Maybe a
990
991 Details: the "real" types of T1,T2 are:
992 T1 :: forall r a. (r~[a]) => a -> T r
993 T2 :: forall r a b. (r~[a]) => a -> b -> T r
994
995 So the selector loooks like this:
996 f :: forall a. T [a] -> Maybe a
997 f (a:*) (t:T [a])
998 = case t of
999 T1 c (g:[a]~[c]) (v:Maybe c) -> v `cast` Maybe (right (sym g))
1000 T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
1001 T3 -> error "T3 does not have field f"
1002
1003 Note the forall'd tyvars of the selector are just the free tyvars
1004 of the result type; there may be other tyvars in the constructor's
1005 type (e.g. 'b' in T2).
1006
1007 Note the need for casts in the result!
1008
1009 Note [Selector running example]
1010 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1011 It's OK to combine GADTs and type families. Here's a running example:
1012
1013 data instance T [a] where
1014 T1 { fld :: b } :: T [Maybe b]
1015
1016 The representation type looks like this
1017 data :R7T a where
1018 T1 { fld :: b } :: :R7T (Maybe b)
1019
1020 and there's coercion from the family type to the representation type
1021 :CoR7T a :: T [a] ~ :R7T a
1022
1023 The selector we want for fld looks like this:
1024
1025 fld :: forall b. T [Maybe b] -> b
1026 fld = /\b. \(d::T [Maybe b]).
1027 case d `cast` :CoR7T (Maybe b) of
1028 T1 (x::b) -> x
1029
1030 The scrutinee of the case has type :R7T (Maybe b), which can be
1031 gotten by appying the eq_spec to the univ_tvs of the data con.
1032
1033 -}