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