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