1{- 2(c) The University of Glasgow 2006 3(c) The AQUA Project, Glasgow University, 1996-1998 4 5 6TcTyClsDecls: Typecheck type and class declarations 7-} 8 9{-# LANGUAGE CPP, TupleSections, ScopedTypeVariables, MultiWayIf #-} 10{-# LANGUAGE TypeFamilies #-} 11{-# LANGUAGE ViewPatterns #-} 12 13{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} 14 15module TcTyClsDecls ( 16 tcTyAndClassDecls, 17 18 -- Functions used by TcInstDcls to check 19 -- data/type family instance declarations 20 kcConDecls, tcConDecls, dataDeclChecks, checkValidTyCon, 21 tcFamTyPats, tcTyFamInstEqn, 22 tcAddTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt, 23 unravelFamInstPats, addConsistencyConstraints, 24 wrongKindOfFamily 25 ) where 26 27#include "HsVersions.h" 28 29import GhcPrelude 30 31import GHC.Hs 32import HscTypes 33import BuildTyCl 34import TcRnMonad 35import TcEnv 36import TcValidity 37import TcHsSyn 38import TcTyDecls 39import TcClassDcl 40import {-# SOURCE #-} TcInstDcls( tcInstDecls1 ) 41import TcDeriv (DerivInfo(..)) 42import TcUnify ( unifyKind, checkTvConstraints ) 43import TcHsType 44import ClsInst( AssocInstInfo(..) ) 45import TcMType 46import TysWiredIn ( unitTy, makeRecoveryTyCon ) 47import TcType 48import RnEnv( lookupConstructorFields ) 49import FamInst 50import FamInstEnv 51import Coercion 52import TcOrigin 53import Type 54import TyCoRep -- for checkValidRoles 55import TyCoPpr( pprTyVars, pprWithExplicitKindsWhen ) 56import Class 57import CoAxiom 58import TyCon 59import DataCon 60import Id 61import Var 62import VarEnv 63import VarSet 64import Module 65import Name 66import NameSet 67import NameEnv 68import Outputable 69import Maybes 70import Unify 71import Util 72import SrcLoc 73import ListSetOps 74import DynFlags 75import Unique 76import ConLike( ConLike(..) ) 77import BasicTypes 78import qualified GHC.LanguageExtensions as LangExt 79 80import Control.Monad 81import Data.Foldable 82import Data.Function ( on ) 83import Data.Functor.Identity 84import Data.List 85import qualified Data.List.NonEmpty as NE 86import Data.List.NonEmpty ( NonEmpty(..) ) 87import qualified Data.Set as Set 88import Data.Tuple( swap ) 89 90{- 91************************************************************************ 92* * 93\subsection{Type checking for type and class declarations} 94* * 95************************************************************************ 96 97Note [Grouping of type and class declarations] 98~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 99tcTyAndClassDecls is called on a list of `TyClGroup`s. Each group is a strongly 100connected component of mutually dependent types and classes. We kind check and 101type check each group separately to enhance kind polymorphism. Take the 102following example: 103 104 type Id a = a 105 data X = X (Id Int) 106 107If we were to kind check the two declarations together, we would give Id the 108kind * -> *, since we apply it to an Int in the definition of X. But we can do 109better than that, since Id really is kind polymorphic, and should get kind 110forall (k::*). k -> k. Since it does not depend on anything else, it can be 111kind-checked by itself, hence getting the most general kind. We then kind check 112X, which works fine because we then know the polymorphic kind of Id, and simply 113instantiate k to *. 114 115Note [Check role annotations in a second pass] 116~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 117Role inference potentially depends on the types of all of the datacons declared 118in a mutually recursive group. The validity of a role annotation, in turn, 119depends on the result of role inference. Because the types of datacons might 120be ill-formed (see #7175 and Note [Checking GADT return types]) we must check 121*all* the tycons in a group for validity before checking *any* of the roles. 122Thus, we take two passes over the resulting tycons, first checking for general 123validity and then checking for valid role annotations. 124-} 125 126tcTyAndClassDecls :: [TyClGroup GhcRn] -- Mutually-recursive groups in 127 -- dependency order 128 -> TcM ( TcGblEnv -- Input env extended by types and 129 -- classes 130 -- and their implicit Ids,DataCons 131 , [InstInfo GhcRn] -- Source-code instance decls info 132 , [DerivInfo] -- Deriving info 133 ) 134-- Fails if there are any errors 135tcTyAndClassDecls tyclds_s 136 -- The code recovers internally, but if anything gave rise to 137 -- an error we'd better stop now, to avoid a cascade 138 -- Type check each group in dependency order folding the global env 139 = checkNoErrs $ fold_env [] [] tyclds_s 140 where 141 fold_env :: [InstInfo GhcRn] 142 -> [DerivInfo] 143 -> [TyClGroup GhcRn] 144 -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo]) 145 fold_env inst_info deriv_info [] 146 = do { gbl_env <- getGblEnv 147 ; return (gbl_env, inst_info, deriv_info) } 148 fold_env inst_info deriv_info (tyclds:tyclds_s) 149 = do { (tcg_env, inst_info', deriv_info') <- tcTyClGroup tyclds 150 ; setGblEnv tcg_env $ 151 -- remaining groups are typechecked in the extended global env. 152 fold_env (inst_info' ++ inst_info) 153 (deriv_info' ++ deriv_info) 154 tyclds_s } 155 156tcTyClGroup :: TyClGroup GhcRn 157 -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo]) 158-- Typecheck one strongly-connected component of type, class, and instance decls 159-- See Note [TyClGroups and dependency analysis] in GHC.Hs.Decls 160tcTyClGroup (TyClGroup { group_tyclds = tyclds 161 , group_roles = roles 162 , group_kisigs = kisigs 163 , group_instds = instds }) 164 = do { let role_annots = mkRoleAnnotEnv roles 165 166 -- Step 1: Typecheck the standalone kind signatures and type/class declarations 167 ; traceTc "---- tcTyClGroup ---- {" empty 168 ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds)) 169 ; (tyclss, data_deriv_info) <- 170 tcExtendKindEnv (mkPromotionErrorEnv tyclds) $ -- See Note [Type environment evolution] 171 do { kisig_env <- mkNameEnv <$> traverse tcStandaloneKindSig kisigs 172 ; tcTyClDecls tyclds kisig_env role_annots } 173 174 -- Step 1.5: Make sure we don't have any type synonym cycles 175 ; traceTc "Starting synonym cycle check" (ppr tyclss) 176 ; this_uid <- fmap thisPackage getDynFlags 177 ; checkSynCycles this_uid tyclss tyclds 178 ; traceTc "Done synonym cycle check" (ppr tyclss) 179 180 -- Step 2: Perform the validity check on those types/classes 181 -- We can do this now because we are done with the recursive knot 182 -- Do it before Step 3 (adding implicit things) because the latter 183 -- expects well-formed TyCons 184 ; traceTc "Starting validity check" (ppr tyclss) 185 ; tyclss <- concatMapM checkValidTyCl tyclss 186 ; traceTc "Done validity check" (ppr tyclss) 187 ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss 188 -- See Note [Check role annotations in a second pass] 189 190 ; traceTc "---- end tcTyClGroup ---- }" empty 191 192 -- Step 3: Add the implicit things; 193 -- we want them in the environment because 194 -- they may be mentioned in interface files 195 ; gbl_env <- addTyConsToGblEnv tyclss 196 197 -- Step 4: check instance declarations 198 ; (gbl_env', inst_info, datafam_deriv_info) <- 199 setGblEnv gbl_env $ 200 tcInstDecls1 instds 201 202 ; let deriv_info = datafam_deriv_info ++ data_deriv_info 203 ; return (gbl_env', inst_info, deriv_info) } 204 205 206tcTyClGroup (XTyClGroup nec) = noExtCon nec 207 208-- Gives the kind for every TyCon that has a standalone kind signature 209type KindSigEnv = NameEnv Kind 210 211tcTyClDecls 212 :: [LTyClDecl GhcRn] 213 -> KindSigEnv 214 -> RoleAnnotEnv 215 -> TcM ([TyCon], [DerivInfo]) 216tcTyClDecls tyclds kisig_env role_annots 217 = do { -- Step 1: kind-check this group and returns the final 218 -- (possibly-polymorphic) kind of each TyCon and Class 219 -- See Note [Kind checking for type and class decls] 220 tc_tycons <- kcTyClGroup kisig_env tyclds 221 ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons)) 222 223 -- Step 2: type-check all groups together, returning 224 -- the final TyCons and Classes 225 -- 226 -- NB: We have to be careful here to NOT eagerly unfold 227 -- type synonyms, as we have not tested for type synonym 228 -- loops yet and could fall into a black hole. 229 ; fixM $ \ ~(rec_tyclss, _) -> do 230 { tcg_env <- getGblEnv 231 ; let roles = inferRoles (tcg_src tcg_env) role_annots rec_tyclss 232 233 -- Populate environment with knot-tied ATyCon for TyCons 234 -- NB: if the decls mention any ill-staged data cons 235 -- (see Note [Recursion and promoting data constructors]) 236 -- we will have failed already in kcTyClGroup, so no worries here 237 ; (tycons, data_deriv_infos) <- 238 tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $ 239 240 -- Also extend the local type envt with bindings giving 241 -- a TcTyCon for each each knot-tied TyCon or Class 242 -- See Note [Type checking recursive type and class declarations] 243 -- and Note [Type environment evolution] 244 tcExtendKindEnvWithTyCons tc_tycons $ 245 246 -- Kind and type check declarations for this group 247 mapAndUnzipM (tcTyClDecl roles) tyclds 248 ; return (tycons, concat data_deriv_infos) 249 } } 250 where 251 ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma 252 , ppr (tyConBinders tc) <> comma 253 , ppr (tyConResKind tc) 254 , ppr (isTcTyCon tc) ]) 255 256zipRecTyClss :: [TcTyCon] 257 -> [TyCon] -- Knot-tied 258 -> [(Name,TyThing)] 259-- Build a name-TyThing mapping for the TyCons bound by decls 260-- being careful not to look at the knot-tied [TyThing] 261-- The TyThings in the result list must have a visible ATyCon, 262-- because typechecking types (in, say, tcTyClDecl) looks at 263-- this outer constructor 264zipRecTyClss tc_tycons rec_tycons 265 = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ] 266 where 267 rec_tc_env :: NameEnv TyCon 268 rec_tc_env = foldr add_tc emptyNameEnv rec_tycons 269 270 add_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon 271 add_tc tc env = foldr add_one_tc env (tc : tyConATs tc) 272 273 add_one_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon 274 add_one_tc tc env = extendNameEnv env (tyConName tc) tc 275 276 get name = case lookupNameEnv rec_tc_env name of 277 Just tc -> tc 278 other -> pprPanic "zipRecTyClss" (ppr name <+> ppr other) 279 280{- 281************************************************************************ 282* * 283 Kind checking 284* * 285************************************************************************ 286 287Note [Kind checking for type and class decls] 288~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 289Kind checking is done thus: 290 291 1. Make up a kind variable for each parameter of the declarations, 292 and extend the kind environment (which is in the TcLclEnv) 293 294 2. Kind check the declarations 295 296We need to kind check all types in the mutually recursive group 297before we know the kind of the type variables. For example: 298 299 class C a where 300 op :: D b => a -> b -> b 301 302 class D c where 303 bop :: (Monad c) => ... 304 305Here, the kind of the locally-polymorphic type variable "b" 306depends on *all the uses of class D*. For example, the use of 307Monad c in bop's type signature means that D must have kind Type->Type. 308 309Note: we don't treat type synonyms specially (we used to, in the past); 310in particular, even if we have a type synonym cycle, we still kind check 311it normally, and test for cycles later (checkSynCycles). The reason 312we can get away with this is because we have more systematic TYPE r 313inference, which means that we can do unification between kinds that 314aren't lifted (this historically was not true.) 315 316The downside of not directly reading off the kinds of the RHS of 317type synonyms in topological order is that we don't transparently 318support making synonyms of types with higher-rank kinds. But 319you can always specify a CUSK directly to make this work out. 320See tc269 for an example. 321 322Note [CUSKs and PolyKinds] 323~~~~~~~~~~~~~~~~~~~~~~~~~~ 324Consider 325 326 data T (a :: *) = MkT (S a) -- Has CUSK 327 data S a = MkS (T Int) (S a) -- No CUSK 328 329Via inferInitialKinds we get 330 T :: * -> * 331 S :: kappa -> * 332 333Then we call kcTyClDecl on each decl in the group, to constrain the 334kind unification variables. BUT we /skip/ the RHS of any decl with 335a CUSK. Here we skip the RHS of T, so we eventually get 336 S :: forall k. k -> * 337 338This gets us more polymorphism than we would otherwise get, similar 339(but implemented strangely differently from) the treatment of type 340signatures in value declarations. 341 342However, we only want to do so when we have PolyKinds. 343When we have NoPolyKinds, we don't skip those decls, because we have defaulting 344(#16609). Skipping won't bring us more polymorphism when we have defaulting. 345Consider 346 347 data T1 a = MkT1 T2 -- No CUSK 348 data T2 = MkT2 (T1 Maybe) -- Has CUSK 349 350If we skip the rhs of T2 during kind-checking, the kind of a remains unsolved. 351With PolyKinds, we do generalization to get T1 :: forall a. a -> *. And the 352program type-checks. 353But with NoPolyKinds, we do defaulting to get T1 :: * -> *. Defaulting happens 354in quantifyTyVars, which is called from generaliseTcTyCon. Then type-checking 355(T1 Maybe) will throw a type error. 356 357Summary: with PolyKinds, we must skip; with NoPolyKinds, we must /not/ skip. 358 359Open type families 360~~~~~~~~~~~~~~~~~~ 361This treatment of type synonyms only applies to Haskell 98-style synonyms. 362General type functions can be recursive, and hence, appear in `alg_decls'. 363 364The kind of an open type family is solely determinded by its kind signature; 365hence, only kind signatures participate in the construction of the initial 366kind environment (as constructed by `inferInitialKind'). In fact, we ignore 367instances of families altogether in the following. However, we need to include 368the kinds of *associated* families into the construction of the initial kind 369environment. (This is handled by `allDecls'). 370 371See also Note [Kind checking recursive type and class declarations] 372 373Note [How TcTyCons work] 374~~~~~~~~~~~~~~~~~~~~~~~~ 375TcTyCons are used for two distinct purposes 376 3771. When recovering from a type error in a type declaration, 378 we want to put the erroneous TyCon in the environment in a 379 way that won't lead to more errors. We use a TcTyCon for this; 380 see makeRecoveryTyCon. 381 3822. When checking a type/class declaration (in module TcTyClsDecls), we come 383 upon knowledge of the eventual tycon in bits and pieces. 384 385 S1) First, we use inferInitialKinds to look over the user-provided 386 kind signature of a tycon (including, for example, the number 387 of parameters written to the tycon) to get an initial shape of 388 the tycon's kind. We record that shape in a TcTyCon. 389 390 For CUSK tycons, the TcTyCon has the final, generalised kind. 391 For non-CUSK tycons, the TcTyCon has as its tyConBinders only 392 the explicit arguments given -- no kind variables, etc. 393 394 S2) Then, using these initial kinds, we kind-check the body of the 395 tycon (class methods, data constructors, etc.), filling in the 396 metavariables in the tycon's initial kind. 397 398 S3) We then generalize to get the (non-CUSK) tycon's final, fixed 399 kind. Finally, once this has happened for all tycons in a 400 mutually recursive group, we can desugar the lot. 401 402 For convenience, we store partially-known tycons in TcTyCons, which 403 might store meta-variables. These TcTyCons are stored in the local 404 environment in TcTyClsDecls, until the real full TyCons can be created 405 during desugaring. A desugared program should never have a TcTyCon. 406 4073. In a TcTyCon, everything is zonked after the kind-checking pass (S2). 408 4094. tyConScopedTyVars. A challenging piece in all of this is that we 410 end up taking three separate passes over every declaration: 411 - one in inferInitialKind (this pass look only at the head, not the body) 412 - one in kcTyClDecls (to kind-check the body) 413 - a final one in tcTyClDecls (to desugar) 414 415 In the latter two passes, we need to connect the user-written type 416 variables in an LHsQTyVars with the variables in the tycon's 417 inferred kind. Because the tycon might not have a CUSK, this 418 matching up is, in general, quite hard to do. (Look through the 419 git history between Dec 2015 and Apr 2016 for 420 TcHsType.splitTelescopeTvs!) 421 422 Instead of trying, we just store the list of type variables to 423 bring into scope, in the tyConScopedTyVars field of the TcTyCon. 424 These tyvars are brought into scope in TcHsType.bindTyClTyVars. 425 426 In a TcTyCon, why is tyConScopedTyVars :: [(Name,TcTyVar)] rather 427 than just [TcTyVar]? Consider these mutually-recursive decls 428 data T (a :: k1) b = MkT (S a b) 429 data S (c :: k2) d = MkS (T c d) 430 We start with k1 bound to kappa1, and k2 to kappa2; so initially 431 in the (Name,TcTyVar) pairs the Name is that of the TcTyVar. But 432 then kappa1 and kappa2 get unified; so after the zonking in 433 'generalise' in 'kcTyClGroup' the Name and TcTyVar may differ. 434 435See also Note [Type checking recursive type and class declarations]. 436 437Note [Swizzling the tyvars before generaliseTcTyCon] 438~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 439This Note only applies when /inferring/ the kind of a TyCon. 440If there is a separate kind signature, or a CUSK, we take an entirely 441different code path. 442 443For inference, consider 444 class C (f :: k) x where 445 type T f 446 op :: D f => blah 447 class D (g :: j) y where 448 op :: C g => y -> blah 449 450Here C and D are considered mutually recursive. Neither has a CUSK. 451Just before generalisation we have the (un-quantified) kinds 452 C :: k1 -> k2 -> Constraint 453 T :: k1 -> Type 454 D :: k1 -> Type -> Constraint 455Notice that f's kind and g's kind have been unified to 'k1'. We say 456that k1 is the "representative" of k in C's decl, and of j in D's decl. 457 458Now when quantifying, we'd like to end up with 459 C :: forall {k2}. forall k. k -> k2 -> Constraint 460 T :: forall k. k -> Type 461 D :: forall j. j -> Type -> Constraint 462 463That is, we want to swizzle the representative to have the Name given 464by the user. Partly this is to improve error messages and the output of 465:info in GHCi. But it is /also/ important because the code for a 466default method may mention the class variable(s), but at that point 467(tcClassDecl2), we only have the final class tyvars available. 468(Alternatively, we could record the scoped type variables in the 469TyCon, but it's a nuisance to do so.) 470 471Notes: 472 473* On the input to generaliseTyClDecl, the mapping between the 474 user-specified Name and the representative TyVar is recorded in the 475 tyConScopedTyVars of the TcTyCon. NB: you first need to zonk to see 476 this representative TyVar. 477 478* The swizzling is actually performed by swizzleTcTyConBndrs 479 480* We must do the swizzling across the whole class decl. Consider 481 class C f where 482 type S (f :: k) 483 type T f 484 Here f's kind k is a parameter of C, and its identity is shared 485 with S and T. So if we swizzle the representative k at all, we 486 must do so consistently for the entire declaration. 487 488 Hence the call to check_duplicate_tc_binders is in generaliseTyClDecl, 489 rather than in generaliseTcTyCon. 490 491There are errors to catch here. Suppose we had 492 class E (f :: j) (g :: k) where 493 op :: SameKind f g -> blah 494 495Then, just before generalisation we will have the (unquantified) 496 E :: k1 -> k1 -> Constraint 497 498That's bad! Two distinctly-named tyvars (j and k) have ended up with 499the same representative k1. So when swizzling, we check (in 500check_duplicate_tc_binders) that two distinct source names map 501to the same representative. 502 503Here's an interesting case: 504 class C1 f where 505 type S (f :: k1) 506 type T (f :: k2) 507Here k1 and k2 are different Names, but they end up mapped to the 508same representative TyVar. To make the swizzling consistent (remember 509we must have a single k across C1, S and T) we reject the program. 510 511Another interesting case 512 class C2 f where 513 type S (f :: k) (p::Type) 514 type T (f :: k) (p::Type->Type) 515 516Here the two k's (and the two p's) get distinct Uniques, because they 517are seen by the renamer as locally bound in S and T resp. But again 518the two (distinct) k's end up bound to the same representative TyVar. 519You might argue that this should be accepted, but it's definitely 520rejected (via an entirely different code path) if you add a kind sig: 521 type C2' :: j -> Constraint 522 class C2' f where 523 type S (f :: k) (p::Type) 524We get 525 • Expected kind ‘j’, but ‘f’ has kind ‘k’ 526 • In the associated type family declaration for ‘S’ 527 528So we reject C2 too, even without the kind signature. We have 529to do a bit of work to get a good error message, since both k's 530look the same to the user. 531 532Another case 533 class C3 (f :: k1) where 534 type S (f :: k2) 535 536This will be rejected too. 537 538 539Note [Type environment evolution] 540~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 541As we typecheck a group of declarations the type environment evolves. 542Consider for example: 543 data B (a :: Type) = MkB (Proxy 'MkB) 544 545We do the following steps: 546 547 1. Start of tcTyClDecls: use mkPromotionErrorEnv to initialise the 548 type env with promotion errors 549 B :-> TyConPE 550 MkB :-> DataConPE 551 552 2. kcTyCLGroup 553 - Do inferInitialKinds, which will signal a promotion 554 error if B is used in any of the kinds needed to initialise 555 B's kind (e.g. (a :: Type)) here 556 557 - Extend the type env with these initial kinds (monomorphic for 558 decls that lack a CUSK) 559 B :-> TcTyCon <initial kind> 560 (thereby overriding the B :-> TyConPE binding) 561 and do kcLTyClDecl on each decl to get equality constraints on 562 all those initial kinds 563 564 - Generalise the initial kind, making a poly-kinded TcTyCon 565 566 3. Back in tcTyDecls, extend the envt with bindings of the poly-kinded 567 TcTyCons, again overriding the promotion-error bindings. 568 569 But note that the data constructor promotion errors are still in place 570 so that (in our example) a use of MkB will still be signalled as 571 an error. 572 573 4. Typecheck the decls. 574 575 5. In tcTyClGroup, extend the envt with bindings for TyCon and DataCons 576 577 578Note [Missed opportunity to retain higher-rank kinds] 579~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 580In 'kcTyClGroup', there is a missed opportunity to make kind 581inference work in a few more cases. The idea is analogous 582to Note [Single function non-recursive binding special-case]: 583 584 * If we have an SCC with a single decl, which is non-recursive, 585 instead of creating a unification variable representing the 586 kind of the decl and unifying it with the rhs, we can just 587 read the type directly of the rhs. 588 589 * Furthermore, we can update our SCC analysis to ignore 590 dependencies on declarations which have CUSKs: we don't 591 have to kind-check these all at once, since we can use 592 the CUSK to initialize the kind environment. 593 594Unfortunately this requires reworking a bit of the code in 595'kcLTyClDecl' so I've decided to punt unless someone shouts about it. 596 597Note [Don't process associated types in getInitialKind] 598~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 599Previously, we processed associated types in the thing_inside in getInitialKind, 600but this was wrong -- we want to do ATs sepearately. 601The consequence for not doing it this way is #15142: 602 603 class ListTuple (tuple :: Type) (as :: [(k, Type)]) where 604 type ListToTuple as :: Type 605 606We assign k a kind kappa[1]. When checking the tuple (k, Type), we try to unify 607kappa ~ Type, but this gets deferred because we bumped the TcLevel as we bring 608`tuple` into scope. Thus, when we check ListToTuple, kappa[1] still hasn't 609unified with Type. And then, when we generalize the kind of ListToTuple (which 610indeed has a CUSK, according to the rules), we skolemize the free metavariable 611kappa. Note that we wouldn't skolemize kappa when generalizing the kind of ListTuple, 612because the solveEqualities in kcInferDeclHeader is at TcLevel 1 and so kappa[1] 613will unify with Type. 614 615Bottom line: as associated types should have no effect on a CUSK enclosing class, 616we move processing them to a separate action, run after the outer kind has 617been generalized. 618 619-} 620 621kcTyClGroup :: KindSigEnv -> [LTyClDecl GhcRn] -> TcM [TcTyCon] 622 623-- Kind check this group, kind generalize, and return the resulting local env 624-- This binds the TyCons and Classes of the group, but not the DataCons 625-- See Note [Kind checking for type and class decls] 626-- and Note [Inferring kinds for type declarations] 627kcTyClGroup kisig_env decls 628 = do { mod <- getModule 629 ; traceTc "---- kcTyClGroup ---- {" 630 (text "module" <+> ppr mod $$ vcat (map ppr decls)) 631 632 -- Kind checking; 633 -- 1. Bind kind variables for decls 634 -- 2. Kind-check decls 635 -- 3. Generalise the inferred kinds 636 -- See Note [Kind checking for type and class decls] 637 638 ; cusks_enabled <- xoptM LangExt.CUSKs <&&> xoptM LangExt.PolyKinds 639 -- See Note [CUSKs and PolyKinds] 640 ; let (kindless_decls, kinded_decls) = partitionWith get_kind decls 641 642 get_kind d 643 | Just ki <- lookupNameEnv kisig_env (tcdName (unLoc d)) 644 = Right (d, SAKS ki) 645 646 | cusks_enabled && hsDeclHasCusk (unLoc d) 647 = Right (d, CUSK) 648 649 | otherwise = Left d 650 651 ; checked_tcs <- checkInitialKinds kinded_decls 652 ; inferred_tcs 653 <- tcExtendKindEnvWithTyCons checked_tcs $ 654 pushTcLevelM_ $ -- We are going to kind-generalise, so 655 -- unification variables in here must 656 -- be one level in 657 solveEqualities $ 658 do { -- Step 1: Bind kind variables for all decls 659 mono_tcs <- inferInitialKinds kindless_decls 660 661 ; traceTc "kcTyClGroup: initial kinds" $ 662 ppr_tc_kinds mono_tcs 663 664 -- Step 2: Set extended envt, kind-check the decls 665 -- NB: the environment extension overrides the tycon 666 -- promotion-errors bindings 667 -- See Note [Type environment evolution] 668 ; tcExtendKindEnvWithTyCons mono_tcs $ 669 mapM_ kcLTyClDecl kindless_decls 670 671 ; return mono_tcs } 672 673 -- Step 3: generalisation 674 -- Finally, go through each tycon and give it its final kind, 675 -- with all the required, specified, and inferred variables 676 -- in order. 677 ; let inferred_tc_env = mkNameEnv $ 678 map (\tc -> (tyConName tc, tc)) inferred_tcs 679 ; generalized_tcs <- concatMapM (generaliseTyClDecl inferred_tc_env) 680 kindless_decls 681 682 ; let poly_tcs = checked_tcs ++ generalized_tcs 683 ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs) 684 ; return poly_tcs } 685 where 686 ppr_tc_kinds tcs = vcat (map pp_tc tcs) 687 pp_tc tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc) 688 689type ScopedPairs = [(Name, TcTyVar)] 690 -- The ScopedPairs for a TcTyCon are precisely 691 -- specified-tvs ++ required-tvs 692 -- You can distinguish them because there are tyConArity required-tvs 693 694generaliseTyClDecl :: NameEnv TcTyCon -> LTyClDecl GhcRn -> TcM [TcTyCon] 695-- See Note [Swizzling the tyvars before generaliseTcTyCon] 696generaliseTyClDecl inferred_tc_env (L _ decl) 697 = do { let names_in_this_decl :: [Name] 698 names_in_this_decl = tycld_names decl 699 700 -- Extract the specified/required binders and skolemise them 701 ; tc_with_tvs <- mapM skolemise_tc_tycon names_in_this_decl 702 703 -- Zonk, to manifest the side-effects of skolemisation to the swizzler 704 -- NB: it's important to skolemise them all before this step. E.g. 705 -- class C f where { type T (f :: k) } 706 -- We only skolemise k when looking at T's binders, 707 -- but k appears in f's kind in C's binders. 708 ; tc_infos <- mapM zonk_tc_tycon tc_with_tvs 709 710 -- Swizzle 711 ; swizzled_infos <- tcAddDeclCtxt decl (swizzleTcTyConBndrs tc_infos) 712 713 -- And finally generalise 714 ; mapAndReportM generaliseTcTyCon swizzled_infos } 715 where 716 tycld_names :: TyClDecl GhcRn -> [Name] 717 tycld_names decl = tcdName decl : at_names decl 718 719 at_names :: TyClDecl GhcRn -> [Name] 720 at_names (ClassDecl { tcdATs = ats }) = map (familyDeclName . unLoc) ats 721 at_names _ = [] -- Only class decls have associated types 722 723 skolemise_tc_tycon :: Name -> TcM (TcTyCon, ScopedPairs) 724 -- Zonk and skolemise the Specified and Required binders 725 skolemise_tc_tycon tc_name 726 = do { let tc = lookupNameEnv_NF inferred_tc_env tc_name 727 -- This lookup should not fail 728 ; scoped_prs <- mapSndM zonkAndSkolemise (tcTyConScopedTyVars tc) 729 ; return (tc, scoped_prs) } 730 731 zonk_tc_tycon :: (TcTyCon, ScopedPairs) -> TcM (TcTyCon, ScopedPairs, TcKind) 732 zonk_tc_tycon (tc, scoped_prs) 733 = do { scoped_prs <- mapSndM zonkTcTyVarToTyVar scoped_prs 734 -- We really have to do this again, even though 735 -- we have just done zonkAndSkolemise 736 ; res_kind <- zonkTcType (tyConResKind tc) 737 ; return (tc, scoped_prs, res_kind) } 738 739swizzleTcTyConBndrs :: [(TcTyCon, ScopedPairs, TcKind)] 740 -> TcM [(TcTyCon, ScopedPairs, TcKind)] 741swizzleTcTyConBndrs tc_infos 742 | all no_swizzle swizzle_prs 743 -- This fast path happens almost all the time 744 -- See Note [Non-cloning for tyvar binders] in TcHsType 745 = do { traceTc "Skipping swizzleTcTyConBndrs for" (ppr (map fstOf3 tc_infos)) 746 ; return tc_infos } 747 748 | otherwise 749 = do { check_duplicate_tc_binders 750 751 ; traceTc "swizzleTcTyConBndrs" $ 752 vcat [ text "before" <+> ppr_infos tc_infos 753 , text "swizzle_prs" <+> ppr swizzle_prs 754 , text "after" <+> ppr_infos swizzled_infos ] 755 756 ; return swizzled_infos } 757 758 where 759 swizzled_infos = [ (tc, mapSnd swizzle_var scoped_prs, swizzle_ty kind) 760 | (tc, scoped_prs, kind) <- tc_infos ] 761 762 swizzle_prs :: [(Name,TyVar)] 763 -- Pairs the user-specifed Name with its representative TyVar 764 -- See Note [Swizzling the tyvars before generaliseTcTyCon] 765 swizzle_prs = [ pr | (_, prs, _) <- tc_infos, pr <- prs ] 766 767 no_swizzle :: (Name,TyVar) -> Bool 768 no_swizzle (nm, tv) = nm == tyVarName tv 769 770 ppr_infos infos = vcat [ ppr tc <+> pprTyVars (map snd prs) 771 | (tc, prs, _) <- infos ] 772 773 -- Check for duplicates 774 -- E.g. data SameKind (a::k) (b::k) 775 -- data T (a::k1) (b::k2) = MkT (SameKind a b) 776 -- Here k1 and k2 start as TyVarTvs, and get unified with each other 777 -- If this happens, things get very confused later, so fail fast 778 check_duplicate_tc_binders :: TcM () 779 check_duplicate_tc_binders = unless (null err_prs) $ 780 do { mapM_ report_dup err_prs; failM } 781 782 -------------- Error reporting ------------ 783 err_prs :: [(Name,Name)] 784 err_prs = [ (n1,n2) 785 | pr :| prs <- findDupsEq ((==) `on` snd) swizzle_prs 786 , (n1,_):(n2,_):_ <- [nubBy ((==) `on` fst) (pr:prs)] ] 787 -- This nubBy avoids bogus error reports when we have 788 -- [("f", f), ..., ("f",f)....] in swizzle_prs 789 -- which happens with class C f where { type T f } 790 791 report_dup :: (Name,Name) -> TcM () 792 report_dup (n1,n2) 793 = setSrcSpan (getSrcSpan n2) $ addErrTc $ 794 hang (text "Different names for the same type variable:") 2 info 795 where 796 info | nameOccName n1 /= nameOccName n2 797 = quotes (ppr n1) <+> text "and" <+> quotes (ppr n2) 798 | otherwise -- Same OccNames! See C2 in 799 -- Note [Swizzling the tyvars before generaliseTcTyCon] 800 = vcat [ quotes (ppr n1) <+> text "bound at" <+> ppr (getSrcLoc n1) 801 , quotes (ppr n2) <+> text "bound at" <+> ppr (getSrcLoc n2) ] 802 803 -------------- The swizzler ------------ 804 -- This does a deep traverse, simply doing a 805 -- Name-to-Name change, governed by swizzle_env 806 -- The 'swap' is what gets from the representative TyVar 807 -- back to the original user-specified Name 808 swizzle_env = mkVarEnv (map swap swizzle_prs) 809 810 swizzleMapper :: TyCoMapper () Identity 811 swizzleMapper = TyCoMapper { tcm_tyvar = swizzle_tv 812 , tcm_covar = swizzle_cv 813 , tcm_hole = swizzle_hole 814 , tcm_tycobinder = swizzle_bndr 815 , tcm_tycon = swizzle_tycon } 816 swizzle_hole _ hole = pprPanic "swizzle_hole" (ppr hole) 817 -- These types are pre-zonked 818 swizzle_tycon tc = pprPanic "swizzle_tc" (ppr tc) 819 -- TcTyCons can't appear in kinds (yet) 820 swizzle_tv _ tv = return (mkTyVarTy (swizzle_var tv)) 821 swizzle_cv _ cv = return (mkCoVarCo (swizzle_var cv)) 822 823 swizzle_bndr _ tcv _ 824 = return ((), swizzle_var tcv) 825 826 swizzle_var :: Var -> Var 827 swizzle_var v 828 | Just nm <- lookupVarEnv swizzle_env v 829 = updateVarType swizzle_ty (v `setVarName` nm) 830 | otherwise 831 = updateVarType swizzle_ty v 832 833 swizzle_ty ty = runIdentity (mapType swizzleMapper () ty) 834 835 836generaliseTcTyCon :: (TcTyCon, ScopedPairs, TcKind) -> TcM TcTyCon 837generaliseTcTyCon (tc, scoped_prs, tc_res_kind) 838 -- See Note [Required, Specified, and Inferred for types] 839 = setSrcSpan (getSrcSpan tc) $ 840 addTyConCtxt tc $ 841 do { -- Step 1: Separate Specified from Required variables 842 -- NB: spec_req_tvs = spec_tvs ++ req_tvs 843 -- And req_tvs is 1-1 with tyConTyVars 844 -- See Note [Scoped tyvars in a TcTyCon] in TyCon 845 ; let spec_req_tvs = map snd scoped_prs 846 n_spec = length spec_req_tvs - tyConArity tc 847 (spec_tvs, req_tvs) = splitAt n_spec spec_req_tvs 848 sorted_spec_tvs = scopedSort spec_tvs 849 -- NB: We can't do the sort until we've zonked 850 -- Maintain the L-R order of scoped_tvs 851 852 -- Step 2a: find all the Inferred variables we want to quantify over 853 ; dvs1 <- candidateQTyVarsOfKinds $ 854 (tc_res_kind : map tyVarKind spec_req_tvs) 855 ; let dvs2 = dvs1 `delCandidates` spec_req_tvs 856 857 -- Step 2b: quantify, mainly meaning skolemise the free variables 858 -- Returned 'inferred' are scope-sorted and skolemised 859 ; inferred <- quantifyTyVars dvs2 860 861 ; traceTc "generaliseTcTyCon: pre zonk" 862 (vcat [ text "tycon =" <+> ppr tc 863 , text "spec_req_tvs =" <+> pprTyVars spec_req_tvs 864 , text "tc_res_kind =" <+> ppr tc_res_kind 865 , text "dvs1 =" <+> ppr dvs1 866 , text "inferred =" <+> pprTyVars inferred ]) 867 868 -- Step 3: Final zonk (following kind generalisation) 869 -- See Note [Swizzling the tyvars before generaliseTcTyCon] 870 ; ze <- emptyZonkEnv 871 ; (ze, inferred) <- zonkTyBndrsX ze inferred 872 ; (ze, sorted_spec_tvs) <- zonkTyBndrsX ze sorted_spec_tvs 873 ; (ze, req_tvs) <- zonkTyBndrsX ze req_tvs 874 ; tc_res_kind <- zonkTcTypeToTypeX ze tc_res_kind 875 876 ; traceTc "generaliseTcTyCon: post zonk" $ 877 vcat [ text "tycon =" <+> ppr tc 878 , text "inferred =" <+> pprTyVars inferred 879 , text "spec_req_tvs =" <+> pprTyVars spec_req_tvs 880 , text "sorted_spec_tvs =" <+> pprTyVars sorted_spec_tvs 881 , text "req_tvs =" <+> ppr req_tvs 882 , text "zonk-env =" <+> ppr ze ] 883 884 -- Step 4: Make the TyConBinders. 885 ; let dep_fv_set = candidateKindVars dvs1 886 inferred_tcbs = mkNamedTyConBinders Inferred inferred 887 specified_tcbs = mkNamedTyConBinders Specified sorted_spec_tvs 888 required_tcbs = map (mkRequiredTyConBinder dep_fv_set) req_tvs 889 890 -- Step 5: Assemble the final list. 891 final_tcbs = concat [ inferred_tcbs 892 , specified_tcbs 893 , required_tcbs ] 894 895 -- Step 6: Make the result TcTyCon 896 tycon = mkTcTyCon (tyConName tc) final_tcbs tc_res_kind 897 (mkTyVarNamePairs (sorted_spec_tvs ++ req_tvs)) 898 True {- it's generalised now -} 899 (tyConFlavour tc) 900 901 ; traceTc "generaliseTcTyCon done" $ 902 vcat [ text "tycon =" <+> ppr tc 903 , text "tc_res_kind =" <+> ppr tc_res_kind 904 , text "dep_fv_set =" <+> ppr dep_fv_set 905 , text "inferred_tcbs =" <+> ppr inferred_tcbs 906 , text "specified_tcbs =" <+> ppr specified_tcbs 907 , text "required_tcbs =" <+> ppr required_tcbs 908 , text "final_tcbs =" <+> ppr final_tcbs ] 909 910 -- Step 7: Check for validity. 911 -- We do this here because we're about to put the tycon into the 912 -- the environment, and we don't want anything malformed there 913 ; checkTyConTelescope tycon 914 915 ; return tycon } 916 917{- Note [Required, Specified, and Inferred for types] 918~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 919Each forall'd type variable in a type or kind is one of 920 921 * Required: an argument must be provided at every call site 922 923 * Specified: the argument can be inferred at call sites, but 924 may be instantiated with visible type/kind application 925 926 * Inferred: the must be inferred at call sites; it 927 is unavailable for use with visible type/kind application. 928 929Why have Inferred at all? Because we just can't make user-facing 930promises about the ordering of some variables. These might swizzle 931around even between minor released. By forbidding visible type 932application, we ensure users aren't caught unawares. 933 934Go read Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep. 935 936The question for this Note is this: 937 given a TyClDecl, how are its quantified type variables classified? 938Much of the debate is memorialized in #15743. 939 940Here is our design choice. When inferring the ordering of variables 941for a TyCl declaration (that is, for those variables that he user 942has not specified the order with an explicit `forall`), we use the 943following order: 944 945 1. Inferred variables 946 2. Specified variables; in the left-to-right order in which 947 the user wrote them, modified by scopedSort (see below) 948 to put them in depdendency order. 949 3. Required variables before a top-level :: 950 4. All variables after a top-level :: 951 952If this ordering does not make a valid telescope, we reject the definition. 953 954Example: 955 data SameKind :: k -> k -> * 956 data Bad a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d) 957 958For Bad: 959 - a, c, d, x are Required; they are explicitly listed by the user 960 as the positional arguments of Bad 961 - b is Specified; it appears explicitly in a kind signature 962 - k, the kind of a, is Inferred; it is not mentioned explicitly at all 963 964Putting variables in the order Inferred, Specified, Required 965gives us this telescope: 966 Inferred: k 967 Specified: b : Proxy a 968 Required : (a : k) (c : Proxy b) (d : Proxy a) (x : SameKind b d) 969 970But this order is ill-scoped, because b's kind mentions a, which occurs 971after b in the telescope. So we reject Bad. 972 973Associated types 974~~~~~~~~~~~~~~~~ 975For associated types everything above is determined by the 976associated-type declaration alone, ignoring the class header. 977Here is an example (#15592) 978 class C (a :: k) b where 979 type F (x :: b a) 980 981In the kind of C, 'k' is Specified. But what about F? 982In the kind of F, 983 984 * Should k be Inferred or Specified? It's Specified for C, 985 but not mentioned in F's declaration. 986 987 * In which order should the Specified variables a and b occur? 988 It's clearly 'a' then 'b' in C's declaration, but the L-R ordering 989 in F's declaration is 'b' then 'a'. 990 991In both cases we make the choice by looking at F's declaration alone, 992so it gets the kind 993 F :: forall {k}. forall b a. b a -> Type 994 995How it works 996~~~~~~~~~~~~ 997These design choices are implemented by two completely different code 998paths for 999 1000 * Declarations with a standalone kind signature or a complete user-specified 1001 kind signature (CUSK). Handled by the kcCheckDeclHeader. 1002 1003 * Declarations without a kind signature (standalone or CUSK) are handled by 1004 kcInferDeclHeader; see Note [Inferring kinds for type declarations]. 1005 1006Note that neither code path worries about point (4) above, as this 1007is nicely handled by not mangling the res_kind. (Mangling res_kinds is done 1008*after* all this stuff, in tcDataDefn's call to etaExpandAlgTyCon.) 1009 1010We can tell Inferred apart from Specified by looking at the scoped 1011tyvars; Specified are always included there. 1012 1013Design alternatives 1014~~~~~~~~~~~~~~~~~~~ 1015* For associated types we considered putting the class variables 1016 before the local variables, in a nod to the treatment for class 1017 methods. But it got too compilicated; see #15592, comment:21ff. 1018 1019* We rigidly require the ordering above, even though we could be much more 1020 permissive. Relevant musings are at 1021 https://gitlab.haskell.org/ghc/ghc/issues/15743#note_161623 1022 The bottom line conclusion is that, if the user wants a different ordering, 1023 then can specify it themselves, and it is better to be predictable and dumb 1024 than clever and capricious. 1025 1026 I (Richard) conjecture we could be fully permissive, allowing all classes 1027 of variables to intermix. We would have to augment ScopedSort to refuse to 1028 reorder Required variables (or check that it wouldn't have). But this would 1029 allow more programs. See #15743 for examples. Interestingly, Idris seems 1030 to allow this intermixing. The intermixing would be fully specified, in that 1031 we can be sure that inference wouldn't change between versions. However, 1032 would users be able to predict it? That I cannot answer. 1033 1034Test cases (and tickets) relevant to these design decisions 1035~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1036 T15591* 1037 T15592* 1038 T15743* 1039 1040Note [Inferring kinds for type declarations] 1041~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1042This note deals with /inference/ for type declarations 1043that do not have a CUSK. Consider 1044 data T (a :: k1) k2 (x :: k2) = MkT (S a k2 x) 1045 data S (b :: k3) k4 (y :: k4) = MkS (T b k4 y) 1046 1047We do kind inference as follows: 1048 1049* Step 1: inferInitialKinds, and in particular kcInferDeclHeader. 1050 Make a unification variable for each of the Required and Specified 1051 type variables in the header. 1052 1053 Record the connection between the Names the user wrote and the 1054 fresh unification variables in the tcTyConScopedTyVars field 1055 of the TcTyCon we are making 1056 [ (a, aa) 1057 , (k1, kk1) 1058 , (k2, kk2) 1059 , (x, xx) ] 1060 (I'm using the convention that double letter like 'aa' or 'kk' 1061 mean a unification variable.) 1062 1063 These unification variables 1064 - Are TyVarTvs: that is, unification variables that can 1065 unify only with other type variables. 1066 See Note [Signature skolems] in TcType 1067 1068 - Have complete fresh Names; see TcMType 1069 Note [Unification variables need fresh Names] 1070 1071 Assign initial monomorophic kinds to S, T 1072 T :: kk1 -> * -> kk2 -> * 1073 S :: kk3 -> * -> kk4 -> * 1074 1075* Step 2: kcTyClDecl. Extend the environment with a TcTyCon for S and 1076 T, with these monomorphic kinds. Now kind-check the declarations, 1077 and solve the resulting equalities. The goal here is to discover 1078 constraints on all these unification variables. 1079 1080 Here we find that kk1 := kk3, and kk2 := kk4. 1081 1082 This is why we can't use skolems for kk1 etc; they have to 1083 unify with each other. 1084 1085* Step 3: generaliseTcTyCon. Generalise each TyCon in turn. 1086 We find the free variables of the kind, skolemise them, 1087 sort them out into Inferred/Required/Specified (see the above 1088 Note [Required, Specified, and Inferred for types]), 1089 and perform some validity checks. 1090 1091 This makes the utterly-final TyConBinders for the TyCon. 1092 1093 All this is very similar at the level of terms: see TcBinds 1094 Note [Quantified variables in partial type signatures] 1095 1096 But there some tricky corners: Note [Tricky scoping in generaliseTcTyCon] 1097 1098* Step 4. Extend the type environment with a TcTyCon for S and T, now 1099 with their utterly-final polymorphic kinds (needed for recursive 1100 occurrences of S, T). Now typecheck the declarations, and build the 1101 final AlgTyCOn for S and T resp. 1102 1103The first three steps are in kcTyClGroup; the fourth is in 1104tcTyClDecls. 1105 1106There are some wrinkles 1107 1108* Do not default TyVarTvs. We always want to kind-generalise over 1109 TyVarTvs, and /not/ default them to Type. By definition a TyVarTv is 1110 not allowed to unify with a type; it must stand for a type 1111 variable. Hence the check in TcSimplify.defaultTyVarTcS, and 1112 TcMType.defaultTyVar. Here's another example (#14555): 1113 data Exp :: [TYPE rep] -> TYPE rep -> Type where 1114 Lam :: Exp (a:xs) b -> Exp xs (a -> b) 1115 We want to kind-generalise over the 'rep' variable. 1116 #14563 is another example. 1117 1118* Duplicate type variables. Consider #11203 1119 data SameKind :: k -> k -> * 1120 data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b) 1121 Here we will unify k1 with k2, but this time doing so is an error, 1122 because k1 and k2 are bound in the same declaration. 1123 1124 We spot this during validity checking (findDupTyVarTvs), 1125 in generaliseTcTyCon. 1126 1127* Required arguments. Even the Required arguments should be made 1128 into TyVarTvs, not skolems. Consider 1129 data T k (a :: k) 1130 Here, k is a Required, dependent variable. For uniformity, it is helpful 1131 to have k be a TyVarTv, in parallel with other dependent variables. 1132 1133* Duplicate skolemisation is expected. When generalising in Step 3, 1134 we may find that one of the variables we want to quantify has 1135 already been skolemised. For example, suppose we have already 1136 generalise S. When we come to T we'll find that kk1 (now the same as 1137 kk3) has already been skolemised. 1138 1139 That's fine -- but it means that 1140 a) when collecting quantification candidates, in 1141 candidateQTyVarsOfKind, we must collect skolems 1142 b) quantifyTyVars should be a no-op on such a skolem 1143 1144Note [Tricky scoping in generaliseTcTyCon] 1145~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1146Consider #16342 1147 class C (a::ka) x where 1148 cop :: D a x => x -> Proxy a -> Proxy a 1149 cop _ x = x :: Proxy (a::ka) 1150 1151 class D (b::kb) y where 1152 dop :: C b y => y -> Proxy b -> Proxy b 1153 dop _ x = x :: Proxy (b::kb) 1154 1155C and D are mutually recursive, by the time we get to 1156generaliseTcTyCon we'll have unified kka := kkb. 1157 1158But when typechecking the default declarations for 'cop' and 'dop' in 1159tcDlassDecl2 we need {a, ka} and {b, kb} respectively to be in scope. 1160But at that point all we have is the utterly-final Class itself. 1161 1162Conclusion: the classTyVars of a class must have the same Name as 1163that originally assigned by the user. In our example, C must have 1164classTyVars {a, ka, x} while D has classTyVars {a, kb, y}. Despite 1165the fact that kka and kkb got unified! 1166 1167We achieve this sleight of hand in generaliseTcTyCon, using 1168the specialised function zonkRecTyVarBndrs. We make the call 1169 zonkRecTyVarBndrs [ka,a,x] [kkb,aa,xxx] 1170where the [ka,a,x] are the Names originally assigned by the user, and 1171[kkb,aa,xx] are the corresponding (post-zonking, skolemised) TcTyVars. 1172zonkRecTyVarBndrs builds a recursive ZonkEnv that binds 1173 kkb :-> (ka :: <zonked kind of kkb>) 1174 aa :-> (a :: <konked kind of aa>) 1175 etc 1176That is, it maps each skolemised TcTyVars to the utterly-final 1177TyVar to put in the class, with its correct user-specified name. 1178When generalising D we'll do the same thing, but the ZonkEnv will map 1179 kkb :-> (kb :: <zonked kind of kkb>) 1180 bb :-> (b :: <konked kind of bb>) 1181 etc 1182Note that 'kkb' again appears in the domain of the mapping, but this 1183time mapped to 'kb'. That's how C and D end up with differently-named 1184final TyVars despite the fact that we unified kka:=kkb 1185 1186zonkRecTyVarBndrs we need to do knot-tying because of the need to 1187apply this same substitution to the kind of each. 1188 1189Note [Inferring visible dependent quantification] 1190~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1191Consider 1192 1193 data T k :: k -> Type where 1194 MkT1 :: T Type Int 1195 MkT2 :: T (Type -> Type) Maybe 1196 1197This looks like it should work. However, it is polymorphically recursive, 1198as the uses of T in the constructor types specialize the k in the kind 1199of T. This trips up our dear users (#17131, #17541), and so we add 1200a "landmark" context (which cannot be suppressed) whenever we 1201spot inferred visible dependent quantification (VDQ). 1202 1203It's hard to know when we've actually been tripped up by polymorphic recursion 1204specifically, so we just include a note to users whenever we infer VDQ. The 1205testsuite did not show up a single spurious inclusion of this message. 1206 1207The context is added in addVDQNote, which looks for a visible TyConBinder 1208that also appears in the TyCon's kind. (I first looked at the kind for 1209a visible, dependent quantifier, but Note [No polymorphic recursion] in 1210TcHsType defeats that approach.) addVDQNote is used in kcTyClDecl, 1211which is used only when inferring the kind of a tycon (never with a CUSK or 1212SAK). 1213 1214Once upon a time, I (Richard E) thought that the tycon-kind could 1215not be a forall-type. But this is wrong: data T :: forall k. k -> Type 1216(with -XNoCUSKs) could end up here. And this is all OK. 1217 1218 1219-} 1220 1221-------------- 1222tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a 1223tcExtendKindEnvWithTyCons tcs 1224 = tcExtendKindEnvList [ (tyConName tc, ATcTyCon tc) | tc <- tcs ] 1225 1226-------------- 1227mkPromotionErrorEnv :: [LTyClDecl GhcRn] -> TcTypeEnv 1228-- Maps each tycon/datacon to a suitable promotion error 1229-- tc :-> APromotionErr TyConPE 1230-- dc :-> APromotionErr RecDataConPE 1231-- See Note [Recursion and promoting data constructors] 1232 1233mkPromotionErrorEnv decls 1234 = foldr (plusNameEnv . mk_prom_err_env . unLoc) 1235 emptyNameEnv decls 1236 1237mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv 1238mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats }) 1239 = unitNameEnv nm (APromotionErr ClassPE) 1240 `plusNameEnv` 1241 mkNameEnv [ (familyDeclName at, APromotionErr TyConPE) 1242 | L _ at <- ats ] 1243 1244mk_prom_err_env (DataDecl { tcdLName = L _ name 1245 , tcdDataDefn = HsDataDefn { dd_cons = cons } }) 1246 = unitNameEnv name (APromotionErr TyConPE) 1247 `plusNameEnv` 1248 mkNameEnv [ (con, APromotionErr RecDataConPE) 1249 | L _ con' <- cons 1250 , L _ con <- getConNames con' ] 1251 1252mk_prom_err_env decl 1253 = unitNameEnv (tcdName decl) (APromotionErr TyConPE) 1254 -- Works for family declarations too 1255 1256-------------- 1257inferInitialKinds :: [LTyClDecl GhcRn] -> TcM [TcTyCon] 1258-- Returns a TcTyCon for each TyCon bound by the decls, 1259-- each with its initial kind 1260 1261inferInitialKinds decls 1262 = do { traceTc "inferInitialKinds {" $ ppr (map (tcdName . unLoc) decls) 1263 ; tcs <- concatMapM infer_initial_kind decls 1264 ; traceTc "inferInitialKinds done }" empty 1265 ; return tcs } 1266 where 1267 infer_initial_kind = addLocM (getInitialKind InitialKindInfer) 1268 1269-- Check type/class declarations against their standalone kind signatures or 1270-- CUSKs, producing a generalized TcTyCon for each. 1271checkInitialKinds :: [(LTyClDecl GhcRn, SAKS_or_CUSK)] -> TcM [TcTyCon] 1272checkInitialKinds decls 1273 = do { traceTc "checkInitialKinds {" $ ppr (mapFst (tcdName . unLoc) decls) 1274 ; tcs <- concatMapM check_initial_kind decls 1275 ; traceTc "checkInitialKinds done }" empty 1276 ; return tcs } 1277 where 1278 check_initial_kind (ldecl, msig) = 1279 addLocM (getInitialKind (InitialKindCheck msig)) ldecl 1280 1281-- | Get the initial kind of a TyClDecl, either generalized or non-generalized, 1282-- depending on the 'InitialKindStrategy'. 1283getInitialKind :: InitialKindStrategy -> TyClDecl GhcRn -> TcM [TcTyCon] 1284 1285-- Allocate a fresh kind variable for each TyCon and Class 1286-- For each tycon, return a TcTyCon with kind k 1287-- where k is the kind of tc, derived from the LHS 1288-- of the definition (and probably including 1289-- kind unification variables) 1290-- Example: data T a b = ... 1291-- return (T, kv1 -> kv2 -> kv3) 1292-- 1293-- This pass deals with (ie incorporates into the kind it produces) 1294-- * The kind signatures on type-variable binders 1295-- * The result kinds signature on a TyClDecl 1296-- 1297-- No family instances are passed to checkInitialKinds/inferInitialKinds 1298getInitialKind strategy 1299 (ClassDecl { tcdLName = L _ name 1300 , tcdTyVars = ktvs 1301 , tcdATs = ats }) 1302 = do { cls <- kcDeclHeader strategy name ClassFlavour ktvs $ 1303 return (TheKind constraintKind) 1304 ; let parent_tv_prs = tcTyConScopedTyVars cls 1305 -- See Note [Don't process associated types in getInitialKind] 1306 ; inner_tcs <- 1307 tcExtendNameTyVarEnv parent_tv_prs $ 1308 mapM (addLocM (getAssocFamInitialKind cls)) ats 1309 ; return (cls : inner_tcs) } 1310 where 1311 getAssocFamInitialKind cls = 1312 case strategy of 1313 InitialKindInfer -> get_fam_decl_initial_kind (Just cls) 1314 InitialKindCheck _ -> check_initial_kind_assoc_fam cls 1315 1316getInitialKind strategy 1317 (DataDecl { tcdLName = L _ name 1318 , tcdTyVars = ktvs 1319 , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig 1320 , dd_ND = new_or_data } }) 1321 = do { let flav = newOrDataToFlavour new_or_data 1322 ctxt = DataKindCtxt name 1323 ; tc <- kcDeclHeader strategy name flav ktvs $ 1324 case m_sig of 1325 Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig 1326 Nothing -> dataDeclDefaultResultKind new_or_data 1327 ; return [tc] } 1328 1329getInitialKind InitialKindInfer (FamDecl { tcdFam = decl }) 1330 = do { tc <- get_fam_decl_initial_kind Nothing decl 1331 ; return [tc] } 1332 1333getInitialKind (InitialKindCheck msig) (FamDecl { tcdFam = 1334 FamilyDecl { fdLName = unLoc -> name 1335 , fdTyVars = ktvs 1336 , fdResultSig = unLoc -> resultSig 1337 , fdInfo = info } } ) 1338 = do { let flav = getFamFlav Nothing info 1339 ctxt = TyFamResKindCtxt name 1340 ; tc <- kcDeclHeader (InitialKindCheck msig) name flav ktvs $ 1341 case famResultKindSignature resultSig of 1342 Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig 1343 Nothing -> 1344 case msig of 1345 CUSK -> return (TheKind liftedTypeKind) 1346 SAKS _ -> return AnyKind 1347 ; return [tc] } 1348 1349getInitialKind strategy 1350 (SynDecl { tcdLName = L _ name 1351 , tcdTyVars = ktvs 1352 , tcdRhs = rhs }) 1353 = do { let ctxt = TySynKindCtxt name 1354 ; tc <- kcDeclHeader strategy name TypeSynonymFlavour ktvs $ 1355 case hsTyKindSig rhs of 1356 Just rhs_sig -> TheKind <$> tcLHsKindSig ctxt rhs_sig 1357 Nothing -> return AnyKind 1358 ; return [tc] } 1359 1360getInitialKind _ (DataDecl _ _ _ _ (XHsDataDefn nec)) = noExtCon nec 1361getInitialKind _ (FamDecl {tcdFam = XFamilyDecl nec}) = noExtCon nec 1362getInitialKind _ (XTyClDecl nec) = noExtCon nec 1363 1364get_fam_decl_initial_kind 1365 :: Maybe TcTyCon -- ^ Just cls <=> this is an associated family of class cls 1366 -> FamilyDecl GhcRn 1367 -> TcM TcTyCon 1368get_fam_decl_initial_kind mb_parent_tycon 1369 FamilyDecl { fdLName = L _ name 1370 , fdTyVars = ktvs 1371 , fdResultSig = L _ resultSig 1372 , fdInfo = info } 1373 = kcDeclHeader InitialKindInfer name flav ktvs $ 1374 case resultSig of 1375 KindSig _ ki -> TheKind <$> tcLHsKindSig ctxt ki 1376 TyVarSig _ (L _ (KindedTyVar _ _ ki)) -> TheKind <$> tcLHsKindSig ctxt ki 1377 _ -- open type families have * return kind by default 1378 | tcFlavourIsOpen flav -> return (TheKind liftedTypeKind) 1379 -- closed type families have their return kind inferred 1380 -- by default 1381 | otherwise -> return AnyKind 1382 where 1383 flav = getFamFlav mb_parent_tycon info 1384 ctxt = TyFamResKindCtxt name 1385get_fam_decl_initial_kind _ (XFamilyDecl nec) = noExtCon nec 1386 1387-- See Note [Standalone kind signatures for associated types] 1388check_initial_kind_assoc_fam 1389 :: TcTyCon -- parent class 1390 -> FamilyDecl GhcRn 1391 -> TcM TcTyCon 1392check_initial_kind_assoc_fam cls 1393 FamilyDecl 1394 { fdLName = unLoc -> name 1395 , fdTyVars = ktvs 1396 , fdResultSig = unLoc -> resultSig 1397 , fdInfo = info } 1398 = kcDeclHeader (InitialKindCheck CUSK) name flav ktvs $ 1399 case famResultKindSignature resultSig of 1400 Just ksig -> TheKind <$> tcLHsKindSig ctxt ksig 1401 Nothing -> return (TheKind liftedTypeKind) 1402 where 1403 ctxt = TyFamResKindCtxt name 1404 flav = getFamFlav (Just cls) info 1405check_initial_kind_assoc_fam _ (XFamilyDecl nec) = noExtCon nec 1406 1407{- Note [Standalone kind signatures for associated types] 1408~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1409 1410If associated types had standalone kind signatures, would they wear them 1411 1412---------------------------+------------------------------ 1413 like this? (OUT) | or like this? (IN) 1414---------------------------+------------------------------ 1415 type T :: Type -> Type | class C a where 1416 class C a where | type T :: Type -> Type 1417 type T a | type T a 1418 1419The (IN) variant is syntactically ambiguous: 1420 1421 class C a where 1422 type T :: a -- standalone kind signature? 1423 type T :: a -- declaration header? 1424 1425The (OUT) variant does not suffer from this issue, but it might not be the 1426direction in which we want to take Haskell: we seek to unify type families and 1427functions, and, by extension, associated types with class methods. And yet we 1428give class methods their signatures inside the class, not outside. Neither do 1429we have the counterpart of InstanceSigs for StandaloneKindSignatures. 1430 1431For now, we dodge the question by using CUSKs for associated types instead of 1432standalone kind signatures. This is a simple addition to the rule we used to 1433have before standalone kind signatures: 1434 1435 old rule: associated type has a CUSK iff its parent class has a CUSK 1436 new rule: associated type has a CUSK iff its parent class has a CUSK or a standalone kind signature 1437 1438-} 1439 1440-- See Note [Data declaration default result kind] 1441dataDeclDefaultResultKind :: NewOrData -> TcM ContextKind 1442dataDeclDefaultResultKind new_or_data = do 1443 -- See Note [Implementation of UnliftedNewtypes] 1444 unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes 1445 return $ case new_or_data of 1446 NewType | unlifted_newtypes -> OpenKind 1447 _ -> TheKind liftedTypeKind 1448 1449{- Note [Data declaration default result kind] 1450~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1451 1452When the user has not written an inline result kind annotation on a data 1453declaration, we assume it to be 'Type'. That is, the following declarations 1454D1 and D2 are considered equivalent: 1455 1456 data D1 where ... 1457 data D2 :: Type where ... 1458 1459The consequence of this assumption is that we reject D3 even though we 1460accept D4: 1461 1462 data D3 where 1463 MkD3 :: ... -> D3 param 1464 1465 data D4 :: Type -> Type where 1466 MkD4 :: ... -> D4 param 1467 1468However, there's a twist: when -XUnliftedNewtypes are enabled, we must relax 1469the assumed result kind to (TYPE r) for newtypes: 1470 1471 newtype D5 where 1472 MkD5 :: Int# -> D5 1473 1474dataDeclDefaultResultKind takes care to produce the appropriate result kind. 1475-} 1476 1477--------------------------------- 1478getFamFlav 1479 :: Maybe TcTyCon -- ^ Just cls <=> this is an associated family of class cls 1480 -> FamilyInfo pass 1481 -> TyConFlavour 1482getFamFlav mb_parent_tycon info = 1483 case info of 1484 DataFamily -> DataFamilyFlavour mb_parent_tycon 1485 OpenTypeFamily -> OpenTypeFamilyFlavour mb_parent_tycon 1486 ClosedTypeFamily _ -> ASSERT( isNothing mb_parent_tycon ) -- See Note [Closed type family mb_parent_tycon] 1487 ClosedTypeFamilyFlavour 1488 1489{- Note [Closed type family mb_parent_tycon] 1490~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1491There's no way to write a closed type family inside a class declaration: 1492 1493 class C a where 1494 type family F a where -- error: parse error on input ‘where’ 1495 1496In fact, it is not clear what the meaning of such a declaration would be. 1497Therefore, 'mb_parent_tycon' of any closed type family has to be Nothing. 1498-} 1499 1500------------------------------------------------------------------------ 1501kcLTyClDecl :: LTyClDecl GhcRn -> TcM () 1502 -- See Note [Kind checking for type and class decls] 1503 -- Called only for declarations without a signature (no CUSKs or SAKs here) 1504kcLTyClDecl (L loc decl) 1505 = setSrcSpan loc $ 1506 do { tycon <- kcLookupTcTyCon tc_name 1507 ; traceTc "kcTyClDecl {" (ppr tc_name) 1508 ; addVDQNote tycon $ -- See Note [Inferring visible dependent quantification] 1509 addErrCtxt (tcMkDeclCtxt decl) $ 1510 kcTyClDecl decl tycon 1511 ; traceTc "kcTyClDecl done }" (ppr tc_name) } 1512 where 1513 tc_name = tcdName decl 1514 1515kcTyClDecl :: TyClDecl GhcRn -> TcTyCon -> TcM () 1516-- This function is used solely for its side effect on kind variables 1517-- NB kind signatures on the type variables and 1518-- result kind signature have already been dealt with 1519-- by inferInitialKind, so we can ignore them here. 1520 1521kcTyClDecl (DataDecl { tcdLName = (L _ name) 1522 , tcdDataDefn = defn }) tyCon 1523 | HsDataDefn { dd_cons = cons@((L _ (ConDeclGADT {})) : _) 1524 , dd_ctxt = (L _ []) 1525 , dd_ND = new_or_data } <- defn 1526 = -- See Note [Implementation of UnliftedNewtypes] STEP 2 1527 kcConDecls new_or_data (tyConResKind tyCon) cons 1528 1529 -- hs_tvs and dd_kindSig already dealt with in inferInitialKind 1530 -- This must be a GADT-style decl, 1531 -- (see invariants of DataDefn declaration) 1532 -- so (a) we don't need to bring the hs_tvs into scope, because the 1533 -- ConDecls bind all their own variables 1534 -- (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it 1535 1536 | HsDataDefn { dd_ctxt = ctxt 1537 , dd_cons = cons 1538 , dd_ND = new_or_data } <- defn 1539 = bindTyClTyVars name $ \ _ _ -> 1540 do { _ <- tcHsContext ctxt 1541 ; kcConDecls new_or_data (tyConResKind tyCon) cons 1542 } 1543 1544kcTyClDecl (SynDecl { tcdLName = L _ name, tcdRhs = rhs }) _tycon 1545 = bindTyClTyVars name $ \ _ res_kind -> 1546 discardResult $ tcCheckLHsType rhs res_kind 1547 -- NB: check against the result kind that we allocated 1548 -- in inferInitialKinds. 1549 1550kcTyClDecl (ClassDecl { tcdLName = L _ name 1551 , tcdCtxt = ctxt, tcdSigs = sigs }) _tycon 1552 = bindTyClTyVars name $ \ _ _ -> 1553 do { _ <- tcHsContext ctxt 1554 ; mapM_ (wrapLocM_ kc_sig) sigs } 1555 where 1556 kc_sig (ClassOpSig _ _ nms op_ty) = kcClassSigType skol_info nms op_ty 1557 kc_sig _ = return () 1558 1559 skol_info = TyConSkol ClassFlavour name 1560 1561kcTyClDecl (FamDecl _ (FamilyDecl { fdInfo = fd_info })) fam_tc 1562-- closed type families look at their equations, but other families don't 1563-- do anything here 1564 = case fd_info of 1565 ClosedTypeFamily (Just eqns) -> mapM_ (kcTyFamInstEqn fam_tc) eqns 1566 _ -> return () 1567kcTyClDecl (FamDecl _ (XFamilyDecl nec)) _ = noExtCon nec 1568kcTyClDecl (DataDecl _ _ _ _ (XHsDataDefn nec)) _ = noExtCon nec 1569kcTyClDecl (XTyClDecl nec) _ = noExtCon nec 1570 1571------------------- 1572 1573-- | Unify the kind of the first type provided with the newtype's kind, if 1574-- -XUnliftedNewtypes is enabled and the NewOrData indicates Newtype. If there 1575-- is more than one type provided, do nothing: the newtype is in error, and this 1576-- will be caught in validity checking (which will give a better error than we can 1577-- here.) 1578unifyNewtypeKind :: DynFlags 1579 -> NewOrData 1580 -> [LHsType GhcRn] -- user-written argument types, should be just 1 1581 -> [TcType] -- type-checked argument types, should be just 1 1582 -> TcKind -- expected kind of newtype 1583 -> TcM [TcType] -- casted argument types (should be just 1) 1584 -- result = orig_arg |> kind_co 1585 -- where kind_co :: orig_arg_ki ~N expected_ki 1586unifyNewtypeKind dflags NewType [hs_ty] [tc_ty] ki 1587 | xopt LangExt.UnliftedNewtypes dflags 1588 = do { traceTc "unifyNewtypeKind" (ppr hs_ty $$ ppr tc_ty $$ ppr ki) 1589 ; co <- unifyKind (Just (unLoc hs_ty)) (typeKind tc_ty) ki 1590 ; return [tc_ty `mkCastTy` co] } 1591 -- See comments above: just do nothing here 1592unifyNewtypeKind _ _ _ arg_tys _ = return arg_tys 1593 1594-- Type check the types of the arguments to a data constructor. 1595-- This includes doing kind unification if the type is a newtype. 1596-- See Note [Implementation of UnliftedNewtypes] for why we need 1597-- the first two arguments. 1598kcConArgTys :: NewOrData -> Kind -> [LHsType GhcRn] -> TcM () 1599kcConArgTys new_or_data res_kind arg_tys = do 1600 { arg_tc_tys <- mapM (tcHsOpenType . getBangType) arg_tys 1601 -- See Note [Implementation of UnliftedNewtypes], STEP 2 1602 ; dflags <- getDynFlags 1603 ; discardResult $ 1604 unifyNewtypeKind dflags new_or_data arg_tys arg_tc_tys res_kind 1605 } 1606 1607kcConDecls :: NewOrData 1608 -> Kind -- The result kind signature 1609 -> [LConDecl GhcRn] -- The data constructors 1610 -> TcM () 1611kcConDecls new_or_data res_kind cons 1612 = mapM_ (wrapLocM_ (kcConDecl new_or_data final_res_kind)) cons 1613 where 1614 (_, final_res_kind) = splitPiTys res_kind 1615 -- See Note [kcConDecls result kind] 1616 1617-- Kind check a data constructor. In additional to the data constructor, 1618-- we also need to know about whether or not its corresponding type was 1619-- declared with data or newtype, and we need to know the result kind of 1620-- this type. See Note [Implementation of UnliftedNewtypes] for why 1621-- we need the first two arguments. 1622kcConDecl :: NewOrData 1623 -> Kind -- Result kind of the type constructor 1624 -- Usually Type but can be TYPE UnliftedRep 1625 -- or even TYPE r, in the case of unlifted newtype 1626 -> ConDecl GhcRn 1627 -> TcM () 1628kcConDecl new_or_data res_kind (ConDeclH98 1629 { con_name = name, con_ex_tvs = ex_tvs 1630 , con_mb_cxt = ex_ctxt, con_args = args }) 1631 = addErrCtxt (dataConCtxtName [name]) $ 1632 discardResult $ 1633 bindExplicitTKBndrs_Tv ex_tvs $ 1634 do { _ <- tcHsMbContext ex_ctxt 1635 ; kcConArgTys new_or_data res_kind (hsConDeclArgTys args) 1636 -- We don't need to check the telescope here, 1637 -- because that's done in tcConDecl 1638 } 1639 1640kcConDecl new_or_data res_kind (ConDeclGADT 1641 { con_names = names, con_qvars = qtvs, con_mb_cxt = cxt 1642 , con_args = args, con_res_ty = res_ty }) 1643 | HsQTvs { hsq_ext = implicit_tkv_nms 1644 , hsq_explicit = explicit_tkv_nms } <- qtvs 1645 = -- Even though the GADT-style data constructor's type is closed, 1646 -- we must still kind-check the type, because that may influence 1647 -- the inferred kind of the /type/ constructor. Example: 1648 -- data T f a where 1649 -- MkT :: f a -> T f a 1650 -- If we don't look at MkT we won't get the correct kind 1651 -- for the type constructor T 1652 addErrCtxt (dataConCtxtName names) $ 1653 discardResult $ 1654 bindImplicitTKBndrs_Tv implicit_tkv_nms $ 1655 bindExplicitTKBndrs_Tv explicit_tkv_nms $ 1656 -- Why "_Tv"? See Note [Kind-checking for GADTs] 1657 do { _ <- tcHsMbContext cxt 1658 ; kcConArgTys new_or_data res_kind (hsConDeclArgTys args) 1659 ; _ <- tcHsOpenType res_ty 1660 ; return () } 1661kcConDecl _ _ (ConDeclGADT _ _ _ (XLHsQTyVars nec) _ _ _ _) = noExtCon nec 1662kcConDecl _ _ (XConDecl nec) = noExtCon nec 1663 1664{- Note [kcConDecls result kind] 1665~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1666We might have e.g. 1667 data T a :: Type -> Type where ... 1668or 1669 newtype instance N a :: Type -> Type where .. 1670in which case, the 'res_kind' passed to kcConDecls will be 1671 Type->Type 1672 1673We must look past those arrows, or even foralls, to the Type in the 1674corner, to pass to kcConDecl c.f. #16828. Hence the splitPiTys here. 1675 1676I am a bit concerned about tycons with a declaration like 1677 data T a :: Type -> forall k. k -> Type where ... 1678 1679It does not have a CUSK, so kcInferDeclHeader will make a TcTyCon 1680with tyConResKind of Type -> forall k. k -> Type. Even that is fine: 1681the splitPiTys will look past the forall. But I'm bothered about 1682what if the type "in the corner" mentions k? This is incredibly 1683obscure but something like this could be bad: 1684 data T a :: Type -> foral k. k -> TYPE (F k) where ... 1685 1686I bet we are not quite right here, but my brain suffered a buffer 1687overflow and I thought it best to nail the common cases right now. 1688 1689Note [Recursion and promoting data constructors] 1690~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1691We don't want to allow promotion in a strongly connected component 1692when kind checking. 1693 1694Consider: 1695 data T f = K (f (K Any)) 1696 1697When kind checking the `data T' declaration the local env contains the 1698mappings: 1699 T -> ATcTyCon <some initial kind> 1700 K -> APromotionErr 1701 1702APromotionErr is only used for DataCons, and only used during type checking 1703in tcTyClGroup. 1704 1705Note [Kind-checking for GADTs] 1706~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1707Consider 1708 1709 data Proxy a where 1710 MkProxy1 :: forall k (b :: k). Proxy b 1711 MkProxy2 :: forall j (c :: j). Proxy c 1712 1713It seems reasonable that this should be accepted. But something very strange 1714is going on here: when we're kind-checking this declaration, we need to unify 1715the kind of `a` with k and j -- even though k and j's scopes are local to the type of 1716MkProxy{1,2}. The best approach we've come up with is to use TyVarTvs during 1717the kind-checking pass. First off, note that it's OK if the kind-checking pass 1718is too permissive: we'll snag the problems in the type-checking pass later. 1719(This extra permissiveness might happen with something like 1720 1721 data SameKind :: k -> k -> Type 1722 data Bad a where 1723 MkBad :: forall k1 k2 (a :: k1) (b :: k2). Bad (SameKind a b) 1724 1725which would be accepted if k1 and k2 were TyVarTvs. This is correctly rejected 1726in the second pass, though. Test case: polykinds/TyVarTvKinds3) 1727Recall that the kind-checking pass exists solely to collect constraints 1728on the kinds and to power unification. 1729 1730To achieve the use of TyVarTvs, we must be careful to use specialized functions 1731that produce TyVarTvs, not ordinary skolems. This is why we need 1732kcExplicitTKBndrs and kcImplicitTKBndrs in TcHsType, separate from their 1733tc... variants. 1734 1735The drawback of this approach is sometimes it will accept a definition that 1736a (hypothetical) declarative specification would likely reject. As a general 1737rule, we don't want to allow polymorphic recursion without a CUSK. Indeed, 1738the whole point of CUSKs is to allow polymorphic recursion. Yet, the TyVarTvs 1739approach allows a limited form of polymorphic recursion *without* a CUSK. 1740 1741To wit: 1742 data T a = forall k (b :: k). MkT (T b) Int 1743 (test case: dependent/should_compile/T14066a) 1744 1745Note that this is polymorphically recursive, with the recursive occurrence 1746of T used at a kind other than a's kind. The approach outlined here accepts 1747this definition, because this kind is still a kind variable (and so the 1748TyVarTvs unify). Stepping back, I (Richard) have a hard time envisioning a 1749way to describe exactly what declarations will be accepted and which will 1750be rejected (without a CUSK). However, the accepted definitions are indeed 1751well-kinded and any rejected definitions would be accepted with a CUSK, 1752and so this wrinkle need not cause anyone to lose sleep. 1753 1754************************************************************************ 1755* * 1756\subsection{Type checking} 1757* * 1758************************************************************************ 1759 1760Note [Type checking recursive type and class declarations] 1761~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1762At this point we have completed *kind-checking* of a mutually 1763recursive group of type/class decls (done in kcTyClGroup). However, 1764we discarded the kind-checked types (eg RHSs of data type decls); 1765note that kcTyClDecl returns (). There are two reasons: 1766 1767 * It's convenient, because we don't have to rebuild a 1768 kinded HsDecl (a fairly elaborate type) 1769 1770 * It's necessary, because after kind-generalisation, the 1771 TyCons/Classes may now be kind-polymorphic, and hence need 1772 to be given kind arguments. 1773 1774Example: 1775 data T f a = MkT (f a) (T f a) 1776During kind-checking, we give T the kind T :: k1 -> k2 -> * 1777and figure out constraints on k1, k2 etc. Then we generalise 1778to get T :: forall k. (k->*) -> k -> * 1779So now the (T f a) in the RHS must be elaborated to (T k f a). 1780 1781However, during tcTyClDecl of T (above) we will be in a recursive 1782"knot". So we aren't allowed to look at the TyCon T itself; we are only 1783allowed to put it (lazily) in the returned structures. But when 1784kind-checking the RHS of T's decl, we *do* need to know T's kind (so 1785that we can correctly elaboarate (T k f a). How can we get T's kind 1786without looking at T? Delicate answer: during tcTyClDecl, we extend 1787 1788 *Global* env with T -> ATyCon (the (not yet built) final TyCon for T) 1789 *Local* env with T -> ATcTyCon (TcTyCon with the polymorphic kind of T) 1790 1791Then: 1792 1793 * During TcHsType.tcTyVar we look in the *local* env, to get the 1794 fully-known, not knot-tied TcTyCon for T. 1795 1796 * Then, in TcHsSyn.zonkTcTypeToType (and zonkTcTyCon in particular) 1797 we look in the *global* env to get the TyCon. 1798 1799This fancy footwork (with two bindings for T) is only necessary for the 1800TyCons or Classes of this recursive group. Earlier, finished groups, 1801live in the global env only. 1802 1803See also Note [Kind checking recursive type and class declarations] 1804 1805Note [Kind checking recursive type and class declarations] 1806~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1807Before we can type-check the decls, we must kind check them. This 1808is done by establishing an "initial kind", which is a rather uninformed 1809guess at a tycon's kind (by counting arguments, mainly) and then 1810using this initial kind for recursive occurrences. 1811 1812The initial kind is stored in exactly the same way during 1813kind-checking as it is during type-checking (Note [Type checking 1814recursive type and class declarations]): in the *local* environment, 1815with ATcTyCon. But we still must store *something* in the *global* 1816environment. Even though we discard the result of kind-checking, we 1817sometimes need to produce error messages. These error messages will 1818want to refer to the tycons being checked, except that they don't 1819exist yet, and it would be Terribly Annoying to get the error messages 1820to refer back to HsSyn. So we create a TcTyCon and put it in the 1821global env. This tycon can print out its name and knows its kind, but 1822any other action taken on it will panic. Note that TcTyCons are *not* 1823knot-tied, unlike the rather valid but knot-tied ones that occur 1824during type-checking. 1825 1826Note [Declarations for wired-in things] 1827~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1828For wired-in things we simply ignore the declaration 1829and take the wired-in information. That avoids complications. 1830e.g. the need to make the data constructor worker name for 1831 a constraint tuple match the wired-in one 1832 1833Note [Implementation of UnliftedNewtypes] 1834~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1835Expected behavior of UnliftedNewtypes: 1836 1837* Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0013-unlifted-newtypes.rst 1838* Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/98 1839 1840What follows is a high-level overview of the implementation of the 1841proposal. 1842 1843STEP 1: Getting the initial kind, as done by inferInitialKind. We have 1844two sub-cases (assuming we have a newtype and -XUnliftedNewtypes is enabled): 1845 1846* With a CUSK: no change in kind-checking; the tycon is given the kind 1847 the user writes, whatever it may be. 1848 1849* Without a CUSK: If there is no kind signature, the tycon is given 1850 a kind `TYPE r`, for a fresh unification variable `r`. 1851 1852STEP 2: Kind-checking, as done by kcTyClDecl. This step is skipped for CUSKs. 1853The key function here is kcConDecl, which looks at an individual constructor 1854declaration. In the unlifted-newtypes case (i.e., -XUnliftedNewtypes and, 1855indeed, we are processing a newtype), we call unifyNewtypeKind, which is a 1856thin wrapper around unifyKind, unifying the kind of the one argument and the 1857result kind of the newtype tycon. 1858 1859Examples of newtypes affected by STEP 2, assuming -XUnliftedNewtypes is 1860enabled (we use r0 to denote a unification variable): 1861 1862newtype Foo rep = MkFoo (forall (a :: TYPE rep). a) 1863+ kcConDecl unifies (TYPE r0) with (TYPE rep), where (TYPE r0) 1864 is the kind that inferInitialKind invented for (Foo rep). 1865 1866data Color = Red | Blue 1867type family Interpret (x :: Color) :: RuntimeRep where 1868 Interpret 'Red = 'IntRep 1869 Interpret 'Blue = 'WordRep 1870data family Foo (x :: Color) :: TYPE (Interpret x) 1871newtype instance Foo 'Red = FooRedC Int# 1872+ kcConDecl unifies TYPE (Interpret 'Red) with TYPE 'IntRep 1873 1874Note that, in the GADT case, we might have a kind signature with arrows 1875(newtype XYZ a b :: Type -> Type where ...). We want only the final 1876component of the kind for checking in kcConDecl, so we call etaExpandAlgTyCon 1877in kcTyClDecl. 1878 1879STEP 3: Type-checking (desugaring), as done by tcTyClDecl. The key function 1880here is tcConDecl. Once again, we must call unifyNewtypeKind, for two reasons: 1881 1882 A. It is possible that a GADT has a CUSK. (Note that this is *not* 1883 possible for H98 types. Recall that CUSK types don't go through 1884 kcTyClDecl, so we might not have done this kind check. 1885 B. We need to produce the coercion to put on the argument type 1886 if the kinds are different (for both H98 and GADT). 1887 1888Example of (B): 1889 1890type family F a where 1891 F Int = LiftedRep 1892 1893newtype N :: TYPE (F Int) where 1894 MkN :: Int -> N 1895 1896We really need to have the argument to MkN be (Int |> TYPE (sym axF)), where 1897axF :: F Int ~ LiftedRep. That way, the argument kind is the same as the 1898newtype kind, which is the principal correctness condition for newtypes. 1899This call to unifyNewtypeKind is what produces that coercion. 1900 1901Note that this is possible in the H98 case only for a data family, because 1902the H98 syntax doesn't permit a kind signature on the newtype itself. 1903 1904 19051. In tcFamDecl1, we suppress a tcIsLiftedTypeKind check if 1906 UnliftedNewtypes is on. This allows us to write things like: 1907 data family Foo :: TYPE 'IntRep 1908 19092. In a newtype instance (with -XUnliftedNewtypes), if the user does 1910 not write a kind signature, we want to allow the possibility that 1911 the kind is not Type, so we use newOpenTypeKind instead of liftedTypeKind. 1912 This is done in tcDataFamInstHeader in TcInstDcls. Example: 1913 1914 data family Bar (a :: RuntimeRep) :: TYPE a 1915 newtype instance Bar 'IntRep = BarIntC Int# 1916 newtype instance Bar 'WordRep :: TYPE 'WordRep where 1917 BarWordC :: Word# -> Bar 'WordRep 1918 1919 The data instance corresponding to IntRep does not specify a kind signature, 1920 so tc_kind_sig just returns `TYPE r0` (where `r0` is a fresh metavariable). 1921 The data instance corresponding to WordRep does have a kind signature, so 1922 we use that kind signature. 1923 19243. A data family and its newtype instance may be declared with slightly 1925 different kinds. See Note [Unifying data family kinds] in TcInstDcls. 1926 1927There's also a change in the renamer: 1928 1929* In GHC.RenameSource.rnTyClDecl, enabling UnliftedNewtypes changes what is means 1930 for a newtype to have a CUSK. This is necessary since UnliftedNewtypes 1931 means that, for newtypes without kind signatures, we must use the field 1932 inside the data constructor to determine the result kind. 1933 See Note [Unlifted Newtypes and CUSKs] for more detail. 1934 1935For completeness, it was also necessary to make coerce work on 1936unlifted types, resolving #13595. 1937 1938-} 1939 1940tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM (TyCon, [DerivInfo]) 1941tcTyClDecl roles_info (L loc decl) 1942 | Just thing <- wiredInNameTyThing_maybe (tcdName decl) 1943 = case thing of -- See Note [Declarations for wired-in things] 1944 ATyCon tc -> return (tc, wiredInDerivInfo tc decl) 1945 _ -> pprPanic "tcTyClDecl" (ppr thing) 1946 1947 | otherwise 1948 = setSrcSpan loc $ tcAddDeclCtxt decl $ 1949 do { traceTc "---- tcTyClDecl ---- {" (ppr decl) 1950 ; (tc, deriv_infos) <- tcTyClDecl1 Nothing roles_info decl 1951 ; traceTc "---- tcTyClDecl end ---- }" (ppr tc) 1952 ; return (tc, deriv_infos) } 1953 1954noDerivInfos :: a -> (a, [DerivInfo]) 1955noDerivInfos a = (a, []) 1956 1957wiredInDerivInfo :: TyCon -> TyClDecl GhcRn -> [DerivInfo] 1958wiredInDerivInfo tycon decl 1959 | DataDecl { tcdDataDefn = dataDefn } <- decl 1960 , HsDataDefn { dd_derivs = derivs } <- dataDefn 1961 = [ DerivInfo { di_rep_tc = tycon 1962 , di_scoped_tvs = 1963 if isFunTyCon tycon || isPrimTyCon tycon 1964 then [] -- no tyConTyVars 1965 else mkTyVarNamePairs (tyConTyVars tycon) 1966 , di_clauses = unLoc derivs 1967 , di_ctxt = tcMkDeclCtxt decl } ] 1968wiredInDerivInfo _ _ = [] 1969 1970 -- "type family" declarations 1971tcTyClDecl1 :: Maybe Class -> RolesInfo -> TyClDecl GhcRn -> TcM (TyCon, [DerivInfo]) 1972tcTyClDecl1 parent _roles_info (FamDecl { tcdFam = fd }) 1973 = fmap noDerivInfos $ 1974 tcFamDecl1 parent fd 1975 1976 -- "type" synonym declaration 1977tcTyClDecl1 _parent roles_info 1978 (SynDecl { tcdLName = L _ tc_name 1979 , tcdRhs = rhs }) 1980 = ASSERT( isNothing _parent ) 1981 fmap noDerivInfos $ 1982 tcTySynRhs roles_info tc_name rhs 1983 1984 -- "data/newtype" declaration 1985tcTyClDecl1 _parent roles_info 1986 decl@(DataDecl { tcdLName = L _ tc_name 1987 , tcdDataDefn = defn }) 1988 = ASSERT( isNothing _parent ) 1989 tcDataDefn (tcMkDeclCtxt decl) roles_info tc_name defn 1990 1991tcTyClDecl1 _parent roles_info 1992 (ClassDecl { tcdLName = L _ class_name 1993 , tcdCtxt = hs_ctxt 1994 , tcdMeths = meths 1995 , tcdFDs = fundeps 1996 , tcdSigs = sigs 1997 , tcdATs = ats 1998 , tcdATDefs = at_defs }) 1999 = ASSERT( isNothing _parent ) 2000 do { clas <- tcClassDecl1 roles_info class_name hs_ctxt 2001 meths fundeps sigs ats at_defs 2002 ; return (noDerivInfos (classTyCon clas)) } 2003 2004tcTyClDecl1 _ _ (XTyClDecl nec) = noExtCon nec 2005 2006 2007{- ********************************************************************* 2008* * 2009 Class declarations 2010* * 2011********************************************************************* -} 2012 2013tcClassDecl1 :: RolesInfo -> Name -> LHsContext GhcRn 2014 -> LHsBinds GhcRn -> [LHsFunDep GhcRn] -> [LSig GhcRn] 2015 -> [LFamilyDecl GhcRn] -> [LTyFamDefltDecl GhcRn] 2016 -> TcM Class 2017tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs 2018 = fixM $ \ clas -> 2019 -- We need the knot because 'clas' is passed into tcClassATs 2020 bindTyClTyVars class_name $ \ binders res_kind -> 2021 do { checkClassKindSig res_kind 2022 ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders) 2023 ; let tycon_name = class_name -- We use the same name 2024 roles = roles_info tycon_name -- for TyCon and Class 2025 2026 ; (ctxt, fds, sig_stuff, at_stuff) 2027 <- pushTcLevelM_ $ 2028 solveEqualities $ 2029 checkTvConstraints skol_info (binderVars binders) $ 2030 -- The checkTvConstraints is needed bring into scope the 2031 -- skolems bound by the class decl header (#17841) 2032 do { ctxt <- tcHsContext hs_ctxt 2033 ; fds <- mapM (addLocM tc_fundep) fundeps 2034 ; sig_stuff <- tcClassSigs class_name sigs meths 2035 ; at_stuff <- tcClassATs class_name clas ats at_defs 2036 ; return (ctxt, fds, sig_stuff, at_stuff) } 2037 2038 -- The solveEqualities will report errors for any 2039 -- unsolved equalities, so these zonks should not encounter 2040 -- any unfilled coercion variables unless there is such an error 2041 -- The zonk also squeeze out the TcTyCons, and converts 2042 -- Skolems to tyvars. 2043 ; ze <- emptyZonkEnv 2044 ; ctxt <- zonkTcTypesToTypesX ze ctxt 2045 ; sig_stuff <- mapM (zonkTcMethInfoToMethInfoX ze) sig_stuff 2046 -- ToDo: do we need to zonk at_stuff? 2047 2048 -- TODO: Allow us to distinguish between abstract class, 2049 -- and concrete class with no methods (maybe by 2050 -- specifying a trailing where or not 2051 2052 ; mindef <- tcClassMinimalDef class_name sigs sig_stuff 2053 ; is_boot <- tcIsHsBootOrSig 2054 ; let body | is_boot, null ctxt, null at_stuff, null sig_stuff 2055 = Nothing 2056 | otherwise 2057 = Just (ctxt, at_stuff, sig_stuff, mindef) 2058 2059 ; clas <- buildClass class_name binders roles fds body 2060 ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$ 2061 ppr fds) 2062 ; return clas } 2063 where 2064 skol_info = TyConSkol ClassFlavour class_name 2065 tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ; 2066 ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ; 2067 ; return (tvs1', tvs2') } 2068 2069 2070{- Note [Associated type defaults] 2071~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2072 2073The following is an example of associated type defaults: 2074 class C a where 2075 data D a 2076 2077 type F a b :: * 2078 type F a b = [a] -- Default 2079 2080Note that we can get default definitions only for type families, not data 2081families. 2082-} 2083 2084tcClassATs :: Name -- The class name (not knot-tied) 2085 -> Class -- The class parent of this associated type 2086 -> [LFamilyDecl GhcRn] -- Associated types. 2087 -> [LTyFamDefltDecl GhcRn] -- Associated type defaults. 2088 -> TcM [ClassATItem] 2089tcClassATs class_name cls ats at_defs 2090 = do { -- Complain about associated type defaults for non associated-types 2091 sequence_ [ failWithTc (badATErr class_name n) 2092 | n <- map at_def_tycon at_defs 2093 , not (n `elemNameSet` at_names) ] 2094 ; mapM tc_at ats } 2095 where 2096 at_def_tycon :: LTyFamDefltDecl GhcRn -> Name 2097 at_def_tycon = tyFamInstDeclName . unLoc 2098 2099 at_fam_name :: LFamilyDecl GhcRn -> Name 2100 at_fam_name = familyDeclName . unLoc 2101 2102 at_names = mkNameSet (map at_fam_name ats) 2103 2104 at_defs_map :: NameEnv [LTyFamDefltDecl GhcRn] 2105 -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs' 2106 at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv 2107 (at_def_tycon at_def) [at_def]) 2108 emptyNameEnv at_defs 2109 2110 tc_at at = do { fam_tc <- addLocM (tcFamDecl1 (Just cls)) at 2111 ; let at_defs = lookupNameEnv at_defs_map (at_fam_name at) 2112 `orElse` [] 2113 ; atd <- tcDefaultAssocDecl fam_tc at_defs 2114 ; return (ATI fam_tc atd) } 2115 2116------------------------- 2117tcDefaultAssocDecl :: 2118 TyCon -- ^ Family TyCon (not knot-tied) 2119 -> [LTyFamDefltDecl GhcRn] -- ^ Defaults 2120 -> TcM (Maybe (KnotTied Type, SrcSpan)) -- ^ Type checked RHS 2121tcDefaultAssocDecl _ [] 2122 = return Nothing -- No default declaration 2123 2124tcDefaultAssocDecl _ (d1:_:_) 2125 = failWithTc (text "More than one default declaration for" 2126 <+> ppr (tyFamInstDeclName (unLoc d1))) 2127 2128tcDefaultAssocDecl fam_tc 2129 [L loc (TyFamInstDecl { tfid_eqn = 2130 HsIB { hsib_ext = imp_vars 2131 , hsib_body = FamEqn { feqn_tycon = L _ tc_name 2132 , feqn_bndrs = mb_expl_bndrs 2133 , feqn_pats = hs_pats 2134 , feqn_rhs = hs_rhs_ty }}})] 2135 = -- See Note [Type-checking default assoc decls] 2136 setSrcSpan loc $ 2137 tcAddFamInstCtxt (text "default type instance") tc_name $ 2138 do { traceTc "tcDefaultAssocDecl 1" (ppr tc_name) 2139 ; let fam_tc_name = tyConName fam_tc 2140 vis_arity = length (tyConVisibleTyVars fam_tc) 2141 vis_pats = numVisibleArgs hs_pats 2142 2143 -- Kind of family check 2144 ; ASSERT( fam_tc_name == tc_name ) 2145 checkTc (isTypeFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc) 2146 2147 -- Arity check 2148 ; checkTc (vis_pats == vis_arity) 2149 (wrongNumberOfParmsErr vis_arity) 2150 2151 -- Typecheck RHS 2152 -- 2153 -- You might think we should pass in some AssocInstInfo, as we're looking 2154 -- at an associated type. But this would be wrong, because an associated 2155 -- type default LHS can mention *different* type variables than the 2156 -- enclosing class. So it's treated more as a freestanding beast. 2157 ; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc NotAssociated 2158 imp_vars (mb_expl_bndrs `orElse` []) 2159 hs_pats hs_rhs_ty 2160 2161 ; let fam_tvs = tyConTyVars fam_tc 2162 ppr_eqn = ppr_default_eqn pats rhs_ty 2163 pats_vis = tyConArgFlags fam_tc pats 2164 ; traceTc "tcDefaultAssocDecl 2" (vcat 2165 [ text "fam_tvs" <+> ppr fam_tvs 2166 , text "qtvs" <+> ppr qtvs 2167 , text "pats" <+> ppr pats 2168 , text "rhs_ty" <+> ppr rhs_ty 2169 ]) 2170 ; pat_tvs <- zipWithM (extract_tv ppr_eqn) pats pats_vis 2171 ; check_all_distinct_tvs ppr_eqn $ zip pat_tvs pats_vis 2172 ; let subst = zipTvSubst pat_tvs (mkTyVarTys fam_tvs) 2173 ; pure $ Just (substTyUnchecked subst rhs_ty, loc) 2174 -- We also perform other checks for well-formedness and validity 2175 -- later, in checkValidClass 2176 } 2177 where 2178 -- Checks that a pattern on the LHS of a default is a type 2179 -- variable. If so, return the underlying type variable, and if 2180 -- not, throw an error. 2181 -- See Note [Type-checking default assoc decls] 2182 extract_tv :: SDoc -- The pretty-printed default equation 2183 -- (only used for error message purposes) 2184 -> Type -- The particular type pattern from which to extract 2185 -- its underlying type variable 2186 -> ArgFlag -- The visibility of the type pattern 2187 -- (only used for error message purposes) 2188 -> TcM TyVar 2189 extract_tv ppr_eqn pat pat_vis = 2190 case getTyVar_maybe pat of 2191 Just tv -> pure tv 2192 Nothing -> failWithTc $ 2193 pprWithExplicitKindsWhen (isInvisibleArgFlag pat_vis) $ 2194 hang (text "Illegal argument" <+> quotes (ppr pat) <+> text "in:") 2195 2 (vcat [ppr_eqn, suggestion]) 2196 2197 2198 -- Checks that no type variables in an associated default declaration are 2199 -- duplicated. If that is the case, throw an error. 2200 -- See Note [Type-checking default assoc decls] 2201 check_all_distinct_tvs :: 2202 SDoc -- The pretty-printed default equation (only used 2203 -- for error message purposes) 2204 -> [(TyVar, ArgFlag)] -- The type variable arguments in the associated 2205 -- default declaration, along with their respective 2206 -- visibilities (the latter are only used for error 2207 -- message purposes) 2208 -> TcM () 2209 check_all_distinct_tvs ppr_eqn pat_tvs_vis = 2210 let dups = findDupsEq ((==) `on` fst) pat_tvs_vis in 2211 traverse_ 2212 (\d -> let (pat_tv, pat_vis) = NE.head d in failWithTc $ 2213 pprWithExplicitKindsWhen (isInvisibleArgFlag pat_vis) $ 2214 hang (text "Illegal duplicate variable" 2215 <+> quotes (ppr pat_tv) <+> text "in:") 2216 2 (vcat [ppr_eqn, suggestion])) 2217 dups 2218 2219 ppr_default_eqn :: [Type] -> Type -> SDoc 2220 ppr_default_eqn pats rhs_ty = 2221 quotes (text "type" <+> ppr (mkTyConApp fam_tc pats) 2222 <+> equals <+> ppr rhs_ty) 2223 2224 suggestion :: SDoc 2225 suggestion = text "The arguments to" <+> quotes (ppr fam_tc) 2226 <+> text "must all be distinct type variables" 2227 2228tcDefaultAssocDecl _ [L _ (TyFamInstDecl (HsIB _ (XFamEqn x)))] = noExtCon x 2229tcDefaultAssocDecl _ [L _ (TyFamInstDecl (XHsImplicitBndrs x))] = noExtCon x 2230 2231 2232{- Note [Type-checking default assoc decls] 2233~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2234Consider this default declaration for an associated type 2235 2236 class C a where 2237 type F (a :: k) b :: Type 2238 type F (x :: j) y = Proxy x -> y 2239 2240Note that the class variable 'a' doesn't scope over the default assoc 2241decl (rather oddly I think), and (less oddly) neither does the second 2242argument 'b' of the associated type 'F', or the kind variable 'k'. 2243Instead, the default decl is treated more like a top-level type 2244instance. 2245 2246However we store the default rhs (Proxy x -> y) in F's TyCon, using 2247F's own type variables, so we need to convert it to (Proxy a -> b). 2248We do this by creating a substitution [j |-> k, x |-> a, b |-> y] and 2249applying this substitution to the RHS. 2250 2251In order to create this substitution, we must first ensure that all of 2252the arguments in the default instance consist of distinct type variables. 2253One might think that this is a simple task that could be implemented earlier 2254in the compiler, perhaps in the parser or the renamer. However, there are some 2255tricky corner cases that really do require the full power of typechecking to 2256weed out, as the examples below should illustrate. 2257 2258First, we must check that all arguments are type variables. As a motivating 2259example, consider this erroneous program (inspired by #11361): 2260 2261 class C a where 2262 type F (a :: k) b :: Type 2263 type F x b = x 2264 2265If you squint, you'll notice that the kind of `x` is actually Type. However, 2266we cannot substitute from [Type |-> k], so we reject this default. 2267 2268Next, we must check that all arguments are distinct. Here is another offending 2269example, this time taken from #13971: 2270 2271 class C2 (a :: j) where 2272 type F2 (a :: j) (b :: k) 2273 type F2 (x :: z) y = SameKind x y 2274 data SameKind :: k -> k -> Type 2275 2276All of the arguments in the default equation for `F2` are type variables, so 2277that passes the first check. However, if we were to build this substitution, 2278then both `j` and `k` map to `z`! In terms of visible kind application, it's as 2279if we had written `type F2 @z @z x y = SameKind @z x y`, which makes it clear 2280that we have duplicated a use of `z` on the LHS. Therefore, `F2`'s default is 2281also rejected. 2282 2283Since the LHS of an associated type family default is always just variables, 2284it won't contain any tycons. Accordingly, the patterns used in the substitution 2285won't actually be knot-tied, even though we're in the knot. This is too 2286delicate for my taste, but it works. 2287-} 2288 2289{- ********************************************************************* 2290* * 2291 Type family declarations 2292* * 2293********************************************************************* -} 2294 2295tcFamDecl1 :: Maybe Class -> FamilyDecl GhcRn -> TcM TyCon 2296tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info 2297 , fdLName = tc_lname@(L _ tc_name) 2298 , fdResultSig = L _ sig 2299 , fdInjectivityAnn = inj }) 2300 | DataFamily <- fam_info 2301 = bindTyClTyVars tc_name $ \ binders res_kind -> do 2302 { traceTc "data family:" (ppr tc_name) 2303 ; checkFamFlag tc_name 2304 2305 -- Check that the result kind is OK 2306 -- We allow things like 2307 -- data family T (a :: Type) :: forall k. k -> Type 2308 -- We treat T as having arity 1, but result kind forall k. k -> Type 2309 -- But we want to check that the result kind finishes in 2310 -- Type or a kind-variable 2311 -- For the latter, consider 2312 -- data family D a :: forall k. Type -> k 2313 -- When UnliftedNewtypes is enabled, we loosen this restriction 2314 -- on the return kind. See Note [Implementation of UnliftedNewtypes], wrinkle (1). 2315 ; let (_, final_res_kind) = splitPiTys res_kind 2316 ; checkDataKindSig DataFamilySort final_res_kind 2317 ; tc_rep_name <- newTyConRepName tc_name 2318 ; let inj = Injective $ replicate (length binders) True 2319 tycon = mkFamilyTyCon tc_name binders 2320 res_kind 2321 (resultVariableName sig) 2322 (DataFamilyTyCon tc_rep_name) 2323 parent inj 2324 ; return tycon } 2325 2326 | OpenTypeFamily <- fam_info 2327 = bindTyClTyVars tc_name $ \ binders res_kind -> do 2328 { traceTc "open type family:" (ppr tc_name) 2329 ; checkFamFlag tc_name 2330 ; inj' <- tcInjectivity binders inj 2331 ; checkResultSigFlag tc_name sig -- check after injectivity for better errors 2332 ; let tycon = mkFamilyTyCon tc_name binders res_kind 2333 (resultVariableName sig) OpenSynFamilyTyCon 2334 parent inj' 2335 ; return tycon } 2336 2337 | ClosedTypeFamily mb_eqns <- fam_info 2338 = -- Closed type families are a little tricky, because they contain the definition 2339 -- of both the type family and the equations for a CoAxiom. 2340 do { traceTc "Closed type family:" (ppr tc_name) 2341 -- the variables in the header scope only over the injectivity 2342 -- declaration but this is not involved here 2343 ; (inj', binders, res_kind) 2344 <- bindTyClTyVars tc_name $ \ binders res_kind -> 2345 do { inj' <- tcInjectivity binders inj 2346 ; return (inj', binders, res_kind) } 2347 2348 ; checkFamFlag tc_name -- make sure we have -XTypeFamilies 2349 ; checkResultSigFlag tc_name sig 2350 2351 -- If Nothing, this is an abstract family in a hs-boot file; 2352 -- but eqns might be empty in the Just case as well 2353 ; case mb_eqns of 2354 Nothing -> 2355 return $ mkFamilyTyCon tc_name binders res_kind 2356 (resultVariableName sig) 2357 AbstractClosedSynFamilyTyCon parent 2358 inj' 2359 Just eqns -> do { 2360 2361 -- Process the equations, creating CoAxBranches 2362 ; let tc_fam_tc = mkTcTyCon tc_name binders res_kind 2363 noTcTyConScopedTyVars 2364 False {- this doesn't matter here -} 2365 ClosedTypeFamilyFlavour 2366 2367 ; branches <- mapAndReportM (tcTyFamInstEqn tc_fam_tc NotAssociated) eqns 2368 -- Do not attempt to drop equations dominated by earlier 2369 -- ones here; in the case of mutual recursion with a data 2370 -- type, we get a knot-tying failure. Instead we check 2371 -- for this afterwards, in TcValidity.checkValidCoAxiom 2372 -- Example: tc265 2373 2374 -- Create a CoAxiom, with the correct src location. 2375 ; co_ax_name <- newFamInstAxiomName tc_lname [] 2376 2377 ; let mb_co_ax 2378 | null eqns = Nothing -- mkBranchedCoAxiom fails on empty list 2379 | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches) 2380 2381 fam_tc = mkFamilyTyCon tc_name binders res_kind (resultVariableName sig) 2382 (ClosedSynFamilyTyCon mb_co_ax) parent inj' 2383 2384 -- We check for instance validity later, when doing validity 2385 -- checking for the tycon. Exception: checking equations 2386 -- overlap done by dropDominatedAxioms 2387 ; return fam_tc } } 2388 2389#if __GLASGOW_HASKELL__ <= 810 2390 | otherwise = panic "tcFamInst1" -- Silence pattern-exhaustiveness checker 2391#endif 2392tcFamDecl1 _ (XFamilyDecl nec) = noExtCon nec 2393 2394-- | Maybe return a list of Bools that say whether a type family was declared 2395-- injective in the corresponding type arguments. Length of the list is equal to 2396-- the number of arguments (including implicit kind/coercion arguments). 2397-- True on position 2398-- N means that a function is injective in its Nth argument. False means it is 2399-- not. 2400tcInjectivity :: [TyConBinder] -> Maybe (LInjectivityAnn GhcRn) 2401 -> TcM Injectivity 2402tcInjectivity _ Nothing 2403 = return NotInjective 2404 2405 -- User provided an injectivity annotation, so for each tyvar argument we 2406 -- check whether a type family was declared injective in that argument. We 2407 -- return a list of Bools, where True means that corresponding type variable 2408 -- was mentioned in lInjNames (type family is injective in that argument) and 2409 -- False means that it was not mentioned in lInjNames (type family is not 2410 -- injective in that type variable). We also extend injectivity information to 2411 -- kind variables, so if a user declares: 2412 -- 2413 -- type family F (a :: k1) (b :: k2) = (r :: k3) | r -> a 2414 -- 2415 -- then we mark both `a` and `k1` as injective. 2416 -- NB: the return kind is considered to be *input* argument to a type family. 2417 -- Since injectivity allows to infer input arguments from the result in theory 2418 -- we should always mark the result kind variable (`k3` in this example) as 2419 -- injective. The reason is that result type has always an assigned kind and 2420 -- therefore we can always infer the result kind if we know the result type. 2421 -- But this does not seem to be useful in any way so we don't do it. (Another 2422 -- reason is that the implementation would not be straightforward.) 2423tcInjectivity tcbs (Just (L loc (InjectivityAnn _ lInjNames))) 2424 = setSrcSpan loc $ 2425 do { let tvs = binderVars tcbs 2426 ; dflags <- getDynFlags 2427 ; checkTc (xopt LangExt.TypeFamilyDependencies dflags) 2428 (text "Illegal injectivity annotation" $$ 2429 text "Use TypeFamilyDependencies to allow this") 2430 ; inj_tvs <- mapM (tcLookupTyVar . unLoc) lInjNames 2431 ; inj_tvs <- mapM zonkTcTyVarToTyVar inj_tvs -- zonk the kinds 2432 ; let inj_ktvs = filterVarSet isTyVar $ -- no injective coercion vars 2433 closeOverKinds (mkVarSet inj_tvs) 2434 ; let inj_bools = map (`elemVarSet` inj_ktvs) tvs 2435 ; traceTc "tcInjectivity" (vcat [ ppr tvs, ppr lInjNames, ppr inj_tvs 2436 , ppr inj_ktvs, ppr inj_bools ]) 2437 ; return $ Injective inj_bools } 2438 2439tcTySynRhs :: RolesInfo -> Name 2440 -> LHsType GhcRn -> TcM TyCon 2441tcTySynRhs roles_info tc_name hs_ty 2442 = bindTyClTyVars tc_name $ \ binders res_kind -> 2443 do { env <- getLclEnv 2444 ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env)) 2445 ; rhs_ty <- pushTcLevelM_ $ 2446 solveEqualities $ 2447 tcCheckLHsType hs_ty res_kind 2448 ; rhs_ty <- zonkTcTypeToType rhs_ty 2449 ; let roles = roles_info tc_name 2450 tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty 2451 ; return tycon } 2452 2453tcDataDefn :: SDoc -> RolesInfo -> Name 2454 -> HsDataDefn GhcRn -> TcM (TyCon, [DerivInfo]) 2455 -- NB: not used for newtype/data instances (whether associated or not) 2456tcDataDefn err_ctxt roles_info tc_name 2457 (HsDataDefn { dd_ND = new_or_data, dd_cType = cType 2458 , dd_ctxt = ctxt 2459 , dd_kindSig = mb_ksig -- Already in tc's kind 2460 -- via inferInitialKinds 2461 , dd_cons = cons 2462 , dd_derivs = derivs }) 2463 = bindTyClTyVars tc_name $ \ tycon_binders res_kind -> 2464 -- The TyCon tyvars must scope over 2465 -- - the stupid theta (dd_ctxt) 2466 -- - for H98 constructors only, the ConDecl 2467 -- But it does no harm to bring them into scope 2468 -- over GADT ConDecls as well; and it's awkward not to 2469 do { gadt_syntax <- dataDeclChecks tc_name new_or_data ctxt cons 2470 ; (extra_bndrs, final_res_kind) <- etaExpandAlgTyCon tycon_binders res_kind 2471 2472 ; tcg_env <- getGblEnv 2473 ; let hsc_src = tcg_src tcg_env 2474 ; unless (mk_permissive_kind hsc_src cons) $ 2475 checkDataKindSig (DataDeclSort new_or_data) final_res_kind 2476 2477 ; stupid_tc_theta <- pushTcLevelM_ $ solveEqualities $ tcHsContext ctxt 2478 ; stupid_theta <- zonkTcTypesToTypes stupid_tc_theta 2479 ; kind_signatures <- xoptM LangExt.KindSignatures 2480 2481 -- Check that we don't use kind signatures without Glasgow extensions 2482 ; when (isJust mb_ksig) $ 2483 checkTc (kind_signatures) (badSigTyDecl tc_name) 2484 2485 ; tycon <- fixM $ \ tycon -> do 2486 { let final_bndrs = tycon_binders `chkAppend` extra_bndrs 2487 res_ty = mkTyConApp tycon (mkTyVarTys (binderVars final_bndrs)) 2488 roles = roles_info tc_name 2489 ; data_cons <- tcConDecls 2490 tycon 2491 new_or_data 2492 final_bndrs 2493 final_res_kind 2494 res_ty 2495 cons 2496 ; tc_rhs <- mk_tc_rhs hsc_src tycon data_cons 2497 ; tc_rep_nm <- newTyConRepName tc_name 2498 ; return (mkAlgTyCon tc_name 2499 final_bndrs 2500 final_res_kind 2501 roles 2502 (fmap unLoc cType) 2503 stupid_theta tc_rhs 2504 (VanillaAlgTyCon tc_rep_nm) 2505 gadt_syntax) } 2506 ; tctc <- tcLookupTcTyCon tc_name 2507 -- 'tctc' is a 'TcTyCon' and has the 'tcTyConScopedTyVars' that we need 2508 -- unlike the finalized 'tycon' defined above which is an 'AlgTyCon' 2509 ; let deriv_info = DerivInfo { di_rep_tc = tycon 2510 , di_scoped_tvs = tcTyConScopedTyVars tctc 2511 , di_clauses = unLoc derivs 2512 , di_ctxt = err_ctxt } 2513 ; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs) 2514 ; return (tycon, [deriv_info]) } 2515 where 2516 -- Abstract data types in hsig files can have arbitrary kinds, 2517 -- because they may be implemented by type synonyms 2518 -- (which themselves can have arbitrary kinds, not just *). See #13955. 2519 -- 2520 -- Note that this is only a property that data type declarations possess, 2521 -- so one could not have, say, a data family instance in an hsig file that 2522 -- has kind `Bool`. Therefore, this check need only occur in the code that 2523 -- typechecks data type declarations. 2524 mk_permissive_kind HsigFile [] = True 2525 mk_permissive_kind _ _ = False 2526 2527 -- In hs-boot, a 'data' declaration with no constructors 2528 -- indicates a nominally distinct abstract data type. 2529 mk_tc_rhs HsBootFile _ [] 2530 = return AbstractTyCon 2531 2532 mk_tc_rhs HsigFile _ [] -- ditto 2533 = return AbstractTyCon 2534 2535 mk_tc_rhs _ tycon data_cons 2536 = case new_or_data of 2537 DataType -> return (mkDataTyConRhs data_cons) 2538 NewType -> ASSERT( not (null data_cons) ) 2539 mkNewTyConRhs tc_name tycon (head data_cons) 2540tcDataDefn _ _ _ (XHsDataDefn nec) = noExtCon nec 2541 2542 2543------------------------- 2544kcTyFamInstEqn :: TcTyCon -> LTyFamInstEqn GhcRn -> TcM () 2545-- Used for the equations of a closed type family only 2546-- Not used for data/type instances 2547kcTyFamInstEqn tc_fam_tc 2548 (L loc (HsIB { hsib_ext = imp_vars 2549 , hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name 2550 , feqn_bndrs = mb_expl_bndrs 2551 , feqn_pats = hs_pats 2552 , feqn_rhs = hs_rhs_ty }})) 2553 = setSrcSpan loc $ 2554 do { traceTc "kcTyFamInstEqn" (vcat 2555 [ text "tc_name =" <+> ppr eqn_tc_name 2556 , text "fam_tc =" <+> ppr tc_fam_tc <+> dcolon <+> ppr (tyConKind tc_fam_tc) 2557 , text "hsib_vars =" <+> ppr imp_vars 2558 , text "feqn_bndrs =" <+> ppr mb_expl_bndrs 2559 , text "feqn_pats =" <+> ppr hs_pats ]) 2560 -- this check reports an arity error instead of a kind error; easier for user 2561 ; let vis_pats = numVisibleArgs hs_pats 2562 ; checkTc (vis_pats == vis_arity) $ 2563 wrongNumberOfParmsErr vis_arity 2564 ; discardResult $ 2565 bindImplicitTKBndrs_Q_Tv imp_vars $ 2566 bindExplicitTKBndrs_Q_Tv AnyKind (mb_expl_bndrs `orElse` []) $ 2567 do { (_fam_app, res_kind) <- tcFamTyPats tc_fam_tc hs_pats 2568 ; tcCheckLHsType hs_rhs_ty res_kind } 2569 -- Why "_Tv" here? Consider (#14066 2570 -- type family Bar x y where 2571 -- Bar (x :: a) (y :: b) = Int 2572 -- Bar (x :: c) (y :: d) = Bool 2573 -- During kind-checking, a,b,c,d should be TyVarTvs and unify appropriately 2574 } 2575 where 2576 vis_arity = length (tyConVisibleTyVars tc_fam_tc) 2577 2578kcTyFamInstEqn _ (L _ (XHsImplicitBndrs nec)) = noExtCon nec 2579kcTyFamInstEqn _ (L _ (HsIB _ (XFamEqn nec))) = noExtCon nec 2580 2581 2582-------------------------- 2583tcTyFamInstEqn :: TcTyCon -> AssocInstInfo -> LTyFamInstEqn GhcRn 2584 -> TcM (KnotTied CoAxBranch) 2585-- Needs to be here, not in TcInstDcls, because closed families 2586-- (typechecked here) have TyFamInstEqns 2587 2588tcTyFamInstEqn fam_tc mb_clsinfo 2589 (L loc (HsIB { hsib_ext = imp_vars 2590 , hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name 2591 , feqn_bndrs = mb_expl_bndrs 2592 , feqn_pats = hs_pats 2593 , feqn_rhs = hs_rhs_ty }})) 2594 = ASSERT( getName fam_tc == eqn_tc_name ) 2595 setSrcSpan loc $ 2596 do { traceTc "tcTyFamInstEqn" $ 2597 vcat [ ppr fam_tc <+> ppr hs_pats 2598 , text "fam tc bndrs" <+> pprTyVars (tyConTyVars fam_tc) 2599 , case mb_clsinfo of 2600 NotAssociated -> empty 2601 InClsInst { ai_class = cls } -> text "class" <+> ppr cls <+> pprTyVars (classTyVars cls) ] 2602 2603 -- First, check the arity of visible arguments 2604 -- If we wait until validity checking, we'll get kind errors 2605 -- below when an arity error will be much easier to understand. 2606 ; let vis_arity = length (tyConVisibleTyVars fam_tc) 2607 vis_pats = numVisibleArgs hs_pats 2608 ; checkTc (vis_pats == vis_arity) $ 2609 wrongNumberOfParmsErr vis_arity 2610 ; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc mb_clsinfo 2611 imp_vars (mb_expl_bndrs `orElse` []) 2612 hs_pats hs_rhs_ty 2613 -- Don't print results they may be knot-tied 2614 -- (tcFamInstEqnGuts zonks to Type) 2615 ; return (mkCoAxBranch qtvs [] [] pats rhs_ty 2616 (map (const Nominal) qtvs) 2617 loc) } 2618 2619tcTyFamInstEqn _ _ _ = panic "tcTyFamInstEqn" 2620 2621{- 2622Kind check type patterns and kind annotate the embedded type variables. 2623 type instance F [a] = rhs 2624 2625 * Here we check that a type instance matches its kind signature, but we do 2626 not check whether there is a pattern for each type index; the latter 2627 check is only required for type synonym instances. 2628 2629Note [Instantiating a family tycon] 2630~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2631It's possible that kind-checking the result of a family tycon applied to 2632its patterns will instantiate the tycon further. For example, we might 2633have 2634 2635 type family F :: k where 2636 F = Int 2637 F = Maybe 2638 2639After checking (F :: forall k. k) (with no visible patterns), we still need 2640to instantiate the k. With data family instances, this problem can be even 2641more intricate, due to Note [Arity of data families] in FamInstEnv. See 2642indexed-types/should_compile/T12369 for an example. 2643 2644So, the kind-checker must return the new skolems and args (that is, Type 2645or (Type -> Type) for the equations above) and the instantiated kind. 2646 2647Note [Generalising in tcTyFamInstEqnGuts] 2648~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2649Suppose we have something like 2650 type instance forall (a::k) b. F t1 t2 = rhs 2651 2652Then imp_vars = [k], exp_bndrs = [a::k, b] 2653 2654We want to quantify over 2655 * k, a, and b (all user-specified) 2656 * and any inferred free kind vars from 2657 - the kinds of k, a, b 2658 - the types t1, t2 2659 2660However, unlike a type signature like 2661 f :: forall (a::k). blah 2662 2663we do /not/ care about the Inferred/Specified designation 2664or order for the final quantified tyvars. Type-family 2665instances are not invoked directly in Haskell source code, 2666so visible type application etc plays no role. 2667 2668So, the simple thing is 2669 - gather candidates from [k, a, b] and pats 2670 - quantify over them 2671 2672Hence the slightly mysterious call: 2673 candidateQTyVarsOfTypes (pats ++ mkTyVarTys scoped_tvs) 2674 2675Simple, neat, but a little non-obvious! 2676-} 2677 2678-------------------------- 2679tcTyFamInstEqnGuts :: TyCon -> AssocInstInfo 2680 -> [Name] -> [LHsTyVarBndr GhcRn] -- Implicit and explicicit binder 2681 -> HsTyPats GhcRn -- Patterns 2682 -> LHsType GhcRn -- RHS 2683 -> TcM ([TyVar], [TcType], TcType) -- (tyvars, pats, rhs) 2684-- Used only for type families, not data families 2685tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty 2686 = do { traceTc "tcTyFamInstEqnGuts {" (ppr fam_tc) 2687 2688 -- By now, for type families (but not data families) we should 2689 -- have checked that the number of patterns matches tyConArity 2690 2691 -- This code is closely related to the code 2692 -- in TcHsType.kcCheckDeclHeader_cusk 2693 ; (imp_tvs, (exp_tvs, (lhs_ty, rhs_ty))) 2694 <- pushTcLevelM_ $ 2695 solveEqualities $ 2696 bindImplicitTKBndrs_Q_Skol imp_vars $ 2697 bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $ 2698 do { (lhs_ty, rhs_kind) <- tcFamTyPats fam_tc hs_pats 2699 -- Ensure that the instance is consistent with its 2700 -- parent class (#16008) 2701 ; addConsistencyConstraints mb_clsinfo lhs_ty 2702 ; rhs_ty <- tcCheckLHsType hs_rhs_ty rhs_kind 2703 ; return (lhs_ty, rhs_ty) } 2704 2705 -- See Note [Generalising in tcTyFamInstEqnGuts] 2706 -- This code (and the stuff immediately above) is very similar 2707 -- to that in tcDataFamInstHeader. Maybe we should abstract the 2708 -- common code; but for the moment I concluded that it's 2709 -- clearer to duplicate it. Still, if you fix a bug here, 2710 -- check there too! 2711 ; let scoped_tvs = imp_tvs ++ exp_tvs 2712 ; dvs <- candidateQTyVarsOfTypes (lhs_ty : mkTyVarTys scoped_tvs) 2713 ; qtvs <- quantifyTyVars dvs 2714 2715 ; traceTc "tcTyFamInstEqnGuts 2" $ 2716 vcat [ ppr fam_tc 2717 , text "scoped_tvs" <+> pprTyVars scoped_tvs 2718 , text "lhs_ty" <+> ppr lhs_ty 2719 , text "dvs" <+> ppr dvs 2720 , text "qtvs" <+> pprTyVars qtvs ] 2721 2722 ; (ze, qtvs) <- zonkTyBndrs qtvs 2723 ; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty 2724 ; rhs_ty <- zonkTcTypeToTypeX ze rhs_ty 2725 2726 ; let pats = unravelFamInstPats lhs_ty 2727 -- Note that we do this after solveEqualities 2728 -- so that any strange coercions inside lhs_ty 2729 -- have been solved before we attempt to unravel it 2730 ; traceTc "tcTyFamInstEqnGuts }" (ppr fam_tc <+> pprTyVars qtvs) 2731 ; return (qtvs, pats, rhs_ty) } 2732 2733----------------- 2734tcFamTyPats :: TyCon 2735 -> HsTyPats GhcRn -- Patterns 2736 -> TcM (TcType, TcKind) -- (lhs_type, lhs_kind) 2737-- Used for both type and data families 2738tcFamTyPats fam_tc hs_pats 2739 = do { traceTc "tcFamTyPats {" $ 2740 vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity ] 2741 2742 ; let fun_ty = mkTyConApp fam_tc [] 2743 2744 ; (fam_app, res_kind) <- unsetWOptM Opt_WarnPartialTypeSignatures $ 2745 setXOptM LangExt.PartialTypeSignatures $ 2746 -- See Note [Wildcards in family instances] in 2747 -- GHC.Rename.Source 2748 tcInferApps typeLevelMode lhs_fun fun_ty hs_pats 2749 2750 -- Hack alert: see Note [tcFamTyPats: zonking the result kind] 2751 ; res_kind <- zonkTcType res_kind 2752 2753 ; traceTc "End tcFamTyPats }" $ 2754 vcat [ ppr fam_tc, text "res_kind:" <+> ppr res_kind ] 2755 2756 ; return (fam_app, res_kind) } 2757 where 2758 fam_name = tyConName fam_tc 2759 fam_arity = tyConArity fam_tc 2760 lhs_fun = noLoc (HsTyVar noExtField NotPromoted (noLoc fam_name)) 2761 2762{- Note [tcFamTyPats: zonking the result kind] 2763~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2764Consider (#19250) 2765 F :: forall k. k -> k 2766 type instance F (x :: Constraint) = () 2767 2768The tricky point is this: 2769 is that () an empty type tuple (() :: Type), or 2770 an empty constraint tuple (() :: Constraint)? 2771We work this out in a hacky way, by looking at the expected kind: 2772see Note [Inferring tuple kinds]. 2773 2774In this case, we kind-check the RHS using the kind gotten from the LHS: 2775see the call to tcCheckLHsType in tcTyFamInstEqnGuts in GHC.Tc.Tycl. 2776 2777But we want the kind from the LHS to be /zonked/, so that when 2778kind-checking the RHS (tcCheckLHsType) we can "see" what we learned 2779from kind-checking the LHS (tcFamTyPats). In our example above, the 2780type of the LHS is just `kappa` (by instantiating the forall k), but 2781then we learn (from x::Constraint) that kappa ~ Constraint. We want 2782that info when kind-checking the RHS. 2783 2784Easy solution: just zonk that return kind. Of course this won't help 2785if there is lots of type-family reduction to do, but it works fine in 2786common cases. 2787-} 2788 2789unravelFamInstPats :: TcType -> [TcType] 2790-- Decompose fam_app to get the argument patterns 2791-- 2792-- We expect fam_app to look like (F t1 .. tn) 2793-- tcInferApps is capable of returning ((F ty1 |> co) ty2), 2794-- but that can't happen here because we already checked the 2795-- arity of F matches the number of pattern 2796unravelFamInstPats fam_app 2797 = case splitTyConApp_maybe fam_app of 2798 Just (_, pats) -> pats 2799 Nothing -> panic "unravelFamInstPats: Ill-typed LHS of family instance" 2800 -- The Nothing case cannot happen for type families, because 2801 -- we don't call unravelFamInstPats until we've solved the 2802 -- equalities. For data families, it shouldn't happen either, 2803 -- we need to fail hard and early if it does. See trac issue #15905 2804 -- for an example of this happening. 2805 2806addConsistencyConstraints :: AssocInstInfo -> TcType -> TcM () 2807-- In the corresponding positions of the class and type-family, 2808-- ensure the the family argument is the same as the class argument 2809-- E.g class C a b c d where 2810-- F c x y a :: Type 2811-- Here the first arg of F should be the same as the third of C 2812-- and the fourth arg of F should be the same as the first of C 2813-- 2814-- We emit /Derived/ constraints (a bit like fundeps) to encourage 2815-- unification to happen, but without actually reporting errors. 2816-- If, despite the efforts, corresponding positions do not match, 2817-- checkConsistentFamInst will complain 2818addConsistencyConstraints mb_clsinfo fam_app 2819 | InClsInst { ai_inst_env = inst_env } <- mb_clsinfo 2820 , Just (fam_tc, pats) <- tcSplitTyConApp_maybe fam_app 2821 = do { let eqs = [ (cls_ty, pat) 2822 | (fam_tc_tv, pat) <- tyConTyVars fam_tc `zip` pats 2823 , Just cls_ty <- [lookupVarEnv inst_env fam_tc_tv] ] 2824 ; traceTc "addConsistencyConstraints" (ppr eqs) 2825 ; emitDerivedEqs AssocFamPatOrigin eqs } 2826 -- Improve inference 2827 -- Any mis-match is reports by checkConsistentFamInst 2828 | otherwise 2829 = return () 2830 2831{- Note [Constraints in patterns] 2832~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2833NB: This isn't the whole story. See comment in tcFamTyPats. 2834 2835At first glance, it seems there is a complicated story to tell in tcFamTyPats 2836around constraint solving. After all, type family patterns can now do 2837GADT pattern-matching, which is jolly complicated. But, there's a key fact 2838which makes this all simple: everything is at top level! There cannot 2839be untouchable type variables. There can't be weird interaction between 2840case branches. There can't be global skolems. 2841 2842This means that the semantics of type-level GADT matching is a little 2843different than term level. If we have 2844 2845 data G a where 2846 MkGBool :: G Bool 2847 2848And then 2849 2850 type family F (a :: G k) :: k 2851 type instance F MkGBool = True 2852 2853we get 2854 2855 axF : F Bool (MkGBool <Bool>) ~ True 2856 2857Simple! No casting on the RHS, because we can affect the kind parameter 2858to F. 2859 2860If we ever introduce local type families, this all gets a lot more 2861complicated, and will end up looking awfully like term-level GADT 2862pattern-matching. 2863 2864 2865** The new story ** 2866 2867Here is really what we want: 2868 2869The matcher really can't deal with covars in arbitrary spots in coercions. 2870But it can deal with covars that are arguments to GADT data constructors. 2871So we somehow want to allow covars only in precisely those spots, then use 2872them as givens when checking the RHS. TODO (RAE): Implement plan. 2873 2874Note [Quantified kind variables of a family pattern] 2875~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2876Consider type family KindFam (p :: k1) (q :: k1) 2877 data T :: Maybe k1 -> k2 -> * 2878 type instance KindFam (a :: Maybe k) b = T a b -> Int 2879The HsBSig for the family patterns will be ([k], [a]) 2880 2881Then in the family instance we want to 2882 * Bring into scope [ "k" -> k:*, "a" -> a:k ] 2883 * Kind-check the RHS 2884 * Quantify the type instance over k and k', as well as a,b, thus 2885 type instance [k, k', a:Maybe k, b:k'] 2886 KindFam (Maybe k) k' a b = T k k' a b -> Int 2887 2888Notice that in the third step we quantify over all the visibly-mentioned 2889type variables (a,b), but also over the implicitly mentioned kind variables 2890(k, k'). In this case one is bound explicitly but often there will be 2891none. The role of the kind signature (a :: Maybe k) is to add a constraint 2892that 'a' must have that kind, and to bring 'k' into scope. 2893 2894 2895 2896************************************************************************ 2897* * 2898 Data types 2899* * 2900************************************************************************ 2901-} 2902 2903dataDeclChecks :: Name -> NewOrData 2904 -> LHsContext GhcRn -> [LConDecl GhcRn] 2905 -> TcM Bool 2906dataDeclChecks tc_name new_or_data (L _ stupid_theta) cons 2907 = do { -- Check that we don't use GADT syntax in H98 world 2908 gadtSyntax_ok <- xoptM LangExt.GADTSyntax 2909 ; let gadt_syntax = consUseGadtSyntax cons 2910 ; checkTc (gadtSyntax_ok || not gadt_syntax) (badGadtDecl tc_name) 2911 2912 -- Check that the stupid theta is empty for a GADT-style declaration 2913 ; checkTc (null stupid_theta || not gadt_syntax) (badStupidTheta tc_name) 2914 2915 -- Check that a newtype has exactly one constructor 2916 -- Do this before checking for empty data decls, so that 2917 -- we don't suggest -XEmptyDataDecls for newtypes 2918 ; checkTc (new_or_data == DataType || isSingleton cons) 2919 (newtypeConError tc_name (length cons)) 2920 2921 -- Check that there's at least one condecl, 2922 -- or else we're reading an hs-boot file, or -XEmptyDataDecls 2923 ; empty_data_decls <- xoptM LangExt.EmptyDataDecls 2924 ; is_boot <- tcIsHsBootOrSig -- Are we compiling an hs-boot file? 2925 ; checkTc (not (null cons) || empty_data_decls || is_boot) 2926 (emptyConDeclsErr tc_name) 2927 ; return gadt_syntax } 2928 2929 2930----------------------------------- 2931consUseGadtSyntax :: [LConDecl a] -> Bool 2932consUseGadtSyntax (L _ (ConDeclGADT {}) : _) = True 2933consUseGadtSyntax _ = False 2934 -- All constructors have same shape 2935 2936----------------------------------- 2937tcConDecls :: KnotTied TyCon -> NewOrData 2938 -> [TyConBinder] -> TcKind -- binders and result kind of tycon 2939 -> KnotTied Type -> [LConDecl GhcRn] -> TcM [DataCon] 2940tcConDecls rep_tycon new_or_data tmpl_bndrs res_kind res_tmpl 2941 = concatMapM $ addLocM $ 2942 tcConDecl rep_tycon (mkTyConTagMap rep_tycon) 2943 tmpl_bndrs res_kind res_tmpl new_or_data 2944 -- It's important that we pay for tag allocation here, once per TyCon, 2945 -- See Note [Constructor tag allocation], fixes #14657 2946 2947tcConDecl :: KnotTied TyCon -- Representation tycon. Knot-tied! 2948 -> NameEnv ConTag 2949 -> [TyConBinder] -> TcKind -- tycon binders and result kind 2950 -> KnotTied Type 2951 -- Return type template (T tys), where T is the family TyCon 2952 -> NewOrData 2953 -> ConDecl GhcRn 2954 -> TcM [DataCon] 2955 2956tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data 2957 (ConDeclH98 { con_name = name 2958 , con_ex_tvs = explicit_tkv_nms 2959 , con_mb_cxt = hs_ctxt 2960 , con_args = hs_args }) 2961 = addErrCtxt (dataConCtxtName [name]) $ 2962 do { -- NB: the tyvars from the declaration header are in scope 2963 2964 -- Get hold of the existential type variables 2965 -- e.g. data T a = forall k (b::k) f. MkT a (f b) 2966 -- Here tmpl_bndrs = {a} 2967 -- hs_qvars = HsQTvs { hsq_implicit = {k} 2968 -- , hsq_explicit = {f,b} } 2969 2970 ; traceTc "tcConDecl 1" (vcat [ ppr name, ppr explicit_tkv_nms ]) 2971 2972 ; (exp_tvs, (ctxt, arg_tys, field_lbls, stricts)) 2973 <- pushTcLevelM_ $ 2974 solveEqualities $ 2975 bindExplicitTKBndrs_Skol explicit_tkv_nms $ 2976 do { ctxt <- tcHsMbContext hs_ctxt 2977 ; btys <- tcConArgs hs_args 2978 ; field_lbls <- lookupConstructorFields (unLoc name) 2979 ; let (arg_tys, stricts) = unzip btys 2980 ; dflags <- getDynFlags 2981 ; final_arg_tys <- 2982 unifyNewtypeKind dflags new_or_data 2983 (hsConDeclArgTys hs_args) 2984 arg_tys res_kind 2985 ; return (ctxt, final_arg_tys, field_lbls, stricts) 2986 } 2987 2988 -- exp_tvs have explicit, user-written binding sites 2989 -- the kvs below are those kind variables entirely unmentioned by the user 2990 -- and discovered only by generalization 2991 2992 ; kvs <- kindGeneralizeAll (mkSpecForAllTys (binderVars tmpl_bndrs) $ 2993 mkSpecForAllTys exp_tvs $ 2994 mkPhiTy ctxt $ 2995 mkVisFunTys arg_tys $ 2996 unitTy) 2997 -- That type is a lie, of course. (It shouldn't end in ()!) 2998 -- And we could construct a proper result type from the info 2999 -- at hand. But the result would mention only the tmpl_tvs, 3000 -- and so it just creates more work to do it right. Really, 3001 -- we're only doing this to find the right kind variables to 3002 -- quantify over, and this type is fine for that purpose. 3003 3004 -- Zonk to Types 3005 ; (ze, qkvs) <- zonkTyBndrs kvs 3006 ; (ze, user_qtvs) <- zonkTyBndrsX ze exp_tvs 3007 ; arg_tys <- zonkTcTypesToTypesX ze arg_tys 3008 ; ctxt <- zonkTcTypesToTypesX ze ctxt 3009 3010 ; fam_envs <- tcGetFamInstEnvs 3011 3012 -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here 3013 ; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls) 3014 ; let 3015 univ_tvbs = tyConTyVarBinders tmpl_bndrs 3016 univ_tvs = binderVars univ_tvbs 3017 ex_tvbs = mkTyVarBinders Inferred qkvs ++ 3018 mkTyVarBinders Specified user_qtvs 3019 ex_tvs = qkvs ++ user_qtvs 3020 -- For H98 datatypes, the user-written tyvar binders are precisely 3021 -- the universals followed by the existentials. 3022 -- See Note [DataCon user type variable binders] in DataCon. 3023 user_tvbs = univ_tvbs ++ ex_tvbs 3024 buildOneDataCon (L _ name) = do 3025 { is_infix <- tcConIsInfixH98 name hs_args 3026 ; rep_nm <- newTyConRepName name 3027 3028 ; buildDataCon fam_envs name is_infix rep_nm 3029 stricts Nothing field_lbls 3030 univ_tvs ex_tvs user_tvbs 3031 [{- no eq_preds -}] ctxt arg_tys 3032 res_tmpl rep_tycon tag_map 3033 -- NB: we put data_tc, the type constructor gotten from the 3034 -- constructor type signature into the data constructor; 3035 -- that way checkValidDataCon can complain if it's wrong. 3036 } 3037 ; traceTc "tcConDecl 2" (ppr name) 3038 ; mapM buildOneDataCon [name] 3039 } 3040 3041tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data 3042 -- NB: don't use res_kind here, as it's ill-scoped. Instead, we get 3043 -- the res_kind by typechecking the result type. 3044 (ConDeclGADT { con_names = names 3045 , con_qvars = qtvs 3046 , con_mb_cxt = cxt, con_args = hs_args 3047 , con_res_ty = hs_res_ty }) 3048 | HsQTvs { hsq_ext = implicit_tkv_nms 3049 , hsq_explicit = explicit_tkv_nms } <- qtvs 3050 = addErrCtxt (dataConCtxtName names) $ 3051 do { traceTc "tcConDecl 1 gadt" (ppr names) 3052 ; let (L _ name : _) = names 3053 3054 ; (imp_tvs, (exp_tvs, (ctxt, arg_tys, res_ty, field_lbls, stricts))) 3055 <- pushTcLevelM_ $ -- We are going to generalise 3056 solveEqualities $ -- We won't get another crack, and we don't 3057 -- want an error cascade 3058 bindImplicitTKBndrs_Skol implicit_tkv_nms $ 3059 bindExplicitTKBndrs_Skol explicit_tkv_nms $ 3060 do { ctxt <- tcHsMbContext cxt 3061 ; btys <- tcConArgs hs_args 3062 ; let (arg_tys, stricts) = unzip btys 3063 ; res_ty <- tcHsOpenType hs_res_ty 3064 -- See Note [Implementation of UnliftedNewtypes] 3065 ; dflags <- getDynFlags 3066 ; final_arg_tys <- 3067 unifyNewtypeKind dflags new_or_data 3068 (hsConDeclArgTys hs_args) 3069 arg_tys (typeKind res_ty) 3070 ; field_lbls <- lookupConstructorFields name 3071 ; return (ctxt, final_arg_tys, res_ty, field_lbls, stricts) 3072 } 3073 ; imp_tvs <- zonkAndScopedSort imp_tvs 3074 ; let user_tvs = imp_tvs ++ exp_tvs 3075 3076 ; tkvs <- kindGeneralizeAll (mkSpecForAllTys user_tvs $ 3077 mkPhiTy ctxt $ 3078 mkVisFunTys arg_tys $ 3079 res_ty) 3080 3081 -- Zonk to Types 3082 ; (ze, tkvs) <- zonkTyBndrs tkvs 3083 ; (ze, user_tvs) <- zonkTyBndrsX ze user_tvs 3084 ; arg_tys <- zonkTcTypesToTypesX ze arg_tys 3085 ; ctxt <- zonkTcTypesToTypesX ze ctxt 3086 ; res_ty <- zonkTcTypeToTypeX ze res_ty 3087 3088 ; let (univ_tvs, ex_tvs, tkvs', user_tvs', eq_preds, arg_subst) 3089 = rejigConRes tmpl_bndrs res_tmpl tkvs user_tvs res_ty 3090 -- NB: this is a /lazy/ binding, so we pass six thunks to 3091 -- buildDataCon without yet forcing the guards in rejigConRes 3092 -- See Note [Checking GADT return types] 3093 3094 -- Compute the user-written tyvar binders. These have the same 3095 -- tyvars as univ_tvs/ex_tvs, but perhaps in a different order. 3096 -- See Note [DataCon user type variable binders] in DataCon. 3097 tkv_bndrs = mkTyVarBinders Inferred tkvs' 3098 user_tv_bndrs = mkTyVarBinders Specified user_tvs' 3099 all_user_bndrs = tkv_bndrs ++ user_tv_bndrs 3100 3101 ctxt' = substTys arg_subst ctxt 3102 arg_tys' = substTys arg_subst arg_tys 3103 res_ty' = substTy arg_subst res_ty 3104 3105 3106 ; fam_envs <- tcGetFamInstEnvs 3107 3108 -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here 3109 ; traceTc "tcConDecl 2" (ppr names $$ ppr field_lbls) 3110 ; let 3111 buildOneDataCon (L _ name) = do 3112 { is_infix <- tcConIsInfixGADT name hs_args 3113 ; rep_nm <- newTyConRepName name 3114 3115 ; buildDataCon fam_envs name is_infix 3116 rep_nm 3117 stricts Nothing field_lbls 3118 univ_tvs ex_tvs all_user_bndrs eq_preds 3119 ctxt' arg_tys' res_ty' rep_tycon tag_map 3120 -- NB: we put data_tc, the type constructor gotten from the 3121 -- constructor type signature into the data constructor; 3122 -- that way checkValidDataCon can complain if it's wrong. 3123 } 3124 ; traceTc "tcConDecl 2" (ppr names) 3125 ; mapM buildOneDataCon names 3126 } 3127tcConDecl _ _ _ _ _ _ (ConDeclGADT _ _ _ (XLHsQTyVars nec) _ _ _ _) 3128 = noExtCon nec 3129tcConDecl _ _ _ _ _ _ (XConDecl nec) = noExtCon nec 3130 3131tcConIsInfixH98 :: Name 3132 -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn]) 3133 -> TcM Bool 3134tcConIsInfixH98 _ details 3135 = case details of 3136 InfixCon {} -> return True 3137 _ -> return False 3138 3139tcConIsInfixGADT :: Name 3140 -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn]) 3141 -> TcM Bool 3142tcConIsInfixGADT con details 3143 = case details of 3144 InfixCon {} -> return True 3145 RecCon {} -> return False 3146 PrefixCon arg_tys -- See Note [Infix GADT constructors] 3147 | isSymOcc (getOccName con) 3148 , [_ty1,_ty2] <- arg_tys 3149 -> do { fix_env <- getFixityEnv 3150 ; return (con `elemNameEnv` fix_env) } 3151 | otherwise -> return False 3152 3153tcConArgs :: HsConDeclDetails GhcRn 3154 -> TcM [(TcType, HsSrcBang)] 3155tcConArgs (PrefixCon btys) 3156 = mapM tcConArg btys 3157tcConArgs (InfixCon bty1 bty2) 3158 = do { bty1' <- tcConArg bty1 3159 ; bty2' <- tcConArg bty2 3160 ; return [bty1', bty2'] } 3161tcConArgs (RecCon fields) 3162 = mapM tcConArg btys 3163 where 3164 -- We need a one-to-one mapping from field_names to btys 3165 combined = map (\(L _ f) -> (cd_fld_names f,cd_fld_type f)) 3166 (unLoc fields) 3167 explode (ns,ty) = zip ns (repeat ty) 3168 exploded = concatMap explode combined 3169 (_,btys) = unzip exploded 3170 3171 3172tcConArg :: LHsType GhcRn -> TcM (TcType, HsSrcBang) 3173tcConArg bty 3174 = do { traceTc "tcConArg 1" (ppr bty) 3175 ; arg_ty <- tcHsOpenType (getBangType bty) 3176 -- Newtypes can't have unboxed types, but we check 3177 -- that in checkValidDataCon; this tcConArg stuff 3178 -- doesn't happen for GADT-style declarations 3179 ; traceTc "tcConArg 2" (ppr bty) 3180 ; return (arg_ty, getBangStrictness bty) } 3181 3182{- 3183Note [Infix GADT constructors] 3184~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 3185We do not currently have syntax to declare an infix constructor in GADT syntax, 3186but it makes a (small) difference to the Show instance. So as a slightly 3187ad-hoc solution, we regard a GADT data constructor as infix if 3188 a) it is an operator symbol 3189 b) it has two arguments 3190 c) there is a fixity declaration for it 3191For example: 3192 infix 6 (:--:) 3193 data T a where 3194 (:--:) :: t1 -> t2 -> T Int 3195 3196 3197Note [Checking GADT return types] 3198~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 3199There is a delicacy around checking the return types of a datacon. The 3200central problem is dealing with a declaration like 3201 3202 data T a where 3203 MkT :: T a -> Q a 3204 3205Note that the return type of MkT is totally bogus. When creating the T 3206tycon, we also need to create the MkT datacon, which must have a "rejigged" 3207return type. That is, the MkT datacon's type must be transformed to have 3208a uniform return type with explicit coercions for GADT-like type parameters. 3209This rejigging is what rejigConRes does. The problem is, though, that checking 3210that the return type is appropriate is much easier when done over *Type*, 3211not *HsType*, and doing a call to tcMatchTy will loop because T isn't fully 3212defined yet. 3213 3214So, we want to make rejigConRes lazy and then check the validity of 3215the return type in checkValidDataCon. To do this we /always/ return a 32166-tuple from rejigConRes (so that we can compute the return type from it, which 3217checkValidDataCon needs), but the first three fields may be bogus if 3218the return type isn't valid (the last equation for rejigConRes). 3219 3220This is better than an earlier solution which reduced the number of 3221errors reported in one pass. See #7175, and #10836. 3222-} 3223 3224-- Example 3225-- data instance T (b,c) where 3226-- TI :: forall e. e -> T (e,e) 3227-- 3228-- The representation tycon looks like this: 3229-- data :R7T b c where 3230-- TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1 3231-- In this case orig_res_ty = T (e,e) 3232 3233rejigConRes :: [KnotTied TyConBinder] -> KnotTied Type -- Template for result type; e.g. 3234 -- data instance T [a] b c ... 3235 -- gives template ([a,b,c], T [a] b c) 3236 -> [TyVar] -- The constructor's inferred type variables 3237 -> [TyVar] -- The constructor's user-written, specified 3238 -- type variables 3239 -> KnotTied Type -- res_ty 3240 -> ([TyVar], -- Universal 3241 [TyVar], -- Existential (distinct OccNames from univs) 3242 [TyVar], -- The constructor's rejigged, user-written, 3243 -- inferred type variables 3244 [TyVar], -- The constructor's rejigged, user-written, 3245 -- specified type variables 3246 [EqSpec], -- Equality predicates 3247 TCvSubst) -- Substitution to apply to argument types 3248 -- We don't check that the TyCon given in the ResTy is 3249 -- the same as the parent tycon, because checkValidDataCon will do it 3250-- NB: All arguments may potentially be knot-tied 3251rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty 3252 -- E.g. data T [a] b c where 3253 -- MkT :: forall x y z. T [(x,y)] z z 3254 -- The {a,b,c} are the tmpl_tvs, and the {x,y,z} are the dc_tvs 3255 -- (NB: unlike the H98 case, the dc_tvs are not all existential) 3256 -- Then we generate 3257 -- Univ tyvars Eq-spec 3258 -- a a~(x,y) 3259 -- b b~z 3260 -- z 3261 -- Existentials are the leftover type vars: [x,y] 3262 -- The user-written type variables are what is listed in the forall: 3263 -- [x, y, z] (all specified). We must rejig these as well. 3264 -- See Note [DataCon user type variable binders] in DataCon. 3265 -- So we return ( [a,b,z], [x,y] 3266 -- , [], [x,y,z] 3267 -- , [a~(x,y),b~z], <arg-subst> ) 3268 | Just subst <- tcMatchTy res_tmpl res_ty 3269 = let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tmpl_tvs dc_tvs subst 3270 raw_ex_tvs = dc_tvs `minusList` univ_tvs 3271 (arg_subst, substed_ex_tvs) = substTyVarBndrs kind_subst raw_ex_tvs 3272 3273 -- After rejigging the existential tyvars, the resulting substitution 3274 -- gives us exactly what we need to rejig the user-written tyvars, 3275 -- since the dcUserTyVarBinders invariant guarantees that the 3276 -- substitution has *all* the tyvars in its domain. 3277 -- See Note [DataCon user type variable binders] in DataCon. 3278 subst_user_tvs = map (getTyVar "rejigConRes" . substTyVar arg_subst) 3279 substed_inferred_tvs = subst_user_tvs dc_inferred_tvs 3280 substed_specified_tvs = subst_user_tvs dc_specified_tvs 3281 3282 substed_eqs = map (substEqSpec arg_subst) raw_eqs 3283 in 3284 (univ_tvs, substed_ex_tvs, substed_inferred_tvs, substed_specified_tvs, 3285 substed_eqs, arg_subst) 3286 3287 | otherwise 3288 -- If the return type of the data constructor doesn't match the parent 3289 -- type constructor, or the arity is wrong, the tcMatchTy will fail 3290 -- e.g data T a b where 3291 -- T1 :: Maybe a -- Wrong tycon 3292 -- T2 :: T [a] -- Wrong arity 3293 -- We are detect that later, in checkValidDataCon, but meanwhile 3294 -- we must do *something*, not just crash. So we do something simple 3295 -- albeit bogus, relying on checkValidDataCon to check the 3296 -- bad-result-type error before seeing that the other fields look odd 3297 -- See Note [Checking GADT return types] 3298 = (tmpl_tvs, dc_tvs `minusList` tmpl_tvs, dc_inferred_tvs, dc_specified_tvs, 3299 [], emptyTCvSubst) 3300 where 3301 dc_tvs = dc_inferred_tvs ++ dc_specified_tvs 3302 tmpl_tvs = binderVars tmpl_bndrs 3303 3304{- Note [mkGADTVars] 3305~~~~~~~~~~~~~~~~~~~~ 3306Running example: 3307 3308data T (k1 :: *) (k2 :: *) (a :: k2) (b :: k2) where 3309 MkT :: forall (x1 : *) (y :: x1) (z :: *). 3310 T x1 * (Proxy (y :: x1), z) z 3311 3312We need the rejigged type to be 3313 3314 MkT :: forall (x1 :: *) (k2 :: *) (a :: k2) (b :: k2). 3315 forall (y :: x1) (z :: *). 3316 (k2 ~ *, a ~ (Proxy x1 y, z), b ~ z) 3317 => T x1 k2 a b 3318 3319You might naively expect that z should become a universal tyvar, 3320not an existential. (After all, x1 becomes a universal tyvar.) 3321But z has kind * while b has kind k2, so the return type 3322 T x1 k2 a z 3323is ill-kinded. Another way to say it is this: the universal 3324tyvars must have exactly the same kinds as the tyConTyVars. 3325 3326So we need an existential tyvar and a heterogeneous equality 3327constraint. (The b ~ z is a bit redundant with the k2 ~ * that 3328comes before in that b ~ z implies k2 ~ *. I'm sure we could do 3329some analysis that could eliminate k2 ~ *. But we don't do this 3330yet.) 3331 3332The data con signature has already been fully kind-checked. 3333The return type 3334 3335 T x1 * (Proxy (y :: x1), z) z 3336becomes 3337 qtkvs = [x1 :: *, y :: x1, z :: *] 3338 res_tmpl = T x1 * (Proxy x1 y, z) z 3339 3340We start off by matching (T k1 k2 a b) with (T x1 * (Proxy x1 y, z) z). We 3341know this match will succeed because of the validity check (actually done 3342later, but laziness saves us -- see Note [Checking GADT return types]). 3343Thus, we get 3344 3345 subst := { k1 |-> x1, k2 |-> *, a |-> (Proxy x1 y, z), b |-> z } 3346 3347Now, we need to figure out what the GADT equalities should be. In this case, 3348we *don't* want (k1 ~ x1) to be a GADT equality: it should just be a 3349renaming. The others should be GADT equalities. We also need to make 3350sure that the universally-quantified variables of the datacon match up 3351with the tyvars of the tycon, as required for Core context well-formedness. 3352(This last bit is why we have to rejig at all!) 3353 3354`choose` walks down the tycon tyvars, figuring out what to do with each one. 3355It carries two substitutions: 3356 - t_sub's domain is *template* or *tycon* tyvars, mapping them to variables 3357 mentioned in the datacon signature. 3358 - r_sub's domain is *result* tyvars, names written by the programmer in 3359 the datacon signature. The final rejigged type will use these names, but 3360 the subst is still needed because sometimes the printed name of these variables 3361 is different. (See choose_tv_name, below.) 3362 3363Before explaining the details of `choose`, let's just look at its operation 3364on our example: 3365 3366 choose [] [] {} {} [k1, k2, a, b] 3367 --> -- first branch of `case` statement 3368 choose 3369 univs: [x1 :: *] 3370 eq_spec: [] 3371 t_sub: {k1 |-> x1} 3372 r_sub: {x1 |-> x1} 3373 t_tvs: [k2, a, b] 3374 --> -- second branch of `case` statement 3375 choose 3376 univs: [k2 :: *, x1 :: *] 3377 eq_spec: [k2 ~ *] 3378 t_sub: {k1 |-> x1, k2 |-> k2} 3379 r_sub: {x1 |-> x1} 3380 t_tvs: [a, b] 3381 --> -- second branch of `case` statement 3382 choose 3383 univs: [a :: k2, k2 :: *, x1 :: *] 3384 eq_spec: [ a ~ (Proxy x1 y, z) 3385 , k2 ~ * ] 3386 t_sub: {k1 |-> x1, k2 |-> k2, a |-> a} 3387 r_sub: {x1 |-> x1} 3388 t_tvs: [b] 3389 --> -- second branch of `case` statement 3390 choose 3391 univs: [b :: k2, a :: k2, k2 :: *, x1 :: *] 3392 eq_spec: [ b ~ z 3393 , a ~ (Proxy x1 y, z) 3394 , k2 ~ * ] 3395 t_sub: {k1 |-> x1, k2 |-> k2, a |-> a, b |-> z} 3396 r_sub: {x1 |-> x1} 3397 t_tvs: [] 3398 --> -- end of recursion 3399 ( [x1 :: *, k2 :: *, a :: k2, b :: k2] 3400 , [k2 ~ *, a ~ (Proxy x1 y, z), b ~ z] 3401 , {x1 |-> x1} ) 3402 3403`choose` looks up each tycon tyvar in the matching (it *must* be matched!). 3404 3405* If it finds a bare result tyvar (the first branch of the `case` 3406 statement), it checks to make sure that the result tyvar isn't yet 3407 in the list of univ_tvs. If it is in that list, then we have a 3408 repeated variable in the return type, and we in fact need a GADT 3409 equality. 3410 3411* It then checks to make sure that the kind of the result tyvar 3412 matches the kind of the template tyvar. This check is what forces 3413 `z` to be existential, as it should be, explained above. 3414 3415* Assuming no repeated variables or kind-changing, we wish to use the 3416 variable name given in the datacon signature (that is, `x1` not 3417 `k1`), not the tycon signature (which may have been made up by 3418 GHC). So, we add a mapping from the tycon tyvar to the result tyvar 3419 to t_sub. 3420 3421* If we discover that a mapping in `subst` gives us a non-tyvar (the 3422 second branch of the `case` statement), then we have a GADT equality 3423 to create. We create a fresh equality, but we don't extend any 3424 substitutions. The template variable substitution is meant for use 3425 in universal tyvar kinds, and these shouldn't be affected by any 3426 GADT equalities. 3427 3428This whole algorithm is quite delicate, indeed. I (Richard E.) see two ways 3429of simplifying it: 3430 34311) The first branch of the `case` statement is really an optimization, used 3432in order to get fewer GADT equalities. It might be possible to make a GADT 3433equality for *every* univ. tyvar, even if the equality is trivial, and then 3434either deal with the bigger type or somehow reduce it later. 3435 34362) This algorithm strives to use the names for type variables as specified 3437by the user in the datacon signature. If we always used the tycon tyvar 3438names, for example, this would be simplified. This change would almost 3439certainly degrade error messages a bit, though. 3440-} 3441 3442-- ^ From information about a source datacon definition, extract out 3443-- what the universal variables and the GADT equalities should be. 3444-- See Note [mkGADTVars]. 3445mkGADTVars :: [TyVar] -- ^ The tycon vars 3446 -> [TyVar] -- ^ The datacon vars 3447 -> TCvSubst -- ^ The matching between the template result type 3448 -- and the actual result type 3449 -> ( [TyVar] 3450 , [EqSpec] 3451 , TCvSubst ) -- ^ The univ. variables, the GADT equalities, 3452 -- and a subst to apply to the GADT equalities 3453 -- and existentials. 3454mkGADTVars tmpl_tvs dc_tvs subst 3455 = choose [] [] empty_subst empty_subst tmpl_tvs 3456 where 3457 in_scope = mkInScopeSet (mkVarSet tmpl_tvs `unionVarSet` mkVarSet dc_tvs) 3458 `unionInScope` getTCvInScope subst 3459 empty_subst = mkEmptyTCvSubst in_scope 3460 3461 choose :: [TyVar] -- accumulator of univ tvs, reversed 3462 -> [EqSpec] -- accumulator of GADT equalities, reversed 3463 -> TCvSubst -- template substitution 3464 -> TCvSubst -- res. substitution 3465 -> [TyVar] -- template tvs (the univ tvs passed in) 3466 -> ( [TyVar] -- the univ_tvs 3467 , [EqSpec] -- GADT equalities 3468 , TCvSubst ) -- a substitution to fix kinds in ex_tvs 3469 3470 choose univs eqs _t_sub r_sub [] 3471 = (reverse univs, reverse eqs, r_sub) 3472 choose univs eqs t_sub r_sub (t_tv:t_tvs) 3473 | Just r_ty <- lookupTyVar subst t_tv 3474 = case getTyVar_maybe r_ty of 3475 Just r_tv 3476 | not (r_tv `elem` univs) 3477 , tyVarKind r_tv `eqType` (substTy t_sub (tyVarKind t_tv)) 3478 -> -- simple, well-kinded variable substitution. 3479 choose (r_tv:univs) eqs 3480 (extendTvSubst t_sub t_tv r_ty') 3481 (extendTvSubst r_sub r_tv r_ty') 3482 t_tvs 3483 where 3484 r_tv1 = setTyVarName r_tv (choose_tv_name r_tv t_tv) 3485 r_ty' = mkTyVarTy r_tv1 3486 3487 -- Not a simple substitution: make an equality predicate 3488 _ -> choose (t_tv':univs) (mkEqSpec t_tv' r_ty : eqs) 3489 (extendTvSubst t_sub t_tv (mkTyVarTy t_tv')) 3490 -- We've updated the kind of t_tv, 3491 -- so add it to t_sub (#14162) 3492 r_sub t_tvs 3493 where 3494 t_tv' = updateTyVarKind (substTy t_sub) t_tv 3495 3496 | otherwise 3497 = pprPanic "mkGADTVars" (ppr tmpl_tvs $$ ppr subst) 3498 3499 -- choose an appropriate name for a univ tyvar. 3500 -- This *must* preserve the Unique of the result tv, so that we 3501 -- can detect repeated variables. It prefers user-specified names 3502 -- over system names. A result variable with a system name can 3503 -- happen with GHC-generated implicit kind variables. 3504 choose_tv_name :: TyVar -> TyVar -> Name 3505 choose_tv_name r_tv t_tv 3506 | isSystemName r_tv_name 3507 = setNameUnique t_tv_name (getUnique r_tv_name) 3508 3509 | otherwise 3510 = r_tv_name 3511 3512 where 3513 r_tv_name = getName r_tv 3514 t_tv_name = getName t_tv 3515 3516{- 3517Note [Substitution in template variables kinds] 3518~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 3519 3520data G (a :: Maybe k) where 3521 MkG :: G Nothing 3522 3523With explicit kind variables 3524 3525data G k (a :: Maybe k) where 3526 MkG :: G k1 (Nothing k1) 3527 3528Note how k1 is distinct from k. So, when we match the template 3529`G k a` against `G k1 (Nothing k1)`, we get a subst 3530[ k |-> k1, a |-> Nothing k1 ]. Even though this subst has two 3531mappings, we surely don't want to add (k, k1) to the list of 3532GADT equalities -- that would be overly complex and would create 3533more untouchable variables than we need. So, when figuring out 3534which tyvars are GADT-like and which aren't (the fundamental 3535job of `choose`), we want to treat `k` as *not* GADT-like. 3536Instead, we wish to substitute in `a`'s kind, to get (a :: Maybe k1) 3537instead of (a :: Maybe k). This is the reason for dealing 3538with a substitution in here. 3539 3540However, we do not *always* want to substitute. Consider 3541 3542data H (a :: k) where 3543 MkH :: H Int 3544 3545With explicit kind variables: 3546 3547data H k (a :: k) where 3548 MkH :: H * Int 3549 3550Here, we have a kind-indexed GADT. The subst in question is 3551[ k |-> *, a |-> Int ]. Now, we *don't* want to substitute in `a`'s 3552kind, because that would give a constructor with the type 3553 3554MkH :: forall (k :: *) (a :: *). (k ~ *) -> (a ~ Int) -> H k a 3555 3556The problem here is that a's kind is wrong -- it needs to be k, not *! 3557So, if the matching for a variable is anything but another bare variable, 3558we drop the mapping from the substitution before proceeding. This 3559was not an issue before kind-indexed GADTs because this case could 3560never happen. 3561 3562************************************************************************ 3563* * 3564 Validity checking 3565* * 3566************************************************************************ 3567 3568Validity checking is done once the mutually-recursive knot has been 3569tied, so we can look at things freely. 3570-} 3571 3572checkValidTyCl :: TyCon -> TcM [TyCon] 3573-- The returned list is either a singleton (if valid) 3574-- or a list of "fake tycons" (if not); the fake tycons 3575-- include any implicits, like promoted data constructors 3576-- See Note [Recover from validity error] 3577checkValidTyCl tc 3578 = setSrcSpan (getSrcSpan tc) $ 3579 addTyConCtxt tc $ 3580 recoverM recovery_code $ 3581 do { traceTc "Starting validity for tycon" (ppr tc) 3582 ; checkValidTyCon tc 3583 ; traceTc "Done validity for tycon" (ppr tc) 3584 ; return [tc] } 3585 where 3586 recovery_code -- See Note [Recover from validity error] 3587 = do { traceTc "Aborted validity for tycon" (ppr tc) 3588 ; return (concatMap mk_fake_tc $ 3589 ATyCon tc : implicitTyConThings tc) } 3590 3591 mk_fake_tc (ATyCon tc) 3592 | isClassTyCon tc = [tc] -- Ugh! Note [Recover from validity error] 3593 | otherwise = [makeRecoveryTyCon tc] 3594 mk_fake_tc (AConLike (RealDataCon dc)) 3595 = [makeRecoveryTyCon (promoteDataCon dc)] 3596 mk_fake_tc _ = [] 3597 3598{- Note [Recover from validity error] 3599~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 3600We recover from a validity error in a type or class, which allows us 3601to report multiple validity errors. In the failure case we return a 3602TyCon of the right kind, but with no interesting behaviour 3603(makeRecoveryTyCon). Why? Suppose we have 3604 type T a = Fun 3605where Fun is a type family of arity 1. The RHS is invalid, but we 3606want to go on checking validity of subsequent type declarations. 3607So we replace T with an abstract TyCon which will do no harm. 3608See indexed-types/should_fail/BadSock and #10896 3609 3610Some notes: 3611 3612* We must make fakes for promoted DataCons too. Consider (#15215) 3613 data T a = MkT ... 3614 data S a = ...T...MkT.... 3615 If there is an error in the definition of 'T' we add a "fake type 3616 constructor" to the type environment, so that we can continue to 3617 typecheck 'S'. But we /were not/ adding a fake anything for 'MkT' 3618 and so there was an internal error when we met 'MkT' in the body of 3619 'S'. 3620 3621* Painfully, we *don't* want to do this for classes. 3622 Consider tcfail041: 3623 class (?x::Int) => C a where ... 3624 instance C Int 3625 The class is invalid because of the superclass constraint. But 3626 we still want it to look like a /class/, else the instance bleats 3627 that the instance is mal-formed because it hasn't got a class in 3628 the head. 3629 3630 This is really bogus; now we have in scope a Class that is invalid 3631 in some way, with unknown downstream consequences. A better 3632 alternative might be to make a fake class TyCon. A job for another day. 3633-} 3634 3635------------------------- 3636-- For data types declared with record syntax, we require 3637-- that each constructor that has a field 'f' 3638-- (a) has the same result type 3639-- (b) has the same type for 'f' 3640-- module alpha conversion of the quantified type variables 3641-- of the constructor. 3642-- 3643-- Note that we allow existentials to match because the 3644-- fields can never meet. E.g 3645-- data T where 3646-- T1 { f1 :: b, f2 :: a, f3 ::Int } :: T 3647-- T2 { f1 :: c, f2 :: c, f3 ::Int } :: T 3648-- Here we do not complain about f1,f2 because they are existential 3649 3650checkValidTyCon :: TyCon -> TcM () 3651checkValidTyCon tc 3652 | isPrimTyCon tc -- Happens when Haddock'ing GHC.Prim 3653 = return () 3654 3655 | isWiredInName (getName tc) 3656 -- validity-checking wired-in tycons is a waste of 3657 -- time. More importantly, a wired-in tycon might 3658 -- violate assumptions. Example: (~) has a superclass 3659 -- mentioning (~#), which is ill-kinded in source Haskell 3660 = traceTc "Skipping validity check for wired-in" (ppr tc) 3661 3662 | otherwise 3663 = do { traceTc "checkValidTyCon" (ppr tc $$ ppr (tyConClass_maybe tc)) 3664 ; if | Just cl <- tyConClass_maybe tc 3665 -> checkValidClass cl 3666 3667 | Just syn_rhs <- synTyConRhs_maybe tc 3668 -> do { checkValidType syn_ctxt syn_rhs 3669 ; checkTySynRhs syn_ctxt syn_rhs } 3670 3671 | Just fam_flav <- famTyConFlav_maybe tc 3672 -> case fam_flav of 3673 { ClosedSynFamilyTyCon (Just ax) 3674 -> tcAddClosedTypeFamilyDeclCtxt tc $ 3675 checkValidCoAxiom ax 3676 ; ClosedSynFamilyTyCon Nothing -> return () 3677 ; AbstractClosedSynFamilyTyCon -> 3678 do { hsBoot <- tcIsHsBootOrSig 3679 ; checkTc hsBoot $ 3680 text "You may define an abstract closed type family" $$ 3681 text "only in a .hs-boot file" } 3682 ; DataFamilyTyCon {} -> return () 3683 ; OpenSynFamilyTyCon -> return () 3684 ; BuiltInSynFamTyCon _ -> return () } 3685 3686 | otherwise -> do 3687 { -- Check the context on the data decl 3688 traceTc "cvtc1" (ppr tc) 3689 ; checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc) 3690 3691 ; traceTc "cvtc2" (ppr tc) 3692 3693 ; dflags <- getDynFlags 3694 ; existential_ok <- xoptM LangExt.ExistentialQuantification 3695 ; gadt_ok <- xoptM LangExt.GADTs 3696 ; let ex_ok = existential_ok || gadt_ok 3697 -- Data cons can have existential context 3698 ; mapM_ (checkValidDataCon dflags ex_ok tc) data_cons 3699 ; mapM_ (checkPartialRecordField data_cons) (tyConFieldLabels tc) 3700 3701 -- Check that fields with the same name share a type 3702 ; mapM_ check_fields groups }} 3703 where 3704 syn_ctxt = TySynCtxt name 3705 name = tyConName tc 3706 data_cons = tyConDataCons tc 3707 3708 groups = equivClasses cmp_fld (concatMap get_fields data_cons) 3709 cmp_fld (f1,_) (f2,_) = flLabel f1 `compare` flLabel f2 3710 get_fields con = dataConFieldLabels con `zip` repeat con 3711 -- dataConFieldLabels may return the empty list, which is fine 3712 3713 -- See Note [GADT record selectors] in TcTyDecls 3714 -- We must check (a) that the named field has the same 3715 -- type in each constructor 3716 -- (b) that those constructors have the same result type 3717 -- 3718 -- However, the constructors may have differently named type variable 3719 -- and (worse) we don't know how the correspond to each other. E.g. 3720 -- C1 :: forall a b. { f :: a, g :: b } -> T a b 3721 -- C2 :: forall d c. { f :: c, g :: c } -> T c d 3722 -- 3723 -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's 3724 -- result type against other candidates' types BOTH WAYS ROUND. 3725 -- If they magically agrees, take the substitution and 3726 -- apply them to the latter ones, and see if they match perfectly. 3727 check_fields ((label, con1) :| other_fields) 3728 -- These fields all have the same name, but are from 3729 -- different constructors in the data type 3730 = recoverM (return ()) $ mapM_ checkOne other_fields 3731 -- Check that all the fields in the group have the same type 3732 -- NB: this check assumes that all the constructors of a given 3733 -- data type use the same type variables 3734 where 3735 res1 = dataConOrigResTy con1 3736 fty1 = dataConFieldType con1 lbl 3737 lbl = flLabel label 3738 3739 checkOne (_, con2) -- Do it both ways to ensure they are structurally identical 3740 = do { checkFieldCompat lbl con1 con2 res1 res2 fty1 fty2 3741 ; checkFieldCompat lbl con2 con1 res2 res1 fty2 fty1 } 3742 where 3743 res2 = dataConOrigResTy con2 3744 fty2 = dataConFieldType con2 lbl 3745 3746checkPartialRecordField :: [DataCon] -> FieldLabel -> TcM () 3747-- Checks the partial record field selector, and warns. 3748-- See Note [Checking partial record field] 3749checkPartialRecordField all_cons fld 3750 = setSrcSpan loc $ 3751 warnIfFlag Opt_WarnPartialFields 3752 (not is_exhaustive && not (startsWithUnderscore occ_name)) 3753 (sep [text "Use of partial record field selector" <> colon, 3754 nest 2 $ quotes (ppr occ_name)]) 3755 where 3756 sel_name = flSelector fld 3757 loc = getSrcSpan sel_name 3758 occ_name = getOccName sel_name 3759 3760 (cons_with_field, cons_without_field) = partition has_field all_cons 3761 has_field con = fld `elem` (dataConFieldLabels con) 3762 is_exhaustive = all (dataConCannotMatch inst_tys) cons_without_field 3763 3764 con1 = ASSERT( not (null cons_with_field) ) head cons_with_field 3765 (univ_tvs, _, eq_spec, _, _, _) = dataConFullSig con1 3766 eq_subst = mkTvSubstPrs (map eqSpecPair eq_spec) 3767 inst_tys = substTyVars eq_subst univ_tvs 3768 3769checkFieldCompat :: FieldLabelString -> DataCon -> DataCon 3770 -> Type -> Type -> Type -> Type -> TcM () 3771checkFieldCompat fld con1 con2 res1 res2 fty1 fty2 3772 = do { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2) 3773 ; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) } 3774 where 3775 mb_subst1 = tcMatchTy res1 res2 3776 mb_subst2 = tcMatchTyX (expectJust "checkFieldCompat" mb_subst1) fty1 fty2 3777 3778------------------------------- 3779checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM () 3780checkValidDataCon dflags existential_ok tc con 3781 = setSrcSpan (getSrcSpan con) $ 3782 addErrCtxt (dataConCtxt con) $ 3783 do { -- Check that the return type of the data constructor 3784 -- matches the type constructor; eg reject this: 3785 -- data T a where { MkT :: Bogus a } 3786 -- It's important to do this first: 3787 -- see Note [Checking GADT return types] 3788 -- and c.f. Note [Check role annotations in a second pass] 3789 let tc_tvs = tyConTyVars tc 3790 res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs) 3791 orig_res_ty = dataConOrigResTy con 3792 ; traceTc "checkValidDataCon" (vcat 3793 [ ppr con, ppr tc, ppr tc_tvs 3794 , ppr res_ty_tmpl <+> dcolon <+> ppr (tcTypeKind res_ty_tmpl) 3795 , ppr orig_res_ty <+> dcolon <+> ppr (tcTypeKind orig_res_ty)]) 3796 3797 3798 ; checkTc (isJust (tcMatchTy res_ty_tmpl orig_res_ty)) 3799 (badDataConTyCon con res_ty_tmpl) 3800 -- Note that checkTc aborts if it finds an error. This is 3801 -- critical to avoid panicking when we call dataConUserType 3802 -- on an un-rejiggable datacon! 3803 3804 ; traceTc "checkValidDataCon 2" (ppr (dataConUserType con)) 3805 3806 -- Check that the result type is a *monotype* 3807 -- e.g. reject this: MkT :: T (forall a. a->a) 3808 -- Reason: it's really the argument of an equality constraint 3809 ; checkValidMonoType orig_res_ty 3810 3811 -- Check all argument types for validity 3812 ; checkValidType ctxt (dataConUserType con) 3813 3814 -- If we are dealing with a newtype, we allow levity polymorphism 3815 -- regardless of whether or not UnliftedNewtypes is enabled. A 3816 -- later check in checkNewDataCon handles this, producing a 3817 -- better error message than checkForLevPoly would. 3818 ; unless (isNewTyCon tc) 3819 (mapM_ (checkForLevPoly empty) (dataConOrigArgTys con)) 3820 3821 -- Extra checks for newtype data constructors 3822 ; when (isNewTyCon tc) (checkNewDataCon con) 3823 3824 -- Check that existentials are allowed if they are used 3825 ; checkTc (existential_ok || isVanillaDataCon con) 3826 (badExistential con) 3827 3828 -- Check that UNPACK pragmas and bangs work out 3829 -- E.g. reject data T = MkT {-# UNPACK #-} Int -- No "!" 3830 -- data T = MkT {-# UNPACK #-} !a -- Can't unpack 3831 ; zipWith3M_ check_bang (dataConSrcBangs con) (dataConImplBangs con) [1..] 3832 3833 -- Check the dcUserTyVarBinders invariant 3834 -- See Note [DataCon user type variable binders] in DataCon 3835 -- checked here because we sometimes build invalid DataCons before 3836 -- erroring above here 3837 ; when debugIsOn $ 3838 do { let (univs, exs, eq_spec, _, _, _) = dataConFullSig con 3839 user_tvs = dataConUserTyVars con 3840 user_tvbs_invariant 3841 = Set.fromList (filterEqSpec eq_spec univs ++ exs) 3842 == Set.fromList user_tvs 3843 ; MASSERT2( user_tvbs_invariant 3844 , vcat ([ ppr con 3845 , ppr univs 3846 , ppr exs 3847 , ppr eq_spec 3848 , ppr user_tvs ])) } 3849 3850 ; traceTc "Done validity of data con" $ 3851 vcat [ ppr con 3852 , text "Datacon user type:" <+> ppr (dataConUserType con) 3853 , text "Datacon rep type:" <+> ppr (dataConRepType con) 3854 , text "Rep typcon binders:" <+> ppr (tyConBinders (dataConTyCon con)) 3855 , case tyConFamInst_maybe (dataConTyCon con) of 3856 Nothing -> text "not family" 3857 Just (f, _) -> ppr (tyConBinders f) ] 3858 } 3859 where 3860 ctxt = ConArgCtxt (dataConName con) 3861 3862 check_bang :: HsSrcBang -> HsImplBang -> Int -> TcM () 3863 check_bang (HsSrcBang _ _ SrcLazy) _ n 3864 | not (xopt LangExt.StrictData dflags) 3865 = addErrTc 3866 (bad_bang n (text "Lazy annotation (~) without StrictData")) 3867 check_bang (HsSrcBang _ want_unpack strict_mark) rep_bang n 3868 | isSrcUnpacked want_unpack, not is_strict 3869 = addWarnTc NoReason (bad_bang n (text "UNPACK pragma lacks '!'")) 3870 | isSrcUnpacked want_unpack 3871 , case rep_bang of { HsUnpack {} -> False; _ -> True } 3872 -- If not optimising, we don't unpack (rep_bang is never 3873 -- HsUnpack), so don't complain! This happens, e.g., in Haddock. 3874 -- See dataConSrcToImplBang. 3875 , not (gopt Opt_OmitInterfacePragmas dflags) 3876 -- When typechecking an indefinite package in Backpack, we 3877 -- may attempt to UNPACK an abstract type. The test here will 3878 -- conclude that this is unusable, but it might become usable 3879 -- when we actually fill in the abstract type. As such, don't 3880 -- warn in this case (it gives users the wrong idea about whether 3881 -- or not UNPACK on abstract types is supported; it is!) 3882 , unitIdIsDefinite (thisPackage dflags) 3883 = addWarnTc NoReason (bad_bang n (text "Ignoring unusable UNPACK pragma")) 3884 where 3885 is_strict = case strict_mark of 3886 NoSrcStrict -> xopt LangExt.StrictData dflags 3887 bang -> isSrcStrict bang 3888 3889 check_bang _ _ _ 3890 = return () 3891 3892 bad_bang n herald 3893 = hang herald 2 (text "on the" <+> speakNth n 3894 <+> text "argument of" <+> quotes (ppr con)) 3895------------------------------- 3896checkNewDataCon :: DataCon -> TcM () 3897-- Further checks for the data constructor of a newtype 3898checkNewDataCon con 3899 = do { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys)) 3900 -- One argument 3901 3902 ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes 3903 ; let allowedArgType = 3904 unlifted_newtypes || isLiftedType_maybe arg_ty1 == Just True 3905 ; checkTc allowedArgType $ vcat 3906 [ text "A newtype cannot have an unlifted argument type" 3907 , text "Perhaps you intended to use UnliftedNewtypes" 3908 ] 3909 3910 ; check_con (null eq_spec) $ 3911 text "A newtype constructor must have a return type of form T a1 ... an" 3912 -- Return type is (T a b c) 3913 3914 ; check_con (null theta) $ 3915 text "A newtype constructor cannot have a context in its type" 3916 3917 ; check_con (null ex_tvs) $ 3918 text "A newtype constructor cannot have existential type variables" 3919 -- No existentials 3920 3921 ; checkTc (all ok_bang (dataConSrcBangs con)) 3922 (newtypeStrictError con) 3923 -- No strictness annotations 3924 } 3925 where 3926 (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) 3927 = dataConFullSig con 3928 check_con what msg 3929 = checkTc what (msg $$ ppr con <+> dcolon <+> ppr (dataConUserType con)) 3930 3931 (arg_ty1 : _) = arg_tys 3932 3933 ok_bang (HsSrcBang _ _ SrcStrict) = False 3934 ok_bang (HsSrcBang _ _ SrcLazy) = False 3935 ok_bang _ = True 3936 3937------------------------------- 3938checkValidClass :: Class -> TcM () 3939checkValidClass cls 3940 = do { constrained_class_methods <- xoptM LangExt.ConstrainedClassMethods 3941 ; multi_param_type_classes <- xoptM LangExt.MultiParamTypeClasses 3942 ; nullary_type_classes <- xoptM LangExt.NullaryTypeClasses 3943 ; fundep_classes <- xoptM LangExt.FunctionalDependencies 3944 ; undecidable_super_classes <- xoptM LangExt.UndecidableSuperClasses 3945 3946 -- Check that the class is unary, unless multiparameter type classes 3947 -- are enabled; also recognize deprecated nullary type classes 3948 -- extension (subsumed by multiparameter type classes, #8993) 3949 ; checkTc (multi_param_type_classes || cls_arity == 1 || 3950 (nullary_type_classes && cls_arity == 0)) 3951 (classArityErr cls_arity cls) 3952 ; checkTc (fundep_classes || null fundeps) (classFunDepsErr cls) 3953 3954 -- Check the super-classes 3955 ; checkValidTheta (ClassSCCtxt (className cls)) theta 3956 3957 -- Now check for cyclic superclasses 3958 -- If there are superclass cycles, checkClassCycleErrs bails. 3959 ; unless undecidable_super_classes $ 3960 case checkClassCycles cls of 3961 Just err -> setSrcSpan (getSrcSpan cls) $ 3962 addErrTc err 3963 Nothing -> return () 3964 3965 -- Check the class operations. 3966 -- But only if there have been no earlier errors 3967 -- See Note [Abort when superclass cycle is detected] 3968 ; whenNoErrs $ 3969 mapM_ (check_op constrained_class_methods) op_stuff 3970 3971 -- Check the associated type defaults are well-formed and instantiated 3972 ; mapM_ check_at at_stuff } 3973 where 3974 (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls 3975 cls_arity = length (tyConVisibleTyVars (classTyCon cls)) 3976 -- Ignore invisible variables 3977 cls_tv_set = mkVarSet tyvars 3978 3979 check_op constrained_class_methods (sel_id, dm) 3980 = setSrcSpan (getSrcSpan sel_id) $ 3981 addErrCtxt (classOpCtxt sel_id op_ty) $ do 3982 { traceTc "class op type" (ppr op_ty) 3983 ; checkValidType ctxt op_ty 3984 -- This implements the ambiguity check, among other things 3985 -- Example: tc223 3986 -- class Error e => Game b mv e | b -> mv e where 3987 -- newBoard :: MonadState b m => m () 3988 -- Here, MonadState has a fundep m->b, so newBoard is fine 3989 3990 -- a method cannot be levity polymorphic, as we have to store the 3991 -- method in a dictionary 3992 -- example of what this prevents: 3993 -- class BoundedX (a :: TYPE r) where minBound :: a 3994 -- See Note [Levity polymorphism checking] in DsMonad 3995 ; checkForLevPoly empty tau1 3996 3997 ; unless constrained_class_methods $ 3998 mapM_ check_constraint (tail (cls_pred:op_theta)) 3999 4000 ; check_dm ctxt sel_id cls_pred tau2 dm 4001 } 4002 where 4003 ctxt = FunSigCtxt op_name True -- Report redundant class constraints 4004 op_name = idName sel_id 4005 op_ty = idType sel_id 4006 (_,cls_pred,tau1) = tcSplitMethodTy op_ty 4007 -- See Note [Splitting nested sigma types in class type signatures] 4008 (_,op_theta,tau2) = tcSplitNestedSigmaTys tau1 4009 4010 check_constraint :: TcPredType -> TcM () 4011 check_constraint pred -- See Note [Class method constraints] 4012 = when (not (isEmptyVarSet pred_tvs) && 4013 pred_tvs `subVarSet` cls_tv_set) 4014 (addErrTc (badMethPred sel_id pred)) 4015 where 4016 pred_tvs = tyCoVarsOfType pred 4017 4018 check_at (ATI fam_tc m_dflt_rhs) 4019 = do { checkTc (cls_arity == 0 || any (`elemVarSet` cls_tv_set) fam_tvs) 4020 (noClassTyVarErr cls fam_tc) 4021 -- Check that the associated type mentions at least 4022 -- one of the class type variables 4023 -- The check is disabled for nullary type classes, 4024 -- since there is no possible ambiguity (#10020) 4025 4026 -- Check that any default declarations for associated types are valid 4027 ; whenIsJust m_dflt_rhs $ \ (rhs, loc) -> 4028 setSrcSpan loc $ 4029 tcAddFamInstCtxt (text "default type instance") (getName fam_tc) $ 4030 checkValidTyFamEqn fam_tc fam_tvs (mkTyVarTys fam_tvs) rhs } 4031 where 4032 fam_tvs = tyConTyVars fam_tc 4033 4034 check_dm :: UserTypeCtxt -> Id -> PredType -> Type -> DefMethInfo -> TcM () 4035 -- Check validity of the /top-level/ generic-default type 4036 -- E.g for class C a where 4037 -- default op :: forall b. (a~b) => blah 4038 -- we do not want to do an ambiguity check on a type with 4039 -- a free TyVar 'a' (#11608). See TcType 4040 -- Note [TyVars and TcTyVars during type checking] in TcType 4041 -- Hence the mkDefaultMethodType to close the type. 4042 check_dm ctxt sel_id vanilla_cls_pred vanilla_tau 4043 (Just (dm_name, dm_spec@(GenericDM dm_ty))) 4044 = setSrcSpan (getSrcSpan dm_name) $ do 4045 -- We have carefully set the SrcSpan on the generic 4046 -- default-method Name to be that of the generic 4047 -- default type signature 4048 4049 -- First, we check that that the method's default type signature 4050 -- aligns with the non-default type signature. 4051 -- See Note [Default method type signatures must align] 4052 let cls_pred = mkClassPred cls $ mkTyVarTys $ classTyVars cls 4053 -- Note that the second field of this tuple contains the context 4054 -- of the default type signature, making it apparent that we 4055 -- ignore method contexts completely when validity-checking 4056 -- default type signatures. See the end of 4057 -- Note [Default method type signatures must align] 4058 -- to learn why this is OK. 4059 -- 4060 -- See also 4061 -- Note [Splitting nested sigma types in class type signatures] 4062 -- for an explanation of why we don't use tcSplitSigmaTy here. 4063 (_, _, dm_tau) = tcSplitNestedSigmaTys dm_ty 4064 4065 -- Given this class definition: 4066 -- 4067 -- class C a b where 4068 -- op :: forall p q. (Ord a, D p q) 4069 -- => a -> b -> p -> (a, b) 4070 -- default op :: forall r s. E r 4071 -- => a -> b -> s -> (a, b) 4072 -- 4073 -- We want to match up two types of the form: 4074 -- 4075 -- Vanilla type sig: C aa bb => aa -> bb -> p -> (aa, bb) 4076 -- Default type sig: C a b => a -> b -> s -> (a, b) 4077 -- 4078 -- Notice that the two type signatures can be quantified over 4079 -- different class type variables! Therefore, it's important that 4080 -- we include the class predicate parts to match up a with aa and 4081 -- b with bb. 4082 vanilla_phi_ty = mkPhiTy [vanilla_cls_pred] vanilla_tau 4083 dm_phi_ty = mkPhiTy [cls_pred] dm_tau 4084 4085 traceTc "check_dm" $ vcat 4086 [ text "vanilla_phi_ty" <+> ppr vanilla_phi_ty 4087 , text "dm_phi_ty" <+> ppr dm_phi_ty ] 4088 4089 -- Actually checking that the types align is done with a call to 4090 -- tcMatchTys. We need to get a match in both directions to rule 4091 -- out degenerate cases like these: 4092 -- 4093 -- class Foo a where 4094 -- foo1 :: a -> b 4095 -- default foo1 :: a -> Int 4096 -- 4097 -- foo2 :: a -> Int 4098 -- default foo2 :: a -> b 4099 unless (isJust $ tcMatchTys [dm_phi_ty, vanilla_phi_ty] 4100 [vanilla_phi_ty, dm_phi_ty]) $ addErrTc $ 4101 hang (text "The default type signature for" 4102 <+> ppr sel_id <> colon) 4103 2 (ppr dm_ty) 4104 $$ (text "does not match its corresponding" 4105 <+> text "non-default type signature") 4106 4107 -- Now do an ambiguity check on the default type signature. 4108 checkValidType ctxt (mkDefaultMethodType cls sel_id dm_spec) 4109 check_dm _ _ _ _ _ = return () 4110 4111checkFamFlag :: Name -> TcM () 4112-- Check that we don't use families without -XTypeFamilies 4113-- The parser won't even parse them, but I suppose a GHC API 4114-- client might have a go! 4115checkFamFlag tc_name 4116 = do { idx_tys <- xoptM LangExt.TypeFamilies 4117 ; checkTc idx_tys err_msg } 4118 where 4119 err_msg = hang (text "Illegal family declaration for" <+> quotes (ppr tc_name)) 4120 2 (text "Enable TypeFamilies to allow indexed type families") 4121 4122checkResultSigFlag :: Name -> FamilyResultSig GhcRn -> TcM () 4123checkResultSigFlag tc_name (TyVarSig _ tvb) 4124 = do { ty_fam_deps <- xoptM LangExt.TypeFamilyDependencies 4125 ; checkTc ty_fam_deps $ 4126 hang (text "Illegal result type variable" <+> ppr tvb <+> text "for" <+> quotes (ppr tc_name)) 4127 2 (text "Enable TypeFamilyDependencies to allow result variable names") } 4128checkResultSigFlag _ _ = return () -- other cases OK 4129 4130{- Note [Class method constraints] 4131~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 4132Haskell 2010 is supposed to reject 4133 class C a where 4134 op :: Eq a => a -> a 4135where the method type constrains only the class variable(s). (The extension 4136-XConstrainedClassMethods switches off this check.) But regardless 4137we should not reject 4138 class C a where 4139 op :: (?x::Int) => a -> a 4140as pointed out in #11793. So the test here rejects the program if 4141 * -XConstrainedClassMethods is off 4142 * the tyvars of the constraint are non-empty 4143 * all the tyvars are class tyvars, none are locally quantified 4144 4145Note [Abort when superclass cycle is detected] 4146~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 4147We must avoid doing the ambiguity check for the methods (in 4148checkValidClass.check_op) when there are already errors accumulated. 4149This is because one of the errors may be a superclass cycle, and 4150superclass cycles cause canonicalization to loop. Here is a 4151representative example: 4152 4153 class D a => C a where 4154 meth :: D a => () 4155 class C a => D a 4156 4157This fixes #9415, #9739 4158 4159Note [Default method type signatures must align] 4160~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 4161GHC enforces the invariant that a class method's default type signature 4162must "align" with that of the method's non-default type signature, as per 4163GHC #12918. For instance, if you have: 4164 4165 class Foo a where 4166 bar :: forall b. Context => a -> b 4167 4168Then a default type signature for bar must be alpha equivalent to 4169(forall b. a -> b). That is, the types must be the same modulo differences in 4170contexts. So the following would be acceptable default type signatures: 4171 4172 default bar :: forall b. Context1 => a -> b 4173 default bar :: forall x. Context2 => a -> x 4174 4175But the following are NOT acceptable default type signatures: 4176 4177 default bar :: forall b. b -> a 4178 default bar :: forall x. x 4179 default bar :: a -> Int 4180 4181Note that a is bound by the class declaration for Foo itself, so it is 4182not allowed to differ in the default type signature. 4183 4184The default type signature (default bar :: a -> Int) deserves special mention, 4185since (a -> Int) is a straightforward instantiation of (forall b. a -> b). To 4186write this, you need to declare the default type signature like so: 4187 4188 default bar :: forall b. (b ~ Int). a -> b 4189 4190As noted in #12918, there are several reasons to do this: 4191 41921. It would make no sense to have a type that was flat-out incompatible with 4193 the non-default type signature. For instance, if you had: 4194 4195 class Foo a where 4196 bar :: a -> Int 4197 default bar :: a -> Bool 4198 4199 Then that would always fail in an instance declaration. So this check 4200 nips such cases in the bud before they have the chance to produce 4201 confusing error messages. 4202 42032. Internally, GHC uses TypeApplications to instantiate the default method in 4204 an instance. See Note [Default methods in instances] in TcInstDcls. 4205 Thus, GHC needs to know exactly what the universally quantified type 4206 variables are, and when instantiated that way, the default method's type 4207 must match the expected type. 4208 42093. Aesthetically, by only allowing the default type signature to differ in its 4210 context, we are making it more explicit the ways in which the default type 4211 signature is less polymorphic than the non-default type signature. 4212 4213You might be wondering: why are the contexts allowed to be different, but not 4214the rest of the type signature? That's because default implementations often 4215rely on assumptions that the more general, non-default type signatures do not. 4216For instance, in the Enum class declaration: 4217 4218 class Enum a where 4219 enum :: [a] 4220 default enum :: (Generic a, GEnum (Rep a)) => [a] 4221 enum = map to genum 4222 4223 class GEnum f where 4224 genum :: [f a] 4225 4226The default implementation for enum only works for types that are instances of 4227Generic, and for which their generic Rep type is an instance of GEnum. But 4228clearly enum doesn't _have_ to use this implementation, so naturally, the 4229context for enum is allowed to be different to accommodate this. As a result, 4230when we validity-check default type signatures, we ignore contexts completely. 4231 4232Note that when checking whether two type signatures match, we must take care to 4233split as many foralls as it takes to retrieve the tau types we which to check. 4234See Note [Splitting nested sigma types in class type signatures]. 4235 4236Note [Splitting nested sigma types in class type signatures] 4237~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 4238Consider this type synonym and class definition: 4239 4240 type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t 4241 4242 class Each s t a b where 4243 each :: Traversal s t a b 4244 default each :: (Traversable g, s ~ g a, t ~ g b) => Traversal s t a b 4245 4246It might seem obvious that the tau types in both type signatures for `each` 4247are the same, but actually getting GHC to conclude this is surprisingly tricky. 4248That is because in general, the form of a class method's non-default type 4249signature is: 4250 4251 forall a. C a => forall d. D d => E a b 4252 4253And the general form of a default type signature is: 4254 4255 forall f. F f => E a f -- The variable `a` comes from the class 4256 4257So it you want to get the tau types in each type signature, you might find it 4258reasonable to call tcSplitSigmaTy twice on the non-default type signature, and 4259call it once on the default type signature. For most classes and methods, this 4260will work, but Each is a bit of an exceptional case. The way `each` is written, 4261it doesn't quantify any additional type variables besides those of the Each 4262class itself, so the non-default type signature for `each` is actually this: 4263 4264 forall s t a b. Each s t a b => Traversal s t a b 4265 4266Notice that there _appears_ to only be one forall. But there's actually another 4267forall lurking in the Traversal type synonym, so if you call tcSplitSigmaTy 4268twice, you'll also go under the forall in Traversal! That is, you'll end up 4269with: 4270 4271 (a -> f b) -> s -> f t 4272 4273A problem arises because you only call tcSplitSigmaTy once on the default type 4274signature for `each`, which gives you 4275 4276 Traversal s t a b 4277 4278Or, equivalently: 4279 4280 forall f. Applicative f => (a -> f b) -> s -> f t 4281 4282This is _not_ the same thing as (a -> f b) -> s -> f t! So now tcMatchTy will 4283say that the tau types for `each` are not equal. 4284 4285A solution to this problem is to use tcSplitNestedSigmaTys instead of 4286tcSplitSigmaTy. tcSplitNestedSigmaTys will always split any foralls that it 4287sees until it can't go any further, so if you called it on the default type 4288signature for `each`, it would return (a -> f b) -> s -> f t like we desired. 4289 4290Note [Checking partial record field] 4291~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 4292This check checks the partial record field selector, and warns (#7169). 4293 4294For example: 4295 4296 data T a = A { m1 :: a, m2 :: a } | B { m1 :: a } 4297 4298The function 'm2' is partial record field, and will fail when it is applied to 4299'B'. The warning identifies such partial fields. The check is performed at the 4300declaration of T, not at the call-sites of m2. 4301 4302The warning can be suppressed by prefixing the field-name with an underscore. 4303For example: 4304 4305 data T a = A { m1 :: a, _m2 :: a } | B { m1 :: a } 4306 4307************************************************************************ 4308* * 4309 Checking role validity 4310* * 4311************************************************************************ 4312-} 4313 4314checkValidRoleAnnots :: RoleAnnotEnv -> TyCon -> TcM () 4315checkValidRoleAnnots role_annots tc 4316 | isTypeSynonymTyCon tc = check_no_roles 4317 | isFamilyTyCon tc = check_no_roles 4318 | isAlgTyCon tc = check_roles 4319 | otherwise = return () 4320 where 4321 -- Role annotations are given only on *explicit* variables, 4322 -- but a tycon stores roles for all variables. 4323 -- So, we drop the implicit roles (which are all Nominal, anyway). 4324 name = tyConName tc 4325 roles = tyConRoles tc 4326 (vis_roles, vis_vars) = unzip $ mapMaybe pick_vis $ 4327 zip roles (tyConBinders tc) 4328 role_annot_decl_maybe = lookupRoleAnnot role_annots name 4329 4330 pick_vis :: (Role, TyConBinder) -> Maybe (Role, TyVar) 4331 pick_vis (role, tvb) 4332 | isVisibleTyConBinder tvb = Just (role, binderVar tvb) 4333 | otherwise = Nothing 4334 4335 check_roles 4336 = whenIsJust role_annot_decl_maybe $ 4337 \decl@(L loc (RoleAnnotDecl _ _ the_role_annots)) -> 4338 addRoleAnnotCtxt name $ 4339 setSrcSpan loc $ do 4340 { role_annots_ok <- xoptM LangExt.RoleAnnotations 4341 ; checkTc role_annots_ok $ needXRoleAnnotations tc 4342 ; checkTc (vis_vars `equalLength` the_role_annots) 4343 (wrongNumberOfRoles vis_vars decl) 4344 ; _ <- zipWith3M checkRoleAnnot vis_vars the_role_annots vis_roles 4345 -- Representational or phantom roles for class parameters 4346 -- quickly lead to incoherence. So, we require 4347 -- IncoherentInstances to have them. See #8773, #14292 4348 ; incoherent_roles_ok <- xoptM LangExt.IncoherentInstances 4349 ; checkTc ( incoherent_roles_ok 4350 || (not $ isClassTyCon tc) 4351 || (all (== Nominal) vis_roles)) 4352 incoherentRoles 4353 4354 ; lint <- goptM Opt_DoCoreLinting 4355 ; when lint $ checkValidRoles tc } 4356 4357 check_no_roles 4358 = whenIsJust role_annot_decl_maybe illegalRoleAnnotDecl 4359 4360checkRoleAnnot :: TyVar -> Located (Maybe Role) -> Role -> TcM () 4361checkRoleAnnot _ (L _ Nothing) _ = return () 4362checkRoleAnnot tv (L _ (Just r1)) r2 4363 = when (r1 /= r2) $ 4364 addErrTc $ badRoleAnnot (tyVarName tv) r1 r2 4365 4366-- This is a double-check on the role inference algorithm. It is only run when 4367-- -dcore-lint is enabled. See Note [Role inference] in TcTyDecls 4368checkValidRoles :: TyCon -> TcM () 4369-- If you edit this function, you may need to update the GHC formalism 4370-- See Note [GHC Formalism] in CoreLint 4371checkValidRoles tc 4372 | isAlgTyCon tc 4373 -- tyConDataCons returns an empty list for data families 4374 = mapM_ check_dc_roles (tyConDataCons tc) 4375 | Just rhs <- synTyConRhs_maybe tc 4376 = check_ty_roles (zipVarEnv (tyConTyVars tc) (tyConRoles tc)) Representational rhs 4377 | otherwise 4378 = return () 4379 where 4380 check_dc_roles datacon 4381 = do { traceTc "check_dc_roles" (ppr datacon <+> ppr (tyConRoles tc)) 4382 ; mapM_ (check_ty_roles role_env Representational) $ 4383 eqSpecPreds eq_spec ++ theta ++ arg_tys } 4384 -- See Note [Role-checking data constructor arguments] in TcTyDecls 4385 where 4386 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) 4387 = dataConFullSig datacon 4388 univ_roles = zipVarEnv univ_tvs (tyConRoles tc) 4389 -- zipVarEnv uses zipEqual, but we don't want that for ex_tvs 4390 ex_roles = mkVarEnv (map (, Nominal) ex_tvs) 4391 role_env = univ_roles `plusVarEnv` ex_roles 4392 4393 check_ty_roles env role ty 4394 | Just ty' <- coreView ty -- #14101 4395 = check_ty_roles env role ty' 4396 4397 check_ty_roles env role (TyVarTy tv) 4398 = case lookupVarEnv env tv of 4399 Just role' -> unless (role' `ltRole` role || role' == role) $ 4400 report_error $ text "type variable" <+> quotes (ppr tv) <+> 4401 text "cannot have role" <+> ppr role <+> 4402 text "because it was assigned role" <+> ppr role' 4403 Nothing -> report_error $ text "type variable" <+> quotes (ppr tv) <+> 4404 text "missing in environment" 4405 4406 check_ty_roles env Representational (TyConApp tc tys) 4407 = let roles' = tyConRoles tc in 4408 zipWithM_ (maybe_check_ty_roles env) roles' tys 4409 4410 check_ty_roles env Nominal (TyConApp _ tys) 4411 = mapM_ (check_ty_roles env Nominal) tys 4412 4413 check_ty_roles _ Phantom ty@(TyConApp {}) 4414 = pprPanic "check_ty_roles" (ppr ty) 4415 4416 check_ty_roles env role (AppTy ty1 ty2) 4417 = check_ty_roles env role ty1 4418 >> check_ty_roles env Nominal ty2 4419 4420 check_ty_roles env role (FunTy _ ty1 ty2) 4421 = check_ty_roles env role ty1 4422 >> check_ty_roles env role ty2 4423 4424 check_ty_roles env role (ForAllTy (Bndr tv _) ty) 4425 = check_ty_roles env Nominal (tyVarKind tv) 4426 >> check_ty_roles (extendVarEnv env tv Nominal) role ty 4427 4428 check_ty_roles _ _ (LitTy {}) = return () 4429 4430 check_ty_roles env role (CastTy t _) 4431 = check_ty_roles env role t 4432 4433 check_ty_roles _ role (CoercionTy co) 4434 = unless (role == Phantom) $ 4435 report_error $ text "coercion" <+> ppr co <+> text "has bad role" <+> ppr role 4436 4437 maybe_check_ty_roles env role ty 4438 = when (role == Nominal || role == Representational) $ 4439 check_ty_roles env role ty 4440 4441 report_error doc 4442 = addErrTc $ vcat [text "Internal error in role inference:", 4443 doc, 4444 text "Please report this as a GHC bug: https://www.haskell.org/ghc/reportabug"] 4445 4446{- 4447************************************************************************ 4448* * 4449 Error messages 4450* * 4451************************************************************************ 4452-} 4453 4454addVDQNote :: TcTyCon -> TcM a -> TcM a 4455-- See Note [Inferring visible dependent quantification] 4456-- Only types without a signature (CUSK or SAK) here 4457addVDQNote tycon thing_inside 4458 | ASSERT2( isTcTyCon tycon, ppr tycon ) 4459 ASSERT2( not (tcTyConIsPoly tycon), ppr tycon $$ ppr tc_kind ) 4460 has_vdq 4461 = addLandmarkErrCtxt vdq_warning thing_inside 4462 | otherwise 4463 = thing_inside 4464 where 4465 -- Check whether a tycon has visible dependent quantification. 4466 -- This will *always* be a TcTyCon. Furthermore, it will *always* 4467 -- be an ungeneralised TcTyCon, straight out of kcInferDeclHeader. 4468 -- Thus, all the TyConBinders will be anonymous. Thus, the 4469 -- free variables of the tycon's kind will be the same as the free 4470 -- variables from all the binders. 4471 has_vdq = any is_vdq_tcb (tyConBinders tycon) 4472 tc_kind = tyConKind tycon 4473 kind_fvs = tyCoVarsOfType tc_kind 4474 4475 is_vdq_tcb tcb = (binderVar tcb `elemVarSet` kind_fvs) && 4476 isVisibleTyConBinder tcb 4477 4478 vdq_warning = vcat 4479 [ text "NB: Type" <+> quotes (ppr tycon) <+> 4480 text "was inferred to use visible dependent quantification." 4481 , text "Most types with visible dependent quantification are" 4482 , text "polymorphically recursive and need a standalone kind" 4483 , text "signature. Perhaps supply one, with StandaloneKindSignatures." 4484 ] 4485 4486tcAddTyFamInstCtxt :: TyFamInstDecl GhcRn -> TcM a -> TcM a 4487tcAddTyFamInstCtxt decl 4488 = tcAddFamInstCtxt (text "type instance") (tyFamInstDeclName decl) 4489 4490tcMkDataFamInstCtxt :: DataFamInstDecl GhcRn -> SDoc 4491tcMkDataFamInstCtxt decl@(DataFamInstDecl { dfid_eqn = 4492 HsIB { hsib_body = eqn }}) 4493 = tcMkFamInstCtxt (pprDataFamInstFlavour decl <+> text "instance") 4494 (unLoc (feqn_tycon eqn)) 4495tcMkDataFamInstCtxt (DataFamInstDecl (XHsImplicitBndrs nec)) 4496 = noExtCon nec 4497 4498tcAddDataFamInstCtxt :: DataFamInstDecl GhcRn -> TcM a -> TcM a 4499tcAddDataFamInstCtxt decl 4500 = addErrCtxt (tcMkDataFamInstCtxt decl) 4501 4502tcMkFamInstCtxt :: SDoc -> Name -> SDoc 4503tcMkFamInstCtxt flavour tycon 4504 = hsep [ text "In the" <+> flavour <+> text "declaration for" 4505 , quotes (ppr tycon) ] 4506 4507tcAddFamInstCtxt :: SDoc -> Name -> TcM a -> TcM a 4508tcAddFamInstCtxt flavour tycon thing_inside 4509 = addErrCtxt (tcMkFamInstCtxt flavour tycon) thing_inside 4510 4511tcAddClosedTypeFamilyDeclCtxt :: TyCon -> TcM a -> TcM a 4512tcAddClosedTypeFamilyDeclCtxt tc 4513 = addErrCtxt ctxt 4514 where 4515 ctxt = text "In the equations for closed type family" <+> 4516 quotes (ppr tc) 4517 4518resultTypeMisMatch :: FieldLabelString -> DataCon -> DataCon -> SDoc 4519resultTypeMisMatch field_name con1 con2 4520 = vcat [sep [text "Constructors" <+> ppr con1 <+> text "and" <+> ppr con2, 4521 text "have a common field" <+> quotes (ppr field_name) <> comma], 4522 nest 2 $ text "but have different result types"] 4523 4524fieldTypeMisMatch :: FieldLabelString -> DataCon -> DataCon -> SDoc 4525fieldTypeMisMatch field_name con1 con2 4526 = sep [text "Constructors" <+> ppr con1 <+> text "and" <+> ppr con2, 4527 text "give different types for field", quotes (ppr field_name)] 4528 4529dataConCtxtName :: [Located Name] -> SDoc 4530dataConCtxtName [con] 4531 = text "In the definition of data constructor" <+> quotes (ppr con) 4532dataConCtxtName con 4533 = text "In the definition of data constructors" <+> interpp'SP con 4534 4535dataConCtxt :: Outputable a => a -> SDoc 4536dataConCtxt con = text "In the definition of data constructor" <+> quotes (ppr con) 4537 4538classOpCtxt :: Var -> Type -> SDoc 4539classOpCtxt sel_id tau = sep [text "When checking the class method:", 4540 nest 2 (pprPrefixOcc sel_id <+> dcolon <+> ppr tau)] 4541 4542classArityErr :: Int -> Class -> SDoc 4543classArityErr n cls 4544 | n == 0 = mkErr "No" "no-parameter" 4545 | otherwise = mkErr "Too many" "multi-parameter" 4546 where 4547 mkErr howMany allowWhat = 4548 vcat [text (howMany ++ " parameters for class") <+> quotes (ppr cls), 4549 parens (text ("Enable MultiParamTypeClasses to allow " 4550 ++ allowWhat ++ " classes"))] 4551 4552classFunDepsErr :: Class -> SDoc 4553classFunDepsErr cls 4554 = vcat [text "Fundeps in class" <+> quotes (ppr cls), 4555 parens (text "Enable FunctionalDependencies to allow fundeps")] 4556 4557badMethPred :: Id -> TcPredType -> SDoc 4558badMethPred sel_id pred 4559 = vcat [ hang (text "Constraint" <+> quotes (ppr pred) 4560 <+> text "in the type of" <+> quotes (ppr sel_id)) 4561 2 (text "constrains only the class type variables") 4562 , text "Enable ConstrainedClassMethods to allow it" ] 4563 4564noClassTyVarErr :: Class -> TyCon -> SDoc 4565noClassTyVarErr clas fam_tc 4566 = sep [ text "The associated type" <+> quotes (ppr fam_tc <+> hsep (map ppr (tyConTyVars fam_tc))) 4567 , text "mentions none of the type or kind variables of the class" <+> 4568 quotes (ppr clas <+> hsep (map ppr (classTyVars clas)))] 4569 4570badDataConTyCon :: DataCon -> Type -> SDoc 4571badDataConTyCon data_con res_ty_tmpl 4572 | ASSERT( all isTyVar tvs ) 4573 tcIsForAllTy actual_res_ty 4574 = nested_foralls_contexts_suggestion 4575 | isJust (tcSplitPredFunTy_maybe actual_res_ty) 4576 = nested_foralls_contexts_suggestion 4577 | otherwise 4578 = hang (text "Data constructor" <+> quotes (ppr data_con) <+> 4579 text "returns type" <+> quotes (ppr actual_res_ty)) 4580 2 (text "instead of an instance of its parent type" <+> quotes (ppr res_ty_tmpl)) 4581 where 4582 actual_res_ty = dataConOrigResTy data_con 4583 4584 -- This suggestion is useful for suggesting how to correct code like what 4585 -- was reported in #12087: 4586 -- 4587 -- data F a where 4588 -- MkF :: Ord a => Eq a => a -> F a 4589 -- 4590 -- Although nested foralls or contexts are allowed in function type 4591 -- signatures, it is much more difficult to engineer GADT constructor type 4592 -- signatures to allow something similar, so we error in the latter case. 4593 -- Nevertheless, we can at least suggest how a user might reshuffle their 4594 -- exotic GADT constructor type signature so that GHC will accept. 4595 nested_foralls_contexts_suggestion = 4596 text "GADT constructor type signature cannot contain nested" 4597 <+> quotes forAllLit <> text "s or contexts" 4598 $+$ hang (text "Suggestion: instead use this type signature:") 4599 2 (ppr (dataConName data_con) <+> dcolon <+> ppr suggested_ty) 4600 4601 -- To construct a type that GHC would accept (suggested_ty), we: 4602 -- 4603 -- 1) Find the existentially quantified type variables and the class 4604 -- predicates from the datacon. (NB: We don't need the universally 4605 -- quantified type variables, since rejigConRes won't substitute them in 4606 -- the result type if it fails, as in this scenario.) 4607 -- 2) Split apart the return type (which is headed by a forall or a 4608 -- context) using tcSplitNestedSigmaTys, collecting the type variables 4609 -- and class predicates we find, as well as the rho type lurking 4610 -- underneath the nested foralls and contexts. 4611 -- 3) Smash together the type variables and class predicates from 1) and 4612 -- 2), and prepend them to the rho type from 2). 4613 (tvs, theta, rho) = tcSplitNestedSigmaTys (dataConUserType data_con) 4614 suggested_ty = mkSpecSigmaTy tvs theta rho 4615 4616badGadtDecl :: Name -> SDoc 4617badGadtDecl tc_name 4618 = vcat [ text "Illegal generalised algebraic data declaration for" <+> quotes (ppr tc_name) 4619 , nest 2 (parens $ text "Enable the GADTs extension to allow this") ] 4620 4621badExistential :: DataCon -> SDoc 4622badExistential con 4623 = hang (text "Data constructor" <+> quotes (ppr con) <+> 4624 text "has existential type variables, a context, or a specialised result type") 4625 2 (vcat [ ppr con <+> dcolon <+> ppr (dataConUserType con) 4626 , parens $ text "Enable ExistentialQuantification or GADTs to allow this" ]) 4627 4628badStupidTheta :: Name -> SDoc 4629badStupidTheta tc_name 4630 = text "A data type declared in GADT style cannot have a context:" <+> quotes (ppr tc_name) 4631 4632newtypeConError :: Name -> Int -> SDoc 4633newtypeConError tycon n 4634 = sep [text "A newtype must have exactly one constructor,", 4635 nest 2 $ text "but" <+> quotes (ppr tycon) <+> text "has" <+> speakN n ] 4636 4637newtypeStrictError :: DataCon -> SDoc 4638newtypeStrictError con 4639 = sep [text "A newtype constructor cannot have a strictness annotation,", 4640 nest 2 $ text "but" <+> quotes (ppr con) <+> text "does"] 4641 4642newtypeFieldErr :: DataCon -> Int -> SDoc 4643newtypeFieldErr con_name n_flds 4644 = sep [text "The constructor of a newtype must have exactly one field", 4645 nest 2 $ text "but" <+> quotes (ppr con_name) <+> text "has" <+> speakN n_flds] 4646 4647badSigTyDecl :: Name -> SDoc 4648badSigTyDecl tc_name 4649 = vcat [ text "Illegal kind signature" <+> 4650 quotes (ppr tc_name) 4651 , nest 2 (parens $ text "Use KindSignatures to allow kind signatures") ] 4652 4653emptyConDeclsErr :: Name -> SDoc 4654emptyConDeclsErr tycon 4655 = sep [quotes (ppr tycon) <+> text "has no constructors", 4656 nest 2 $ text "(EmptyDataDecls permits this)"] 4657 4658wrongKindOfFamily :: TyCon -> SDoc 4659wrongKindOfFamily family 4660 = text "Wrong category of family instance; declaration was for a" 4661 <+> kindOfFamily 4662 where 4663 kindOfFamily | isTypeFamilyTyCon family = text "type family" 4664 | isDataFamilyTyCon family = text "data family" 4665 | otherwise = pprPanic "wrongKindOfFamily" (ppr family) 4666 4667-- | Produce an error for oversaturated type family equations with too many 4668-- required arguments. 4669-- See Note [Oversaturated type family equations] in TcValidity. 4670wrongNumberOfParmsErr :: Arity -> SDoc 4671wrongNumberOfParmsErr max_args 4672 = text "Number of parameters must match family declaration; expected" 4673 <+> ppr max_args 4674 4675badRoleAnnot :: Name -> Role -> Role -> SDoc 4676badRoleAnnot var annot inferred 4677 = hang (text "Role mismatch on variable" <+> ppr var <> colon) 4678 2 (sep [ text "Annotation says", ppr annot 4679 , text "but role", ppr inferred 4680 , text "is required" ]) 4681 4682wrongNumberOfRoles :: [a] -> LRoleAnnotDecl GhcRn -> SDoc 4683wrongNumberOfRoles tyvars d@(L _ (RoleAnnotDecl _ _ annots)) 4684 = hang (text "Wrong number of roles listed in role annotation;" $$ 4685 text "Expected" <+> (ppr $ length tyvars) <> comma <+> 4686 text "got" <+> (ppr $ length annots) <> colon) 4687 2 (ppr d) 4688wrongNumberOfRoles _ (L _ (XRoleAnnotDecl nec)) = noExtCon nec 4689 4690 4691illegalRoleAnnotDecl :: LRoleAnnotDecl GhcRn -> TcM () 4692illegalRoleAnnotDecl (L loc (RoleAnnotDecl _ tycon _)) 4693 = setErrCtxt [] $ 4694 setSrcSpan loc $ 4695 addErrTc (text "Illegal role annotation for" <+> ppr tycon <> char ';' $$ 4696 text "they are allowed only for datatypes and classes.") 4697illegalRoleAnnotDecl (L _ (XRoleAnnotDecl nec)) = noExtCon nec 4698 4699needXRoleAnnotations :: TyCon -> SDoc 4700needXRoleAnnotations tc 4701 = text "Illegal role annotation for" <+> ppr tc <> char ';' $$ 4702 text "did you intend to use RoleAnnotations?" 4703 4704incoherentRoles :: SDoc 4705incoherentRoles = (text "Roles other than" <+> quotes (text "nominal") <+> 4706 text "for class parameters can lead to incoherence.") $$ 4707 (text "Use IncoherentInstances to allow this; bad role found") 4708 4709addTyConCtxt :: TyCon -> TcM a -> TcM a 4710addTyConCtxt tc = addTyConFlavCtxt name flav 4711 where 4712 name = getName tc 4713 flav = tyConFlavour tc 4714 4715addRoleAnnotCtxt :: Name -> TcM a -> TcM a 4716addRoleAnnotCtxt name 4717 = addErrCtxt $ 4718 text "while checking a role annotation for" <+> quotes (ppr name) 4719