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