More tc-tracing
[ghc.git] / compiler / typecheck / TcTyClsDecls.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The AQUA Project, Glasgow University, 1996-1998
4
5
6 TcTyClsDecls: Typecheck type and class declarations
7 -}
8
9 {-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
10 {-# LANGUAGE TypeFamilies #-}
11
12 module TcTyClsDecls (
13 tcTyAndClassDecls,
14
15 -- Functions used by TcInstDcls to check
16 -- data/type family instance declarations
17 kcDataDefn, tcConDecls, dataDeclChecks, checkValidTyCon,
18 tcFamTyPats, tcTyFamInstEqn,
19 tcAddTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt,
20 wrongKindOfFamily, dataConCtxt
21 ) where
22
23 #include "HsVersions.h"
24
25 import GhcPrelude
26
27 import HsSyn
28 import HscTypes
29 import BuildTyCl
30 import TcRnMonad
31 import TcEnv
32 import TcValidity
33 import TcHsSyn
34 import TcTyDecls
35 import TcClassDcl
36 import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
37 import TcDeriv (DerivInfo)
38 import TcEvidence ( tcCoercionKind, isEmptyTcEvBinds )
39 import TcUnify ( checkConstraints )
40 import TcHsType
41 import TcMType
42 import TysWiredIn ( unitTy )
43 import TcType
44 import RnEnv( lookupConstructorFields )
45 import FamInst
46 import FamInstEnv
47 import Coercion
48 import Type
49 import TyCoRep -- for checkValidRoles
50 import Kind
51 import Class
52 import CoAxiom
53 import TyCon
54 import DataCon
55 import Id
56 import Var
57 import VarEnv
58 import VarSet
59 import Module
60 import Name
61 import NameSet
62 import NameEnv
63 import Outputable
64 import Maybes
65 import Unify
66 import Util
67 import Pair
68 import SrcLoc
69 import ListSetOps
70 import DynFlags
71 import Unique
72 import ConLike( ConLike(..) )
73 import BasicTypes
74 import qualified GHC.LanguageExtensions as LangExt
75
76 import Control.Monad
77 import Data.List
78 import Data.List.NonEmpty ( NonEmpty(..) )
79
80 {-
81 ************************************************************************
82 * *
83 \subsection{Type checking for type and class declarations}
84 * *
85 ************************************************************************
86
87 Note [Grouping of type and class declarations]
88 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
89 tcTyAndClassDecls is called on a list of `TyClGroup`s. Each group is a strongly
90 connected component of mutually dependent types and classes. We kind check and
91 type check each group separately to enhance kind polymorphism. Take the
92 following example:
93
94 type Id a = a
95 data X = X (Id Int)
96
97 If we were to kind check the two declarations together, we would give Id the
98 kind * -> *, since we apply it to an Int in the definition of X. But we can do
99 better than that, since Id really is kind polymorphic, and should get kind
100 forall (k::*). k -> k. Since it does not depend on anything else, it can be
101 kind-checked by itself, hence getting the most general kind. We then kind check
102 X, which works fine because we then know the polymorphic kind of Id, and simply
103 instantiate k to *.
104
105 Note [Check role annotations in a second pass]
106 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
107 Role inference potentially depends on the types of all of the datacons declared
108 in a mutually recursive group. The validity of a role annotation, in turn,
109 depends on the result of role inference. Because the types of datacons might
110 be ill-formed (see #7175 and Note [Checking GADT return types]) we must check
111 *all* the tycons in a group for validity before checking *any* of the roles.
112 Thus, we take two passes over the resulting tycons, first checking for general
113 validity and then checking for valid role annotations.
114 -}
115
116 tcTyAndClassDecls :: [TyClGroup GhcRn] -- Mutually-recursive groups in
117 -- dependency order
118 -> TcM ( TcGblEnv -- Input env extended by types and
119 -- classes
120 -- and their implicit Ids,DataCons
121 , [InstInfo GhcRn] -- Source-code instance decls info
122 , [DerivInfo] -- data family deriving info
123 )
124 -- Fails if there are any errors
125 tcTyAndClassDecls tyclds_s
126 -- The code recovers internally, but if anything gave rise to
127 -- an error we'd better stop now, to avoid a cascade
128 -- Type check each group in dependency order folding the global env
129 = checkNoErrs $ fold_env [] [] tyclds_s
130 where
131 fold_env :: [InstInfo GhcRn]
132 -> [DerivInfo]
133 -> [TyClGroup GhcRn]
134 -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
135 fold_env inst_info deriv_info []
136 = do { gbl_env <- getGblEnv
137 ; return (gbl_env, inst_info, deriv_info) }
138 fold_env inst_info deriv_info (tyclds:tyclds_s)
139 = do { (tcg_env, inst_info', deriv_info') <- tcTyClGroup tyclds
140 ; setGblEnv tcg_env $
141 -- remaining groups are typechecked in the extended global env.
142 fold_env (inst_info' ++ inst_info)
143 (deriv_info' ++ deriv_info)
144 tyclds_s }
145
146 tcTyClGroup :: TyClGroup GhcRn
147 -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
148 -- Typecheck one strongly-connected component of type, class, and instance decls
149 -- See Note [TyClGroups and dependency analysis] in HsDecls
150 tcTyClGroup (TyClGroup { group_tyclds = tyclds
151 , group_roles = roles
152 , group_instds = instds })
153 = do { let role_annots = mkRoleAnnotEnv roles
154
155 -- Step 1: Typecheck the type/class declarations
156 ; traceTc "---- tcTyClGroup ---- {" empty
157 ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds))
158 ; tyclss <- tcTyClDecls tyclds role_annots
159
160 -- Step 1.5: Make sure we don't have any type synonym cycles
161 ; traceTc "Starting synonym cycle check" (ppr tyclss)
162 ; this_uid <- fmap thisPackage getDynFlags
163 ; checkSynCycles this_uid tyclss tyclds
164 ; traceTc "Done synonym cycle check" (ppr tyclss)
165
166 -- Step 2: Perform the validity check on those types/classes
167 -- We can do this now because we are done with the recursive knot
168 -- Do it before Step 3 (adding implicit things) because the latter
169 -- expects well-formed TyCons
170 ; traceTc "Starting validity check" (ppr tyclss)
171 ; tyclss <- concatMapM checkValidTyCl tyclss
172 ; traceTc "Done validity check" (ppr tyclss)
173 ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
174 -- See Note [Check role annotations in a second pass]
175
176 ; traceTc "---- end tcTyClGroup ---- }" empty
177
178 -- Step 3: Add the implicit things;
179 -- we want them in the environment because
180 -- they may be mentioned in interface files
181 ; gbl_env <- addTyConsToGblEnv tyclss
182
183 -- Step 4: check instance declarations
184 ; setGblEnv gbl_env $
185 tcInstDecls1 instds }
186
187 tcTyClGroup (XTyClGroup _) = panic "tcTyClGroup"
188
189 tcTyClDecls :: [LTyClDecl GhcRn] -> RoleAnnotEnv -> TcM [TyCon]
190 tcTyClDecls tyclds role_annots
191 = tcExtendKindEnv promotion_err_env $ --- See Note [Type environment evolution]
192 do { -- Step 1: kind-check this group and returns the final
193 -- (possibly-polymorphic) kind of each TyCon and Class
194 -- See Note [Kind checking for type and class decls]
195 tc_tycons <- kcTyClGroup tyclds
196 ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
197
198 -- Step 2: type-check all groups together, returning
199 -- the final TyCons and Classes
200 --
201 -- NB: We have to be careful here to NOT eagerly unfold
202 -- type synonyms, as we have not tested for type synonym
203 -- loops yet and could fall into a black hole.
204 ; fixM $ \ ~rec_tyclss -> do
205 { tcg_env <- getGblEnv
206 ; let roles = inferRoles (tcg_src tcg_env) role_annots rec_tyclss
207
208 -- Populate environment with knot-tied ATyCon for TyCons
209 -- NB: if the decls mention any ill-staged data cons
210 -- (see Note [Recursion and promoting data constructors])
211 -- we will have failed already in kcTyClGroup, so no worries here
212 ; tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $
213
214 -- Also extend the local type envt with bindings giving
215 -- the (polymorphic) kind of each knot-tied TyCon or Class
216 -- See Note [Type checking recursive type and class declarations]
217 -- and Note [Type environment evolution]
218 tcExtendKindEnvWithTyCons tc_tycons $
219
220 -- Kind and type check declarations for this group
221 mapM (tcTyClDecl roles) tyclds
222 } }
223 where
224 promotion_err_env = mkPromotionErrorEnv tyclds
225 ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
226 , ppr (tyConBinders tc) <> comma
227 , ppr (tyConResKind tc) ])
228
229 zipRecTyClss :: [TcTyCon]
230 -> [TyCon] -- Knot-tied
231 -> [(Name,TyThing)]
232 -- Build a name-TyThing mapping for the TyCons bound by decls
233 -- being careful not to look at the knot-tied [TyThing]
234 -- The TyThings in the result list must have a visible ATyCon,
235 -- because typechecking types (in, say, tcTyClDecl) looks at
236 -- this outer constructor
237 zipRecTyClss tc_tycons rec_tycons
238 = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ]
239 where
240 rec_tc_env :: NameEnv TyCon
241 rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
242
243 add_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
244 add_tc tc env = foldr add_one_tc env (tc : tyConATs tc)
245
246 add_one_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
247 add_one_tc tc env = extendNameEnv env (tyConName tc) tc
248
249 get name = case lookupNameEnv rec_tc_env name of
250 Just tc -> tc
251 other -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
252
253 {-
254 ************************************************************************
255 * *
256 Kind checking
257 * *
258 ************************************************************************
259
260 Note [Kind checking for type and class decls]
261 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
262 Kind checking is done thus:
263
264 1. Make up a kind variable for each parameter of the declarations,
265 and extend the kind environment (which is in the TcLclEnv)
266
267 2. Kind check the declarations
268
269 We need to kind check all types in the mutually recursive group
270 before we know the kind of the type variables. For example:
271
272 class C a where
273 op :: D b => a -> b -> b
274
275 class D c where
276 bop :: (Monad c) => ...
277
278 Here, the kind of the locally-polymorphic type variable "b"
279 depends on *all the uses of class D*. For example, the use of
280 Monad c in bop's type signature means that D must have kind Type->Type.
281
282 Note: we don't treat type synonyms specially (we used to, in the past);
283 in particular, even if we have a type synonym cycle, we still kind check
284 it normally, and test for cycles later (checkSynCycles). The reason
285 we can get away with this is because we have more systematic TYPE r
286 inference, which means that we can do unification between kinds that
287 aren't lifted (this historically was not true.)
288
289 The downside of not directly reading off the kinds off the RHS of
290 type synonyms in topological order is that we don't transparently
291 support making synonyms of types with higher-rank kinds. But
292 you can always specify a CUSK directly to make this work out.
293 See tc269 for an example.
294
295 Note [Skip decls with CUSKs in kcLTyClDecl]
296 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
297 Consider
298
299 data T (a :: *) = MkT (S a) -- Has CUSK
300 data S a = MkS (T Int) (S a) -- No CUSK
301
302 Via getInitialKinds we get
303 T :: * -> *
304 S :: kappa -> *
305
306 Then we call kcTyClDecl on each decl in the group, to constrain the
307 kind unification variables. BUT we /skip/ the RHS of any decl with
308 a CUSK. Here we skip the RHS of T, so we eventually get
309 S :: forall k. k -> *
310
311 This gets us more polymorphism than we would otherwise get, similar
312 (but implemented strangely differently from) the treatment of type
313 signatures in value declarations.
314
315 Open type families
316 ~~~~~~~~~~~~~~~~~~
317 This treatment of type synonyms only applies to Haskell 98-style synonyms.
318 General type functions can be recursive, and hence, appear in `alg_decls'.
319
320 The kind of an open type family is solely determinded by its kind signature;
321 hence, only kind signatures participate in the construction of the initial
322 kind environment (as constructed by `getInitialKind'). In fact, we ignore
323 instances of families altogether in the following. However, we need to include
324 the kinds of *associated* families into the construction of the initial kind
325 environment. (This is handled by `allDecls').
326
327 See also Note [Kind checking recursive type and class declarations]
328
329 Note [How TcTyCons work]
330 ~~~~~~~~~~~~~~~~~~~~~~~~
331 TcTyCons are used for two distinct purposes
332
333 1. When recovering from a type error in a type declaration,
334 we want to put the erroneous TyCon in the environment in a
335 way that won't lead to more errors. We use a TcTyCon for this;
336 see makeRecoveryTyCon.
337
338 2. When checking a type/class declaration (in module TcTyClsDecls), we come
339 upon knowledge of the eventual tycon in bits and pieces.
340
341 S1) First, we use getInitialKinds to look over the user-provided
342 kind signature of a tycon (including, for example, the number
343 of parameters written to the tycon) to get an initial shape of
344 the tycon's kind. We record that shape in a TcTyCon.
345
346 S2) Then, using these initial kinds, we kind-check the body of the
347 tycon (class methods, data constructors, etc.), filling in the
348 metavariables in the tycon's initial kind.
349
350 S3) We then generalize to get the tycon's final, fixed
351 kind. Finally, once this has happened for all tycons in a
352 mutually recursive group, we can desugar the lot.
353
354 For convenience, we store partially-known tycons in TcTyCons, which
355 might store meta-variables. These TcTyCons are stored in the local
356 environment in TcTyClsDecls, until the real full TyCons can be created
357 during desugaring. A desugared program should never have a TcTyCon.
358
359 A challenging piece in all of this is that we end up taking three separate
360 passes over every declaration:
361 - one in getInitialKind (this pass look only at the head, not the body)
362 - one in kcTyClDecls (to kind-check the body)
363 - a final one in tcTyClDecls (to desugar)
364 In the latter two passes, we need to connect the user-written type
365 variables in an LHsQTyVars with the variables in the tycon's
366 inferred kind. Because the tycon might not have a CUSK, this
367 matching up is, in general, quite hard to do. (Look through the
368 git history between Dec 2015 and Apr 2016 for
369 TcHsType.splitTelescopeTvs!) Instead of trying, we just store the
370 list of type variables to bring into scope, in the
371 tyConScopedTyVars field of the TcTyCon. These tyvars are brought
372 into scope in kcTyClTyVars and tcTyClTyVars, both in TcHsType.
373
374 In a TcTyCon, everything is zonked after the kind-checking pass (S2).
375
376 Note [Check telescope again during generalisation]
377 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
378 The telescope check before kind generalisation is useful to catch something
379 like this:
380
381 data T a k = MkT (Proxy (a :: k))
382
383 Clearly, the k has to come first. Checking for this problem must come before
384 kind generalisation, as described in Note [Bad telescopes] in
385 TcValidity.
386
387 However, we have to check again *after* kind generalisation, to catch something
388 like this:
389
390 data SameKind :: k -> k -> Type -- to force unification
391 data S a (b :: a) (d :: SameKind c b)
392
393 Note that c has no explicit binding site. As such, it's quantified by kind
394 generalisation. (Note that kcHsTyVarBndrs does not return such variables
395 as binders in its returned TcTyCon.) The user-written part of this telescope
396 is well-ordered; no earlier variables depend on later ones. However, after
397 kind generalisation, we put c up front, like so:
398
399 data S {c :: a} a (b :: a) (d :: SameKind c b)
400
401 We now have a problem. We could detect this problem just by looking at the
402 free vars of the kinds of the generalised variables (the kvs), but we get
403 such a nice error message out of checkValidTelescope that it seems like the
404 right thing to do.
405
406 Note [Type environment evolution]
407 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
408 As we typecheck a group of declarations the type environment evolves.
409 Consider for example:
410 data B (a :: Type) = MkB (Proxy 'MkB)
411
412 We do the following steps:
413
414 1. Start of tcTyClDecls: use mkPromotionErrorEnv to initialise the
415 type env with promotion errors
416 B :-> TyConPE
417 MkB :-> DataConPE
418
419 2. kcTyCLGruup
420 - Do getInitialKinds, which will signal a promotion
421 error if B is used in any of the kinds needed to initialse
422 B's kind (e.g. (a :: Type)) here
423
424 - Extend the type env with these initial kinds (monomorphic for
425 decls that lack a CUSK)
426 B :-> TcTyCon <initial kind>
427 (thereby overriding the B :-> TyConPE binding)
428 and do kcLTyClDecl on each decl to get equality constraints on
429 all those inital kinds
430
431 - Generalise the inital kind, making a poly-kinded TcTyCon
432
433 3. Back in tcTyDecls, extend the envt with bindings of the poly-kinded
434 TcTyCons, again overriding the promotion-error bindings.
435
436 But note that the data constructor promotion errors are still in place
437 so that (in our example) a use of MkB will sitll be signalled as
438 an error.
439
440 4. Typecheck the decls.
441
442 5. In tcTyClGroup, extend the envt with bindings for TyCon and DataCons
443
444
445 Note [Missed opportunity to retain higher-rank kinds]
446 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
447 In 'kcTyClGroup', there is a missed opportunity to make kind
448 inference work in a few more cases. The idea is analogous
449 to Note [Single function non-recursive binding special-case]:
450
451 * If we have an SCC with a single decl, which is non-recursive,
452 instead of creating a unification variable representing the
453 kind of the decl and unifying it with the rhs, we can just
454 read the type directly of the rhs.
455
456 * Furthermore, we can update our SCC analysis to ignore
457 dependencies on declarations which have CUSKs: we don't
458 have to kind-check these all at once, since we can use
459 the CUSK to initialize the kind environment.
460
461 Unfortunately this requires reworking a bit of the code in
462 'kcLTyClDecl' so I've decided to punt unless someone shouts about it.
463 -}
464
465 kcTyClGroup :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
466
467 -- Kind check this group, kind generalize, and return the resulting local env
468 -- This binds the TyCons and Classes of the group, but not the DataCons
469 -- See Note [Kind checking for type and class decls]
470 -- Third return value is Nothing if the tycon be unsaturated; otherwise,
471 -- the arity
472 kcTyClGroup decls
473 = do { mod <- getModule
474 ; traceTc "---- kcTyClGroup ---- {" (text "module" <+> ppr mod $$ vcat (map ppr decls))
475
476 -- Kind checking;
477 -- 1. Bind kind variables for decls
478 -- 2. Kind-check decls
479 -- 3. Generalise the inferred kinds
480 -- See Note [Kind checking for type and class decls]
481
482 -- Step 1: Bind kind variables for all decls
483 ; initial_tcs <- getInitialKinds decls
484 ; traceTc "kcTyClGroup: initial kinds" $
485 ppr_tc_kinds initial_tcs
486
487 -- Step 2: Set extended envt, kind-check the decls
488 -- NB: the environment extension overrides the tycon
489 -- promotion-errors bindings
490 -- See Note [Type environment evolution]
491
492 ; solveEqualities $
493 tcExtendKindEnvWithTyCons initial_tcs $
494 mapM_ kcLTyClDecl decls
495
496 -- Step 3: generalisation
497 -- Kind checking done for this group
498 -- Now we have to kind generalize the flexis
499 ; poly_tcs <- mapAndReportM generalise initial_tcs
500
501 ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs)
502 ; return poly_tcs }
503
504 where
505 ppr_tc_kinds tcs = vcat (map pp_tc tcs)
506 pp_tc tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc)
507
508 generalise :: TcTyCon -> TcM TcTyCon
509 -- For polymorphic things this is a no-op
510 generalise tc
511 = setSrcSpan (getSrcSpan tc) $
512 addTyConCtxt tc $
513 do { let name = tyConName tc
514 ; tc_binders <- mapM zonkTcTyVarBinder (tyConBinders tc)
515 ; tc_res_kind <- zonkTcType (tyConResKind tc)
516 ; let scoped_tvs = tcTyConScopedTyVars tc
517 user_tyvars = tcTyConUserTyVars tc
518
519 -- See Note [checkValidDependency]
520 ; checkValidDependency tc_binders tc_res_kind
521
522 -- See Note [Bad telescopes] in TcValidity
523 ; checkValidTelescope tc_binders user_tyvars empty
524 ; kvs <- kindGeneralize (mkTyConKind tc_binders tc_res_kind)
525
526 ; let all_binders = mkNamedTyConBinders Inferred kvs ++ tc_binders
527
528 ; (env, all_binders') <- zonkTyVarBindersX emptyZonkEnv all_binders
529 ; tc_res_kind' <- zonkTcTypeToType env tc_res_kind
530 ; scoped_tvs' <- zonkSigTyVarPairs scoped_tvs
531
532 -- See Note [Check telescope again during generalisation]
533 ; let extra = text "NB: Implicitly declared variables come before others."
534 ; checkValidTelescope all_binders user_tyvars extra
535
536 -- Make sure tc_kind' has the final, zonked kind variables
537 ; traceTc "Generalise kind" $
538 vcat [ ppr name, ppr tc_binders, ppr (mkTyConKind tc_binders tc_res_kind)
539 , ppr kvs, ppr all_binders, ppr tc_res_kind
540 , ppr all_binders', ppr tc_res_kind'
541 , ppr scoped_tvs ]
542
543 ; return (mkTcTyCon name user_tyvars all_binders' tc_res_kind'
544 scoped_tvs'
545 (tyConFlavour tc)) }
546
547
548 --------------
549 tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a
550 tcExtendKindEnvWithTyCons tcs
551 = tcExtendKindEnvList [ (tyConName tc, ATcTyCon tc) | tc <- tcs ]
552
553 --------------
554 mkPromotionErrorEnv :: [LTyClDecl GhcRn] -> TcTypeEnv
555 -- Maps each tycon/datacon to a suitable promotion error
556 -- tc :-> APromotionErr TyConPE
557 -- dc :-> APromotionErr RecDataConPE
558 -- See Note [Recursion and promoting data constructors]
559
560 mkPromotionErrorEnv decls
561 = foldr (plusNameEnv . mk_prom_err_env . unLoc)
562 emptyNameEnv decls
563
564 mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv
565 mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats })
566 = unitNameEnv nm (APromotionErr ClassPE)
567 `plusNameEnv`
568 mkNameEnv [ (name, APromotionErr TyConPE)
569 | L _ (FamilyDecl { fdLName = L _ name }) <- ats ]
570
571 mk_prom_err_env (DataDecl { tcdLName = L _ name
572 , tcdDataDefn = HsDataDefn { dd_cons = cons } })
573 = unitNameEnv name (APromotionErr TyConPE)
574 `plusNameEnv`
575 mkNameEnv [ (con, APromotionErr RecDataConPE)
576 | L _ con' <- cons, L _ con <- getConNames con' ]
577
578 mk_prom_err_env decl
579 = unitNameEnv (tcdName decl) (APromotionErr TyConPE)
580 -- Works for family declarations too
581
582 --------------
583 getInitialKinds :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
584 -- Returns a TcTyCon for each TyCon bound by the decls,
585 -- each with its initial kind
586
587 getInitialKinds decls = concatMapM (addLocM getInitialKind) decls
588
589 getInitialKind :: TyClDecl GhcRn -> TcM [TcTyCon]
590 -- Allocate a fresh kind variable for each TyCon and Class
591 -- For each tycon, return a TcTyCon with kind k
592 -- where k is the kind of tc, derived from the LHS
593 -- of the definition (and probably including
594 -- kind unification variables)
595 -- Example: data T a b = ...
596 -- return (T, kv1 -> kv2 -> kv3)
597 --
598 -- This pass deals with (ie incorporates into the kind it produces)
599 -- * The kind signatures on type-variable binders
600 -- * The result kinds signature on a TyClDecl
601 --
602 -- No family instances are passed to getInitialKinds
603
604 getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
605 = do { let cusk = hsDeclHasCusk decl
606 ; (tycon, inner_tcs) <-
607 kcLHsQTyVars name ClassFlavour cusk ktvs $
608 do { inner_tcs <- getFamDeclInitialKinds (Just cusk) ats
609 ; return (constraintKind, inner_tcs) }
610 ; return (tycon : inner_tcs) }
611
612 getInitialKind decl@(DataDecl { tcdLName = L _ name
613 , tcdTyVars = ktvs
614 , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
615 , dd_ND = new_or_data } })
616 = do { (tycon, _) <-
617 kcLHsQTyVars name (newOrDataToFlavour new_or_data) (hsDeclHasCusk decl) ktvs $
618 do { res_k <- case m_sig of
619 Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig
620 Nothing -> return liftedTypeKind
621 ; return (res_k, ()) }
622 ; return [tycon] }
623
624 getInitialKind (FamDecl { tcdFam = decl })
625 = do { tc <- getFamDeclInitialKind Nothing decl
626 ; return [tc] }
627
628 getInitialKind decl@(SynDecl { tcdLName = L _ name
629 , tcdTyVars = ktvs
630 , tcdRhs = rhs })
631 = do { (tycon, _) <- kcLHsQTyVars name TypeSynonymFlavour
632 (hsDeclHasCusk decl) ktvs $
633 do { res_k <- case kind_annotation rhs of
634 Nothing -> newMetaKindVar
635 Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig
636 ; return (res_k, ()) }
637 ; return [tycon] }
638 where
639 -- Keep this synchronized with 'hsDeclHasCusk'.
640 kind_annotation (L _ ty) = case ty of
641 HsParTy _ lty -> kind_annotation lty
642 HsKindSig _ _ k -> Just k
643 _ -> Nothing
644
645 getInitialKind (DataDecl _ (L _ _) _ _ (XHsDataDefn _)) = panic "getInitialKind"
646 getInitialKind (XTyClDecl _) = panic "getInitialKind"
647
648 ---------------------------------
649 getFamDeclInitialKinds :: Maybe Bool -- if assoc., CUSKness of assoc. class
650 -> [LFamilyDecl GhcRn]
651 -> TcM [TcTyCon]
652 getFamDeclInitialKinds mb_cusk decls
653 = mapM (addLocM (getFamDeclInitialKind mb_cusk)) decls
654
655 getFamDeclInitialKind :: Maybe Bool -- if assoc., CUSKness of assoc. class
656 -> FamilyDecl GhcRn
657 -> TcM TcTyCon
658 getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName = L _ name
659 , fdTyVars = ktvs
660 , fdResultSig = L _ resultSig
661 , fdInfo = info })
662 = do { (tycon, _) <-
663 kcLHsQTyVars name flav cusk ktvs $
664 do { res_k <- case resultSig of
665 KindSig _ ki -> tcLHsKindSig ctxt ki
666 TyVarSig _ (L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki
667 _ -- open type families have * return kind by default
668 | tcFlavourIsOpen flav -> return liftedTypeKind
669 -- closed type families have their return kind inferred
670 -- by default
671 | otherwise -> newMetaKindVar
672 ; return (res_k, ()) }
673 ; return tycon }
674 where
675 cusk = famDeclHasCusk mb_cusk decl
676 flav = case info of
677 DataFamily -> DataFamilyFlavour (isJust mb_cusk)
678 OpenTypeFamily -> OpenTypeFamilyFlavour (isJust mb_cusk)
679 ClosedTypeFamily _ -> ClosedTypeFamilyFlavour
680 ctxt = TyFamResKindCtxt name
681 getFamDeclInitialKind _ (XFamilyDecl _) = panic "getFamDeclInitialKind"
682
683 ------------------------------------------------------------------------
684 kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
685 -- See Note [Kind checking for type and class decls]
686 kcLTyClDecl (L loc decl)
687 | hsDeclHasCusk decl -- See Note [Skip decls with CUSKs in kcLTyClDecl]
688 = traceTc "kcTyClDecl skipped due to cusk" (ppr tc_name)
689
690 | otherwise
691 = setSrcSpan loc $
692 tcAddDeclCtxt decl $
693 do { traceTc "kcTyClDecl {" (ppr tc_name)
694 ; kcTyClDecl decl
695 ; traceTc "kcTyClDecl done }" (ppr tc_name) }
696 where
697 tc_name = tyClDeclLName decl
698
699 kcTyClDecl :: TyClDecl GhcRn -> TcM ()
700 -- This function is used solely for its side effect on kind variables
701 -- NB kind signatures on the type variables and
702 -- result kind signature have already been dealt with
703 -- by getInitialKind, so we can ignore them here.
704
705 kcTyClDecl (DataDecl { tcdLName = L _ name, tcdDataDefn = defn })
706 | HsDataDefn { dd_cons = cons@(L _ (ConDeclGADT {}) : _), dd_ctxt = L _ [] } <- defn
707 = mapM_ (wrapLocM kcConDecl) cons
708 -- hs_tvs and dd_kindSig already dealt with in getInitialKind
709 -- This must be a GADT-style decl,
710 -- (see invariants of DataDefn declaration)
711 -- so (a) we don't need to bring the hs_tvs into scope, because the
712 -- ConDecls bind all their own variables
713 -- (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it
714
715 | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
716 = kcTyClTyVars name $
717 do { _ <- tcHsContext ctxt
718 ; mapM_ (wrapLocM kcConDecl) cons }
719
720 kcTyClDecl (SynDecl { tcdLName = L _ name, tcdRhs = lrhs })
721 = kcTyClTyVars name $
722 do { syn_tc <- kcLookupTcTyCon name
723 -- NB: check against the result kind that we allocated
724 -- in getInitialKinds.
725 ; discardResult $ tcCheckLHsType lrhs (tyConResKind syn_tc) }
726
727 kcTyClDecl (ClassDecl { tcdLName = L _ name
728 , tcdCtxt = ctxt, tcdSigs = sigs })
729 = kcTyClTyVars name $
730 do { _ <- tcHsContext ctxt
731 ; mapM_ (wrapLocM kc_sig) sigs }
732 where
733 kc_sig (ClassOpSig _ _ nms op_ty)
734 = kcHsSigType (TyConSkol ClassFlavour name) nms op_ty
735 kc_sig _ = return ()
736
737 kcTyClDecl (FamDecl _ (FamilyDecl { fdLName = L _ fam_tc_name
738 , fdInfo = fd_info }))
739 -- closed type families look at their equations, but other families don't
740 -- do anything here
741 = case fd_info of
742 ClosedTypeFamily (Just eqns) ->
743 do { fam_tc <- kcLookupTcTyCon fam_tc_name
744 ; mapM_ (kcTyFamInstEqn fam_tc) eqns }
745 _ -> return ()
746 kcTyClDecl (FamDecl _ (XFamilyDecl _)) = panic "kcTyClDecl"
747 kcTyClDecl (DataDecl _ (L _ _) _ _ (XHsDataDefn _)) = panic "kcTyClDecl"
748 kcTyClDecl (XTyClDecl _) = panic "kcTyClDecl"
749
750 -------------------
751 kcConDecl :: ConDecl GhcRn -> TcM ()
752 kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs
753 , con_mb_cxt = ex_ctxt, con_args = args })
754 = addErrCtxt (dataConCtxtName [name]) $
755 -- See Note [Use SigTvs in kind-checking pass]
756 kcExplicitTKBndrs ex_tvs $
757 do { _ <- tcHsMbContext ex_ctxt
758 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args) }
759 -- We don't need to check the telescope here, because that's
760 -- done in tcConDecl
761
762 kcConDecl (ConDeclGADT { con_names = names
763 , con_qvars = qtvs, con_mb_cxt = cxt
764 , con_args = args, con_res_ty = res_ty })
765 | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = implicit_tkv_nms }
766 , hsq_explicit = explicit_tkv_nms } <- qtvs
767 = -- Even though the data constructor's type is closed, we
768 -- must still kind-check the type, because that may influence
769 -- the inferred kind of the /type/ constructor. Example:
770 -- data T f a where
771 -- MkT :: f a -> T f a
772 -- If we don't look at MkT we won't get the correct kind
773 -- for the type constructor T
774 addErrCtxt (dataConCtxtName names) $
775 discardResult $
776 kcImplicitTKBndrs implicit_tkv_nms $
777 kcExplicitTKBndrs explicit_tkv_nms $
778 do { _ <- tcHsMbContext cxt
779 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
780 ; _ <- tcHsOpenType res_ty
781 ; return () }
782 kcConDecl (XConDecl _) = panic "kcConDecl"
783 kcConDecl (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _) = panic "kcConDecl"
784
785 {-
786 Note [Recursion and promoting data constructors]
787 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
788 We don't want to allow promotion in a strongly connected component
789 when kind checking.
790
791 Consider:
792 data T f = K (f (K Any))
793
794 When kind checking the `data T' declaration the local env contains the
795 mappings:
796 T -> ATcTyCon <some initial kind>
797 K -> APromotionErr
798
799 APromotionErr is only used for DataCons, and only used during type checking
800 in tcTyClGroup.
801
802 Note [Use SigTvs in kind-checking pass]
803 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
804 Consider
805
806 data Proxy a where
807 MkProxy1 :: forall k (b :: k). Proxy b
808 MkProxy2 :: forall j (c :: j). Proxy c
809
810 It seems reasonable that this should be accepted. But something very strange
811 is going on here: when we're kind-checking this declaration, we need to unify
812 the kind of `a` with k and j -- even though k and j's scopes are local to the type of
813 MkProxy{1,2}. The best approach we've come up with is to use SigTvs during
814 the kind-checking pass. First off, note that it's OK if the kind-checking pass
815 is too permissive: we'll snag the problems in the type-checking pass later.
816 (This extra permissiveness might happen with something like
817
818 data SameKind :: k -> k -> Type
819 data Bad a where
820 MkBad :: forall k1 k2 (a :: k1) (b :: k2). Bad (SameKind a b)
821
822 which would be accepted if k1 and k2 were SigTvs. This is correctly rejected
823 in the second pass, though. Test case: polykinds/SigTvKinds3)
824 Recall that the kind-checking pass exists solely to collect constraints
825 on the kinds and to power unification.
826
827 To achieve the use of SigTvs, we must be careful to use specialized functions
828 that produce SigTvs, not ordinary skolems. This is why we need
829 kcExplicitTKBndrs and kcImplicitTKBndrs in TcHsType, separate from their
830 tc... variants.
831
832 The drawback of this approach is sometimes it will accept a definition that
833 a (hypothetical) declarative specification would likely reject. As a general
834 rule, we don't want to allow polymorphic recursion without a CUSK. Indeed,
835 the whole point of CUSKs is to allow polymorphic recursion. Yet, the SigTvs
836 approach allows a limited form of polymorphic recursion *without* a CUSK.
837
838 To wit:
839 data T a = forall k (b :: k). MkT (T b) Int
840 (test case: dependent/should_compile/T14066a)
841
842 Note that this is polymorphically recursive, with the recursive occurrence
843 of T used at a kind other than a's kind. The approach outlined here accepts
844 this definition, because this kind is still a kind variable (and so the
845 SigTvs unify). Stepping back, I (Richard) have a hard time envisioning a
846 way to describe exactly what declarations will be accepted and which will
847 be rejected (without a CUSK). However, the accepted definitions are indeed
848 well-kinded and any rejected definitions would be accepted with a CUSK,
849 and so this wrinkle need not cause anyone to lose sleep.
850
851 ************************************************************************
852 * *
853 \subsection{Type checking}
854 * *
855 ************************************************************************
856
857 Note [Type checking recursive type and class declarations]
858 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
859 At this point we have completed *kind-checking* of a mutually
860 recursive group of type/class decls (done in kcTyClGroup). However,
861 we discarded the kind-checked types (eg RHSs of data type decls);
862 note that kcTyClDecl returns (). There are two reasons:
863
864 * It's convenient, because we don't have to rebuild a
865 kinded HsDecl (a fairly elaborate type)
866
867 * It's necessary, because after kind-generalisation, the
868 TyCons/Classes may now be kind-polymorphic, and hence need
869 to be given kind arguments.
870
871 Example:
872 data T f a = MkT (f a) (T f a)
873 During kind-checking, we give T the kind T :: k1 -> k2 -> *
874 and figure out constraints on k1, k2 etc. Then we generalise
875 to get T :: forall k. (k->*) -> k -> *
876 So now the (T f a) in the RHS must be elaborated to (T k f a).
877
878 However, during tcTyClDecl of T (above) we will be in a recursive
879 "knot". So we aren't allowed to look at the TyCon T itself; we are only
880 allowed to put it (lazily) in the returned structures. But when
881 kind-checking the RHS of T's decl, we *do* need to know T's kind (so
882 that we can correctly elaboarate (T k f a). How can we get T's kind
883 without looking at T? Delicate answer: during tcTyClDecl, we extend
884
885 *Global* env with T -> ATyCon (the (not yet built) final TyCon for T)
886 *Local* env with T -> ATcTyCon (TcTyCon with the polymorphic kind of T)
887
888 Then:
889
890 * During TcHsType.kcTyVar we look in the *local* env, to get the
891 known kind for T.
892
893 * But in TcHsType.ds_type (and ds_var_app in particular) we look in
894 the *global* env to get the TyCon. But we must be careful not to
895 force the TyCon or we'll get a loop.
896
897 This fancy footwork (with two bindings for T) is only necessary for the
898 TyCons or Classes of this recursive group. Earlier, finished groups,
899 live in the global env only.
900
901 See also Note [Kind checking recursive type and class declarations]
902
903 Note [Kind checking recursive type and class declarations]
904 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
905 Before we can type-check the decls, we must kind check them. This
906 is done by establishing an "initial kind", which is a rather uninformed
907 guess at a tycon's kind (by counting arguments, mainly) and then
908 using this initial kind for recursive occurrences.
909
910 The initial kind is stored in exactly the same way during kind-checking
911 as it is during type-checking (Note [Type checking recursive type and class
912 declarations]): in the *local* environment, with ATcTyCon. But we still
913 must store *something* in the *global* environment. Even though we
914 discard the result of kind-checking, we sometimes need to produce error
915 messages. These error messages will want to refer to the tycons being
916 checked, except that they don't exist yet, and it would be Terribly
917 Annoying to get the error messages to refer back to HsSyn. So we
918 create a TcTyCon and put it in the global env. This tycon can
919 print out its name and knows its kind,
920 but any other action taken on it will panic. Note
921 that TcTyCons are *not* knot-tied, unlike the rather valid but
922 knot-tied ones that occur during type-checking.
923
924 Note [Declarations for wired-in things]
925 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
926 For wired-in things we simply ignore the declaration
927 and take the wired-in information. That avoids complications.
928 e.g. the need to make the data constructor worker name for
929 a constraint tuple match the wired-in one
930 -}
931
932 tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM TyCon
933 tcTyClDecl roles_info (L loc decl)
934 | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
935 = case thing of -- See Note [Declarations for wired-in things]
936 ATyCon tc -> return tc
937 _ -> pprPanic "tcTyClDecl" (ppr thing)
938
939 | otherwise
940 = setSrcSpan loc $ tcAddDeclCtxt decl $
941 do { traceTc "---- tcTyClDecl ---- {" (ppr decl)
942 ; tc <- tcTyClDecl1 Nothing roles_info decl
943 ; traceTc "---- tcTyClDecl end ---- }" (ppr tc)
944 ; return tc }
945
946 -- "type family" declarations
947 tcTyClDecl1 :: Maybe Class -> RolesInfo -> TyClDecl GhcRn -> TcM TyCon
948 tcTyClDecl1 parent _roles_info (FamDecl { tcdFam = fd })
949 = tcFamDecl1 parent fd
950
951 -- "type" synonym declaration
952 tcTyClDecl1 _parent roles_info
953 (SynDecl { tcdLName = L _ tc_name, tcdRhs = rhs })
954 = ASSERT( isNothing _parent )
955 tcTyClTyVars tc_name $ \ binders res_kind ->
956 tcTySynRhs roles_info tc_name binders res_kind rhs
957
958 -- "data/newtype" declaration
959 tcTyClDecl1 _parent roles_info
960 (DataDecl { tcdLName = L _ tc_name
961 , tcdDataDefn = defn })
962 = ASSERT( isNothing _parent )
963 tcTyClTyVars tc_name $ \ tycon_binders res_kind ->
964 tcDataDefn roles_info tc_name tycon_binders res_kind defn
965
966 tcTyClDecl1 _parent roles_info
967 (ClassDecl { tcdLName = L _ class_name
968 , tcdCtxt = ctxt, tcdMeths = meths
969 , tcdFDs = fundeps, tcdSigs = sigs
970 , tcdATs = ats, tcdATDefs = at_defs })
971 = ASSERT( isNothing _parent )
972 do { clas <- fixM $ \ clas ->
973 -- We need the knot because 'clas' is passed into tcClassATs
974 tcTyClTyVars class_name $ \ binders res_kind ->
975 do { MASSERT( isConstraintKind res_kind )
976 ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders)
977 ; let tycon_name = class_name -- We use the same name
978 roles = roles_info tycon_name -- for TyCon and Class
979
980 ; ctxt' <- solveEqualities $ tcHsContext ctxt
981 ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
982 -- Squeeze out any kind unification variables
983 ; fds' <- mapM (addLocM tc_fundep) fundeps
984 ; sig_stuff <- tcClassSigs class_name sigs meths
985 ; at_stuff <- tcClassATs class_name clas ats at_defs
986 ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
987 -- TODO: Allow us to distinguish between abstract class,
988 -- and concrete class with no methods (maybe by
989 -- specifying a trailing where or not
990 ; is_boot <- tcIsHsBootOrSig
991 ; let body | is_boot, null ctxt', null at_stuff, null sig_stuff
992 = Nothing
993 | otherwise
994 = Just (ctxt', at_stuff, sig_stuff, mindef)
995 ; clas <- buildClass class_name binders roles fds' body
996 ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$
997 ppr fds')
998 ; return clas }
999
1000 ; return (classTyCon clas) }
1001 where
1002 tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
1003 ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
1004 ; return (tvs1', tvs2') }
1005
1006 tcTyClDecl1 _ _ (XTyClDecl _) = panic "tcTyClDecl1"
1007
1008 tcFamDecl1 :: Maybe Class -> FamilyDecl GhcRn -> TcM TyCon
1009 tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_name)
1010 , fdResultSig = L _ sig, fdTyVars = user_tyvars
1011 , fdInjectivityAnn = inj })
1012 | DataFamily <- fam_info
1013 = tcTyClTyVars tc_name $ \ binders res_kind -> do
1014 { traceTc "data family:" (ppr tc_name)
1015 ; checkFamFlag tc_name
1016
1017 -- Check the kind signature, if any.
1018 -- Data families might have a variable return kind.
1019 -- See See Note [Arity of data families] in FamInstEnv.
1020 ; (extra_binders, final_res_kind) <- tcDataKindSig binders res_kind
1021 ; checkTc (tcIsLiftedTypeKind final_res_kind
1022 || isJust (tcGetCastedTyVar_maybe final_res_kind))
1023 (badKindSig False res_kind)
1024
1025 ; tc_rep_name <- newTyConRepName tc_name
1026 ; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
1027 final_res_kind
1028 (resultVariableName sig)
1029 (DataFamilyTyCon tc_rep_name)
1030 parent NotInjective
1031 ; return tycon }
1032
1033 | OpenTypeFamily <- fam_info
1034 = tcTyClTyVars tc_name $ \ binders res_kind -> do
1035 { traceTc "open type family:" (ppr tc_name)
1036 ; checkFamFlag tc_name
1037 ; inj' <- tcInjectivity binders inj
1038 ; let tycon = mkFamilyTyCon tc_name binders res_kind
1039 (resultVariableName sig) OpenSynFamilyTyCon
1040 parent inj'
1041 ; return tycon }
1042
1043 | ClosedTypeFamily mb_eqns <- fam_info
1044 = -- Closed type families are a little tricky, because they contain the definition
1045 -- of both the type family and the equations for a CoAxiom.
1046 do { traceTc "Closed type family:" (ppr tc_name)
1047 -- the variables in the header scope only over the injectivity
1048 -- declaration but this is not involved here
1049 ; (inj', binders, res_kind)
1050 <- tcTyClTyVars tc_name
1051 $ \ binders res_kind ->
1052 do { inj' <- tcInjectivity binders inj
1053 ; return (inj', binders, res_kind) }
1054
1055 ; checkFamFlag tc_name -- make sure we have -XTypeFamilies
1056
1057 -- If Nothing, this is an abstract family in a hs-boot file;
1058 -- but eqns might be empty in the Just case as well
1059 ; case mb_eqns of
1060 Nothing ->
1061 return $ mkFamilyTyCon tc_name binders res_kind
1062 (resultVariableName sig)
1063 AbstractClosedSynFamilyTyCon parent
1064 inj'
1065 Just eqns -> do {
1066
1067 -- Process the equations, creating CoAxBranches
1068 ; let tc_fam_tc = mkTcTyCon tc_name (ppr user_tyvars) binders res_kind
1069 [] ClosedTypeFamilyFlavour
1070
1071 ; branches <- mapAndReportM (tcTyFamInstEqn tc_fam_tc Nothing) eqns
1072 -- Do not attempt to drop equations dominated by earlier
1073 -- ones here; in the case of mutual recursion with a data
1074 -- type, we get a knot-tying failure. Instead we check
1075 -- for this afterwards, in TcValidity.checkValidCoAxiom
1076 -- Example: tc265
1077
1078 -- Create a CoAxiom, with the correct src location. It is Vitally
1079 -- Important that we do not pass the branches into
1080 -- newFamInstAxiomName. They have types that have been zonked inside
1081 -- the knot and we will die if we look at them. This is OK here
1082 -- because there will only be one axiom, so we don't need to
1083 -- differentiate names.
1084 -- See [Zonking inside the knot] in TcHsType
1085 ; co_ax_name <- newFamInstAxiomName tc_lname []
1086
1087 ; let mb_co_ax
1088 | null eqns = Nothing -- mkBranchedCoAxiom fails on empty list
1089 | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)
1090
1091 fam_tc = mkFamilyTyCon tc_name binders res_kind (resultVariableName sig)
1092 (ClosedSynFamilyTyCon mb_co_ax) parent inj'
1093
1094 -- We check for instance validity later, when doing validity
1095 -- checking for the tycon. Exception: checking equations
1096 -- overlap done by dropDominatedAxioms
1097 ; return fam_tc } }
1098
1099 | otherwise = panic "tcFamInst1" -- Silence pattern-exhaustiveness checker
1100 tcFamDecl1 _ (XFamilyDecl _) = panic "tcFamDecl1"
1101
1102 -- | Maybe return a list of Bools that say whether a type family was declared
1103 -- injective in the corresponding type arguments. Length of the list is equal to
1104 -- the number of arguments (including implicit kind/coercion arguments).
1105 -- True on position
1106 -- N means that a function is injective in its Nth argument. False means it is
1107 -- not.
1108 tcInjectivity :: [TyConBinder] -> Maybe (LInjectivityAnn GhcRn)
1109 -> TcM Injectivity
1110 tcInjectivity _ Nothing
1111 = return NotInjective
1112
1113 -- User provided an injectivity annotation, so for each tyvar argument we
1114 -- check whether a type family was declared injective in that argument. We
1115 -- return a list of Bools, where True means that corresponding type variable
1116 -- was mentioned in lInjNames (type family is injective in that argument) and
1117 -- False means that it was not mentioned in lInjNames (type family is not
1118 -- injective in that type variable). We also extend injectivity information to
1119 -- kind variables, so if a user declares:
1120 --
1121 -- type family F (a :: k1) (b :: k2) = (r :: k3) | r -> a
1122 --
1123 -- then we mark both `a` and `k1` as injective.
1124 -- NB: the return kind is considered to be *input* argument to a type family.
1125 -- Since injectivity allows to infer input arguments from the result in theory
1126 -- we should always mark the result kind variable (`k3` in this example) as
1127 -- injective. The reason is that result type has always an assigned kind and
1128 -- therefore we can always infer the result kind if we know the result type.
1129 -- But this does not seem to be useful in any way so we don't do it. (Another
1130 -- reason is that the implementation would not be straightforward.)
1131 tcInjectivity tcbs (Just (L loc (InjectivityAnn _ lInjNames)))
1132 = setSrcSpan loc $
1133 do { let tvs = binderVars tcbs
1134 ; dflags <- getDynFlags
1135 ; checkTc (xopt LangExt.TypeFamilyDependencies dflags)
1136 (text "Illegal injectivity annotation" $$
1137 text "Use TypeFamilyDependencies to allow this")
1138 ; inj_tvs <- mapM (tcLookupTyVar . unLoc) lInjNames
1139 ; inj_tvs <- mapM zonkTcTyVarToTyVar inj_tvs -- zonk the kinds
1140 ; let inj_ktvs = filterVarSet isTyVar $ -- no injective coercion vars
1141 closeOverKinds (mkVarSet inj_tvs)
1142 ; let inj_bools = map (`elemVarSet` inj_ktvs) tvs
1143 ; traceTc "tcInjectivity" (vcat [ ppr tvs, ppr lInjNames, ppr inj_tvs
1144 , ppr inj_ktvs, ppr inj_bools ])
1145 ; return $ Injective inj_bools }
1146
1147 tcTySynRhs :: RolesInfo
1148 -> Name
1149 -> [TyConBinder] -> Kind
1150 -> LHsType GhcRn -> TcM TyCon
1151 tcTySynRhs roles_info tc_name binders res_kind hs_ty
1152 = do { env <- getLclEnv
1153 ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
1154 ; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
1155 ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
1156 ; let roles = roles_info tc_name
1157 tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty
1158 ; return tycon }
1159
1160 tcDataDefn :: RolesInfo -> Name
1161 -> [TyConBinder] -> Kind
1162 -> HsDataDefn GhcRn -> TcM TyCon
1163 -- NB: not used for newtype/data instances (whether associated or not)
1164 tcDataDefn roles_info
1165 tc_name tycon_binders res_kind
1166 (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
1167 , dd_ctxt = ctxt, dd_kindSig = mb_ksig
1168 , dd_cons = cons })
1169 = do { tcg_env <- getGblEnv
1170 ; let hsc_src = tcg_src tcg_env
1171 ; (extra_bndrs, final_res_kind) <- tcDataKindSig tycon_binders res_kind
1172 ; unless (mk_permissive_kind hsc_src cons) $
1173 checkTc (tcIsLiftedTypeKind final_res_kind) (badKindSig True res_kind)
1174
1175 ; let final_bndrs = tycon_binders `chkAppend` extra_bndrs
1176 roles = roles_info tc_name
1177
1178 ; stupid_tc_theta <- solveEqualities $ tcHsContext ctxt
1179 ; stupid_theta <- zonkTcTypeToTypes emptyZonkEnv
1180 stupid_tc_theta
1181 ; kind_signatures <- xoptM LangExt.KindSignatures
1182
1183 -- Check that we don't use kind signatures without Glasgow extensions
1184 ; when (isJust mb_ksig) $
1185 checkTc (kind_signatures) (badSigTyDecl tc_name)
1186
1187 ; gadt_syntax <- dataDeclChecks tc_name new_or_data stupid_theta cons
1188
1189 ; tycon <- fixM $ \ tycon -> do
1190 { let res_ty = mkTyConApp tycon (mkTyVarTys (binderVars final_bndrs))
1191 ; data_cons <- tcConDecls tycon (final_bndrs, res_ty) cons
1192 ; tc_rhs <- mk_tc_rhs hsc_src tycon data_cons
1193 ; tc_rep_nm <- newTyConRepName tc_name
1194 ; return (mkAlgTyCon tc_name
1195 final_bndrs
1196 final_res_kind
1197 roles
1198 (fmap unLoc cType)
1199 stupid_theta tc_rhs
1200 (VanillaAlgTyCon tc_rep_nm)
1201 gadt_syntax) }
1202 ; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs)
1203 ; return tycon }
1204 where
1205 -- Abstract data types in hsig files can have arbitrary kinds,
1206 -- because they may be implemented by type synonyms
1207 -- (which themselves can have arbitrary kinds, not just *)
1208 mk_permissive_kind HsigFile [] = True
1209 mk_permissive_kind _ _ = False
1210
1211 -- In hs-boot, a 'data' declaration with no constructors
1212 -- indicates a nominally distinct abstract data type.
1213 mk_tc_rhs HsBootFile _ []
1214 = return AbstractTyCon
1215
1216 mk_tc_rhs HsigFile _ [] -- ditto
1217 = return AbstractTyCon
1218
1219 mk_tc_rhs _ tycon data_cons
1220 = case new_or_data of
1221 DataType -> return (mkDataTyConRhs data_cons)
1222 NewType -> ASSERT( not (null data_cons) )
1223 mkNewTyConRhs tc_name tycon (head data_cons)
1224 tcDataDefn _ _ _ _ (XHsDataDefn _) = panic "tcDataDefn"
1225
1226 {-
1227 ************************************************************************
1228 * *
1229 Typechecking associated types (in class decls)
1230 (including the associated-type defaults)
1231 * *
1232 ************************************************************************
1233
1234 Note [Associated type defaults]
1235 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1236
1237 The following is an example of associated type defaults:
1238 class C a where
1239 data D a
1240
1241 type F a b :: *
1242 type F a b = [a] -- Default
1243
1244 Note that we can get default definitions only for type families, not data
1245 families.
1246 -}
1247
1248 tcClassATs :: Name -- The class name (not knot-tied)
1249 -> Class -- The class parent of this associated type
1250 -> [LFamilyDecl GhcRn] -- Associated types.
1251 -> [LTyFamDefltEqn GhcRn] -- Associated type defaults.
1252 -> TcM [ClassATItem]
1253 tcClassATs class_name cls ats at_defs
1254 = do { -- Complain about associated type defaults for non associated-types
1255 sequence_ [ failWithTc (badATErr class_name n)
1256 | n <- map at_def_tycon at_defs
1257 , not (n `elemNameSet` at_names) ]
1258 ; mapM tc_at ats }
1259 where
1260 at_def_tycon :: LTyFamDefltEqn GhcRn -> Name
1261 at_def_tycon (L _ eqn) = unLoc (feqn_tycon eqn)
1262
1263 at_fam_name :: LFamilyDecl GhcRn -> Name
1264 at_fam_name (L _ decl) = unLoc (fdLName decl)
1265
1266 at_names = mkNameSet (map at_fam_name ats)
1267
1268 at_defs_map :: NameEnv [LTyFamDefltEqn GhcRn]
1269 -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'
1270 at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv
1271 (at_def_tycon at_def) [at_def])
1272 emptyNameEnv at_defs
1273
1274 tc_at at = do { fam_tc <- addLocM (tcFamDecl1 (Just cls)) at
1275 ; let at_defs = lookupNameEnv at_defs_map (at_fam_name at)
1276 `orElse` []
1277 ; atd <- tcDefaultAssocDecl fam_tc at_defs
1278 ; return (ATI fam_tc atd) }
1279
1280 -------------------------
1281 tcDefaultAssocDecl :: TyCon -- ^ Family TyCon (not knot-tied)
1282 -> [LTyFamDefltEqn GhcRn] -- ^ Defaults
1283 -> TcM (Maybe (Type, SrcSpan)) -- ^ Type checked RHS
1284 tcDefaultAssocDecl _ []
1285 = return Nothing -- No default declaration
1286
1287 tcDefaultAssocDecl _ (d1:_:_)
1288 = failWithTc (text "More than one default declaration for"
1289 <+> ppr (feqn_tycon (unLoc d1)))
1290
1291 tcDefaultAssocDecl fam_tc [L loc (FamEqn { feqn_tycon = L _ tc_name
1292 , feqn_pats = hs_tvs
1293 , feqn_rhs = rhs })]
1294 | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = imp_vars}
1295 , hsq_explicit = exp_vars } <- hs_tvs
1296 = -- See Note [Type-checking default assoc decls]
1297 setSrcSpan loc $
1298 tcAddFamInstCtxt (text "default type instance") tc_name $
1299 do { traceTc "tcDefaultAssocDecl" (ppr tc_name)
1300 ; let fam_tc_name = tyConName fam_tc
1301 fam_arity = length (tyConVisibleTyVars fam_tc)
1302
1303 -- Kind of family check
1304 ; ASSERT( fam_tc_name == tc_name )
1305 checkTc (isTypeFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
1306
1307 -- Arity check
1308 ; checkTc (exp_vars `lengthIs` fam_arity)
1309 (wrongNumberOfParmsErr fam_arity)
1310
1311 -- Typecheck RHS
1312 ; let all_vars = imp_vars ++ map hsLTyVarName exp_vars
1313 pats = map hsLTyVarBndrToType exp_vars
1314
1315 -- NB: Use tcFamTyPats, not tcTyClTyVars. The latter expects to get
1316 -- the LHsQTyVars used for declaring a tycon, but the names here
1317 -- are different.
1318
1319 -- You might think we should pass in some ClsInstInfo, as we're looking
1320 -- at an associated type. But this would be wrong, because an associated
1321 -- type default LHS can mention *different* type variables than the
1322 -- enclosing class. So it's treated more as a freestanding beast.
1323 ; (pats', rhs_ty)
1324 <- tcFamTyPats fam_tc Nothing all_vars pats
1325 (kcTyFamEqnRhs Nothing rhs) $
1326 \tvs pats rhs_kind ->
1327 do { rhs_ty <- solveEqualities $
1328 tcCheckLHsType rhs rhs_kind
1329
1330 -- Zonk the patterns etc into the Type world
1331 ; (ze, _) <- zonkTyBndrsX emptyZonkEnv tvs
1332 ; pats' <- zonkTcTypeToTypes ze pats
1333 ; rhs_ty' <- zonkTcTypeToType ze rhs_ty
1334 ; return (pats', rhs_ty') }
1335
1336 -- See Note [Type-checking default assoc decls]
1337 ; case tcMatchTys pats' (mkTyVarTys (tyConTyVars fam_tc)) of
1338 Just subst -> return (Just (substTyUnchecked subst rhs_ty, loc) )
1339 Nothing -> failWithTc (defaultAssocKindErr fam_tc)
1340 -- We check for well-formedness and validity later,
1341 -- in checkValidClass
1342 }
1343 tcDefaultAssocDecl _ [L _ (XFamEqn _)] = panic "tcDefaultAssocDecl"
1344 tcDefaultAssocDecl _ [L _ (FamEqn _ (L _ _) (XLHsQTyVars _) _ _)]
1345 = panic "tcDefaultAssocDecl"
1346
1347 {- Note [Type-checking default assoc decls]
1348 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1349 Consider this default declaration for an associated type
1350
1351 class C a where
1352 type F (a :: k) b :: *
1353 type F x y = Proxy x -> y
1354
1355 Note that the class variable 'a' doesn't scope over the default assoc
1356 decl (rather oddly I think), and (less oddly) neither does the second
1357 argument 'b' of the associated type 'F', or the kind variable 'k'.
1358 Instead, the default decl is treated more like a top-level type
1359 instance.
1360
1361 However we store the default rhs (Proxy x -> y) in F's TyCon, using
1362 F's own type variables, so we need to convert it to (Proxy a -> b).
1363 We do this by calling tcMatchTys to match them up. This also ensures
1364 that x's kind matches a's and similarly for y and b. The error
1365 message isn't great, mind you. (Trac #11361 was caused by not doing a
1366 proper tcMatchTys here.) -}
1367
1368 -------------------------
1369 kcTyFamInstEqn :: TcTyCon -> LTyFamInstEqn GhcRn -> TcM ()
1370 kcTyFamInstEqn tc_fam_tc
1371 (L loc (HsIB { hsib_ext = HsIBRn { hsib_vars = tv_names }
1372 , hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name
1373 , feqn_pats = pats
1374 , feqn_rhs = hs_ty }}))
1375 = setSrcSpan loc $
1376 do { traceTc "kcTyFamInstEqn" (vcat
1377 [ text "tc_name =" <+> ppr eqn_tc_name
1378 , text "fam_tc =" <+> ppr tc_fam_tc <+> dcolon <+> ppr (tyConKind tc_fam_tc)
1379 , text "hsib_vars =" <+> ppr tv_names
1380 , text "feqn_pats =" <+> ppr pats ])
1381 ; checkTc (fam_name == eqn_tc_name)
1382 (wrongTyFamName fam_name eqn_tc_name)
1383 -- this check reports an arity error instead of a kind error; easier for user
1384 ; checkTc (pats `lengthIs` vis_arity) $
1385 wrongNumberOfParmsErr vis_arity
1386 ; kcFamTyPats tc_fam_tc tv_names pats $ \ rhs_kind ->
1387 discardResult $ kcTyFamEqnRhs Nothing hs_ty rhs_kind }
1388 where
1389 fam_name = tyConName tc_fam_tc
1390 vis_arity = length (tyConVisibleTyVars tc_fam_tc)
1391 kcTyFamInstEqn _ (L _ (XHsImplicitBndrs _)) = panic "kcTyFamInstEqn"
1392 kcTyFamInstEqn _ (L _ (HsIB _ (XFamEqn _))) = panic "kcTyFamInstEqn"
1393
1394 -- Infer the kind of the type on the RHS of a type family eqn. Then use
1395 -- this kind to check the kind of the LHS of the equation. This is useful
1396 -- as the callback to tcFamTyPats.
1397 kcTyFamEqnRhs :: Maybe ClsInstInfo
1398 -> LHsType GhcRn -- ^ Eqn RHS
1399 -> TcKind -- ^ Inferred kind of left-hand side
1400 -> TcM ([TcType], TcKind) -- ^ New pats, inst'ed kind of left-hand side
1401 kcTyFamEqnRhs mb_clsinfo rhs_hs_ty lhs_ki
1402 = do { -- It's still possible the lhs_ki has some foralls. Instantiate these away.
1403 (new_pats, insted_lhs_ki)
1404 <- instantiateTyUntilN mb_kind_env 0 lhs_ki
1405
1406 ; traceTc "kcTyFamEqnRhs" (vcat
1407 [ text "rhs_hs_ty =" <+> ppr rhs_hs_ty
1408 , text "lhs_ki =" <+> ppr lhs_ki
1409 , text "insted_lhs_ki =" <+> ppr insted_lhs_ki
1410 , text "new_pats =" <+> ppr new_pats
1411 ])
1412
1413 ; _ <- tcCheckLHsType rhs_hs_ty insted_lhs_ki
1414
1415 ; return (new_pats, insted_lhs_ki) }
1416 where
1417 mb_kind_env = thdOf3 <$> mb_clsinfo
1418
1419 tcTyFamInstEqn :: TcTyCon -> Maybe ClsInstInfo -> LTyFamInstEqn GhcRn
1420 -> TcM CoAxBranch
1421 -- Needs to be here, not in TcInstDcls, because closed families
1422 -- (typechecked here) have TyFamInstEqns
1423 tcTyFamInstEqn fam_tc mb_clsinfo
1424 (L loc (HsIB { hsib_ext = HsIBRn { hsib_vars = tv_names }
1425 , hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name
1426 , feqn_pats = pats
1427 , feqn_rhs = hs_ty }}))
1428 = ASSERT( getName fam_tc == eqn_tc_name )
1429 setSrcSpan loc $
1430 tcFamTyPats fam_tc mb_clsinfo tv_names pats
1431 (kcTyFamEqnRhs mb_clsinfo hs_ty) $
1432 \tvs pats res_kind ->
1433 do { rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
1434
1435 ; (ze, tvs') <- zonkTyBndrsX emptyZonkEnv tvs
1436 ; pats' <- zonkTcTypeToTypes ze pats
1437 ; rhs_ty' <- zonkTcTypeToType ze rhs_ty
1438 ; traceTc "tcTyFamInstEqn" (ppr fam_tc <+> pprTyVars tvs')
1439 -- don't print out the pats here, as they might be zonked inside the knot
1440 ; return (mkCoAxBranch tvs' [] pats' rhs_ty'
1441 (map (const Nominal) tvs')
1442 loc) }
1443 tcTyFamInstEqn _ _ (L _ (XHsImplicitBndrs _)) = panic "tcTyFamInstEqn"
1444 tcTyFamInstEqn _ _ (L _ (HsIB _ (XFamEqn _))) = panic "tcTyFamInstEqn"
1445
1446 kcDataDefn :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars
1447 -- (associated types only)
1448 -> DataFamInstDecl GhcRn
1449 -> TcKind -- ^ the kind of the tycon applied to pats
1450 -> TcM ([TcType], TcKind)
1451 -- ^ the kind signature might force instantiation
1452 -- of the tycon; this returns any extra args and the inst'ed kind
1453 -- See Note [Instantiating a family tycon]
1454 -- Used for 'data instance' only
1455 -- Ordinary 'data' is handled by kcTyClDec
1456 kcDataDefn mb_kind_env
1457 (DataFamInstDecl { dfid_eqn = HsIB { hsib_body =
1458 FamEqn { feqn_tycon = fam_name
1459 , feqn_pats = pats
1460 , feqn_fixity = fixity
1461 , feqn_rhs = HsDataDefn { dd_ctxt = ctxt
1462 , dd_cons = cons
1463 , dd_kindSig = mb_kind } }}})
1464 res_k
1465 = do { _ <- tcHsContext ctxt
1466 ; checkNoErrs $ mapM_ (wrapLocM kcConDecl) cons
1467 -- See Note [Failing early in kcDataDefn]
1468 ; exp_res_kind <- case mb_kind of
1469 Nothing -> return liftedTypeKind
1470 Just k -> tcLHsKindSig (DataKindCtxt (unLoc fam_name)) k
1471
1472 -- The expected type might have a forall at the type. Normally, we
1473 -- can't skolemise in kinds because we don't have type-level lambda.
1474 -- But here, we're at the top-level of an instance declaration, so
1475 -- we actually have a place to put the regeneralised variables.
1476 -- Thus: skolemise away. cf. Inst.deeplySkolemise and TcUnify.tcSkolemise
1477 -- Examples in indexed-types/should_compile/T12369
1478 ; let (tvs_to_skolemise, inner_res_kind) = tcSplitForAllTys exp_res_kind
1479
1480 ; (skol_subst, tvs') <- tcInstSkolTyVars tvs_to_skolemise
1481 -- we don't need to do anything substantive with the tvs' because the
1482 -- quantifyTyVars in tcFamTyPats will catch them.
1483
1484 ; let inner_res_kind' = substTyAddInScope skol_subst inner_res_kind
1485 tv_prs = zip (map tyVarName tvs_to_skolemise) tvs'
1486 skol_info = SigSkol (InstDeclCtxt False) exp_res_kind tv_prs
1487
1488 ; (ev_binds, (_, new_args, co))
1489 <- solveEqualities $
1490 checkConstraints skol_info tvs' [] $
1491 checkExpectedKindX mb_kind_env pp_fam_app
1492 bogus_ty res_k inner_res_kind'
1493
1494 ; let Pair lhs_ki rhs_ki = tcCoercionKind co
1495
1496 ; when debugIsOn $
1497 do { (_, ev_binds) <- zonkTcEvBinds emptyZonkEnv ev_binds
1498 ; MASSERT( isEmptyTcEvBinds ev_binds )
1499 ; lhs_ki <- zonkTcType lhs_ki
1500 ; rhs_ki <- zonkTcType rhs_ki
1501 ; MASSERT( lhs_ki `tcEqType` rhs_ki ) }
1502
1503 ; return (new_args, lhs_ki) }
1504 where
1505 bogus_ty = pprPanic "kcDataDefn" (ppr fam_name <+> ppr pats)
1506 pp_fam_app = pprFamInstLHS fam_name pats fixity (unLoc ctxt) mb_kind
1507 kcDataDefn _ (DataFamInstDecl (XHsImplicitBndrs _)) _
1508 = panic "kcDataDefn"
1509 kcDataDefn _ (DataFamInstDecl (HsIB _ (FamEqn _ _ _ _ (XHsDataDefn _)))) _
1510 = panic "kcDataDefn"
1511 kcDataDefn _ (DataFamInstDecl (HsIB _ (XFamEqn _))) _
1512 = panic "kcDataDefn"
1513
1514 {-
1515 Kind check type patterns and kind annotate the embedded type variables.
1516 type instance F [a] = rhs
1517
1518 * Here we check that a type instance matches its kind signature, but we do
1519 not check whether there is a pattern for each type index; the latter
1520 check is only required for type synonym instances.
1521
1522 Note [Instantiating a family tycon]
1523 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1524 It's possible that kind-checking the result of a family tycon applied to
1525 its patterns will instantiate the tycon further. For example, we might
1526 have
1527
1528 type family F :: k where
1529 F = Int
1530 F = Maybe
1531
1532 After checking (F :: forall k. k) (with no visible patterns), we still need
1533 to instantiate the k. With data family instances, this problem can be even
1534 more intricate, due to Note [Arity of data families] in FamInstEnv. See
1535 indexed-types/should_compile/T12369 for an example.
1536
1537 So, the kind-checker must return both the new args (that is, Type
1538 (Type -> Type) for the equations above) and the instantiated kind.
1539
1540 Because we don't need this information in the kind-checking phase of
1541 checking closed type families, we don't require these extra pieces of
1542 information in tc_fam_ty_pats.
1543
1544 Note [Failing early in kcDataDefn]
1545 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1546 We need to use checkNoErrs when calling kcConDecl. This is because kcConDecl
1547 calls tcConDecl, which checks that the return type of a GADT-like constructor
1548 is actually an instance of the type head. Without the checkNoErrs, potentially
1549 two bad things could happen:
1550
1551 1) Duplicate error messages, because tcConDecl will be called again during
1552 *type* checking (as opposed to kind checking)
1553 2) If we just keep blindly forging forward after both kind checking and type
1554 checking, we can get a panic in rejigConRes. See Trac #8368.
1555 -}
1556
1557 -----------------
1558 kcFamTyPats :: TcTyCon
1559 -> [Name]
1560 -> HsTyPats GhcRn
1561 -> (TcKind -> TcM ())
1562 -> TcM ()
1563 kcFamTyPats tc_fam_tc tv_names arg_pats kind_checker
1564 = discardResult $
1565 kcImplicitTKBndrs tv_names $
1566 do { let name = tyConName tc_fam_tc
1567 loc = nameSrcSpan name
1568 lhs_fun = L loc (HsTyVar noExt NotPromoted (L loc name))
1569 -- lhs_fun is for error messages only
1570 no_fun = pprPanic "kcFamTyPats" (ppr name)
1571 fun_kind = tyConKind tc_fam_tc
1572
1573 ; (_, _, res_kind_out) <- tcInferApps typeLevelMode Nothing lhs_fun no_fun
1574 fun_kind arg_pats
1575 ; traceTc "kcFamTyPats" (vcat [ ppr tc_fam_tc, ppr arg_pats, ppr res_kind_out ])
1576 ; kind_checker res_kind_out }
1577
1578 tcFamTyPats :: TyCon
1579 -> Maybe ClsInstInfo
1580 -> [Name] -- Implicitly bound kind/type variable names
1581 -> HsTyPats GhcRn -- Type patterns
1582 -> (TcKind -> TcM ([TcType], TcKind))
1583 -- kind-checker for RHS
1584 -- See Note [Instantiating a family tycon]
1585 -> ( [TcTyVar] -- Kind and type variables
1586 -> [TcType] -- Kind and type arguments
1587 -> TcKind
1588 -> TcM a) -- NB: You can use solveEqualities here.
1589 -> TcM a
1590 -- Check the type patterns of a type or data family instance
1591 -- type instance F <pat1> <pat2> = <type>
1592 -- The 'tyvars' are the free type variables of pats
1593 --
1594 -- NB: The family instance declaration may be an associated one,
1595 -- nested inside an instance decl, thus
1596 -- instance C [a] where
1597 -- type F [a] = ...
1598 -- In that case, the type variable 'a' will *already be in scope*
1599 -- (and, if C is poly-kinded, so will its kind parameter).
1600 tcFamTyPats fam_tc mb_clsinfo
1601 tv_names arg_pats kind_checker thing_inside
1602 = do { -- First, check the arity.
1603 -- If we wait until validity checking, we'll get kind
1604 -- errors below when an arity error will be much easier to
1605 -- understand.
1606 let should_check_arity
1607 | DataFamilyFlavour _ <- flav = False
1608 -- why not check data families? See [Arity of data families] in FamInstEnv
1609 | otherwise = True
1610
1611 ; when should_check_arity $
1612 checkTc (arg_pats `lengthIs` vis_arity) $
1613 wrongNumberOfParmsErr vis_arity
1614 -- report only explicit arguments
1615
1616 ; (fam_used_tvs, (typats, (more_typats, res_kind)))
1617 <- solveEqualities $ -- See Note [Constraints in patterns]
1618 tcImplicitQTKBndrs FamInstSkol tv_names $
1619 -- See Note [Kind-checking tyvar binders for associated types]
1620 do { let loc = nameSrcSpan fam_name
1621 lhs_fun = L loc (HsTyVar noExt NotPromoted
1622 (L loc fam_name))
1623 fun_ty = mkTyConApp fam_tc []
1624 fun_kind = tyConKind fam_tc
1625 mb_kind_env = thdOf3 <$> mb_clsinfo
1626
1627 ; (_, args, res_kind_out)
1628 <- tcInferApps typeLevelMode mb_kind_env
1629 lhs_fun fun_ty fun_kind arg_pats
1630
1631 ; traceTc "tcFamTyPats 1" (vcat [ ppr fam_tc, ppr arg_pats, ppr res_kind_out ])
1632
1633 ; stuff <- kind_checker res_kind_out
1634 ; return (args, stuff) }
1635
1636 {- TODO (RAE): This should be cleverer. Consider this:
1637
1638 type family F a
1639
1640 data G a where
1641 MkG :: F a ~ Bool => G a
1642
1643 type family Foo (x :: G a) :: F a
1644 type instance Foo MkG = False
1645
1646 This should probably be accepted. Yet the solveEqualities
1647 will fail, unable to solve (F a ~ Bool)
1648 We want to quantify over that proof.
1649 But see Note [Constraints in patterns]
1650 below, which is missing this piece. -}
1651
1652
1653 -- Find free variables (after zonking) and turn
1654 -- them into skolems, so that we don't subsequently
1655 -- replace a meta kind var with (Any *)
1656 -- Very like kindGeneralize
1657 ; let all_pats = typats `chkAppend` more_typats
1658 ; vars <- zonkTcTypesAndSplitDepVars all_pats
1659 ; qtkvs <- quantifyTyVars emptyVarSet vars
1660
1661 ; when debugIsOn $
1662 do { all_pats <- mapM zonkTcTypeInKnot all_pats
1663 ; MASSERT2( isEmptyVarSet $ coVarsOfTypes all_pats, ppr all_pats ) }
1664 -- This should be the case, because otherwise the solveEqualities
1665 -- above would fail. TODO (RAE): Update once the solveEqualities
1666 -- bit is cleverer.
1667
1668 ; traceTc "tcFamTyPats" (ppr (getName fam_tc)
1669 $$ ppr all_pats $$ ppr qtkvs)
1670 -- Don't print out too much, as we might be in the knot
1671
1672 -- See Note [Free-floating kind vars] in TcHsType
1673 ; let all_mentioned_tvs = mkVarSet qtkvs
1674 -- qtkvs has all the tyvars bound by LHS
1675 -- type patterns
1676 unmentioned_tvs = filterOut (`elemVarSet` all_mentioned_tvs)
1677 fam_used_tvs
1678 -- If there are tyvars left over, we can
1679 -- assume they're free-floating, since they
1680 -- aren't bound by a type pattern
1681 ; checkNoErrs $ reportFloatingKvs fam_name flav
1682 qtkvs unmentioned_tvs
1683
1684 ; scopeTyVars FamInstSkol qtkvs $
1685 -- Extend envt with TcTyVars not TyVars, because the
1686 -- kind checking etc done by thing_inside does not expect
1687 -- to encounter TyVars; it expects TcTyVars
1688 thing_inside qtkvs all_pats res_kind }
1689 where
1690 fam_name = tyConName fam_tc
1691 flav = tyConFlavour fam_tc
1692 vis_arity = length (tyConVisibleTyVars fam_tc)
1693
1694
1695 {-
1696 Note [Constraints in patterns]
1697 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1698 NB: This isn't the whole story. See comment in tcFamTyPats.
1699
1700 At first glance, it seems there is a complicated story to tell in tcFamTyPats
1701 around constraint solving. After all, type family patterns can now do
1702 GADT pattern-matching, which is jolly complicated. But, there's a key fact
1703 which makes this all simple: everything is at top level! There cannot
1704 be untouchable type variables. There can't be weird interaction between
1705 case branches. There can't be global skolems.
1706
1707 This means that the semantics of type-level GADT matching is a little
1708 different than term level. If we have
1709
1710 data G a where
1711 MkGBool :: G Bool
1712
1713 And then
1714
1715 type family F (a :: G k) :: k
1716 type instance F MkGBool = True
1717
1718 we get
1719
1720 axF : F Bool (MkGBool <Bool>) ~ True
1721
1722 Simple! No casting on the RHS, because we can affect the kind parameter
1723 to F.
1724
1725 If we ever introduce local type families, this all gets a lot more
1726 complicated, and will end up looking awfully like term-level GADT
1727 pattern-matching.
1728
1729
1730 ** The new story **
1731
1732 Here is really what we want:
1733
1734 The matcher really can't deal with covars in arbitrary spots in coercions.
1735 But it can deal with covars that are arguments to GADT data constructors.
1736 So we somehow want to allow covars only in precisely those spots, then use
1737 them as givens when checking the RHS. TODO (RAE): Implement plan.
1738
1739
1740 Note [Quantifying over family patterns]
1741 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1742 We need to quantify over two different lots of kind variables:
1743
1744 First, the ones that come from the kinds of the tyvar args of
1745 tcTyVarBndrsKindGen, as usual
1746 data family Dist a
1747
1748 -- Proxy :: forall k. k -> *
1749 data instance Dist (Proxy a) = DP
1750 -- Generates data DistProxy = DP
1751 -- ax8 k (a::k) :: Dist * (Proxy k a) ~ DistProxy k a
1752 -- The 'k' comes from the tcTyVarBndrsKindGen (a::k)
1753
1754 Second, the ones that come from the kind argument of the type family
1755 which we pick up using the (tyCoVarsOfTypes typats) in the result of
1756 the thing_inside of tcHsTyvarBndrsGen.
1757 -- Any :: forall k. k
1758 data instance Dist Any = DA
1759 -- Generates data DistAny k = DA
1760 -- ax7 k :: Dist k (Any k) ~ DistAny k
1761 -- The 'k' comes from kindGeneralizeKinds (Any k)
1762
1763 Note [Quantified kind variables of a family pattern]
1764 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1765 Consider type family KindFam (p :: k1) (q :: k1)
1766 data T :: Maybe k1 -> k2 -> *
1767 type instance KindFam (a :: Maybe k) b = T a b -> Int
1768 The HsBSig for the family patterns will be ([k], [a])
1769
1770 Then in the family instance we want to
1771 * Bring into scope [ "k" -> k:*, "a" -> a:k ]
1772 * Kind-check the RHS
1773 * Quantify the type instance over k and k', as well as a,b, thus
1774 type instance [k, k', a:Maybe k, b:k']
1775 KindFam (Maybe k) k' a b = T k k' a b -> Int
1776
1777 Notice that in the third step we quantify over all the visibly-mentioned
1778 type variables (a,b), but also over the implicitly mentioned kind variables
1779 (k, k'). In this case one is bound explicitly but often there will be
1780 none. The role of the kind signature (a :: Maybe k) is to add a constraint
1781 that 'a' must have that kind, and to bring 'k' into scope.
1782
1783
1784
1785 ************************************************************************
1786 * *
1787 Data types
1788 * *
1789 ************************************************************************
1790 -}
1791
1792 dataDeclChecks :: Name -> NewOrData -> ThetaType -> [LConDecl GhcRn] -> TcM Bool
1793 dataDeclChecks tc_name new_or_data stupid_theta cons
1794 = do { -- Check that we don't use GADT syntax in H98 world
1795 gadtSyntax_ok <- xoptM LangExt.GADTSyntax
1796 ; let gadt_syntax = consUseGadtSyntax cons
1797 ; checkTc (gadtSyntax_ok || not gadt_syntax) (badGadtDecl tc_name)
1798
1799 -- Check that the stupid theta is empty for a GADT-style declaration
1800 ; checkTc (null stupid_theta || not gadt_syntax) (badStupidTheta tc_name)
1801
1802 -- Check that a newtype has exactly one constructor
1803 -- Do this before checking for empty data decls, so that
1804 -- we don't suggest -XEmptyDataDecls for newtypes
1805 ; checkTc (new_or_data == DataType || isSingleton cons)
1806 (newtypeConError tc_name (length cons))
1807
1808 -- Check that there's at least one condecl,
1809 -- or else we're reading an hs-boot file, or -XEmptyDataDecls
1810 ; empty_data_decls <- xoptM LangExt.EmptyDataDecls
1811 ; is_boot <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
1812 ; checkTc (not (null cons) || empty_data_decls || is_boot)
1813 (emptyConDeclsErr tc_name)
1814 ; return gadt_syntax }
1815
1816
1817 -----------------------------------
1818 consUseGadtSyntax :: [LConDecl a] -> Bool
1819 consUseGadtSyntax (L _ (ConDeclGADT { }) : _) = True
1820 consUseGadtSyntax _ = False
1821 -- All constructors have same shape
1822
1823 -----------------------------------
1824 tcConDecls :: TyCon -> ([TyConBinder], Type)
1825 -> [LConDecl GhcRn] -> TcM [DataCon]
1826 -- Why both the tycon tyvars and binders? Because the tyvars
1827 -- have all the names and the binders have the visibilities.
1828 tcConDecls rep_tycon (tmpl_bndrs, res_tmpl)
1829 = concatMapM $ addLocM $
1830 tcConDecl rep_tycon (mkTyConTagMap rep_tycon) tmpl_bndrs res_tmpl
1831 -- It's important that we pay for tag allocation here, once per TyCon,
1832 -- See Note [Constructor tag allocation], fixes #14657
1833
1834 tcConDecl :: TyCon -- Representation tycon. Knot-tied!
1835 -> NameEnv ConTag
1836 -> [TyConBinder] -> Type
1837 -- Return type template (with its template tyvars)
1838 -- (tvs, T tys), where T is the family TyCon
1839 -> ConDecl GhcRn
1840 -> TcM [DataCon]
1841
1842 tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
1843 (ConDeclH98 { con_name = name
1844 , con_ex_tvs = explicit_tkv_nms
1845 , con_mb_cxt = hs_ctxt
1846 , con_args = hs_args })
1847 = addErrCtxt (dataConCtxtName [name]) $
1848 do { -- Get hold of the existential type variables
1849 -- e.g. data T a = forall k (b::k) f. MkT a (f b)
1850 -- Here tmpl_bndrs = {a}
1851 -- hs_qvars = HsQTvs { hsq_implicit = {k}
1852 -- , hsq_explicit = {f,b} }
1853
1854 ; traceTc "tcConDecl 1" (vcat [ ppr name, ppr explicit_tkv_nms ])
1855
1856 ; (exp_tvs, (ctxt, arg_tys, field_lbls, stricts))
1857 <- solveEqualities $
1858 tcExplicitTKBndrs skol_info explicit_tkv_nms $
1859 do { ctxt <- tcHsMbContext hs_ctxt
1860 ; btys <- tcConArgs hs_args
1861 ; field_lbls <- lookupConstructorFields (unLoc name)
1862 ; let (arg_tys, stricts) = unzip btys
1863 ; return (ctxt, arg_tys, field_lbls, stricts)
1864 }
1865
1866 -- exp_tvs have explicit, user-written binding sites
1867 -- the kvs below are those kind variables entirely unmentioned by the user
1868 -- and discovered only by generalization
1869
1870 ; kvs <- quantifyConDecl (mkVarSet (binderVars tmpl_bndrs))
1871 (mkSpecForAllTys exp_tvs $
1872 mkFunTys ctxt $
1873 mkFunTys arg_tys $
1874 unitTy)
1875 -- That type is a lie, of course. (It shouldn't end in ()!)
1876 -- And we could construct a proper result type from the info
1877 -- at hand. But the result would mention only the tmpl_tvs,
1878 -- and so it just creates more work to do it right. Really,
1879 -- we're doing this to get the right behavior around removing
1880 -- any vars bound in exp_binders.
1881
1882 -- Zonk to Types
1883 ; (ze, qkvs) <- zonkTyBndrsX emptyZonkEnv kvs
1884 ; (ze, user_qtvs) <- zonkTyBndrsX ze exp_tvs
1885 ; arg_tys <- zonkTcTypeToTypes ze arg_tys
1886 ; ctxt <- zonkTcTypeToTypes ze ctxt
1887
1888 ; fam_envs <- tcGetFamInstEnvs
1889
1890 -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
1891 ; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls)
1892 ; let
1893 univ_tvbs = tyConTyVarBinders tmpl_bndrs
1894 univ_tvs = binderVars univ_tvbs
1895 ex_tvbs = mkTyVarBinders Inferred qkvs ++
1896 mkTyVarBinders Specified user_qtvs
1897 ex_tvs = qkvs ++ user_qtvs
1898 -- For H98 datatypes, the user-written tyvar binders are precisely
1899 -- the universals followed by the existentials.
1900 -- See Note [DataCon user type variable binders] in DataCon.
1901 user_tvbs = univ_tvbs ++ ex_tvbs
1902 buildOneDataCon (L _ name) = do
1903 { is_infix <- tcConIsInfixH98 name hs_args
1904 ; rep_nm <- newTyConRepName name
1905
1906 ; buildDataCon fam_envs name is_infix rep_nm
1907 stricts Nothing field_lbls
1908 univ_tvs ex_tvs user_tvbs
1909 [{- no eq_preds -}] ctxt arg_tys
1910 res_tmpl rep_tycon tag_map
1911 -- NB: we put data_tc, the type constructor gotten from the
1912 -- constructor type signature into the data constructor;
1913 -- that way checkValidDataCon can complain if it's wrong.
1914 }
1915 ; traceTc "tcConDecl 2" (ppr name)
1916 ; mapM buildOneDataCon [name]
1917 }
1918 where
1919 skol_info = SigTypeSkol (ConArgCtxt (unLoc name))
1920
1921 tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
1922 (ConDeclGADT { con_names = names
1923 , con_qvars = qtvs
1924 , con_mb_cxt = cxt, con_args = hs_args
1925 , con_res_ty = res_ty })
1926 | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = implicit_tkv_nms }
1927 , hsq_explicit = explicit_tkv_nms } <- qtvs
1928 = addErrCtxt (dataConCtxtName names) $
1929 do { traceTc "tcConDecl 1" (ppr names)
1930 ; let (L _ name : _) = names
1931 skol_info = DataConSkol name
1932
1933 ; (imp_tvs, (exp_tvs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))
1934 <- solveEqualities $
1935 tcImplicitTKBndrs skol_info implicit_tkv_nms $
1936 tcExplicitTKBndrs skol_info explicit_tkv_nms $
1937 do { ctxt <- tcHsMbContext cxt
1938 ; btys <- tcConArgs hs_args
1939 ; res_ty' <- tcHsLiftedType res_ty
1940 ; field_lbls <- lookupConstructorFields name
1941 ; let (arg_tys, stricts) = unzip btys
1942 ; return (ctxt, arg_tys, res_ty', field_lbls, stricts)
1943 }
1944 ; let user_tvs = imp_tvs ++ exp_tvs
1945
1946 ; tkvs <- quantifyConDecl emptyVarSet (mkSpecForAllTys user_tvs $
1947 mkFunTys ctxt $
1948 mkFunTys arg_tys $
1949 res_ty)
1950
1951 -- Zonk to Types
1952 ; (ze, tkvs) <- zonkTyBndrsX emptyZonkEnv tkvs
1953 ; (ze, user_tvs) <- zonkTyBndrsX ze user_tvs
1954 ; arg_tys <- zonkTcTypeToTypes ze arg_tys
1955 ; ctxt <- zonkTcTypeToTypes ze ctxt
1956 ; res_ty <- zonkTcTypeToType ze res_ty
1957
1958 ; let (univ_tvs, ex_tvs, tkvs', user_tvs', eq_preds, arg_subst)
1959 = rejigConRes tmpl_bndrs res_tmpl tkvs user_tvs res_ty
1960 -- NB: this is a /lazy/ binding, so we pass six thunks to
1961 -- buildDataCon without yet forcing the guards in rejigConRes
1962 -- See Note [Checking GADT return types]
1963
1964 -- Compute the user-written tyvar binders. These have the same
1965 -- tyvars as univ_tvs/ex_tvs, but perhaps in a different order.
1966 -- See Note [DataCon user type variable binders] in DataCon.
1967 tkv_bndrs = mkTyVarBinders Inferred tkvs'
1968 user_tv_bndrs = mkTyVarBinders Specified user_tvs'
1969 all_user_bndrs = tkv_bndrs ++ user_tv_bndrs
1970
1971 ctxt' = substTys arg_subst ctxt
1972 arg_tys' = substTys arg_subst arg_tys
1973 res_ty' = substTy arg_subst res_ty
1974
1975
1976 ; fam_envs <- tcGetFamInstEnvs
1977
1978 -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
1979 ; traceTc "tcConDecl 2" (ppr names $$ ppr field_lbls)
1980 ; let
1981 buildOneDataCon (L _ name) = do
1982 { is_infix <- tcConIsInfixGADT name hs_args
1983 ; rep_nm <- newTyConRepName name
1984
1985 ; buildDataCon fam_envs name is_infix
1986 rep_nm
1987 stricts Nothing field_lbls
1988 univ_tvs ex_tvs all_user_bndrs eq_preds
1989 ctxt' arg_tys' res_ty' rep_tycon tag_map
1990 -- NB: we put data_tc, the type constructor gotten from the
1991 -- constructor type signature into the data constructor;
1992 -- that way checkValidDataCon can complain if it's wrong.
1993 }
1994 ; traceTc "tcConDecl 2" (ppr names)
1995 ; mapM buildOneDataCon names
1996 }
1997 tcConDecl _ _ _ _ (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _)
1998 = panic "tcConDecl"
1999 tcConDecl _ _ _ _ (XConDecl _) = panic "tcConDecl"
2000
2001 -- | Produce the telescope of kind variables that this datacon is
2002 -- implicitly quantified over. Incoming type need not be zonked.
2003 quantifyConDecl :: TcTyCoVarSet -- outer tvs, not to be quantified over; zonked
2004 -> TcType -> TcM [TcTyVar]
2005 quantifyConDecl gbl_tvs ty
2006 = do { ty <- zonkTcTypeInKnot ty
2007 ; let fvs = candidateQTyVarsOfType ty
2008 ; quantifyTyVars gbl_tvs fvs }
2009
2010 tcConIsInfixH98 :: Name
2011 -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn])
2012 -> TcM Bool
2013 tcConIsInfixH98 _ details
2014 = case details of
2015 InfixCon {} -> return True
2016 _ -> return False
2017
2018 tcConIsInfixGADT :: Name
2019 -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn])
2020 -> TcM Bool
2021 tcConIsInfixGADT con details
2022 = case details of
2023 InfixCon {} -> return True
2024 RecCon {} -> return False
2025 PrefixCon arg_tys -- See Note [Infix GADT constructors]
2026 | isSymOcc (getOccName con)
2027 , [_ty1,_ty2] <- arg_tys
2028 -> do { fix_env <- getFixityEnv
2029 ; return (con `elemNameEnv` fix_env) }
2030 | otherwise -> return False
2031
2032 tcConArgs :: HsConDeclDetails GhcRn
2033 -> TcM [(TcType, HsSrcBang)]
2034 tcConArgs (PrefixCon btys)
2035 = mapM tcConArg btys
2036 tcConArgs (InfixCon bty1 bty2)
2037 = do { bty1' <- tcConArg bty1
2038 ; bty2' <- tcConArg bty2
2039 ; return [bty1', bty2'] }
2040 tcConArgs (RecCon fields)
2041 = mapM tcConArg btys
2042 where
2043 -- We need a one-to-one mapping from field_names to btys
2044 combined = map (\(L _ f) -> (cd_fld_names f,cd_fld_type f)) (unLoc fields)
2045 explode (ns,ty) = zip ns (repeat ty)
2046 exploded = concatMap explode combined
2047 (_,btys) = unzip exploded
2048
2049
2050 tcConArg :: LHsType GhcRn -> TcM (TcType, HsSrcBang)
2051 tcConArg bty
2052 = do { traceTc "tcConArg 1" (ppr bty)
2053 ; arg_ty <- tcHsOpenType (getBangType bty)
2054 -- Newtypes can't have unboxed types, but we check
2055 -- that in checkValidDataCon; this tcConArg stuff
2056 -- doesn't happen for GADT-style declarations
2057 ; traceTc "tcConArg 2" (ppr bty)
2058 ; return (arg_ty, getBangStrictness bty) }
2059
2060 {-
2061 Note [Infix GADT constructors]
2062 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2063 We do not currently have syntax to declare an infix constructor in GADT syntax,
2064 but it makes a (small) difference to the Show instance. So as a slightly
2065 ad-hoc solution, we regard a GADT data constructor as infix if
2066 a) it is an operator symbol
2067 b) it has two arguments
2068 c) there is a fixity declaration for it
2069 For example:
2070 infix 6 (:--:)
2071 data T a where
2072 (:--:) :: t1 -> t2 -> T Int
2073
2074
2075 Note [Checking GADT return types]
2076 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2077 There is a delicacy around checking the return types of a datacon. The
2078 central problem is dealing with a declaration like
2079
2080 data T a where
2081 MkT :: T a -> Q a
2082
2083 Note that the return type of MkT is totally bogus. When creating the T
2084 tycon, we also need to create the MkT datacon, which must have a "rejigged"
2085 return type. That is, the MkT datacon's type must be transformed to have
2086 a uniform return type with explicit coercions for GADT-like type parameters.
2087 This rejigging is what rejigConRes does. The problem is, though, that checking
2088 that the return type is appropriate is much easier when done over *Type*,
2089 not *HsType*, and doing a call to tcMatchTy will loop because T isn't fully
2090 defined yet.
2091
2092 So, we want to make rejigConRes lazy and then check the validity of
2093 the return type in checkValidDataCon. To do this we /always/ return a
2094 6-tuple from rejigConRes (so that we can compute the return type from it, which
2095 checkValidDataCon needs), but the first three fields may be bogus if
2096 the return type isn't valid (the last equation for rejigConRes).
2097
2098 This is better than an earlier solution which reduced the number of
2099 errors reported in one pass. See Trac #7175, and #10836.
2100 -}
2101
2102 -- Example
2103 -- data instance T (b,c) where
2104 -- TI :: forall e. e -> T (e,e)
2105 --
2106 -- The representation tycon looks like this:
2107 -- data :R7T b c where
2108 -- TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
2109 -- In this case orig_res_ty = T (e,e)
2110
2111 rejigConRes :: [TyConBinder] -> Type -- Template for result type; e.g.
2112 -- data instance T [a] b c ...
2113 -- gives template ([a,b,c], T [a] b c)
2114 -- Type must be of kind *!
2115 -> [TyVar] -- The constructor's user-written, inferred
2116 -- type variables
2117 -> [TyVar] -- The constructor's user-written, specified
2118 -- type variables
2119 -> Type -- res_ty type must be of kind *
2120 -> ([TyVar], -- Universal
2121 [TyVar], -- Existential (distinct OccNames from univs)
2122 [TyVar], -- The constructor's rejigged, user-written,
2123 -- inferred type variables
2124 [TyVar], -- The constructor's rejigged, user-written,
2125 -- specified type variables
2126 [EqSpec], -- Equality predicates
2127 TCvSubst) -- Substitution to apply to argument types
2128 -- We don't check that the TyCon given in the ResTy is
2129 -- the same as the parent tycon, because checkValidDataCon will do it
2130
2131 rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty
2132 -- E.g. data T [a] b c where
2133 -- MkT :: forall x y z. T [(x,y)] z z
2134 -- The {a,b,c} are the tmpl_tvs, and the {x,y,z} are the dc_tvs
2135 -- (NB: unlike the H98 case, the dc_tvs are not all existential)
2136 -- Then we generate
2137 -- Univ tyvars Eq-spec
2138 -- a a~(x,y)
2139 -- b b~z
2140 -- z
2141 -- Existentials are the leftover type vars: [x,y]
2142 -- The user-written type variables are what is listed in the forall:
2143 -- [x, y, z] (all specified). We must rejig these as well.
2144 -- See Note [DataCon user type variable binders] in DataCon.
2145 -- So we return ( [a,b,z], [x,y]
2146 -- , [], [x,y,z]
2147 -- , [a~(x,y),b~z], <arg-subst> )
2148 | Just subst <- ASSERT( isLiftedTypeKind (typeKind res_ty) )
2149 ASSERT( isLiftedTypeKind (typeKind res_tmpl) )
2150 tcMatchTy res_tmpl res_ty
2151 = let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tmpl_tvs dc_tvs subst
2152 raw_ex_tvs = dc_tvs `minusList` univ_tvs
2153 (arg_subst, substed_ex_tvs) = substTyVarBndrs kind_subst raw_ex_tvs
2154
2155 -- After rejigging the existential tyvars, the resulting substitution
2156 -- gives us exactly what we need to rejig the user-written tyvars,
2157 -- since the dcUserTyVarBinders invariant guarantees that the
2158 -- substitution has *all* the tyvars in its domain.
2159 -- See Note [DataCon user type variable binders] in DataCon.
2160 subst_user_tvs = map (getTyVar "rejigConRes" . substTyVar arg_subst)
2161 substed_inferred_tvs = subst_user_tvs dc_inferred_tvs
2162 substed_specified_tvs = subst_user_tvs dc_specified_tvs
2163
2164 substed_eqs = map (substEqSpec arg_subst) raw_eqs
2165 in
2166 (univ_tvs, substed_ex_tvs, substed_inferred_tvs, substed_specified_tvs,
2167 substed_eqs, arg_subst)
2168
2169 | otherwise
2170 -- If the return type of the data constructor doesn't match the parent
2171 -- type constructor, or the arity is wrong, the tcMatchTy will fail
2172 -- e.g data T a b where
2173 -- T1 :: Maybe a -- Wrong tycon
2174 -- T2 :: T [a] -- Wrong arity
2175 -- We are detect that later, in checkValidDataCon, but meanwhile
2176 -- we must do *something*, not just crash. So we do something simple
2177 -- albeit bogus, relying on checkValidDataCon to check the
2178 -- bad-result-type error before seeing that the other fields look odd
2179 -- See Note [Checking GADT return types]
2180 = (tmpl_tvs, dc_tvs `minusList` tmpl_tvs, dc_inferred_tvs, dc_specified_tvs,
2181 [], emptyTCvSubst)
2182 where
2183 dc_tvs = dc_inferred_tvs ++ dc_specified_tvs
2184 tmpl_tvs = binderVars tmpl_bndrs
2185
2186 {- Note [mkGADTVars]
2187 ~~~~~~~~~~~~~~~~~~~~
2188 Running example:
2189
2190 data T (k1 :: *) (k2 :: *) (a :: k2) (b :: k2) where
2191 MkT :: forall (x1 : *) (y :: x1) (z :: *).
2192 T x1 * (Proxy (y :: x1), z) z
2193
2194 We need the rejigged type to be
2195
2196 MkT :: forall (x1 :: *) (k2 :: *) (a :: k2) (b :: k2).
2197 forall (y :: x1) (z :: *).
2198 (k2 ~ *, a ~ (Proxy x1 y, z), b ~ z)
2199 => T x1 k2 a b
2200
2201 You might naively expect that z should become a universal tyvar,
2202 not an existential. (After all, x1 becomes a universal tyvar.)
2203 But z has kind * while b has kind k2, so the return type
2204 T x1 k2 a z
2205 is ill-kinded. Another way to say it is this: the universal
2206 tyvars must have exactly the same kinds as the tyConTyVars.
2207
2208 So we need an existential tyvar and a heterogeneous equality
2209 constraint. (The b ~ z is a bit redundant with the k2 ~ * that
2210 comes before in that b ~ z implies k2 ~ *. I'm sure we could do
2211 some analysis that could eliminate k2 ~ *. But we don't do this
2212 yet.)
2213
2214 The data con signature has already been fully kind-checked.
2215 The return type
2216
2217 T x1 * (Proxy (y :: x1), z) z
2218 becomes
2219 qtkvs = [x1 :: *, y :: x1, z :: *]
2220 res_tmpl = T x1 * (Proxy x1 y, z) z
2221
2222 We start off by matching (T k1 k2 a b) with (T x1 * (Proxy x1 y, z) z). We
2223 know this match will succeed because of the validity check (actually done
2224 later, but laziness saves us -- see Note [Checking GADT return types]).
2225 Thus, we get
2226
2227 subst := { k1 |-> x1, k2 |-> *, a |-> (Proxy x1 y, z), b |-> z }
2228
2229 Now, we need to figure out what the GADT equalities should be. In this case,
2230 we *don't* want (k1 ~ x1) to be a GADT equality: it should just be a
2231 renaming. The others should be GADT equalities. We also need to make
2232 sure that the universally-quantified variables of the datacon match up
2233 with the tyvars of the tycon, as required for Core context well-formedness.
2234 (This last bit is why we have to rejig at all!)
2235
2236 `choose` walks down the tycon tyvars, figuring out what to do with each one.
2237 It carries two substitutions:
2238 - t_sub's domain is *template* or *tycon* tyvars, mapping them to variables
2239 mentioned in the datacon signature.
2240 - r_sub's domain is *result* tyvars, names written by the programmer in
2241 the datacon signature. The final rejigged type will use these names, but
2242 the subst is still needed because sometimes the printed name of these variables
2243 is different. (See choose_tv_name, below.)
2244
2245 Before explaining the details of `choose`, let's just look at its operation
2246 on our example:
2247
2248 choose [] [] {} {} [k1, k2, a, b]
2249 --> -- first branch of `case` statement
2250 choose
2251 univs: [x1 :: *]
2252 eq_spec: []
2253 t_sub: {k1 |-> x1}
2254 r_sub: {x1 |-> x1}
2255 t_tvs: [k2, a, b]
2256 --> -- second branch of `case` statement
2257 choose
2258 univs: [k2 :: *, x1 :: *]
2259 eq_spec: [k2 ~ *]
2260 t_sub: {k1 |-> x1, k2 |-> k2}
2261 r_sub: {x1 |-> x1}
2262 t_tvs: [a, b]
2263 --> -- second branch of `case` statement
2264 choose
2265 univs: [a :: k2, k2 :: *, x1 :: *]
2266 eq_spec: [ a ~ (Proxy x1 y, z)
2267 , k2 ~ * ]
2268 t_sub: {k1 |-> x1, k2 |-> k2, a |-> a}
2269 r_sub: {x1 |-> x1}
2270 t_tvs: [b]
2271 --> -- second branch of `case` statement
2272 choose
2273 univs: [b :: k2, a :: k2, k2 :: *, x1 :: *]
2274 eq_spec: [ b ~ z
2275 , a ~ (Proxy x1 y, z)
2276 , k2 ~ * ]
2277 t_sub: {k1 |-> x1, k2 |-> k2, a |-> a, b |-> z}
2278 r_sub: {x1 |-> x1}
2279 t_tvs: []
2280 --> -- end of recursion
2281 ( [x1 :: *, k2 :: *, a :: k2, b :: k2]
2282 , [k2 ~ *, a ~ (Proxy x1 y, z), b ~ z]
2283 , {x1 |-> x1} )
2284
2285 `choose` looks up each tycon tyvar in the matching (it *must* be matched!).
2286
2287 * If it finds a bare result tyvar (the first branch of the `case`
2288 statement), it checks to make sure that the result tyvar isn't yet
2289 in the list of univ_tvs. If it is in that list, then we have a
2290 repeated variable in the return type, and we in fact need a GADT
2291 equality.
2292
2293 * It then checks to make sure that the kind of the result tyvar
2294 matches the kind of the template tyvar. This check is what forces
2295 `z` to be existential, as it should be, explained above.
2296
2297 * Assuming no repeated variables or kind-changing, we wish to use the
2298 variable name given in the datacon signature (that is, `x1` not
2299 `k1`), not the tycon signature (which may have been made up by
2300 GHC). So, we add a mapping from the tycon tyvar to the result tyvar
2301 to t_sub.
2302
2303 * If we discover that a mapping in `subst` gives us a non-tyvar (the
2304 second branch of the `case` statement), then we have a GADT equality
2305 to create. We create a fresh equality, but we don't extend any
2306 substitutions. The template variable substitution is meant for use
2307 in universal tyvar kinds, and these shouldn't be affected by any
2308 GADT equalities.
2309
2310 This whole algorithm is quite delicate, indeed. I (Richard E.) see two ways
2311 of simplifying it:
2312
2313 1) The first branch of the `case` statement is really an optimization, used
2314 in order to get fewer GADT equalities. It might be possible to make a GADT
2315 equality for *every* univ. tyvar, even if the equality is trivial, and then
2316 either deal with the bigger type or somehow reduce it later.
2317
2318 2) This algorithm strives to use the names for type variables as specified
2319 by the user in the datacon signature. If we always used the tycon tyvar
2320 names, for example, this would be simplified. This change would almost
2321 certainly degrade error messages a bit, though.
2322 -}
2323
2324 -- ^ From information about a source datacon definition, extract out
2325 -- what the universal variables and the GADT equalities should be.
2326 -- See Note [mkGADTVars].
2327 mkGADTVars :: [TyVar] -- ^ The tycon vars
2328 -> [TyVar] -- ^ The datacon vars
2329 -> TCvSubst -- ^ The matching between the template result type
2330 -- and the actual result type
2331 -> ( [TyVar]
2332 , [EqSpec]
2333 , TCvSubst ) -- ^ The univ. variables, the GADT equalities,
2334 -- and a subst to apply to the GADT equalities
2335 -- and existentials.
2336 mkGADTVars tmpl_tvs dc_tvs subst
2337 = choose [] [] empty_subst empty_subst tmpl_tvs
2338 where
2339 in_scope = mkInScopeSet (mkVarSet tmpl_tvs `unionVarSet` mkVarSet dc_tvs)
2340 `unionInScope` getTCvInScope subst
2341 empty_subst = mkEmptyTCvSubst in_scope
2342
2343 choose :: [TyVar] -- accumulator of univ tvs, reversed
2344 -> [EqSpec] -- accumulator of GADT equalities, reversed
2345 -> TCvSubst -- template substitution
2346 -> TCvSubst -- res. substitution
2347 -> [TyVar] -- template tvs (the univ tvs passed in)
2348 -> ( [TyVar] -- the univ_tvs
2349 , [EqSpec] -- GADT equalities
2350 , TCvSubst ) -- a substitution to fix kinds in ex_tvs
2351
2352 choose univs eqs _t_sub r_sub []
2353 = (reverse univs, reverse eqs, r_sub)
2354 choose univs eqs t_sub r_sub (t_tv:t_tvs)
2355 | Just r_ty <- lookupTyVar subst t_tv
2356 = case getTyVar_maybe r_ty of
2357 Just r_tv
2358 | not (r_tv `elem` univs)
2359 , tyVarKind r_tv `eqType` (substTy t_sub (tyVarKind t_tv))
2360 -> -- simple, well-kinded variable substitution.
2361 choose (r_tv:univs) eqs
2362 (extendTvSubst t_sub t_tv r_ty')
2363 (extendTvSubst r_sub r_tv r_ty')
2364 t_tvs
2365 where
2366 r_tv1 = setTyVarName r_tv (choose_tv_name r_tv t_tv)
2367 r_ty' = mkTyVarTy r_tv1
2368
2369 -- Not a simple substitution: make an equality predicate
2370 _ -> choose (t_tv':univs) (mkEqSpec t_tv' r_ty : eqs)
2371 (extendTvSubst t_sub t_tv (mkTyVarTy t_tv'))
2372 -- We've updated the kind of t_tv,
2373 -- so add it to t_sub (Trac #14162)
2374 r_sub t_tvs
2375 where
2376 t_tv' = updateTyVarKind (substTy t_sub) t_tv
2377
2378 | otherwise
2379 = pprPanic "mkGADTVars" (ppr tmpl_tvs $$ ppr subst)
2380
2381 -- choose an appropriate name for a univ tyvar.
2382 -- This *must* preserve the Unique of the result tv, so that we
2383 -- can detect repeated variables. It prefers user-specified names
2384 -- over system names. A result variable with a system name can
2385 -- happen with GHC-generated implicit kind variables.
2386 choose_tv_name :: TyVar -> TyVar -> Name
2387 choose_tv_name r_tv t_tv
2388 | isSystemName r_tv_name
2389 = setNameUnique t_tv_name (getUnique r_tv_name)
2390
2391 | otherwise
2392 = r_tv_name
2393
2394 where
2395 r_tv_name = getName r_tv
2396 t_tv_name = getName t_tv
2397
2398 {-
2399 Note [Substitution in template variables kinds]
2400 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2401
2402 data G (a :: Maybe k) where
2403 MkG :: G Nothing
2404
2405 With explicit kind variables
2406
2407 data G k (a :: Maybe k) where
2408 MkG :: G k1 (Nothing k1)
2409
2410 Note how k1 is distinct from k. So, when we match the template
2411 `G k a` against `G k1 (Nothing k1)`, we get a subst
2412 [ k |-> k1, a |-> Nothing k1 ]. Even though this subst has two
2413 mappings, we surely don't want to add (k, k1) to the list of
2414 GADT equalities -- that would be overly complex and would create
2415 more untouchable variables than we need. So, when figuring out
2416 which tyvars are GADT-like and which aren't (the fundamental
2417 job of `choose`), we want to treat `k` as *not* GADT-like.
2418 Instead, we wish to substitute in `a`'s kind, to get (a :: Maybe k1)
2419 instead of (a :: Maybe k). This is the reason for dealing
2420 with a substitution in here.
2421
2422 However, we do not *always* want to substitute. Consider
2423
2424 data H (a :: k) where
2425 MkH :: H Int
2426
2427 With explicit kind variables:
2428
2429 data H k (a :: k) where
2430 MkH :: H * Int
2431
2432 Here, we have a kind-indexed GADT. The subst in question is
2433 [ k |-> *, a |-> Int ]. Now, we *don't* want to substitute in `a`'s
2434 kind, because that would give a constructor with the type
2435
2436 MkH :: forall (k :: *) (a :: *). (k ~ *) -> (a ~ Int) -> H k a
2437
2438 The problem here is that a's kind is wrong -- it needs to be k, not *!
2439 So, if the matching for a variable is anything but another bare variable,
2440 we drop the mapping from the substitution before proceeding. This
2441 was not an issue before kind-indexed GADTs because this case could
2442 never happen.
2443
2444 ************************************************************************
2445 * *
2446 Validity checking
2447 * *
2448 ************************************************************************
2449
2450 Validity checking is done once the mutually-recursive knot has been
2451 tied, so we can look at things freely.
2452 -}
2453
2454 checkValidTyCl :: TyCon -> TcM [TyCon]
2455 -- The returned list is either a singleton (if valid)
2456 -- or a list of "fake tycons" (if not); the fake tycons
2457 -- include any implicits, like promoted data constructors
2458 -- See Note [Recover from validity error]
2459 checkValidTyCl tc
2460 = setSrcSpan (getSrcSpan tc) $
2461 addTyConCtxt tc $
2462 recoverM recovery_code
2463 (do { traceTc "Starting validity for tycon" (ppr tc)
2464 ; checkValidTyCon tc
2465 ; traceTc "Done validity for tycon" (ppr tc)
2466 ; return [tc] })
2467 where
2468 recovery_code -- See Note [Recover from validity error]
2469 = do { traceTc "Aborted validity for tycon" (ppr tc)
2470 ; return (concatMap mk_fake_tc $
2471 ATyCon tc : implicitTyConThings tc) }
2472
2473 mk_fake_tc (ATyCon tc)
2474 | isClassTyCon tc = [tc] -- Ugh! Note [Recover from validity error]
2475 | otherwise = [makeRecoveryTyCon tc]
2476 mk_fake_tc (AConLike (RealDataCon dc))
2477 = [makeRecoveryTyCon (promoteDataCon dc)]
2478 mk_fake_tc _ = []
2479
2480 {- Note [Recover from validity error]
2481 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2482 We recover from a validity error in a type or class, which allows us
2483 to report multiple validity errors. In the failure case we return a
2484 TyCon of the right kind, but with no interesting behaviour
2485 (makeRecoveryTyCon). Why? Suppose we have
2486 type T a = Fun
2487 where Fun is a type family of arity 1. The RHS is invalid, but we
2488 want to go on checking validity of subsequent type declarations.
2489 So we replace T with an abstract TyCon which will do no harm.
2490 See indexed-types/should_fail/BadSock and Trac #10896
2491
2492 Some notes:
2493
2494 * We must make fakes for promoted DataCons too. Consider (Trac #15215)
2495 data T a = MkT ...
2496 data S a = ...T...MkT....
2497 If there is an error in the definition of 'T' we add a "fake type
2498 constructor" to the type environment, so that we can continue to
2499 typecheck 'S'. But we /were not/ adding a fake anything for 'MkT'
2500 and so there was an internal error when we met 'MkT' in the body of
2501 'S'.
2502
2503 * Painfully, we *don't* want to do this for classes.
2504 Consider tcfail041:
2505 class (?x::Int) => C a where ...
2506 instance C Int
2507 The class is invalid because of the superclass constraint. But
2508 we still want it to look like a /class/, else the instance bleats
2509 that the instance is mal-formed because it hasn't got a class in
2510 the head.
2511
2512 This is really bogus; now we have in scope a Class that is invalid
2513 in some way, with unknown downstream consequences. A better
2514 alterantive might be to make a fake class TyCon. A job for another day.
2515 -}
2516
2517 -------------------------
2518 -- For data types declared with record syntax, we require
2519 -- that each constructor that has a field 'f'
2520 -- (a) has the same result type
2521 -- (b) has the same type for 'f'
2522 -- module alpha conversion of the quantified type variables
2523 -- of the constructor.
2524 --
2525 -- Note that we allow existentials to match because the
2526 -- fields can never meet. E.g
2527 -- data T where
2528 -- T1 { f1 :: b, f2 :: a, f3 ::Int } :: T
2529 -- T2 { f1 :: c, f2 :: c, f3 ::Int } :: T
2530 -- Here we do not complain about f1,f2 because they are existential
2531
2532 checkValidTyCon :: TyCon -> TcM ()
2533 checkValidTyCon tc
2534 | isPrimTyCon tc -- Happens when Haddock'ing GHC.Prim
2535 = return ()
2536
2537 | otherwise
2538 = do { traceTc "checkValidTyCon" (ppr tc $$ ppr (tyConClass_maybe tc))
2539 ; if | Just cl <- tyConClass_maybe tc
2540 -> checkValidClass cl
2541
2542 | Just syn_rhs <- synTyConRhs_maybe tc
2543 -> do { checkValidType syn_ctxt syn_rhs
2544 ; checkTySynRhs syn_ctxt syn_rhs }
2545
2546 | Just fam_flav <- famTyConFlav_maybe tc
2547 -> case fam_flav of
2548 { ClosedSynFamilyTyCon (Just ax)
2549 -> tcAddClosedTypeFamilyDeclCtxt tc $
2550 checkValidCoAxiom ax
2551 ; ClosedSynFamilyTyCon Nothing -> return ()
2552 ; AbstractClosedSynFamilyTyCon ->
2553 do { hsBoot <- tcIsHsBootOrSig
2554 ; checkTc hsBoot $
2555 text "You may define an abstract closed type family" $$
2556 text "only in a .hs-boot file" }
2557 ; DataFamilyTyCon {} -> return ()
2558 ; OpenSynFamilyTyCon -> return ()
2559 ; BuiltInSynFamTyCon _ -> return () }
2560
2561 | otherwise -> do
2562 { -- Check the context on the data decl
2563 traceTc "cvtc1" (ppr tc)
2564 ; checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc)
2565
2566 ; traceTc "cvtc2" (ppr tc)
2567
2568 ; dflags <- getDynFlags
2569 ; existential_ok <- xoptM LangExt.ExistentialQuantification
2570 ; gadt_ok <- xoptM LangExt.GADTs
2571 ; let ex_ok = existential_ok || gadt_ok
2572 -- Data cons can have existential context
2573 ; mapM_ (checkValidDataCon dflags ex_ok tc) data_cons
2574 ; mapM_ (checkPartialRecordField data_cons) (tyConFieldLabels tc)
2575
2576 -- Check that fields with the same name share a type
2577 ; mapM_ check_fields groups }}
2578 where
2579 syn_ctxt = TySynCtxt name
2580 name = tyConName tc
2581 data_cons = tyConDataCons tc
2582
2583 groups = equivClasses cmp_fld (concatMap get_fields data_cons)
2584 cmp_fld (f1,_) (f2,_) = flLabel f1 `compare` flLabel f2
2585 get_fields con = dataConFieldLabels con `zip` repeat con
2586 -- dataConFieldLabels may return the empty list, which is fine
2587
2588 -- See Note [GADT record selectors] in TcTyDecls
2589 -- We must check (a) that the named field has the same
2590 -- type in each constructor
2591 -- (b) that those constructors have the same result type
2592 --
2593 -- However, the constructors may have differently named type variable
2594 -- and (worse) we don't know how the correspond to each other. E.g.
2595 -- C1 :: forall a b. { f :: a, g :: b } -> T a b
2596 -- C2 :: forall d c. { f :: c, g :: c } -> T c d
2597 --
2598 -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
2599 -- result type against other candidates' types BOTH WAYS ROUND.
2600 -- If they magically agrees, take the substitution and
2601 -- apply them to the latter ones, and see if they match perfectly.
2602 check_fields ((label, con1) :| other_fields)
2603 -- These fields all have the same name, but are from
2604 -- different constructors in the data type
2605 = recoverM (return ()) $ mapM_ checkOne other_fields
2606 -- Check that all the fields in the group have the same type
2607 -- NB: this check assumes that all the constructors of a given
2608 -- data type use the same type variables
2609 where
2610 (_, _, _, res1) = dataConSig con1
2611 fty1 = dataConFieldType con1 lbl
2612 lbl = flLabel label
2613
2614 checkOne (_, con2) -- Do it both ways to ensure they are structurally identical
2615 = do { checkFieldCompat lbl con1 con2 res1 res2 fty1 fty2
2616 ; checkFieldCompat lbl con2 con1 res2 res1 fty2 fty1 }
2617 where
2618 (_, _, _, res2) = dataConSig con2
2619 fty2 = dataConFieldType con2 lbl
2620
2621 checkPartialRecordField :: [DataCon] -> FieldLabel -> TcM ()
2622 -- Checks the partial record field selector, and warns.
2623 -- See Note [Checking partial record field]
2624 checkPartialRecordField all_cons fld
2625 = setSrcSpan loc $
2626 warnIfFlag Opt_WarnPartialFields
2627 (not is_exhaustive && not (startsWithUnderscore occ_name))
2628 (sep [text "Use of partial record field selector" <> colon,
2629 nest 2 $ quotes (ppr occ_name)])
2630 where
2631 sel_name = flSelector fld
2632 loc = getSrcSpan sel_name
2633 occ_name = getOccName sel_name
2634
2635 (cons_with_field, cons_without_field) = partition has_field all_cons
2636 has_field con = fld `elem` (dataConFieldLabels con)
2637 is_exhaustive = all (dataConCannotMatch inst_tys) cons_without_field
2638
2639 con1 = ASSERT( not (null cons_with_field) ) head cons_with_field
2640 (univ_tvs, _, eq_spec, _, _, _) = dataConFullSig con1
2641 eq_subst = mkTvSubstPrs (map eqSpecPair eq_spec)
2642 inst_tys = substTyVars eq_subst univ_tvs
2643
2644 checkFieldCompat :: FieldLabelString -> DataCon -> DataCon
2645 -> Type -> Type -> Type -> Type -> TcM ()
2646 checkFieldCompat fld con1 con2 res1 res2 fty1 fty2
2647 = do { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
2648 ; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
2649 where
2650 mb_subst1 = tcMatchTy res1 res2
2651 mb_subst2 = tcMatchTyX (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
2652
2653 -------------------------------
2654 checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM ()
2655 checkValidDataCon dflags existential_ok tc con
2656 = setSrcSpan (getSrcSpan con) $
2657 addErrCtxt (dataConCtxt con) $
2658 do { -- Check that the return type of the data constructor
2659 -- matches the type constructor; eg reject this:
2660 -- data T a where { MkT :: Bogus a }
2661 -- It's important to do this first:
2662 -- see Note [Checking GADT return types]
2663 -- and c.f. Note [Check role annotations in a second pass]
2664 let tc_tvs = tyConTyVars tc
2665 res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
2666 orig_res_ty = dataConOrigResTy con
2667 ; traceTc "checkValidDataCon" (vcat
2668 [ ppr con, ppr tc, ppr tc_tvs
2669 , ppr res_ty_tmpl <+> dcolon <+> ppr (typeKind res_ty_tmpl)
2670 , ppr orig_res_ty <+> dcolon <+> ppr (typeKind orig_res_ty)])
2671
2672
2673 ; checkTc (isJust (tcMatchTy res_ty_tmpl
2674 orig_res_ty))
2675 (badDataConTyCon con res_ty_tmpl orig_res_ty)
2676 -- Note that checkTc aborts if it finds an error. This is
2677 -- critical to avoid panicking when we call dataConUserType
2678 -- on an un-rejiggable datacon!
2679
2680 ; traceTc "checkValidDataCon 2" (ppr (dataConUserType con))
2681
2682 -- Check that the result type is a *monotype*
2683 -- e.g. reject this: MkT :: T (forall a. a->a)
2684 -- Reason: it's really the argument of an equality constraint
2685 ; checkValidMonoType orig_res_ty
2686
2687 -- Check all argument types for validity
2688 ; checkValidType ctxt (dataConUserType con)
2689 ; mapM_ (checkForLevPoly empty)
2690 (dataConOrigArgTys con)
2691
2692 -- Extra checks for newtype data constructors
2693 ; when (isNewTyCon tc) (checkNewDataCon con)
2694
2695 -- Check that existentials are allowed if they are used
2696 ; checkTc (existential_ok || isVanillaDataCon con)
2697 (badExistential con)
2698
2699 -- Check that UNPACK pragmas and bangs work out
2700 -- E.g. reject data T = MkT {-# UNPACK #-} Int -- No "!"
2701 -- data T = MkT {-# UNPACK #-} !a -- Can't unpack
2702 ; zipWith3M_ check_bang (dataConSrcBangs con) (dataConImplBangs con) [1..]
2703
2704 ; traceTc "Done validity of data con" $
2705 vcat [ ppr con
2706 , text "Datacon user type:" <+> ppr (dataConUserType con)
2707 , text "Datacon rep type:" <+> ppr (dataConRepType con)
2708 , text "Rep typcon binders:" <+> ppr (tyConBinders (dataConTyCon con))
2709 , case tyConFamInst_maybe (dataConTyCon con) of
2710 Nothing -> text "not family"
2711 Just (f, _) -> ppr (tyConBinders f) ]
2712 }
2713 where
2714 ctxt = ConArgCtxt (dataConName con)
2715
2716 check_bang :: HsSrcBang -> HsImplBang -> Int -> TcM ()
2717 check_bang (HsSrcBang _ _ SrcLazy) _ n
2718 | not (xopt LangExt.StrictData dflags)
2719 = addErrTc
2720 (bad_bang n (text "Lazy annotation (~) without StrictData"))
2721 check_bang (HsSrcBang _ want_unpack strict_mark) rep_bang n
2722 | isSrcUnpacked want_unpack, not is_strict
2723 = addWarnTc NoReason (bad_bang n (text "UNPACK pragma lacks '!'"))
2724 | isSrcUnpacked want_unpack
2725 , case rep_bang of { HsUnpack {} -> False; _ -> True }
2726 -- If not optimising, we don't unpack (rep_bang is never
2727 -- HsUnpack), so don't complain! This happens, e.g., in Haddock.
2728 -- See dataConSrcToImplBang.
2729 , not (gopt Opt_OmitInterfacePragmas dflags)
2730 -- When typechecking an indefinite package in Backpack, we
2731 -- may attempt to UNPACK an abstract type. The test here will
2732 -- conclude that this is unusable, but it might become usable
2733 -- when we actually fill in the abstract type. As such, don't
2734 -- warn in this case (it gives users the wrong idea about whether
2735 -- or not UNPACK on abstract types is supported; it is!)
2736 , unitIdIsDefinite (thisPackage dflags)
2737 = addWarnTc NoReason (bad_bang n (text "Ignoring unusable UNPACK pragma"))
2738 where
2739 is_strict = case strict_mark of
2740 NoSrcStrict -> xopt LangExt.StrictData dflags
2741 bang -> isSrcStrict bang
2742
2743 check_bang _ _ _
2744 = return ()
2745
2746 bad_bang n herald
2747 = hang herald 2 (text "on the" <+> speakNth n
2748 <+> text "argument of" <+> quotes (ppr con))
2749 -------------------------------
2750 checkNewDataCon :: DataCon -> TcM ()
2751 -- Further checks for the data constructor of a newtype
2752 checkNewDataCon con
2753 = do { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
2754 -- One argument
2755
2756 ; checkTc (not (isUnliftedType arg_ty1)) $
2757 text "A newtype cannot have an unlifted argument type"
2758
2759 ; check_con (null eq_spec) $
2760 text "A newtype constructor must have a return type of form T a1 ... an"
2761 -- Return type is (T a b c)
2762
2763 ; check_con (null theta) $
2764 text "A newtype constructor cannot have a context in its type"
2765
2766 ; check_con (null ex_tvs) $
2767 text "A newtype constructor cannot have existential type variables"
2768 -- No existentials
2769
2770 ; checkTc (all ok_bang (dataConSrcBangs con))
2771 (newtypeStrictError con)
2772 -- No strictness annotations
2773 }
2774 where
2775 (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
2776 = dataConFullSig con
2777 check_con what msg
2778 = checkTc what (msg $$ ppr con <+> dcolon <+> ppr (dataConUserType con))
2779
2780 (arg_ty1 : _) = arg_tys
2781
2782 ok_bang (HsSrcBang _ _ SrcStrict) = False
2783 ok_bang (HsSrcBang _ _ SrcLazy) = False
2784 ok_bang _ = True
2785
2786 -------------------------------
2787 checkValidClass :: Class -> TcM ()
2788 checkValidClass cls
2789 = do { constrained_class_methods <- xoptM LangExt.ConstrainedClassMethods
2790 ; multi_param_type_classes <- xoptM LangExt.MultiParamTypeClasses
2791 ; nullary_type_classes <- xoptM LangExt.NullaryTypeClasses
2792 ; fundep_classes <- xoptM LangExt.FunctionalDependencies
2793 ; undecidable_super_classes <- xoptM LangExt.UndecidableSuperClasses
2794
2795 -- Check that the class is unary, unless multiparameter type classes
2796 -- are enabled; also recognize deprecated nullary type classes
2797 -- extension (subsumed by multiparameter type classes, Trac #8993)
2798 ; checkTc (multi_param_type_classes || cls_arity == 1 ||
2799 (nullary_type_classes && cls_arity == 0))
2800 (classArityErr cls_arity cls)
2801 ; checkTc (fundep_classes || null fundeps) (classFunDepsErr cls)
2802
2803 -- Check the super-classes
2804 ; checkValidTheta (ClassSCCtxt (className cls)) theta
2805
2806 -- Now check for cyclic superclasses
2807 -- If there are superclass cycles, checkClassCycleErrs bails.
2808 ; unless undecidable_super_classes $
2809 case checkClassCycles cls of
2810 Just err -> setSrcSpan (getSrcSpan cls) $
2811 addErrTc err
2812 Nothing -> return ()
2813
2814 -- Check the class operations.
2815 -- But only if there have been no earlier errors
2816 -- See Note [Abort when superclass cycle is detected]
2817 ; whenNoErrs $
2818 mapM_ (check_op constrained_class_methods) op_stuff
2819
2820 -- Check the associated type defaults are well-formed and instantiated
2821 ; mapM_ check_at at_stuff }
2822 where
2823 (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
2824 cls_arity = length (tyConVisibleTyVars (classTyCon cls))
2825 -- Ignore invisible variables
2826 cls_tv_set = mkVarSet tyvars
2827 mini_env = zipVarEnv tyvars (mkTyVarTys tyvars)
2828 mb_cls = Just (cls, tyvars, mini_env)
2829
2830 check_op constrained_class_methods (sel_id, dm)
2831 = setSrcSpan (getSrcSpan sel_id) $
2832 addErrCtxt (classOpCtxt sel_id op_ty) $ do
2833 { traceTc "class op type" (ppr op_ty)
2834 ; checkValidType ctxt op_ty
2835 -- This implements the ambiguity check, among other things
2836 -- Example: tc223
2837 -- class Error e => Game b mv e | b -> mv e where
2838 -- newBoard :: MonadState b m => m ()
2839 -- Here, MonadState has a fundep m->b, so newBoard is fine
2840
2841 -- a method cannot be levity polymorphic, as we have to store the
2842 -- method in a dictionary
2843 -- example of what this prevents:
2844 -- class BoundedX (a :: TYPE r) where minBound :: a
2845 -- See Note [Levity polymorphism checking] in DsMonad
2846 ; checkForLevPoly empty tau1
2847
2848 ; unless constrained_class_methods $
2849 mapM_ check_constraint (tail (cls_pred:op_theta))
2850
2851 ; check_dm ctxt sel_id cls_pred tau2 dm
2852 }
2853 where
2854 ctxt = FunSigCtxt op_name True -- Report redundant class constraints
2855 op_name = idName sel_id
2856 op_ty = idType sel_id
2857 (_,cls_pred,tau1) = tcSplitMethodTy op_ty
2858 -- See Note [Splitting nested sigma types in class type signatures]
2859 (_,op_theta,tau2) = tcSplitNestedSigmaTys tau1
2860
2861 check_constraint :: TcPredType -> TcM ()
2862 check_constraint pred -- See Note [Class method constraints]
2863 = when (not (isEmptyVarSet pred_tvs) &&
2864 pred_tvs `subVarSet` cls_tv_set)
2865 (addErrTc (badMethPred sel_id pred))
2866 where
2867 pred_tvs = tyCoVarsOfType pred
2868
2869 check_at (ATI fam_tc m_dflt_rhs)
2870 = do { checkTc (cls_arity == 0 || any (`elemVarSet` cls_tv_set) fam_tvs)
2871 (noClassTyVarErr cls fam_tc)
2872 -- Check that the associated type mentions at least
2873 -- one of the class type variables
2874 -- The check is disabled for nullary type classes,
2875 -- since there is no possible ambiguity (Trac #10020)
2876
2877 -- Check that any default declarations for associated types are valid
2878 ; whenIsJust m_dflt_rhs $ \ (rhs, loc) ->
2879 checkValidTyFamEqn mb_cls fam_tc
2880 fam_tvs [] (mkTyVarTys fam_tvs) rhs pp_lhs loc }
2881 where
2882 fam_tvs = tyConTyVars fam_tc
2883 pp_lhs = ppr (mkTyConApp fam_tc (mkTyVarTys fam_tvs))
2884
2885 check_dm :: UserTypeCtxt -> Id -> PredType -> Type -> DefMethInfo -> TcM ()
2886 -- Check validity of the /top-level/ generic-default type
2887 -- E.g for class C a where
2888 -- default op :: forall b. (a~b) => blah
2889 -- we do not want to do an ambiguity check on a type with
2890 -- a free TyVar 'a' (Trac #11608). See TcType
2891 -- Note [TyVars and TcTyVars during type checking] in TcType
2892 -- Hence the mkDefaultMethodType to close the type.
2893 check_dm ctxt sel_id vanilla_cls_pred vanilla_tau
2894 (Just (dm_name, dm_spec@(GenericDM dm_ty)))
2895 = setSrcSpan (getSrcSpan dm_name) $ do
2896 -- We have carefully set the SrcSpan on the generic
2897 -- default-method Name to be that of the generic
2898 -- default type signature
2899
2900 -- First, we check that that the method's default type signature
2901 -- aligns with the non-default type signature.
2902 -- See Note [Default method type signatures must align]
2903 let cls_pred = mkClassPred cls $ mkTyVarTys $ classTyVars cls
2904 -- Note that the second field of this tuple contains the context
2905 -- of the default type signature, making it apparent that we
2906 -- ignore method contexts completely when validity-checking
2907 -- default type signatures. See the end of
2908 -- Note [Default method type signatures must align]
2909 -- to learn why this is OK.
2910 --
2911 -- See also
2912 -- Note [Splitting nested sigma types in class type signatures]
2913 -- for an explanation of why we don't use tcSplitSigmaTy here.
2914 (_, _, dm_tau) = tcSplitNestedSigmaTys dm_ty
2915
2916 -- Given this class definition:
2917 --
2918 -- class C a b where
2919 -- op :: forall p q. (Ord a, D p q)
2920 -- => a -> b -> p -> (a, b)
2921 -- default op :: forall r s. E r
2922 -- => a -> b -> s -> (a, b)
2923 --
2924 -- We want to match up two types of the form:
2925 --
2926 -- Vanilla type sig: C aa bb => aa -> bb -> p -> (aa, bb)
2927 -- Default type sig: C a b => a -> b -> s -> (a, b)
2928 --
2929 -- Notice that the two type signatures can be quantified over
2930 -- different class type variables! Therefore, it's important that
2931 -- we include the class predicate parts to match up a with aa and
2932 -- b with bb.
2933 vanilla_phi_ty = mkPhiTy [vanilla_cls_pred] vanilla_tau
2934 dm_phi_ty = mkPhiTy [cls_pred] dm_tau
2935
2936 traceTc "check_dm" $ vcat
2937 [ text "vanilla_phi_ty" <+> ppr vanilla_phi_ty
2938 , text "dm_phi_ty" <+> ppr dm_phi_ty ]
2939
2940 -- Actually checking that the types align is done with a call to
2941 -- tcMatchTys. We need to get a match in both directions to rule
2942 -- out degenerate cases like these:
2943 --
2944 -- class Foo a where
2945 -- foo1 :: a -> b
2946 -- default foo1 :: a -> Int
2947 --
2948 -- foo2 :: a -> Int
2949 -- default foo2 :: a -> b
2950 unless (isJust $ tcMatchTys [dm_phi_ty, vanilla_phi_ty]
2951 [vanilla_phi_ty, dm_phi_ty]) $ addErrTc $
2952 hang (text "The default type signature for"
2953 <+> ppr sel_id <> colon)
2954 2 (ppr dm_ty)
2955 $$ (text "does not match its corresponding"
2956 <+> text "non-default type signature")
2957
2958 -- Now do an ambiguity check on the default type signature.
2959 checkValidType ctxt (mkDefaultMethodType cls sel_id dm_spec)
2960 check_dm _ _ _ _ _ = return ()
2961
2962 checkFamFlag :: Name -> TcM ()
2963 -- Check that we don't use families without -XTypeFamilies
2964 -- The parser won't even parse them, but I suppose a GHC API
2965 -- client might have a go!
2966 checkFamFlag tc_name
2967 = do { idx_tys <- xoptM LangExt.TypeFamilies
2968 ; checkTc idx_tys err_msg }
2969 where
2970 err_msg = hang (text "Illegal family declaration for" <+> quotes (ppr tc_name))
2971 2 (text "Enable TypeFamilies to allow indexed type families")
2972
2973 {- Note [Class method constraints]
2974 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2975 Haskell 2010 is supposed to reject
2976 class C a where
2977 op :: Eq a => a -> a
2978 where the method type constrains only the class variable(s). (The extension
2979 -XConstrainedClassMethods switches off this check.) But regardless
2980 we should not reject
2981 class C a where
2982 op :: (?x::Int) => a -> a
2983 as pointed out in Trac #11793. So the test here rejects the program if
2984 * -XConstrainedClassMethods is off
2985 * the tyvars of the constraint are non-empty
2986 * all the tyvars are class tyvars, none are locally quantified
2987
2988 Note [Abort when superclass cycle is detected]
2989 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2990 We must avoid doing the ambiguity check for the methods (in
2991 checkValidClass.check_op) when there are already errors accumulated.
2992 This is because one of the errors may be a superclass cycle, and
2993 superclass cycles cause canonicalization to loop. Here is a
2994 representative example:
2995
2996 class D a => C a where
2997 meth :: D a => ()
2998 class C a => D a
2999
3000 This fixes Trac #9415, #9739
3001
3002 Note [Default method type signatures must align]
3003 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3004 GHC enforces the invariant that a class method's default type signature
3005 must "align" with that of the method's non-default type signature, as per
3006 GHC Trac #12918. For instance, if you have:
3007
3008 class Foo a where
3009 bar :: forall b. Context => a -> b
3010
3011 Then a default type signature for bar must be alpha equivalent to
3012 (forall b. a -> b). That is, the types must be the same modulo differences in
3013 contexts. So the following would be acceptable default type signatures:
3014
3015 default bar :: forall b. Context1 => a -> b
3016 default bar :: forall x. Context2 => a -> x
3017
3018 But the following are NOT acceptable default type signatures:
3019
3020 default bar :: forall b. b -> a
3021 default bar :: forall x. x
3022 default bar :: a -> Int
3023
3024 Note that a is bound by the class declaration for Foo itself, so it is
3025 not allowed to differ in the default type signature.
3026
3027 The default type signature (default bar :: a -> Int) deserves special mention,
3028 since (a -> Int) is a straightforward instantiation of (forall b. a -> b). To
3029 write this, you need to declare the default type signature like so:
3030
3031 default bar :: forall b. (b ~ Int). a -> b
3032
3033 As noted in #12918, there are several reasons to do this:
3034
3035 1. It would make no sense to have a type that was flat-out incompatible with
3036 the non-default type signature. For instance, if you had:
3037
3038 class Foo a where
3039 bar :: a -> Int
3040 default bar :: a -> Bool
3041
3042 Then that would always fail in an instance declaration. So this check
3043 nips such cases in the bud before they have the chance to produce
3044 confusing error messages.
3045
3046 2. Internally, GHC uses TypeApplications to instantiate the default method in
3047 an instance. See Note [Default methods in instances] in TcInstDcls.
3048 Thus, GHC needs to know exactly what the universally quantified type
3049 variables are, and when instantiated that way, the default method's type
3050 must match the expected type.
3051
3052 3. Aesthetically, by only allowing the default type signature to differ in its
3053 context, we are making it more explicit the ways in which the default type
3054 signature is less polymorphic than the non-default type signature.
3055
3056 You might be wondering: why are the contexts allowed to be different, but not
3057 the rest of the type signature? That's because default implementations often
3058 rely on assumptions that the more general, non-default type signatures do not.
3059 For instance, in the Enum class declaration:
3060
3061 class Enum a where
3062 enum :: [a]
3063 default enum :: (Generic a, GEnum (Rep a)) => [a]
3064 enum = map to genum
3065
3066 class GEnum f where
3067 genum :: [f a]
3068
3069 The default implementation for enum only works for types that are instances of
3070 Generic, and for which their generic Rep type is an instance of GEnum. But
3071 clearly enum doesn't _have_ to use this implementation, so naturally, the
3072 context for enum is allowed to be different to accomodate this. As a result,
3073 when we validity-check default type signatures, we ignore contexts completely.
3074
3075 Note that when checking whether two type signatures match, we must take care to
3076 split as many foralls as it takes to retrieve the tau types we which to check.
3077 See Note [Splitting nested sigma types in class type signatures].
3078
3079 Note [Splitting nested sigma types in class type signatures]
3080 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3081 Consider this type synonym and class definition:
3082
3083 type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
3084
3085 class Each s t a b where
3086 each :: Traversal s t a b
3087 default each :: (Traversable g, s ~ g a, t ~ g b) => Traversal s t a b
3088
3089 It might seem obvious that the tau types in both type signatures for `each`
3090 are the same, but actually getting GHC to conclude this is surprisingly tricky.
3091 That is because in general, the form of a class method's non-default type
3092 signature is:
3093
3094 forall a. C a => forall d. D d => E a b
3095
3096 And the general form of a default type signature is:
3097
3098 forall f. F f => E a f -- The variable `a` comes from the class
3099
3100 So it you want to get the tau types in each type signature, you might find it
3101 reasonable to call tcSplitSigmaTy twice on the non-default type signature, and
3102 call it once on the default type signature. For most classes and methods, this
3103 will work, but Each is a bit of an exceptional case. The way `each` is written,
3104 it doesn't quantify any additional type variables besides those of the Each
3105 class itself, so the non-default type signature for `each` is actually this:
3106
3107 forall s t a b. Each s t a b => Traversal s t a b
3108
3109 Notice that there _appears_ to only be one forall. But there's actually another
3110 forall lurking in the Traversal type synonym, so if you call tcSplitSigmaTy
3111 twice, you'll also go under the forall in Traversal! That is, you'll end up
3112 with:
3113
3114 (a -> f b) -> s -> f t
3115
3116 A problem arises because you only call tcSplitSigmaTy once on the default type
3117 signature for `each`, which gives you
3118
3119 Traversal s t a b
3120
3121 Or, equivalently:
3122
3123 forall f. Applicative f => (a -> f b) -> s -> f t
3124
3125 This is _not_ the same thing as (a -> f b) -> s -> f t! So now tcMatchTy will
3126 say that the tau types for `each` are not equal.
3127
3128 A solution to this problem is to use tcSplitNestedSigmaTys instead of
3129 tcSplitSigmaTy. tcSplitNestedSigmaTys will always split any foralls that it
3130 sees until it can't go any further, so if you called it on the default type
3131 signature for `each`, it would return (a -> f b) -> s -> f t like we desired.
3132
3133 Note [Checking partial record field]
3134 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3135 This check checks the partial record field selector, and warns (Trac #7169).
3136
3137 For example:
3138
3139 data T a = A { m1 :: a, m2 :: a } | B { m1 :: a }
3140
3141 The function 'm2' is partial record field, and will fail when it is applied to
3142 'B'. The warning identifies such partial fields. The check is performed at the
3143 declaration of T, not at the call-sites of m2.
3144
3145 The warning can be suppressed by prefixing the field-name with an underscore.
3146 For example:
3147
3148 data T a = A { m1 :: a, _m2 :: a } | B { m1 :: a }
3149
3150 Note [checkValidDependency]
3151 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
3152 Consider
3153
3154 data Proxy k (a :: k)
3155 data Proxy2 k a = P (Proxy k a)
3156
3157 (This is test dependent/should_fail/InferDependency.) While it seems GHC can
3158 figure out the dependency between the arguments to Proxy2, this case errors.
3159 The problem is that when we build the initial kind (getInitialKind) for
3160 a tycon, we need to decide whether an argument is dependent or not. At first,
3161 I thought we could just assume that *all* arguments are dependent, and then
3162 patch it up later. However, this causes problems in error messages (where
3163 tycon's have mysterious kinds "forall (a :: k) -> blah") and in unification
3164 (where we try to unify kappa ~ forall (a :: k) -> blah, failing because the
3165 RHS is not a tau-type). Perhaps a cleverer algorithm could sort this out
3166 (say, by storing the dependency flag in a mutable cell and by avoiding
3167 these fancy kinds in error messages depending on the extension in effect)
3168 but it doesn't seem worth it.
3169
3170 So: we choose the dependency for each argument variable once and for all
3171 in getInitialKind. This means that any dependency must be lexically manifest.
3172
3173 checkValidDependency checks to make sure that no lexically non-dependent
3174 argument actually appears in a kind. Note the example above, where the k
3175 in Proxy2 is a dependent argument, but this fact is not lexically
3176 manifest. checkValidDependency will reject. This function must be called
3177 *before* kind generalization, because kind generalization works with
3178 the result of mkTyConKind, which will think that Proxy2's kind is
3179 Type -> k -> Type, where k is unbound. (It won't use a forall for a
3180 "non-dependent" argument k.)
3181 -}
3182
3183 -- | See Note [checkValidDependency]
3184 checkValidDependency :: [TyConBinder] -- zonked
3185 -> TcKind -- zonked (result kind)
3186 -> TcM ()
3187 checkValidDependency binders res_kind
3188 = go (tyCoVarsOfType res_kind) (reverse binders)
3189 where
3190 go :: TyCoVarSet -- fvs from scope
3191 -> [TyConBinder] -- binders, in reverse order
3192 -> TcM ()
3193 go _ [] = return () -- all set
3194 go fvs (tcb : tcbs)
3195 | not (isNamedTyConBinder tcb) && tcb_var `elemVarSet` fvs
3196 = do { setSrcSpan (getSrcSpan tcb_var) $
3197 addErrTc (vcat [ text "Type constructor argument" <+> quotes (ppr tcb_var) <+>
3198 text "is used dependently."
3199 , text "Any dependent arguments must be obviously so, not inferred"
3200 , text "by the type-checker."
3201 , hang (text "Inferred argument kinds:")
3202 2 (vcat (map pp_binder binders))
3203 , text "Suggestion: use" <+> quotes (ppr tcb_var) <+>
3204 text "in a kind to make the dependency clearer." ])
3205 ; go new_fvs tcbs }
3206
3207 | otherwise
3208 = go new_fvs tcbs
3209 where
3210 new_fvs = fvs `delVarSet` tcb_var
3211 `unionVarSet` tyCoVarsOfType tcb_kind
3212
3213 tcb_var = binderVar tcb
3214 tcb_kind = tyVarKind tcb_var
3215
3216 pp_binder binder = ppr (binderVar binder) <+> dcolon <+> ppr (binderKind binder)
3217
3218 {-
3219 ************************************************************************
3220 * *
3221 Checking role validity
3222 * *
3223 ************************************************************************
3224 -}
3225
3226 checkValidRoleAnnots :: RoleAnnotEnv -> TyCon -> TcM ()
3227 checkValidRoleAnnots role_annots tc
3228 | isTypeSynonymTyCon tc = check_no_roles
3229 | isFamilyTyCon tc = check_no_roles
3230 | isAlgTyCon tc = check_roles
3231 | otherwise = return ()
3232 where
3233 -- Role annotations are given only on *explicit* variables,
3234 -- but a tycon stores roles for all variables.
3235 -- So, we drop the implicit roles (which are all Nominal, anyway).
3236 name = tyConName tc
3237 tyvars = tyConTyVars tc
3238 roles = tyConRoles tc
3239 (vis_roles, vis_vars) = unzip $ snd $
3240 partitionInvisibles tc (mkTyVarTy . snd) $
3241 zip roles tyvars
3242 role_annot_decl_maybe = lookupRoleAnnot role_annots name
3243
3244 check_roles
3245 = whenIsJust role_annot_decl_maybe $
3246 \decl@(L loc (RoleAnnotDecl _ _ the_role_annots)) ->
3247 addRoleAnnotCtxt name $
3248 setSrcSpan loc $ do
3249 { role_annots_ok <- xoptM LangExt.RoleAnnotations
3250 ; checkTc role_annots_ok $ needXRoleAnnotations tc
3251 ; checkTc (vis_vars `equalLength` the_role_annots)
3252 (wrongNumberOfRoles vis_vars decl)
3253 ; _ <- zipWith3M checkRoleAnnot vis_vars the_role_annots vis_roles
3254 -- Representational or phantom roles for class parameters
3255 -- quickly lead to incoherence. So, we require
3256 -- IncoherentInstances to have them. See #8773, #14292
3257 ; incoherent_roles_ok <- xoptM LangExt.IncoherentInstances
3258 ; checkTc ( incoherent_roles_ok
3259 || (not $ isClassTyCon tc)
3260 || (all (== Nominal) vis_roles))
3261 incoherentRoles
3262
3263 ; lint <- goptM Opt_DoCoreLinting
3264 ; when lint $ checkValidRoles tc }
3265
3266 check_no_roles
3267 = whenIsJust role_annot_decl_maybe illegalRoleAnnotDecl
3268
3269 checkRoleAnnot :: TyVar -> Located (Maybe Role) -> Role -> TcM ()
3270 checkRoleAnnot _ (L _ Nothing) _ = return ()
3271 checkRoleAnnot tv (L _ (Just r1)) r2
3272 = when (r1 /= r2) $
3273 addErrTc $ badRoleAnnot (tyVarName tv) r1 r2
3274
3275 -- This is a double-check on the role inference algorithm. It is only run when
3276 -- -dcore-lint is enabled. See Note [Role inference] in TcTyDecls
3277 checkValidRoles :: TyCon -> TcM ()
3278 -- If you edit this function, you may need to update the GHC formalism
3279 -- See Note [GHC Formalism] in CoreLint
3280 checkValidRoles tc
3281 | isAlgTyCon tc
3282 -- tyConDataCons returns an empty list for data families
3283 = mapM_ check_dc_roles (tyConDataCons tc)
3284 | Just rhs <- synTyConRhs_maybe tc
3285 = check_ty_roles (zipVarEnv (tyConTyVars tc) (tyConRoles tc)) Representational rhs
3286 | otherwise
3287 = return ()
3288 where
3289 check_dc_roles datacon
3290 = do { traceTc "check_dc_roles" (ppr datacon <+> ppr (tyConRoles tc))
3291 ; mapM_ (check_ty_roles role_env Representational) $
3292 eqSpecPreds eq_spec ++ theta ++ arg_tys }
3293 -- See Note [Role-checking data constructor arguments] in TcTyDecls
3294 where
3295 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
3296 = dataConFullSig datacon
3297 univ_roles = zipVarEnv univ_tvs (tyConRoles tc)
3298 -- zipVarEnv uses zipEqual, but we don't want that for ex_tvs
3299 ex_roles = mkVarEnv (map (, Nominal) ex_tvs)
3300 role_env = univ_roles `plusVarEnv` ex_roles
3301
3302 check_ty_roles env role ty
3303 | Just ty' <- coreView ty -- #14101
3304 = check_ty_roles env role ty'
3305
3306 check_ty_roles env role (TyVarTy tv)
3307 = case lookupVarEnv env tv of
3308 Just role' -> unless (role' `ltRole` role || role' == role) $
3309 report_error $ text "type variable" <+> quotes (ppr tv) <+>
3310 text "cannot have role" <+> ppr role <+>
3311 text "because it was assigned role" <+> ppr role'
3312 Nothing -> report_error $ text "type variable" <+> quotes (ppr tv) <+>
3313 text "missing in environment"
3314
3315 check_ty_roles env Representational (TyConApp tc tys)
3316 = let roles' = tyConRoles tc in
3317 zipWithM_ (maybe_check_ty_roles env) roles' tys
3318
3319 check_ty_roles env Nominal (TyConApp _ tys)
3320 = mapM_ (check_ty_roles env Nominal) tys
3321
3322 check_ty_roles _ Phantom ty@(TyConApp {})
3323 = pprPanic "check_ty_roles" (ppr ty)
3324
3325 check_ty_roles env role (AppTy ty1 ty2)
3326 = check_ty_roles env role ty1
3327 >> check_ty_roles env Nominal ty2
3328
3329 check_ty_roles env role (FunTy ty1 ty2)
3330 = check_ty_roles env role ty1
3331 >> check_ty_roles env role ty2
3332
3333 check_ty_roles env role (ForAllTy (TvBndr tv _) ty)
3334 = check_ty_roles env Nominal (tyVarKind tv)
3335 >> check_ty_roles (extendVarEnv env tv Nominal) role ty
3336
3337 check_ty_roles _ _ (LitTy {}) = return ()
3338
3339 check_ty_roles env role (CastTy t _)
3340 = check_ty_roles env role t
3341
3342 check_ty_roles _ role (CoercionTy co)
3343 = unless (role == Phantom) $
3344 report_error $ text "coercion" <+> ppr co <+> text "has bad role" <+> ppr role
3345
3346 maybe_check_ty_roles env role ty
3347 = when (role == Nominal || role == Representational) $
3348 check_ty_roles env role ty
3349
3350 report_error doc
3351 = addErrTc $ vcat [text "Internal error in role inference:",
3352 doc,
3353 text "Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug"]
3354
3355 {-
3356 ************************************************************************
3357 * *
3358 Error messages
3359 * *
3360 ************************************************************************
3361 -}
3362
3363 tcAddTyFamInstCtxt :: TyFamInstDecl GhcRn -> TcM a -> TcM a
3364 tcAddTyFamInstCtxt decl
3365 = tcAddFamInstCtxt (text "type instance") (tyFamInstDeclName decl)
3366
3367 tcMkDataFamInstCtxt :: DataFamInstDecl GhcRn -> SDoc
3368 tcMkDataFamInstCtxt decl@(DataFamInstDecl { dfid_eqn =
3369 HsIB { hsib_body = eqn }})
3370 = tcMkFamInstCtxt (pprDataFamInstFlavour decl <+> text "instance")
3371 (unLoc (feqn_tycon eqn))
3372 tcMkDataFamInstCtxt (DataFamInstDecl (XHsImplicitBndrs _))
3373 = panic "tcMkDataFamInstCtxt"
3374
3375 tcAddDataFamInstCtxt :: DataFamInstDecl GhcRn -> TcM a -> TcM a
3376 tcAddDataFamInstCtxt decl
3377 = addErrCtxt (tcMkDataFamInstCtxt decl)
3378
3379 tcMkFamInstCtxt :: SDoc -> Name -> SDoc
3380 tcMkFamInstCtxt flavour tycon
3381 = hsep [ text "In the" <+> flavour <+> text "declaration for"
3382 , quotes (ppr tycon) ]
3383
3384 tcAddFamInstCtxt :: SDoc -> Name -> TcM a -> TcM a
3385 tcAddFamInstCtxt flavour tycon thing_inside
3386 = addErrCtxt (tcMkFamInstCtxt flavour tycon) thing_inside
3387
3388 tcAddClosedTypeFamilyDeclCtxt :: TyCon -> TcM a -> TcM a
3389 tcAddClosedTypeFamilyDeclCtxt tc
3390 = addErrCtxt ctxt
3391 where
3392 ctxt = text "In the equations for closed type family" <+>
3393 quotes (ppr tc)
3394
3395 resultTypeMisMatch :: FieldLabelString -> DataCon -> DataCon -> SDoc
3396 resultTypeMisMatch field_name con1 con2
3397 = vcat [sep [text "Constructors" <+> ppr con1 <+> text "and" <+> ppr con2,
3398 text "have a common field" <+> quotes (ppr field_name) <> comma],
3399 nest 2 $ text "but have different result types"]
3400
3401 fieldTypeMisMatch :: FieldLabelString -> DataCon -> DataCon -> SDoc
3402 fieldTypeMisMatch field_name con1 con2
3403 = sep [text "Constructors" <+> ppr con1 <+> text "and" <+> ppr con2,
3404 text "give different types for field", quotes (ppr field_name)]
3405
3406 dataConCtxtName :: [Located Name] -> SDoc
3407 dataConCtxtName [con]
3408 = text "In the definition of data constructor" <+> quotes (ppr con)
3409 dataConCtxtName con
3410 = text "In the definition of data constructors" <+> interpp'SP con
3411
3412 dataConCtxt :: Outputable a => a -> SDoc
3413 dataConCtxt con = text "In the definition of data constructor" <+> quotes (ppr con)
3414
3415 classOpCtxt :: Var -> Type -> SDoc
3416 classOpCtxt sel_id tau = sep [text "When checking the class method:",
3417 nest 2 (pprPrefixOcc sel_id <+> dcolon <+> ppr tau)]
3418
3419 classArityErr :: Int -> Class -> SDoc
3420 classArityErr n cls
3421 | n == 0 = mkErr "No" "no-parameter"
3422 | otherwise = mkErr "Too many" "multi-parameter"
3423 where
3424 mkErr howMany allowWhat =
3425 vcat [text (howMany ++ " parameters for class") <+> quotes (ppr cls),
3426 parens (text ("Enable MultiParamTypeClasses to allow "
3427 ++ allowWhat ++ " classes"))]
3428
3429 classFunDepsErr :: Class -> SDoc
3430 classFunDepsErr cls
3431 = vcat [text "Fundeps in class" <+> quotes (ppr cls),
3432 parens (text "Enable FunctionalDependencies to allow fundeps")]
3433
3434 badMethPred :: Id -> TcPredType -> SDoc
3435 badMethPred sel_id pred
3436 = vcat [ hang (text "Constraint" <+> quotes (ppr pred)
3437 <+> text "in the type of" <+> quotes (ppr sel_id))
3438 2 (text "constrains only the class type variables")
3439 , text "Enable ConstrainedClassMethods to allow it" ]
3440
3441 noClassTyVarErr :: Class -> TyCon -> SDoc
3442 noClassTyVarErr clas fam_tc
3443 = sep [ text "The associated type" <+> quotes (ppr fam_tc)
3444 , text "mentions none of the type or kind variables of the class" <+>
3445 quotes (ppr clas <+> hsep (map ppr (classTyVars clas)))]
3446
3447 badDataConTyCon :: DataCon -> Type -> Type -> SDoc
3448 badDataConTyCon data_con res_ty_tmpl actual_res_ty
3449 | tcIsForAllTy actual_res_ty
3450 = nested_foralls_contexts_suggestion
3451 | isJust (tcSplitPredFunTy_maybe actual_res_ty)
3452 = nested_foralls_contexts_suggestion
3453 | otherwise
3454 = hang (text "Data constructor" <+> quotes (ppr data_con) <+>
3455 text "returns type" <+> quotes (ppr actual_res_ty))
3456 2 (text "instead of an instance of its parent type" <+> quotes (ppr res_ty_tmpl))
3457 where
3458 -- This suggestion is useful for suggesting how to correct code like what
3459 -- was reported in Trac #12087:
3460 --
3461 -- data F a where
3462 -- MkF :: Ord a => Eq a => a -> F a
3463 --
3464 -- Although nested foralls or contexts are allowed in function type
3465 -- signatures, it is much more difficult to engineer GADT constructor type
3466 -- signatures to allow something similar, so we error in the latter case.
3467 -- Nevertheless, we can at least suggest how a user might reshuffle their
3468 -- exotic GADT constructor type signature so that GHC will accept.
3469 nested_foralls_contexts_suggestion =
3470 text "GADT constructor type signature cannot contain nested"
3471 <+> quotes forAllLit <> text "s or contexts"
3472 $+$ hang (text "Suggestion: instead use this type signature:")
3473 2 (ppr (dataConName data_con) <+> dcolon <+> ppr suggested_ty)
3474
3475 -- To construct a type that GHC would accept (suggested_ty), we:
3476 --
3477 -- 1) Find the existentially quantified type variables and the class
3478 -- predicates from the datacon. (NB: We don't need the universally
3479 -- quantified type variables, since rejigConRes won't substitute them in
3480 -- the result type if it fails, as in this scenario.)
3481 -- 2) Split apart the return type (which is headed by a forall or a
3482 -- context) using tcSplitNestedSigmaTys, collecting the type variables
3483 -- and class predicates we find, as well as the rho type lurking
3484 -- underneath the nested foralls and contexts.
3485 -- 3) Smash together the type variables and class predicates from 1) and
3486 -- 2), and prepend them to the rho type from 2).
3487 actual_ex_tvs = dataConExTyVars data_con
3488 actual_theta = dataConTheta data_con
3489 (actual_res_tvs, actual_res_theta, actual_res_rho)
3490 = tcSplitNestedSigmaTys actual_res_ty
3491 suggested_ty = mkSpecForAllTys (actual_ex_tvs ++ actual_res_tvs) $
3492 mkFunTys (actual_theta ++ actual_res_theta)
3493 actual_res_rho
3494
3495 badGadtDecl :: Name -> SDoc
3496 badGadtDecl tc_name
3497 = vcat [ text "Illegal generalised algebraic data declaration for" <+> quotes (ppr tc_name)
3498 , nest 2 (parens $ text "Enable the GADTs extension to allow this") ]
3499
3500 badExistential :: DataCon -> SDoc
3501 badExistential con
3502 = hang (text "Data constructor" <+> quotes (ppr con) <+>
3503 text "has existential type variables, a context, or a specialised result type")
3504 2 (vcat [ ppr con <+> dcolon <+> ppr (dataConUserType con)
3505 , parens $ text "Enable ExistentialQuantification or GADTs to allow this" ])
3506
3507 badStupidTheta :: Name -> SDoc
3508 badStupidTheta tc_name
3509 = text "A data type declared in GADT style cannot have a context:" <+> quotes (ppr tc_name)
3510
3511 newtypeConError :: Name -> Int -> SDoc
3512 newtypeConError tycon n
3513 = sep [text "A newtype must have exactly one constructor,",
3514 nest 2 $ text "but" <+> quotes (ppr tycon) <+> text "has" <+> speakN n ]
3515
3516 newtypeStrictError :: DataCon -> SDoc
3517 newtypeStrictError con
3518 = sep [text "A newtype constructor cannot have a strictness annotation,",
3519 nest 2 $ text "but" <+> quotes (ppr con) <+> text "does"]
3520
3521 newtypeFieldErr :: DataCon -> Int -> SDoc
3522 newtypeFieldErr con_name n_flds
3523 = sep [text "The constructor of a newtype must have exactly one field",
3524 nest 2 $ text "but" <+> quotes (ppr con_name) <+> text "has" <+> speakN n_flds]
3525
3526 badSigTyDecl :: Name -> SDoc
3527 badSigTyDecl tc_name
3528 = vcat [ text "Illegal kind signature" <+>
3529 quotes (ppr tc_name)
3530 , nest 2 (parens $ text "Use KindSignatures to allow kind signatures") ]
3531
3532 emptyConDeclsErr :: Name -> SDoc
3533 emptyConDeclsErr tycon
3534 = sep [quotes (ppr tycon) <+> text "has no constructors",
3535 nest 2 $ text "(EmptyDataDecls permits this)"]
3536
3537 wrongKindOfFamily :: TyCon -> SDoc
3538 wrongKindOfFamily family
3539 = text "Wrong category of family instance; declaration was for a"
3540 <+> kindOfFamily
3541 where
3542 kindOfFamily | isTypeFamilyTyCon family = text "type family"
3543 | isDataFamilyTyCon family = text "data family"
3544 | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
3545
3546 wrongNumberOfParmsErr :: Arity -> SDoc
3547 wrongNumberOfParmsErr max_args
3548 = text "Number of parameters must match family declaration; expected"
3549 <+> ppr max_args
3550
3551 defaultAssocKindErr :: TyCon -> SDoc
3552 defaultAssocKindErr fam_tc
3553 = text "Kind mis-match on LHS of default declaration for"
3554 <+> quotes (ppr fam_tc)
3555
3556 wrongTyFamName :: Name -> Name -> SDoc
3557 wrongTyFamName fam_tc_name eqn_tc_name
3558 = hang (text "Mismatched type name in type family instance.")
3559 2 (vcat [ text "Expected:" <+> ppr fam_tc_name
3560 , text " Actual:" <+> ppr eqn_tc_name ])
3561
3562 badRoleAnnot :: Name -> Role -> Role -> SDoc
3563 badRoleAnnot var annot inferred
3564 = hang (text "Role mismatch on variable" <+> ppr var <> colon)
3565 2 (sep [ text "Annotation says", ppr annot
3566 , text "but role", ppr inferred
3567 , text "is required" ])
3568
3569 wrongNumberOfRoles :: [a] -> LRoleAnnotDecl GhcRn -> SDoc
3570 wrongNumberOfRoles tyvars d@(L _ (RoleAnnotDecl _ _ annots))
3571 = hang (text "Wrong number of roles listed in role annotation;" $$
3572 text "Expected" <+> (ppr $ length tyvars) <> comma <+>
3573 text "got" <+> (ppr $ length annots) <> colon)
3574 2 (ppr d)
3575 wrongNumberOfRoles _ (L _ (XRoleAnnotDecl _)) = panic "wrongNumberOfRoles"
3576
3577 illegalRoleAnnotDecl :: LRoleAnnotDecl GhcRn -> TcM ()
3578 illegalRoleAnnotDecl (L loc (RoleAnnotDecl _ tycon _))
3579 = setErrCtxt [] $
3580 setSrcSpan loc $
3581 addErrTc (text "Illegal role annotation for" <+> ppr tycon <> char ';' $$
3582 text "they are allowed only for datatypes and classes.")
3583 illegalRoleAnnotDecl (L _ (XRoleAnnotDecl _)) = panic "illegalRoleAnnotDecl"
3584
3585 needXRoleAnnotations :: TyCon -> SDoc
3586 needXRoleAnnotations tc
3587 = text "Illegal role annotation for" <+> ppr tc <> char ';' $$
3588 text "did you intend to use RoleAnnotations?"
3589
3590 incoherentRoles :: SDoc
3591 incoherentRoles = (text "Roles other than" <+> quotes (text "nominal") <+>
3592 text "for class parameters can lead to incoherence.") $$
3593 (text "Use IncoherentInstances to allow this; bad role found")
3594
3595 addTyConCtxt :: TyCon -> TcM a -> TcM a
3596 addTyConCtxt tc
3597 = addErrCtxt ctxt
3598 where
3599 name = getName tc
3600 flav = ppr (tyConFlavour tc)
3601 ctxt = hsep [ text "In the", flav
3602 , text "declaration for", quotes (ppr name) ]
3603
3604 addRoleAnnotCtxt :: Name -> TcM a -> TcM a
3605 addRoleAnnotCtxt name
3606 = addErrCtxt $
3607 text "while checking a role annotation for" <+> quotes (ppr name)