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