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