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