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