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