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