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