1{- 2(c) The University of Glasgow 2006 3(c) The GRASP/AQUA Project, Glasgow University, 1992-1998 4-} 5 6{-# LANGUAGE CPP, TupleSections, ViewPatterns #-} 7 8module TcValidity ( 9 Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType, 10 checkValidTheta, 11 checkValidInstance, checkValidInstHead, validDerivPred, 12 checkTySynRhs, 13 checkValidCoAxiom, checkValidCoAxBranch, 14 checkValidTyFamEqn, checkConsistentFamInst, 15 badATErr, arityErr, 16 checkTyConTelescope, 17 allDistinctTyVars 18 ) where 19 20#include "HsVersions.h" 21 22import GhcPrelude 23 24import Maybes 25 26-- friends: 27import TcUnify ( tcSubType_NC ) 28import TcSimplify ( simplifyAmbiguityCheck ) 29import ClsInst ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..), AssocInstInfo(..) ) 30import TyCoFVs 31import TyCoRep 32import TyCoPpr 33import TcType hiding ( sizeType, sizeTypes ) 34import TysWiredIn ( heqTyConName, eqTyConName, coercibleTyConName ) 35import PrelNames 36import Type 37import Unify ( tcMatchTyX_BM, BindFlag(..) ) 38import Coercion 39import CoAxiom 40import Class 41import TyCon 42import Predicate 43import TcOrigin 44 45-- others: 46import IfaceType( pprIfaceType, pprIfaceTypeApp ) 47import ToIface ( toIfaceTyCon, toIfaceTcArgs, toIfaceType ) 48import GHC.Hs -- HsType 49import TcRnMonad -- TcType, amongst others 50import TcEnv ( tcInitTidyEnv, tcInitOpenTidyEnv ) 51import FunDeps 52import FamInstEnv ( isDominatedBy, injectiveBranches, 53 InjectivityCheckResult(..) ) 54import FamInst 55import Name 56import VarEnv 57import VarSet 58import Var ( VarBndr(..), mkTyVar ) 59import FV 60import ErrUtils 61import DynFlags 62import Util 63import ListSetOps 64import SrcLoc 65import Outputable 66import Unique ( mkAlphaTyVarUnique ) 67import Bag ( emptyBag ) 68import qualified GHC.LanguageExtensions as LangExt 69 70import Control.Monad 71import Data.Foldable 72import Data.List ( (\\), nub ) 73import qualified Data.List.NonEmpty as NE 74 75{- 76************************************************************************ 77* * 78 Checking for ambiguity 79* * 80************************************************************************ 81 82Note [The ambiguity check for type signatures] 83~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 84checkAmbiguity is a check on *user-supplied type signatures*. It is 85*purely* there to report functions that cannot possibly be called. So for 86example we want to reject: 87 f :: C a => Int 88The idea is there can be no legal calls to 'f' because every call will 89give rise to an ambiguous constraint. We could soundly omit the 90ambiguity check on type signatures entirely, at the expense of 91delaying ambiguity errors to call sites. Indeed, the flag 92-XAllowAmbiguousTypes switches off the ambiguity check. 93 94What about things like this: 95 class D a b | a -> b where .. 96 h :: D Int b => Int 97The Int may well fix 'b' at the call site, so that signature should 98not be rejected. Moreover, using *visible* fundeps is too 99conservative. Consider 100 class X a b where ... 101 class D a b | a -> b where ... 102 instance D a b => X [a] b where... 103 h :: X a b => a -> a 104Here h's type looks ambiguous in 'b', but here's a legal call: 105 ...(h [True])... 106That gives rise to a (X [Bool] beta) constraint, and using the 107instance means we need (D Bool beta) and that fixes 'beta' via D's 108fundep! 109 110Behind all these special cases there is a simple guiding principle. 111Consider 112 113 f :: <type> 114 f = ...blah... 115 116 g :: <type> 117 g = f 118 119You would think that the definition of g would surely typecheck! 120After all f has exactly the same type, and g=f. But in fact f's type 121is instantiated and the instantiated constraints are solved against 122the originals, so in the case an ambiguous type it won't work. 123Consider our earlier example f :: C a => Int. Then in g's definition, 124we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a), 125and fail. 126 127So in fact we use this as our *definition* of ambiguity. We use a 128very similar test for *inferred* types, to ensure that they are 129unambiguous. See Note [Impedance matching] in TcBinds. 130 131This test is very conveniently implemented by calling 132 tcSubType <type> <type> 133This neatly takes account of the functional dependecy stuff above, 134and implicit parameter (see Note [Implicit parameters and ambiguity]). 135And this is what checkAmbiguity does. 136 137What about this, though? 138 g :: C [a] => Int 139Is every call to 'g' ambiguous? After all, we might have 140 instance C [a] where ... 141at the call site. So maybe that type is ok! Indeed even f's 142quintessentially ambiguous type might, just possibly be callable: 143with -XFlexibleInstances we could have 144 instance C a where ... 145and now a call could be legal after all! Well, we'll reject this 146unless the instance is available *here*. 147 148Note [When to call checkAmbiguity] 149~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 150We call checkAmbiguity 151 (a) on user-specified type signatures 152 (b) in checkValidType 153 154Conncerning (b), you might wonder about nested foralls. What about 155 f :: forall b. (forall a. Eq a => b) -> b 156The nested forall is ambiguous. Originally we called checkAmbiguity 157in the forall case of check_type, but that had two bad consequences: 158 * We got two error messages about (Eq b) in a nested forall like this: 159 g :: forall a. Eq a => forall b. Eq b => a -> a 160 * If we try to check for ambiguity of a nested forall like 161 (forall a. Eq a => b), the implication constraint doesn't bind 162 all the skolems, which results in "No skolem info" in error 163 messages (see #10432). 164 165To avoid this, we call checkAmbiguity once, at the top, in checkValidType. 166(I'm still a bit worried about unbound skolems when the type mentions 167in-scope type variables.) 168 169In fact, because of the co/contra-variance implemented in tcSubType, 170this *does* catch function f above. too. 171 172Concerning (a) the ambiguity check is only used for *user* types, not 173for types coming from inteface files. The latter can legitimately 174have ambiguous types. Example 175 176 class S a where s :: a -> (Int,Int) 177 instance S Char where s _ = (1,1) 178 f:: S a => [a] -> Int -> (Int,Int) 179 f (_::[a]) x = (a*x,b) 180 where (a,b) = s (undefined::a) 181 182Here the worker for f gets the type 183 fw :: forall a. S a => Int -> (# Int, Int #) 184 185 186Note [Implicit parameters and ambiguity] 187~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 188Only a *class* predicate can give rise to ambiguity 189An *implicit parameter* cannot. For example: 190 foo :: (?x :: [a]) => Int 191 foo = length ?x 192is fine. The call site will supply a particular 'x' 193 194Furthermore, the type variables fixed by an implicit parameter 195propagate to the others. E.g. 196 foo :: (Show a, ?x::[a]) => Int 197 foo = show (?x++?x) 198The type of foo looks ambiguous. But it isn't, because at a call site 199we might have 200 let ?x = 5::Int in foo 201and all is well. In effect, implicit parameters are, well, parameters, 202so we can take their type variables into account as part of the 203"tau-tvs" stuff. This is done in the function 'FunDeps.grow'. 204-} 205 206checkAmbiguity :: UserTypeCtxt -> Type -> TcM () 207checkAmbiguity ctxt ty 208 | wantAmbiguityCheck ctxt 209 = do { traceTc "Ambiguity check for" (ppr ty) 210 -- Solve the constraints eagerly because an ambiguous type 211 -- can cause a cascade of further errors. Since the free 212 -- tyvars are skolemised, we can safely use tcSimplifyTop 213 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes 214 ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $ 215 captureConstraints $ 216 tcSubType_NC ctxt ty ty 217 ; simplifyAmbiguityCheck ty wanted 218 219 ; traceTc "Done ambiguity check for" (ppr ty) } 220 221 | otherwise 222 = return () 223 where 224 mk_msg allow_ambiguous 225 = vcat [ text "In the ambiguity check for" <+> what 226 , ppUnless allow_ambiguous ambig_msg ] 227 ambig_msg = text "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes" 228 what | Just n <- isSigMaybe ctxt = quotes (ppr n) 229 | otherwise = pprUserTypeCtxt ctxt 230 231wantAmbiguityCheck :: UserTypeCtxt -> Bool 232wantAmbiguityCheck ctxt 233 = case ctxt of -- See Note [When we don't check for ambiguity] 234 GhciCtxt {} -> False 235 TySynCtxt {} -> False 236 TypeAppCtxt -> False 237 StandaloneKindSigCtxt{} -> False 238 _ -> True 239 240checkUserTypeError :: Type -> TcM () 241-- Check to see if the type signature mentions "TypeError blah" 242-- anywhere in it, and fail if so. 243-- 244-- Very unsatisfactorily (#11144) we need to tidy the type 245-- because it may have come from an /inferred/ signature, not a 246-- user-supplied one. This is really only a half-baked fix; 247-- the other errors in checkValidType don't do tidying, and so 248-- may give bad error messages when given an inferred type. 249checkUserTypeError = check 250 where 251 check ty 252 | Just msg <- userTypeError_maybe ty = fail_with msg 253 | Just (_,ts) <- splitTyConApp_maybe ty = mapM_ check ts 254 | Just (t1,t2) <- splitAppTy_maybe ty = check t1 >> check t2 255 | Just (_,t1) <- splitForAllTy_maybe ty = check t1 256 | otherwise = return () 257 258 fail_with msg = do { env0 <- tcInitTidyEnv 259 ; let (env1, tidy_msg) = tidyOpenType env0 msg 260 ; failWithTcM (env1, pprUserTypeErrorTy tidy_msg) } 261 262 263{- Note [When we don't check for ambiguity] 264~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 265In a few places we do not want to check a user-specified type for ambiguity 266 267* GhciCtxt: Allow ambiguous types in GHCi's :kind command 268 E.g. type family T a :: * -- T :: forall k. k -> * 269 Then :k T should work in GHCi, not complain that 270 (T k) is ambiguous! 271 272* TySynCtxt: type T a b = C a b => blah 273 It may be that when we /use/ T, we'll give an 'a' or 'b' that somehow 274 cure the ambiguity. So we defer the ambiguity check to the use site. 275 276 There is also an implementation reason (#11608). In the RHS of 277 a type synonym we don't (currently) instantiate 'a' and 'b' with 278 TcTyVars before calling checkValidType, so we get asertion failures 279 from doing an ambiguity check on a type with TyVars in it. Fixing this 280 would not be hard, but let's wait till there's a reason. 281 282* TypeAppCtxt: visible type application 283 f @ty 284 No need to check ty for ambiguity 285 286* StandaloneKindSigCtxt: type T :: ksig 287 Kinds need a different ambiguity check than types, and the currently 288 implemented check is only good for types. See #14419, in particular 289 https://gitlab.haskell.org/ghc/ghc/issues/14419#note_160844 290 291************************************************************************ 292* * 293 Checking validity of a user-defined type 294* * 295************************************************************************ 296 297When dealing with a user-written type, we first translate it from an HsType 298to a Type, performing kind checking, and then check various things that should 299be true about it. We don't want to perform these checks at the same time 300as the initial translation because (a) they are unnecessary for interface-file 301types and (b) when checking a mutually recursive group of type and class decls, 302we can't "look" at the tycons/classes yet. Also, the checks are rather 303diverse, and used to really mess up the other code. 304 305One thing we check for is 'rank'. 306 307 Rank 0: monotypes (no foralls) 308 Rank 1: foralls at the front only, Rank 0 inside 309 Rank 2: foralls at the front, Rank 1 on left of fn arrow, 310 311 basic ::= tyvar | T basic ... basic 312 313 r2 ::= forall tvs. cxt => r2a 314 r2a ::= r1 -> r2a | basic 315 r1 ::= forall tvs. cxt => r0 316 r0 ::= r0 -> r0 | basic 317 318Another thing is to check that type synonyms are saturated. 319This might not necessarily show up in kind checking. 320 type A i = i 321 data T k = MkT (k Int) 322 f :: T A -- BAD! 323-} 324 325checkValidType :: UserTypeCtxt -> Type -> TcM () 326-- Checks that a user-written type is valid for the given context 327-- Assumes argument is fully zonked 328-- Not used for instance decls; checkValidInstance instead 329checkValidType ctxt ty 330 = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty)) 331 ; rankn_flag <- xoptM LangExt.RankNTypes 332 ; impred_flag <- xoptM LangExt.ImpredicativeTypes 333 ; let gen_rank :: Rank -> Rank 334 gen_rank r | rankn_flag = ArbitraryRank 335 | otherwise = r 336 337 rank1 = gen_rank r1 338 rank0 = gen_rank r0 339 340 r0 = rankZeroMonoType 341 r1 = LimitedRank True r0 342 343 rank 344 = case ctxt of 345 DefaultDeclCtxt-> MustBeMonoType 346 ResSigCtxt -> MustBeMonoType 347 PatSigCtxt -> rank0 348 RuleSigCtxt _ -> rank1 349 TySynCtxt _ -> rank0 350 351 ExprSigCtxt -> rank1 352 KindSigCtxt -> rank1 353 StandaloneKindSigCtxt{} -> rank1 354 TypeAppCtxt | impred_flag -> ArbitraryRank 355 | otherwise -> tyConArgMonoType 356 -- Normally, ImpredicativeTypes is handled in check_arg_type, 357 -- but visible type applications don't go through there. 358 -- So we do this check here. 359 360 FunSigCtxt {} -> rank1 361 InfSigCtxt {} -> rank1 -- Inferred types should obey the 362 -- same rules as declared ones 363 364 ConArgCtxt _ -> rank1 -- We are given the type of the entire 365 -- constructor, hence rank 1 366 PatSynCtxt _ -> rank1 367 368 ForSigCtxt _ -> rank1 369 SpecInstCtxt -> rank1 370 ThBrackCtxt -> rank1 371 GhciCtxt {} -> ArbitraryRank 372 373 TyVarBndrKindCtxt _ -> rank0 374 DataKindCtxt _ -> rank1 375 TySynKindCtxt _ -> rank1 376 TyFamResKindCtxt _ -> rank1 377 378 _ -> panic "checkValidType" 379 -- Can't happen; not used for *user* sigs 380 381 ; env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty) 382 ; expand <- initialExpandMode 383 ; let ve = ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt 384 , ve_rank = rank, ve_expand = expand } 385 386 -- Check the internal validity of the type itself 387 -- Fail if bad things happen, else we misleading 388 -- (and more complicated) errors in checkAmbiguity 389 ; checkNoErrs $ 390 do { check_type ve ty 391 ; checkUserTypeError ty 392 ; traceTc "done ct" (ppr ty) } 393 394 -- Check for ambiguous types. See Note [When to call checkAmbiguity] 395 -- NB: this will happen even for monotypes, but that should be cheap; 396 -- and there may be nested foralls for the subtype test to examine 397 ; checkAmbiguity ctxt ty 398 399 ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty)) } 400 401checkValidMonoType :: Type -> TcM () 402-- Assumes argument is fully zonked 403checkValidMonoType ty 404 = do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypeList ty) 405 ; expand <- initialExpandMode 406 ; let ve = ValidityEnv{ ve_tidy_env = env, ve_ctxt = SigmaCtxt 407 , ve_rank = MustBeMonoType, ve_expand = expand } 408 ; check_type ve ty } 409 410checkTySynRhs :: UserTypeCtxt -> TcType -> TcM () 411checkTySynRhs ctxt ty 412 | tcReturnsConstraintKind actual_kind 413 = do { ck <- xoptM LangExt.ConstraintKinds 414 ; if ck 415 then when (tcIsConstraintKind actual_kind) 416 (do { dflags <- getDynFlags 417 ; expand <- initialExpandMode 418 ; check_pred_ty emptyTidyEnv dflags ctxt expand ty }) 419 else addErrTcM (constraintSynErr emptyTidyEnv actual_kind) } 420 421 | otherwise 422 = return () 423 where 424 actual_kind = tcTypeKind ty 425 426{- 427Note [Higher rank types] 428~~~~~~~~~~~~~~~~~~~~~~~~ 429Technically 430 Int -> forall a. a->a 431is still a rank-1 type, but it's not Haskell 98 (#5957). So the 432validity checker allow a forall after an arrow only if we allow it 433before -- that is, with Rank2Types or RankNTypes 434-} 435 436data Rank = ArbitraryRank -- Any rank ok 437 438 | LimitedRank -- Note [Higher rank types] 439 Bool -- Forall ok at top 440 Rank -- Use for function arguments 441 442 | MonoType SDoc -- Monotype, with a suggestion of how it could be a polytype 443 444 | MustBeMonoType -- Monotype regardless of flags 445 446instance Outputable Rank where 447 ppr ArbitraryRank = text "ArbitraryRank" 448 ppr (LimitedRank top_forall_ok r) 449 = text "LimitedRank" <+> ppr top_forall_ok 450 <+> parens (ppr r) 451 ppr (MonoType msg) = text "MonoType" <+> parens msg 452 ppr MustBeMonoType = text "MustBeMonoType" 453 454rankZeroMonoType, tyConArgMonoType, synArgMonoType, constraintMonoType :: Rank 455rankZeroMonoType = MonoType (text "Perhaps you intended to use RankNTypes") 456tyConArgMonoType = MonoType (text "GHC doesn't yet support impredicative polymorphism") 457synArgMonoType = MonoType (text "Perhaps you intended to use LiberalTypeSynonyms") 458constraintMonoType = MonoType (vcat [ text "A constraint must be a monotype" 459 , text "Perhaps you intended to use QuantifiedConstraints" ]) 460 461funArgResRank :: Rank -> (Rank, Rank) -- Function argument and result 462funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank) 463funArgResRank other_rank = (other_rank, other_rank) 464 465forAllAllowed :: Rank -> Bool 466forAllAllowed ArbitraryRank = True 467forAllAllowed (LimitedRank forall_ok _) = forall_ok 468forAllAllowed _ = False 469 470allConstraintsAllowed :: UserTypeCtxt -> Bool 471-- We don't allow arbitrary constraints in kinds 472allConstraintsAllowed (TyVarBndrKindCtxt {}) = False 473allConstraintsAllowed (DataKindCtxt {}) = False 474allConstraintsAllowed (TySynKindCtxt {}) = False 475allConstraintsAllowed (TyFamResKindCtxt {}) = False 476allConstraintsAllowed (StandaloneKindSigCtxt {}) = False 477allConstraintsAllowed _ = True 478 479-- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the 480-- context for the type of a term, where visible, dependent quantification is 481-- currently disallowed. 482-- 483-- An example of something that is unambiguously the type of a term is the 484-- @forall a -> a -> a@ in @foo :: forall a -> a -> a@. On the other hand, the 485-- same type in @type family Foo :: forall a -> a -> a@ is unambiguously the 486-- kind of a type, not the type of a term, so it is permitted. 487-- 488-- For more examples, see 489-- @testsuite/tests/dependent/should_compile/T16326_Compile*.hs@ (for places 490-- where VDQ is permitted) and 491-- @testsuite/tests/dependent/should_fail/T16326_Fail*.hs@ (for places where 492-- VDQ is disallowed). 493vdqAllowed :: UserTypeCtxt -> Bool 494-- Currently allowed in the kinds of types... 495vdqAllowed (KindSigCtxt {}) = True 496vdqAllowed (StandaloneKindSigCtxt {}) = True 497vdqAllowed (TySynCtxt {}) = True 498vdqAllowed (ThBrackCtxt {}) = True 499vdqAllowed (GhciCtxt {}) = True 500vdqAllowed (TyVarBndrKindCtxt {}) = True 501vdqAllowed (DataKindCtxt {}) = True 502vdqAllowed (TySynKindCtxt {}) = True 503vdqAllowed (TyFamResKindCtxt {}) = True 504-- ...but not in the types of terms. 505vdqAllowed (ConArgCtxt {}) = False 506 -- We could envision allowing VDQ in data constructor types so long as the 507 -- constructor is only ever used at the type level, but for now, GHC adopts 508 -- the stance that VDQ is never allowed in data constructor types. 509vdqAllowed (FunSigCtxt {}) = False 510vdqAllowed (InfSigCtxt {}) = False 511vdqAllowed (ExprSigCtxt {}) = False 512vdqAllowed (TypeAppCtxt {}) = False 513vdqAllowed (PatSynCtxt {}) = False 514vdqAllowed (PatSigCtxt {}) = False 515vdqAllowed (RuleSigCtxt {}) = False 516vdqAllowed (ResSigCtxt {}) = False 517vdqAllowed (ForSigCtxt {}) = False 518vdqAllowed (DefaultDeclCtxt {}) = False 519-- We count class constraints as "types of terms". All of the cases below deal 520-- with class constraints. 521vdqAllowed (InstDeclCtxt {}) = False 522vdqAllowed (SpecInstCtxt {}) = False 523vdqAllowed (GenSigCtxt {}) = False 524vdqAllowed (ClassSCCtxt {}) = False 525vdqAllowed (SigmaCtxt {}) = False 526vdqAllowed (DataTyCtxt {}) = False 527vdqAllowed (DerivClauseCtxt {}) = False 528 529{- 530Note [Correctness and performance of type synonym validity checking] 531~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 532Consider the type A arg1 arg2, where A is a type synonym. How should we check 533this type for validity? We have three distinct choices, corresponding to the 534three constructors of ExpandMode: 535 5361. Expand the application of A, and check the resulting type (`Expand`). 5372. Don't expand the application of A. Only check the arguments (`NoExpand`). 5383. Check the arguments *and* check the expanded type (`Both`). 539 540It's tempting to think that we could always just pick choice (3), but this 541results in serious performance issues when checking a type like in the 542signature for `f` below: 543 544 type S = ... 545 f :: S (S (S (S (S (S ....(S Int)...)))) 546 547When checking the type of `f`, we'll check the outer `S` application with and 548without expansion, and in *each* of those checks, we'll check the next `S` 549application with and without expansion... the result is exponential blowup! So 550clearly we don't want to use `Both` 100% of the time. 551 552On the other hand, neither is it correct to use exclusively `Expand` or 553exclusively `NoExpand` 100% of the time: 554 555* If one always expands, then one can miss erroneous programs like the one in 556 the `tcfail129` test case: 557 558 type Foo a = String -> Maybe a 559 type Bar m = m Int 560 blah = undefined :: Bar Foo 561 562 If we expand `Bar Foo` immediately, we'll miss the fact that the `Foo` type 563 synonyms is unsaturated. 564* If one never expands and only checks the arguments, then one can miss 565 erroneous programs like the one in #16059: 566 567 type Foo b = Eq b => b 568 f :: forall b (a :: Foo b). Int 569 570 The kind of `a` contains a constraint, which is illegal, but this will only 571 be caught if `Foo b` is expanded. 572 573Therefore, it's impossible to have these validity checks be simultaneously 574correct and performant if one sticks exclusively to a single `ExpandMode`. In 575that case, the solution is to vary the `ExpandMode`s! In more detail: 576 5771. When we start validity checking, we start with `Expand` if 578 LiberalTypeSynonyms is enabled (see Note [Liberal type synonyms] for why we 579 do this), and we start with `Both` otherwise. The `initialExpandMode` 580 function is responsible for this. 5812. When expanding an application of a type synonym (in `check_syn_tc_app`), we 582 determine which things to check based on the current `ExpandMode` argument. 583 Importantly, if the current mode is `Both`, then we check the arguments in 584 `NoExpand` mode and check the expanded type in `Both` mode. 585 586 Switching to `NoExpand` when checking the arguments is vital to avoid 587 exponential blowup. One consequence of this choice is that if you have 588 the following type synonym in one module (with RankNTypes enabled): 589 590 {-# LANGUAGE RankNTypes #-} 591 module A where 592 type A = forall a. a 593 594 And you define the following in a separate module *without* RankNTypes 595 enabled: 596 597 module B where 598 599 import A 600 601 type Const a b = a 602 f :: Const Int A -> Int 603 604 Then `f` will be accepted, even though `A` (which is technically a rank-n 605 type) appears in its type. We view this as an acceptable compromise, since 606 `A` never appears in the type of `f` post-expansion. If `A` _did_ appear in 607 a type post-expansion, such as in the following variant: 608 609 g :: Const A A -> Int 610 611 Then that would be rejected unless RankNTypes were enabled. 612-} 613 614-- | When validity-checking an application of a type synonym, should we 615-- check the arguments, check the expanded type, or both? 616-- See Note [Correctness and performance of type synonym validity checking] 617data ExpandMode 618 = Expand -- ^ Only check the expanded type. 619 | NoExpand -- ^ Only check the arguments. 620 | Both -- ^ Check both the arguments and the expanded type. 621 622instance Outputable ExpandMode where 623 ppr e = text $ case e of 624 Expand -> "Expand" 625 NoExpand -> "NoExpand" 626 Both -> "Both" 627 628-- | If @LiberalTypeSynonyms@ is enabled, we start in 'Expand' mode for the 629-- reasons explained in @Note [Liberal type synonyms]@. Otherwise, we start 630-- in 'Both' mode. 631initialExpandMode :: TcM ExpandMode 632initialExpandMode = do 633 liberal_flag <- xoptM LangExt.LiberalTypeSynonyms 634 pure $ if liberal_flag then Expand else Both 635 636-- | Information about a type being validity-checked. 637data ValidityEnv = ValidityEnv 638 { ve_tidy_env :: TidyEnv 639 , ve_ctxt :: UserTypeCtxt 640 , ve_rank :: Rank 641 , ve_expand :: ExpandMode } 642 643instance Outputable ValidityEnv where 644 ppr (ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt 645 , ve_rank = rank, ve_expand = expand }) = 646 hang (text "ValidityEnv") 647 2 (vcat [ text "ve_tidy_env" <+> ppr env 648 , text "ve_ctxt" <+> pprUserTypeCtxt ctxt 649 , text "ve_rank" <+> ppr rank 650 , text "ve_expand" <+> ppr expand ]) 651 652---------------------------------------- 653check_type :: ValidityEnv -> Type -> TcM () 654-- The args say what the *type context* requires, independent 655-- of *flag* settings. You test the flag settings at usage sites. 656-- 657-- Rank is allowed rank for function args 658-- Rank 0 means no for-alls anywhere 659 660check_type _ (TyVarTy _) = return () 661 662check_type ve (AppTy ty1 ty2) 663 = do { check_type ve ty1 664 ; check_arg_type False ve ty2 } 665 666check_type ve ty@(TyConApp tc tys) 667 | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc 668 = check_syn_tc_app ve ty tc tys 669 | isUnboxedTupleTyCon tc = check_ubx_tuple ve ty tys 670 | otherwise = mapM_ (check_arg_type False ve) tys 671 672check_type _ (LitTy {}) = return () 673 674check_type ve (CastTy ty _) = check_type ve ty 675 676-- Check for rank-n types, such as (forall x. x -> x) or (Show x => x). 677-- 678-- Critically, this case must come *after* the case for TyConApp. 679-- See Note [Liberal type synonyms]. 680check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt 681 , ve_rank = rank, ve_expand = expand }) ty 682 | not (null tvbs && null theta) 683 = do { traceTc "check_type" (ppr ty $$ ppr rank) 684 ; checkTcM (forAllAllowed rank) (forAllTyErr env rank ty) 685 -- Reject e.g. (Maybe (?x::Int => Int)), 686 -- with a decent error message 687 688 ; checkConstraintsOK ve theta ty 689 -- Reject forall (a :: Eq b => b). blah 690 -- In a kind signature we don't allow constraints 691 692 ; checkTcM (all (isInvisibleArgFlag . binderArgFlag) tvbs 693 || vdqAllowed ctxt) 694 (illegalVDQTyErr env ty) 695 -- Reject visible, dependent quantification in the type of a 696 -- term (e.g., `f :: forall a -> a -> Maybe a`) 697 698 ; check_valid_theta env' SigmaCtxt expand theta 699 -- Allow type T = ?x::Int => Int -> Int 700 -- but not type T = ?x::Int 701 702 ; check_type (ve{ve_tidy_env = env'}) tau 703 -- Allow foralls to right of arrow 704 705 ; checkEscapingKind env' tvbs' theta tau } 706 where 707 (tvbs, phi) = tcSplitForAllVarBndrs ty 708 (theta, tau) = tcSplitPhiTy phi 709 (env', tvbs') = tidyTyCoVarBinders env tvbs 710 711check_type (ve@ValidityEnv{ve_rank = rank}) (FunTy _ arg_ty res_ty) 712 = do { check_type (ve{ve_rank = arg_rank}) arg_ty 713 ; check_type (ve{ve_rank = res_rank}) res_ty } 714 where 715 (arg_rank, res_rank) = funArgResRank rank 716 717check_type _ ty = pprPanic "check_type" (ppr ty) 718 719---------------------------------------- 720check_syn_tc_app :: ValidityEnv 721 -> KindOrType -> TyCon -> [KindOrType] -> TcM () 722-- Used for type synonyms and type synonym families, 723-- which must be saturated, 724-- but not data families, which need not be saturated 725check_syn_tc_app (ve@ValidityEnv{ ve_ctxt = ctxt, ve_expand = expand }) 726 ty tc tys 727 | tys `lengthAtLeast` tc_arity -- Saturated 728 -- Check that the synonym has enough args 729 -- This applies equally to open and closed synonyms 730 -- It's OK to have an *over-applied* type synonym 731 -- data Tree a b = ... 732 -- type Foo a = Tree [a] 733 -- f :: Foo a b -> ... 734 = case expand of 735 _ | isTypeFamilyTyCon tc 736 -> check_args_only expand 737 -- See Note [Correctness and performance of type synonym validity 738 -- checking] 739 Expand -> check_expansion_only expand 740 NoExpand -> check_args_only expand 741 Both -> check_args_only NoExpand *> check_expansion_only Both 742 743 | GhciCtxt True <- ctxt -- Accept outermost under-saturated type synonym or 744 -- type family constructors in GHCi :kind commands. 745 -- See Note [Unsaturated type synonyms in GHCi] 746 = check_args_only expand 747 748 | otherwise 749 = failWithTc (tyConArityErr tc tys) 750 where 751 tc_arity = tyConArity tc 752 753 check_arg :: ExpandMode -> KindOrType -> TcM () 754 check_arg expand = 755 check_arg_type (isTypeSynonymTyCon tc) (ve{ve_expand = expand}) 756 757 check_args_only, check_expansion_only :: ExpandMode -> TcM () 758 check_args_only expand = mapM_ (check_arg expand) tys 759 760 check_expansion_only expand 761 = ASSERT2( isTypeSynonymTyCon tc, ppr tc ) 762 case tcView ty of 763 Just ty' -> let err_ctxt = text "In the expansion of type synonym" 764 <+> quotes (ppr tc) 765 in addErrCtxt err_ctxt $ 766 check_type (ve{ve_expand = expand}) ty' 767 Nothing -> pprPanic "check_syn_tc_app" (ppr ty) 768 769{- 770Note [Unsaturated type synonyms in GHCi] 771~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 772Generally speaking, GHC disallows unsaturated uses of type synonyms or type 773families. For instance, if one defines `type Const a b = a`, then GHC will not 774permit using `Const` unless it is applied to (at least) two arguments. There is 775an exception to this rule, however: GHCi's :kind command. For instance, it 776is quite common to look up the kind of a type constructor like so: 777 778 λ> :kind Const 779 Const :: j -> k -> j 780 λ> :kind Const Int 781 Const Int :: k -> Type 782 783Strictly speaking, the two uses of `Const` above are unsaturated, but this 784is an extremely benign (and useful) example of unsaturation, so we allow it 785here as a special case. 786 787That being said, we do not allow unsaturation carte blanche in GHCi. Otherwise, 788this GHCi interaction would be possible: 789 790 λ> newtype Fix f = MkFix (f (Fix f)) 791 λ> type Id a = a 792 λ> :kind Fix Id 793 Fix Id :: Type 794 795This is rather dodgy, so we move to disallow this. We only permit unsaturated 796synonyms in GHCi if they are *top-level*—that is, if the synonym is the 797outermost type being applied. This allows `Const` and `Const Int` in the 798first example, but not `Fix Id` in the second example, as `Id` is not the 799outermost type being applied (`Fix` is). 800 801We track this outermost property in the GhciCtxt constructor of UserTypeCtxt. 802A field of True in GhciCtxt indicates that we're in an outermost position. Any 803time we invoke `check_arg` to check the validity of an argument, we switch the 804field to False. 805-} 806 807---------------------------------------- 808check_ubx_tuple :: ValidityEnv -> KindOrType -> [KindOrType] -> TcM () 809check_ubx_tuple (ve@ValidityEnv{ve_tidy_env = env}) ty tys 810 = do { ub_tuples_allowed <- xoptM LangExt.UnboxedTuples 811 ; checkTcM ub_tuples_allowed (ubxArgTyErr env ty) 812 813 ; impred <- xoptM LangExt.ImpredicativeTypes 814 ; let rank' = if impred then ArbitraryRank else tyConArgMonoType 815 -- c.f. check_arg_type 816 -- However, args are allowed to be unlifted, or 817 -- more unboxed tuples, so can't use check_arg_ty 818 ; mapM_ (check_type (ve{ve_rank = rank'})) tys } 819 820---------------------------------------- 821check_arg_type 822 :: Bool -- ^ Is this the argument to a type synonym? 823 -> ValidityEnv -> KindOrType -> TcM () 824-- The sort of type that can instantiate a type variable, 825-- or be the argument of a type constructor. 826-- Not an unboxed tuple, but now *can* be a forall (since impredicativity) 827-- Other unboxed types are very occasionally allowed as type 828-- arguments depending on the kind of the type constructor 829-- 830-- For example, we want to reject things like: 831-- 832-- instance Ord a => Ord (forall s. T s a) 833-- and 834-- g :: T s (forall b.b) 835-- 836-- NB: unboxed tuples can have polymorphic or unboxed args. 837-- This happens in the workers for functions returning 838-- product types with polymorphic components. 839-- But not in user code. 840-- Anyway, they are dealt with by a special case in check_tau_type 841 842check_arg_type _ _ (CoercionTy {}) = return () 843 844check_arg_type type_syn (ve@ValidityEnv{ve_ctxt = ctxt, ve_rank = rank}) ty 845 = do { impred <- xoptM LangExt.ImpredicativeTypes 846 ; let rank' = case rank of -- Predictive => must be monotype 847 -- Rank-n arguments to type synonyms are OK, provided 848 -- that LiberalTypeSynonyms is enabled. 849 _ | type_syn -> synArgMonoType 850 MustBeMonoType -> MustBeMonoType -- Monotype, regardless 851 _other | impred -> ArbitraryRank 852 | otherwise -> tyConArgMonoType 853 -- Make sure that MustBeMonoType is propagated, 854 -- so that we don't suggest -XImpredicativeTypes in 855 -- (Ord (forall a.a)) => a -> a 856 -- and so that if it Must be a monotype, we check that it is! 857 ctxt' :: UserTypeCtxt 858 ctxt' 859 | GhciCtxt _ <- ctxt = GhciCtxt False 860 -- When checking an argument, set the field of GhciCtxt to 861 -- False to indicate that we are no longer in an outermost 862 -- position (and thus unsaturated synonyms are no longer 863 -- allowed). 864 -- See Note [Unsaturated type synonyms in GHCi] 865 | otherwise = ctxt 866 867 ; check_type (ve{ve_ctxt = ctxt', ve_rank = rank'}) ty } 868 869---------------------------------------- 870forAllTyErr :: TidyEnv -> Rank -> Type -> (TidyEnv, SDoc) 871forAllTyErr env rank ty 872 = ( env 873 , vcat [ hang herald 2 (ppr_tidy env ty) 874 , suggestion ] ) 875 where 876 (tvs, _theta, _tau) = tcSplitSigmaTy ty 877 herald | null tvs = text "Illegal qualified type:" 878 | otherwise = text "Illegal polymorphic type:" 879 suggestion = case rank of 880 LimitedRank {} -> text "Perhaps you intended to use RankNTypes" 881 MonoType d -> d 882 _ -> Outputable.empty -- Polytype is always illegal 883 884-- | Reject type variables that would escape their escape through a kind. 885-- See @Note [Type variables escaping through kinds]@. 886checkEscapingKind :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> TcM () 887checkEscapingKind env tvbs theta tau = 888 case occCheckExpand (binderVars tvbs) phi_kind of 889 -- Ensure that none of the tvs occur in the kind of the forall 890 -- /after/ expanding type synonyms. 891 -- See Note [Phantom type variables in kinds] in Type 892 Nothing -> failWithTcM $ forAllEscapeErr env tvbs theta tau tau_kind 893 Just _ -> pure () 894 where 895 tau_kind = tcTypeKind tau 896 phi_kind | null theta = tau_kind 897 | otherwise = liftedTypeKind 898 -- If there are any constraints, the kind is *. (#11405) 899 900forAllEscapeErr :: TidyEnv -> [TyVarBinder] -> ThetaType -> Type -> Kind 901 -> (TidyEnv, SDoc) 902forAllEscapeErr env tvbs theta tau tau_kind 903 = ( env 904 , vcat [ hang (text "Quantified type's kind mentions quantified type variable") 905 2 (text "type:" <+> quotes (ppr (mkSigmaTy tvbs theta tau))) 906 -- NB: Don't tidy this type since the tvbs were already tidied 907 -- previously, and re-tidying them will make the names of type 908 -- variables different from tau_kind. 909 , hang (text "where the body of the forall has this kind:") 910 2 (quotes (ppr_tidy env tau_kind)) ] ) 911 912{- 913Note [Type variables escaping through kinds] 914~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 915Consider: 916 917 type family T (r :: RuntimeRep) :: TYPE r 918 foo :: forall r. T r 919 920Something smells funny about the type of `foo`. If you spell out the kind 921explicitly, it becomes clearer from where the smell originates: 922 923 foo :: ((forall r. T r) :: TYPE r) 924 925The type variable `r` appears in the result kind, which escapes the scope of 926its binding site! This is not desirable, so we establish a validity check 927(`checkEscapingKind`) to catch any type variables that might escape through 928kinds in this way. 929-} 930 931ubxArgTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc) 932ubxArgTyErr env ty 933 = ( env, vcat [ sep [ text "Illegal unboxed tuple type as function argument:" 934 , ppr_tidy env ty ] 935 , text "Perhaps you intended to use UnboxedTuples" ] ) 936 937checkConstraintsOK :: ValidityEnv -> ThetaType -> Type -> TcM () 938checkConstraintsOK ve theta ty 939 | null theta = return () 940 | allConstraintsAllowed (ve_ctxt ve) = return () 941 | otherwise 942 = -- We are in a kind, where we allow only equality predicates 943 -- See Note [Constraints in kinds] in TyCoRep, and #16263 944 checkTcM (all isEqPred theta) $ 945 constraintTyErr (ve_tidy_env ve) ty 946 947constraintTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc) 948constraintTyErr env ty 949 = (env, text "Illegal constraint in a kind:" <+> ppr_tidy env ty) 950 951-- | Reject a use of visible, dependent quantification in the type of a term. 952illegalVDQTyErr :: TidyEnv -> Type -> (TidyEnv, SDoc) 953illegalVDQTyErr env ty = 954 (env, vcat 955 [ hang (text "Illegal visible, dependent quantification" <+> 956 text "in the type of a term:") 957 2 (ppr_tidy env ty) 958 , text "(GHC does not yet support this)" ] ) 959 960{- 961Note [Liberal type synonyms] 962~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 963If -XLiberalTypeSynonyms is on, expand closed type synonyms *before* 964doing validity checking. This allows us to instantiate a synonym defn 965with a for-all type, or with a partially-applied type synonym. 966 e.g. type T a b = a 967 type S m = m () 968 f :: S (T Int) 969Here, T is partially applied, so it's illegal in H98. But if you 970expand S first, then T we get just 971 f :: Int 972which is fine. 973 974IMPORTANT: suppose T is a type synonym. Then we must do validity 975checking on an appliation (T ty1 ty2) 976 977 *either* before expansion (i.e. check ty1, ty2) 978 *or* after expansion (i.e. expand T ty1 ty2, and then check) 979 BUT NOT BOTH 980 981If we do both, we get exponential behaviour!! 982 983 data TIACons1 i r c = c i ::: r c 984 type TIACons2 t x = TIACons1 t (TIACons1 t x) 985 type TIACons3 t x = TIACons2 t (TIACons1 t x) 986 type TIACons4 t x = TIACons2 t (TIACons2 t x) 987 type TIACons7 t x = TIACons4 t (TIACons3 t x) 988 989The order in which you do validity checking is also somewhat delicate. Consider 990the `check_type` function, which drives the validity checking for unsaturated 991uses of type synonyms. There is a special case for rank-n types, such as 992(forall x. x -> x) or (Show x => x), since those require at least one language 993extension to use. It used to be the case that this case came before every other 994case, but this can lead to bugs. Imagine you have this scenario (from #15954): 995 996 type A a = Int 997 type B (a :: Type -> Type) = forall x. x -> x 998 type C = B A 999 1000If the rank-n case came first, then in the process of checking for `forall`s 1001or contexts, we would expand away `B A` to `forall x. x -> x`. This is because 1002the functions that split apart `forall`s/contexts 1003(tcSplitForAllVarBndrs/tcSplitPhiTy) expand type synonyms! If `B A` is expanded 1004away to `forall x. x -> x` before the actually validity checks occur, we will 1005have completely obfuscated the fact that we had an unsaturated application of 1006the `A` type synonym. 1007 1008We have since learned from our mistakes and now put this rank-n case /after/ 1009the case for TyConApp, which ensures that an unsaturated `A` TyConApp will be 1010caught properly. But be careful! We can't make the rank-n case /last/ either, 1011as the FunTy case must came after the rank-n case. Otherwise, something like 1012(Eq a => Int) would be treated as a function type (FunTy), which just 1013wouldn't do. 1014 1015************************************************************************ 1016* * 1017\subsection{Checking a theta or source type} 1018* * 1019************************************************************************ 1020 1021Note [Implicit parameters in instance decls] 1022~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1023Implicit parameters _only_ allowed in type signatures; not in instance 1024decls, superclasses etc. The reason for not allowing implicit params in 1025instances is a bit subtle. If we allowed 1026 instance (?x::Int, Eq a) => Foo [a] where ... 1027then when we saw 1028 (e :: (?x::Int) => t) 1029it would be unclear how to discharge all the potential uses of the ?x 1030in e. For example, a constraint Foo [Int] might come out of e, and 1031applying the instance decl would show up two uses of ?x. #8912. 1032-} 1033 1034checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM () 1035-- Assumes argument is fully zonked 1036checkValidTheta ctxt theta 1037 = addErrCtxtM (checkThetaCtxt ctxt theta) $ 1038 do { env <- tcInitOpenTidyEnv (tyCoVarsOfTypesList theta) 1039 ; expand <- initialExpandMode 1040 ; check_valid_theta env ctxt expand theta } 1041 1042------------------------- 1043check_valid_theta :: TidyEnv -> UserTypeCtxt -> ExpandMode 1044 -> [PredType] -> TcM () 1045check_valid_theta _ _ _ [] 1046 = return () 1047check_valid_theta env ctxt expand theta 1048 = do { dflags <- getDynFlags 1049 ; warnTcM (Reason Opt_WarnDuplicateConstraints) 1050 (wopt Opt_WarnDuplicateConstraints dflags && notNull dups) 1051 (dupPredWarn env dups) 1052 ; traceTc "check_valid_theta" (ppr theta) 1053 ; mapM_ (check_pred_ty env dflags ctxt expand) theta } 1054 where 1055 (_,dups) = removeDups nonDetCmpType theta 1056 -- It's OK to use nonDetCmpType because dups only appears in the 1057 -- warning 1058 1059------------------------- 1060{- Note [Validity checking for constraints] 1061~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1062We look through constraint synonyms so that we can see the underlying 1063constraint(s). For example 1064 type Foo = ?x::Int 1065 instance Foo => C T 1066We should reject the instance because it has an implicit parameter in 1067the context. 1068 1069But we record, in 'under_syn', whether we have looked under a synonym 1070to avoid requiring language extensions at the use site. Main example 1071(#9838): 1072 1073 {-# LANGUAGE ConstraintKinds #-} 1074 module A where 1075 type EqShow a = (Eq a, Show a) 1076 1077 module B where 1078 import A 1079 foo :: EqShow a => a -> String 1080 1081We don't want to require ConstraintKinds in module B. 1082-} 1083 1084check_pred_ty :: TidyEnv -> DynFlags -> UserTypeCtxt -> ExpandMode 1085 -> PredType -> TcM () 1086-- Check the validity of a predicate in a signature 1087-- See Note [Validity checking for constraints] 1088check_pred_ty env dflags ctxt expand pred 1089 = do { check_type ve pred 1090 ; check_pred_help False env dflags ctxt pred } 1091 where 1092 rank | xopt LangExt.QuantifiedConstraints dflags 1093 = ArbitraryRank 1094 | otherwise 1095 = constraintMonoType 1096 1097 ve :: ValidityEnv 1098 ve = ValidityEnv{ ve_tidy_env = env 1099 , ve_ctxt = SigmaCtxt 1100 , ve_rank = rank 1101 , ve_expand = expand } 1102 1103check_pred_help :: Bool -- True <=> under a type synonym 1104 -> TidyEnv 1105 -> DynFlags -> UserTypeCtxt 1106 -> PredType -> TcM () 1107check_pred_help under_syn env dflags ctxt pred 1108 | Just pred' <- tcView pred -- Switch on under_syn when going under a 1109 -- synonym (#9838, yuk) 1110 = check_pred_help True env dflags ctxt pred' 1111 1112 | otherwise -- A bit like classifyPredType, but not the same 1113 -- E.g. we treat (~) like (~#); and we look inside tuples 1114 = case classifyPredType pred of 1115 ClassPred cls tys 1116 | isCTupleClass cls -> check_tuple_pred under_syn env dflags ctxt pred tys 1117 | otherwise -> check_class_pred env dflags ctxt pred cls tys 1118 1119 EqPred NomEq _ _ -> -- a ~# b 1120 check_eq_pred env dflags pred 1121 1122 EqPred ReprEq _ _ -> -- Ugh! When inferring types we may get 1123 -- f :: (a ~R# b) => blha 1124 -- And we want to treat that like (Coercible a b) 1125 -- We should probably check argument shapes, but we 1126 -- didn't do so before, so I'm leaving it for now 1127 return () 1128 1129 ForAllPred _ theta head -> check_quant_pred env dflags ctxt pred theta head 1130 IrredPred {} -> check_irred_pred under_syn env dflags ctxt pred 1131 1132check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TcM () 1133check_eq_pred env dflags pred 1134 = -- Equational constraints are valid in all contexts if type 1135 -- families are permitted 1136 checkTcM (xopt LangExt.TypeFamilies dflags 1137 || xopt LangExt.GADTs dflags) 1138 (eqPredTyErr env pred) 1139 1140check_quant_pred :: TidyEnv -> DynFlags -> UserTypeCtxt 1141 -> PredType -> ThetaType -> PredType -> TcM () 1142check_quant_pred env dflags _ctxt pred theta head_pred 1143 = addErrCtxt (text "In the quantified constraint" <+> quotes (ppr pred)) $ 1144 do { -- Check the instance head 1145 case classifyPredType head_pred of 1146 ClassPred cls tys -> checkValidInstHead SigmaCtxt cls tys 1147 -- SigmaCtxt tells checkValidInstHead that 1148 -- this is the head of a quantified constraint 1149 IrredPred {} | hasTyVarHead head_pred 1150 -> return () 1151 _ -> failWithTcM (badQuantHeadErr env pred) 1152 1153 -- Check for termination 1154 ; unless (xopt LangExt.UndecidableInstances dflags) $ 1155 checkInstTermination theta head_pred 1156 } 1157 1158check_tuple_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM () 1159check_tuple_pred under_syn env dflags ctxt pred ts 1160 = do { -- See Note [ConstraintKinds in predicates] 1161 checkTcM (under_syn || xopt LangExt.ConstraintKinds dflags) 1162 (predTupleErr env pred) 1163 ; mapM_ (check_pred_help under_syn env dflags ctxt) ts } 1164 -- This case will not normally be executed because without 1165 -- -XConstraintKinds tuple types are only kind-checked as * 1166 1167check_irred_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM () 1168check_irred_pred under_syn env dflags ctxt pred 1169 -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint 1170 -- where X is a type function 1171 = do { -- If it looks like (x t1 t2), require ConstraintKinds 1172 -- see Note [ConstraintKinds in predicates] 1173 -- But (X t1 t2) is always ok because we just require ConstraintKinds 1174 -- at the definition site (#9838) 1175 failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags) 1176 && hasTyVarHead pred) 1177 (predIrredErr env pred) 1178 1179 -- Make sure it is OK to have an irred pred in this context 1180 -- See Note [Irreducible predicates in superclasses] 1181 ; failIfTcM (is_superclass ctxt 1182 && not (xopt LangExt.UndecidableInstances dflags) 1183 && has_tyfun_head pred) 1184 (predSuperClassErr env pred) } 1185 where 1186 is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False } 1187 has_tyfun_head ty 1188 = case tcSplitTyConApp_maybe ty of 1189 Just (tc, _) -> isTypeFamilyTyCon tc 1190 Nothing -> False 1191 1192{- Note [ConstraintKinds in predicates] 1193~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1194Don't check for -XConstraintKinds under a type synonym, because that 1195was done at the type synonym definition site; see #9838 1196e.g. module A where 1197 type C a = (Eq a, Ix a) -- Needs -XConstraintKinds 1198 module B where 1199 import A 1200 f :: C a => a -> a -- Does *not* need -XConstraintKinds 1201 1202Note [Irreducible predicates in superclasses] 1203~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1204Allowing type-family calls in class superclasses is somewhat dangerous 1205because we can write: 1206 1207 type family Fooish x :: * -> Constraint 1208 type instance Fooish () = Foo 1209 class Fooish () a => Foo a where 1210 1211This will cause the constraint simplifier to loop because every time we canonicalise a 1212(Foo a) class constraint we add a (Fooish () a) constraint which will be immediately 1213solved to add+canonicalise another (Foo a) constraint. -} 1214 1215------------------------- 1216check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt 1217 -> PredType -> Class -> [TcType] -> TcM () 1218check_class_pred env dflags ctxt pred cls tys 1219 | isEqPredClass cls -- (~) and (~~) are classified as classes, 1220 -- but here we want to treat them as equalities 1221 = -- pprTrace "check_class" (ppr cls) $ 1222 check_eq_pred env dflags pred 1223 1224 | isIPClass cls 1225 = do { check_arity 1226 ; checkTcM (okIPCtxt ctxt) (badIPPred env pred) } 1227 1228 | otherwise -- Includes Coercible 1229 = do { check_arity 1230 ; checkSimplifiableClassConstraint env dflags ctxt cls tys 1231 ; checkTcM arg_tys_ok (predTyVarErr env pred) } 1232 where 1233 check_arity = checkTc (tys `lengthIs` classArity cls) 1234 (tyConArityErr (classTyCon cls) tys) 1235 1236 -- Check the arguments of a class constraint 1237 flexible_contexts = xopt LangExt.FlexibleContexts dflags 1238 undecidable_ok = xopt LangExt.UndecidableInstances dflags 1239 arg_tys_ok = case ctxt of 1240 SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine 1241 InstDeclCtxt {} -> checkValidClsArgs (flexible_contexts || undecidable_ok) cls tys 1242 -- Further checks on head and theta 1243 -- in checkInstTermination 1244 _ -> checkValidClsArgs flexible_contexts cls tys 1245 1246checkSimplifiableClassConstraint :: TidyEnv -> DynFlags -> UserTypeCtxt 1247 -> Class -> [TcType] -> TcM () 1248-- See Note [Simplifiable given constraints] 1249checkSimplifiableClassConstraint env dflags ctxt cls tys 1250 | not (wopt Opt_WarnSimplifiableClassConstraints dflags) 1251 = return () 1252 | xopt LangExt.MonoLocalBinds dflags 1253 = return () 1254 1255 | DataTyCtxt {} <- ctxt -- Don't do this check for the "stupid theta" 1256 = return () -- of a data type declaration 1257 1258 | cls `hasKey` coercibleTyConKey 1259 = return () -- Oddly, we treat (Coercible t1 t2) as unconditionally OK 1260 -- matchGlobalInst will reply "yes" because we can reduce 1261 -- (Coercible a b) to (a ~R# b) 1262 1263 | otherwise 1264 = do { result <- matchGlobalInst dflags False cls tys 1265 ; case result of 1266 OneInst { cir_what = what } 1267 -> addWarnTc (Reason Opt_WarnSimplifiableClassConstraints) 1268 (simplifiable_constraint_warn what) 1269 _ -> return () } 1270 where 1271 pred = mkClassPred cls tys 1272 1273 simplifiable_constraint_warn :: InstanceWhat -> SDoc 1274 simplifiable_constraint_warn what 1275 = vcat [ hang (text "The constraint" <+> quotes (ppr (tidyType env pred)) 1276 <+> text "matches") 1277 2 (ppr what) 1278 , hang (text "This makes type inference for inner bindings fragile;") 1279 2 (text "either use MonoLocalBinds, or simplify it using the instance") ] 1280 1281{- Note [Simplifiable given constraints] 1282~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1283A type signature like 1284 f :: Eq [(a,b)] => a -> b 1285is very fragile, for reasons described at length in TcInteract 1286Note [Instance and Given overlap]. As that Note discusses, for the 1287most part the clever stuff in TcInteract means that we don't use a 1288top-level instance if a local Given might fire, so there is no 1289fragility. But if we /infer/ the type of a local let-binding, things 1290can go wrong (#11948 is an example, discussed in the Note). 1291 1292So this warning is switched on only if we have NoMonoLocalBinds; in 1293that case the warning discourages users from writing simplifiable 1294class constraints. 1295 1296The warning only fires if the constraint in the signature 1297matches the top-level instances in only one way, and with no 1298unifiers -- that is, under the same circumstances that 1299TcInteract.matchInstEnv fires an interaction with the top 1300level instances. For example (#13526), consider 1301 1302 instance {-# OVERLAPPABLE #-} Eq (T a) where ... 1303 instance Eq (T Char) where .. 1304 f :: Eq (T a) => ... 1305 1306We don't want to complain about this, even though the context 1307(Eq (T a)) matches an instance, because the user may be 1308deliberately deferring the choice so that the Eq (T Char) 1309has a chance to fire when 'f' is called. And the fragility 1310only matters when there's a risk that the instance might 1311fire instead of the local 'given'; and there is no such 1312risk in this case. Just use the same rules as for instance 1313firing! 1314-} 1315 1316------------------------- 1317okIPCtxt :: UserTypeCtxt -> Bool 1318 -- See Note [Implicit parameters in instance decls] 1319okIPCtxt (FunSigCtxt {}) = True 1320okIPCtxt (InfSigCtxt {}) = True 1321okIPCtxt ExprSigCtxt = True 1322okIPCtxt TypeAppCtxt = True 1323okIPCtxt PatSigCtxt = True 1324okIPCtxt ResSigCtxt = True 1325okIPCtxt GenSigCtxt = True 1326okIPCtxt (ConArgCtxt {}) = True 1327okIPCtxt (ForSigCtxt {}) = True -- ?? 1328okIPCtxt ThBrackCtxt = True 1329okIPCtxt (GhciCtxt {}) = True 1330okIPCtxt SigmaCtxt = True 1331okIPCtxt (DataTyCtxt {}) = True 1332okIPCtxt (PatSynCtxt {}) = True 1333okIPCtxt (TySynCtxt {}) = True -- e.g. type Blah = ?x::Int 1334 -- #11466 1335 1336okIPCtxt (KindSigCtxt {}) = False 1337okIPCtxt (StandaloneKindSigCtxt {}) = False 1338okIPCtxt (ClassSCCtxt {}) = False 1339okIPCtxt (InstDeclCtxt {}) = False 1340okIPCtxt (SpecInstCtxt {}) = False 1341okIPCtxt (RuleSigCtxt {}) = False 1342okIPCtxt DefaultDeclCtxt = False 1343okIPCtxt DerivClauseCtxt = False 1344okIPCtxt (TyVarBndrKindCtxt {}) = False 1345okIPCtxt (DataKindCtxt {}) = False 1346okIPCtxt (TySynKindCtxt {}) = False 1347okIPCtxt (TyFamResKindCtxt {}) = False 1348 1349{- 1350Note [Kind polymorphic type classes] 1351~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1352MultiParam check: 1353 1354 class C f where... -- C :: forall k. k -> Constraint 1355 instance C Maybe where... 1356 1357 The dictionary gets type [C * Maybe] even if it's not a MultiParam 1358 type class. 1359 1360Flexibility check: 1361 1362 class C f where... -- C :: forall k. k -> Constraint 1363 data D a = D a 1364 instance C D where 1365 1366 The dictionary gets type [C * (D *)]. IA0_TODO it should be 1367 generalized actually. 1368-} 1369 1370checkThetaCtxt :: UserTypeCtxt -> ThetaType -> TidyEnv -> TcM (TidyEnv, SDoc) 1371checkThetaCtxt ctxt theta env 1372 = return ( env 1373 , vcat [ text "In the context:" <+> pprTheta (tidyTypes env theta) 1374 , text "While checking" <+> pprUserTypeCtxt ctxt ] ) 1375 1376eqPredTyErr, predTupleErr, predIrredErr, 1377 predSuperClassErr, badQuantHeadErr :: TidyEnv -> PredType -> (TidyEnv, SDoc) 1378badQuantHeadErr env pred 1379 = ( env 1380 , hang (text "Quantified predicate must have a class or type variable head:") 1381 2 (ppr_tidy env pred) ) 1382eqPredTyErr env pred 1383 = ( env 1384 , text "Illegal equational constraint" <+> ppr_tidy env pred $$ 1385 parens (text "Use GADTs or TypeFamilies to permit this") ) 1386predTupleErr env pred 1387 = ( env 1388 , hang (text "Illegal tuple constraint:" <+> ppr_tidy env pred) 1389 2 (parens constraintKindsMsg) ) 1390predIrredErr env pred 1391 = ( env 1392 , hang (text "Illegal constraint:" <+> ppr_tidy env pred) 1393 2 (parens constraintKindsMsg) ) 1394predSuperClassErr env pred 1395 = ( env 1396 , hang (text "Illegal constraint" <+> quotes (ppr_tidy env pred) 1397 <+> text "in a superclass context") 1398 2 (parens undecidableMsg) ) 1399 1400predTyVarErr :: TidyEnv -> PredType -> (TidyEnv, SDoc) 1401predTyVarErr env pred 1402 = (env 1403 , vcat [ hang (text "Non type-variable argument") 1404 2 (text "in the constraint:" <+> ppr_tidy env pred) 1405 , parens (text "Use FlexibleContexts to permit this") ]) 1406 1407badIPPred :: TidyEnv -> PredType -> (TidyEnv, SDoc) 1408badIPPred env pred 1409 = ( env 1410 , text "Illegal implicit parameter" <+> quotes (ppr_tidy env pred) ) 1411 1412constraintSynErr :: TidyEnv -> Type -> (TidyEnv, SDoc) 1413constraintSynErr env kind 1414 = ( env 1415 , hang (text "Illegal constraint synonym of kind:" <+> quotes (ppr_tidy env kind)) 1416 2 (parens constraintKindsMsg) ) 1417 1418dupPredWarn :: TidyEnv -> [NE.NonEmpty PredType] -> (TidyEnv, SDoc) 1419dupPredWarn env dups 1420 = ( env 1421 , text "Duplicate constraint" <> plural primaryDups <> text ":" 1422 <+> pprWithCommas (ppr_tidy env) primaryDups ) 1423 where 1424 primaryDups = map NE.head dups 1425 1426tyConArityErr :: TyCon -> [TcType] -> SDoc 1427-- For type-constructor arity errors, be careful to report 1428-- the number of /visible/ arguments required and supplied, 1429-- ignoring the /invisible/ arguments, which the user does not see. 1430-- (e.g. #10516) 1431tyConArityErr tc tks 1432 = arityErr (ppr (tyConFlavour tc)) (tyConName tc) 1433 tc_type_arity tc_type_args 1434 where 1435 vis_tks = filterOutInvisibleTypes tc tks 1436 1437 -- tc_type_arity = number of *type* args expected 1438 -- tc_type_args = number of *type* args encountered 1439 tc_type_arity = count isVisibleTyConBinder (tyConBinders tc) 1440 tc_type_args = length vis_tks 1441 1442arityErr :: Outputable a => SDoc -> a -> Int -> Int -> SDoc 1443arityErr what name n m 1444 = hsep [ text "The" <+> what, quotes (ppr name), text "should have", 1445 n_arguments <> comma, text "but has been given", 1446 if m==0 then text "none" else int m] 1447 where 1448 n_arguments | n == 0 = text "no arguments" 1449 | n == 1 = text "1 argument" 1450 | True = hsep [int n, text "arguments"] 1451 1452{- 1453************************************************************************ 1454* * 1455\subsection{Checking for a decent instance head type} 1456* * 1457************************************************************************ 1458 1459@checkValidInstHead@ checks the type {\em and} its syntactic constraints: 1460it must normally look like: @instance Foo (Tycon a b c ...) ...@ 1461 1462The exceptions to this syntactic checking: (1)~if the @GlasgowExts@ 1463flag is on, or (2)~the instance is imported (they must have been 1464compiled elsewhere). In these cases, we let them go through anyway. 1465 1466We can also have instances for functions: @instance Foo (a -> b) ...@. 1467-} 1468 1469checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM () 1470checkValidInstHead ctxt clas cls_args 1471 = do { dflags <- getDynFlags 1472 ; is_boot <- tcIsHsBootOrSig 1473 ; is_sig <- tcIsHsig 1474 ; check_special_inst_head dflags is_boot is_sig ctxt clas cls_args 1475 ; checkValidTypePats (classTyCon clas) cls_args 1476 } 1477 1478{- 1479 1480Note [Instances of built-in classes in signature files] 1481~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1482 1483User defined instances for KnownNat, KnownSymbol and Typeable are 1484disallowed -- they are generated when needed by GHC itself on-the-fly. 1485 1486However, if they occur in a Backpack signature file, they have an 1487entirely different meaning. Suppose in M.hsig we see 1488 1489 signature M where 1490 data T :: Nat 1491 instance KnownNat T 1492 1493That says that any module satisfying M.hsig must provide a KnownNat 1494instance for T. We absolultely need that instance when compiling a 1495module that imports M.hsig: see #15379 and 1496Note [Fabricating Evidence for Literals in Backpack] in ClsInst. 1497 1498Hence, checkValidInstHead accepts a user-written instance declaration 1499in hsig files, where `is_sig` is True. 1500 1501-} 1502 1503check_special_inst_head :: DynFlags -> Bool -> Bool 1504 -> UserTypeCtxt -> Class -> [Type] -> TcM () 1505-- Wow! There are a surprising number of ad-hoc special cases here. 1506check_special_inst_head dflags is_boot is_sig ctxt clas cls_args 1507 1508 -- If not in an hs-boot file, abstract classes cannot have instances 1509 | isAbstractClass clas 1510 , not is_boot 1511 = failWithTc abstract_class_msg 1512 1513 -- For Typeable, don't complain about instances for 1514 -- standalone deriving; they are no-ops, and we warn about 1515 -- it in TcDeriv.deriveStandalone. 1516 | clas_nm == typeableClassName 1517 , not is_sig 1518 -- Note [Instances of built-in classes in signature files] 1519 , hand_written_bindings 1520 = failWithTc rejected_class_msg 1521 1522 -- Handwritten instances of KnownNat/KnownSymbol class 1523 -- are always forbidden (#12837) 1524 | clas_nm `elem` [ knownNatClassName, knownSymbolClassName ] 1525 , not is_sig 1526 -- Note [Instances of built-in classes in signature files] 1527 , hand_written_bindings 1528 = failWithTc rejected_class_msg 1529 1530 -- For the most part we don't allow 1531 -- instances for (~), (~~), or Coercible; 1532 -- but we DO want to allow them in quantified constraints: 1533 -- f :: (forall a b. Coercible a b => Coercible (m a) (m b)) => ...m... 1534 | clas_nm `elem` [ heqTyConName, eqTyConName, coercibleTyConName ] 1535 , not quantified_constraint 1536 = failWithTc rejected_class_msg 1537 1538 -- Check for hand-written Generic instances (disallowed in Safe Haskell) 1539 | clas_nm `elem` genericClassNames 1540 , hand_written_bindings 1541 = do { failIfTc (safeLanguageOn dflags) gen_inst_err 1542 ; when (safeInferOn dflags) (recordUnsafeInfer emptyBag) } 1543 1544 | clas_nm == hasFieldClassName 1545 = checkHasFieldInst clas cls_args 1546 1547 | isCTupleClass clas 1548 = failWithTc tuple_class_msg 1549 1550 -- Check language restrictions on the args to the class 1551 | check_h98_arg_shape 1552 , Just msg <- mb_ty_args_msg 1553 = failWithTc (instTypeErr clas cls_args msg) 1554 1555 | otherwise 1556 = pure () 1557 where 1558 clas_nm = getName clas 1559 ty_args = filterOutInvisibleTypes (classTyCon clas) cls_args 1560 1561 hand_written_bindings 1562 = case ctxt of 1563 InstDeclCtxt stand_alone -> not stand_alone 1564 SpecInstCtxt -> False 1565 DerivClauseCtxt -> False 1566 _ -> True 1567 1568 check_h98_arg_shape = case ctxt of 1569 SpecInstCtxt -> False 1570 DerivClauseCtxt -> False 1571 SigmaCtxt -> False 1572 _ -> True 1573 -- SigmaCtxt: once we are in quantified-constraint land, we 1574 -- aren't so picky about enforcing H98-language restrictions 1575 -- E.g. we want to allow a head like Coercible (m a) (m b) 1576 1577 1578 -- When we are looking at the head of a quantified constraint, 1579 -- check_quant_pred sets ctxt to SigmaCtxt 1580 quantified_constraint = case ctxt of 1581 SigmaCtxt -> True 1582 _ -> False 1583 1584 head_type_synonym_msg = parens ( 1585 text "All instance types must be of the form (T t1 ... tn)" $$ 1586 text "where T is not a synonym." $$ 1587 text "Use TypeSynonymInstances if you want to disable this.") 1588 1589 head_type_args_tyvars_msg = parens (vcat [ 1590 text "All instance types must be of the form (T a1 ... an)", 1591 text "where a1 ... an are *distinct type variables*,", 1592 text "and each type variable appears at most once in the instance head.", 1593 text "Use FlexibleInstances if you want to disable this."]) 1594 1595 head_one_type_msg = parens $ 1596 text "Only one type can be given in an instance head." $$ 1597 text "Use MultiParamTypeClasses if you want to allow more, or zero." 1598 1599 rejected_class_msg = text "Class" <+> quotes (ppr clas_nm) 1600 <+> text "does not support user-specified instances" 1601 tuple_class_msg = text "You can't specify an instance for a tuple constraint" 1602 1603 gen_inst_err = rejected_class_msg $$ nest 2 (text "(in Safe Haskell)") 1604 1605 abstract_class_msg = text "Cannot define instance for abstract class" 1606 <+> quotes (ppr clas_nm) 1607 1608 mb_ty_args_msg 1609 | not (xopt LangExt.TypeSynonymInstances dflags) 1610 , not (all tcInstHeadTyNotSynonym ty_args) 1611 = Just head_type_synonym_msg 1612 1613 | not (xopt LangExt.FlexibleInstances dflags) 1614 , not (all tcInstHeadTyAppAllTyVars ty_args) 1615 = Just head_type_args_tyvars_msg 1616 1617 | length ty_args /= 1 1618 , not (xopt LangExt.MultiParamTypeClasses dflags) 1619 , not (xopt LangExt.NullaryTypeClasses dflags && null ty_args) 1620 = Just head_one_type_msg 1621 1622 | otherwise 1623 = Nothing 1624 1625tcInstHeadTyNotSynonym :: Type -> Bool 1626-- Used in Haskell-98 mode, for the argument types of an instance head 1627-- These must not be type synonyms, but everywhere else type synonyms 1628-- are transparent, so we need a special function here 1629tcInstHeadTyNotSynonym ty 1630 = case ty of -- Do not use splitTyConApp, 1631 -- because that expands synonyms! 1632 TyConApp tc _ -> not (isTypeSynonymTyCon tc) 1633 _ -> True 1634 1635tcInstHeadTyAppAllTyVars :: Type -> Bool 1636-- Used in Haskell-98 mode, for the argument types of an instance head 1637-- These must be a constructor applied to type variable arguments 1638-- or a type-level literal. 1639-- But we allow kind instantiations. 1640tcInstHeadTyAppAllTyVars ty 1641 | Just (tc, tys) <- tcSplitTyConApp_maybe (dropCasts ty) 1642 = ok (filterOutInvisibleTypes tc tys) -- avoid kinds 1643 | LitTy _ <- ty = True -- accept type literals (#13833) 1644 | otherwise 1645 = False 1646 where 1647 -- Check that all the types are type variables, 1648 -- and that each is distinct 1649 ok tys = equalLength tvs tys && hasNoDups tvs 1650 where 1651 tvs = mapMaybe tcGetTyVar_maybe tys 1652 1653dropCasts :: Type -> Type 1654-- See Note [Casts during validity checking] 1655-- This function can turn a well-kinded type into an ill-kinded 1656-- one, so I've kept it local to this module 1657-- To consider: drop only HoleCo casts 1658dropCasts (CastTy ty _) = dropCasts ty 1659dropCasts (AppTy t1 t2) = mkAppTy (dropCasts t1) (dropCasts t2) 1660dropCasts ty@(FunTy _ t1 t2) = ty { ft_arg = dropCasts t1, ft_res = dropCasts t2 } 1661dropCasts (TyConApp tc tys) = mkTyConApp tc (map dropCasts tys) 1662dropCasts (ForAllTy b ty) = ForAllTy (dropCastsB b) (dropCasts ty) 1663dropCasts ty = ty -- LitTy, TyVarTy, CoercionTy 1664 1665dropCastsB :: TyVarBinder -> TyVarBinder 1666dropCastsB b = b -- Don't bother in the kind of a forall 1667 1668instTypeErr :: Class -> [Type] -> SDoc -> SDoc 1669instTypeErr cls tys msg 1670 = hang (hang (text "Illegal instance declaration for") 1671 2 (quotes (pprClassPred cls tys))) 1672 2 msg 1673 1674-- | See Note [Validity checking of HasField instances] 1675checkHasFieldInst :: Class -> [Type] -> TcM () 1676checkHasFieldInst cls tys@[_k_ty, x_ty, r_ty, _a_ty] = 1677 case splitTyConApp_maybe r_ty of 1678 Nothing -> whoops (text "Record data type must be specified") 1679 Just (tc, _) 1680 | isFamilyTyCon tc 1681 -> whoops (text "Record data type may not be a data family") 1682 | otherwise -> case isStrLitTy x_ty of 1683 Just lbl 1684 | isJust (lookupTyConFieldLabel lbl tc) 1685 -> whoops (ppr tc <+> text "already has a field" 1686 <+> quotes (ppr lbl)) 1687 | otherwise -> return () 1688 Nothing 1689 | null (tyConFieldLabels tc) -> return () 1690 | otherwise -> whoops (ppr tc <+> text "has fields") 1691 where 1692 whoops = addErrTc . instTypeErr cls tys 1693checkHasFieldInst _ tys = pprPanic "checkHasFieldInst" (ppr tys) 1694 1695{- Note [Casts during validity checking] 1696~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1697Consider the (bogus) 1698 instance Eq Char# 1699We elaborate to 'Eq (Char# |> UnivCo(hole))' where the hole is an 1700insoluble equality constraint for * ~ #. We'll report the insoluble 1701constraint separately, but we don't want to *also* complain that Eq is 1702not applied to a type constructor. So we look gaily look through 1703CastTys here. 1704 1705Another example: Eq (Either a). Then we actually get a cast in 1706the middle: 1707 Eq ((Either |> g) a) 1708 1709 1710Note [Validity checking of HasField instances] 1711~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1712The HasField class has magic constraint solving behaviour (see Note 1713[HasField instances] in TcInteract). However, we permit users to 1714declare their own instances, provided they do not clash with the 1715built-in behaviour. In particular, we forbid: 1716 1717 1. `HasField _ r _` where r is a variable 1718 1719 2. `HasField _ (T ...) _` if T is a data family 1720 (because it might have fields introduced later) 1721 1722 3. `HasField x (T ...) _` where x is a variable, 1723 if T has any fields at all 1724 1725 4. `HasField "foo" (T ...) _` if T has a "foo" field 1726 1727The usual functional dependency checks also apply. 1728 1729 1730Note [Valid 'deriving' predicate] 1731~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1732validDerivPred checks for OK 'deriving' context. See Note [Exotic 1733derived instance contexts] in TcDeriv. However the predicate is 1734here because it uses sizeTypes, fvTypes. 1735 1736It checks for three things 1737 1738 * No repeated variables (hasNoDups fvs) 1739 1740 * No type constructors. This is done by comparing 1741 sizeTypes tys == length (fvTypes tys) 1742 sizeTypes counts variables and constructors; fvTypes returns variables. 1743 So if they are the same, there must be no constructors. But there 1744 might be applications thus (f (g x)). 1745 1746 Note that tys only includes the visible arguments of the class type 1747 constructor. Including the non-visible arguments can cause the following, 1748 perfectly valid instance to be rejected: 1749 class Category (cat :: k -> k -> *) where ... 1750 newtype T (c :: * -> * -> *) a b = MkT (c a b) 1751 instance Category c => Category (T c) where ... 1752 since the first argument to Category is a non-visible *, which sizeTypes 1753 would count as a constructor! See #11833. 1754 1755 * Also check for a bizarre corner case, when the derived instance decl 1756 would look like 1757 instance C a b => D (T a) where ... 1758 Note that 'b' isn't a parameter of T. This gives rise to all sorts of 1759 problems; in particular, it's hard to compare solutions for equality 1760 when finding the fixpoint, and that means the inferContext loop does 1761 not converge. See #5287. 1762 1763Note [Equality class instances] 1764~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1765We can't have users writing instances for the equality classes. But we 1766still need to be able to write instances for them ourselves. So we allow 1767instances only in the defining module. 1768 1769-} 1770 1771validDerivPred :: TyVarSet -> PredType -> Bool 1772-- See Note [Valid 'deriving' predicate] 1773validDerivPred tv_set pred 1774 = case classifyPredType pred of 1775 ClassPred cls tys -> cls `hasKey` typeableClassKey 1776 -- Typeable constraints are bigger than they appear due 1777 -- to kind polymorphism, but that's OK 1778 || check_tys cls tys 1779 EqPred {} -> False -- reject equality constraints 1780 _ -> True -- Non-class predicates are ok 1781 where 1782 check_tys cls tys 1783 = hasNoDups fvs 1784 -- use sizePred to ignore implicit args 1785 && lengthIs fvs (sizePred pred) 1786 && all (`elemVarSet` tv_set) fvs 1787 where tys' = filterOutInvisibleTypes (classTyCon cls) tys 1788 fvs = fvTypes tys' 1789 1790{- 1791************************************************************************ 1792* * 1793\subsection{Checking instance for termination} 1794* * 1795************************************************************************ 1796-} 1797 1798{- Note [Instances and constraint synonyms] 1799~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1800Currently, we don't allow instances for constraint synonyms at all. 1801Consider these (#13267): 1802 type C1 a = Show (a -> Bool) 1803 instance C1 Int where -- I1 1804 show _ = "ur" 1805 1806This elicits "show is not a (visible) method of class C1", which isn't 1807a great message. But it comes from the renamer, so it's hard to improve. 1808 1809This needs a bit more care: 1810 type C2 a = (Show a, Show Int) 1811 instance C2 Int -- I2 1812 1813If we use (splitTyConApp_maybe tau) in checkValidInstance to decompose 1814the instance head, we'll expand the synonym on fly, and it'll look like 1815 instance (%,%) (Show Int, Show Int) 1816and we /really/ don't want that. So we carefully do /not/ expand 1817synonyms, by matching on TyConApp directly. 1818-} 1819 1820checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type -> TcM () 1821checkValidInstance ctxt hs_type ty 1822 | not is_tc_app 1823 = failWithTc (hang (text "Instance head is not headed by a class:") 1824 2 ( ppr tau)) 1825 1826 | isNothing mb_cls 1827 = failWithTc (vcat [ text "Illegal instance for a" <+> ppr (tyConFlavour tc) 1828 , text "A class instance must be for a class" ]) 1829 1830 | not arity_ok 1831 = failWithTc (text "Arity mis-match in instance head") 1832 1833 | otherwise 1834 = do { setSrcSpan head_loc $ 1835 checkValidInstHead ctxt clas inst_tys 1836 1837 ; traceTc "checkValidInstance {" (ppr ty) 1838 1839 ; env0 <- tcInitTidyEnv 1840 ; expand <- initialExpandMode 1841 ; check_valid_theta env0 ctxt expand theta 1842 1843 -- The Termination and Coverate Conditions 1844 -- Check that instance inference will terminate (if we care) 1845 -- For Haskell 98 this will already have been done by checkValidTheta, 1846 -- but as we may be using other extensions we need to check. 1847 -- 1848 -- Note that the Termination Condition is *more conservative* than 1849 -- the checkAmbiguity test we do on other type signatures 1850 -- e.g. Bar a => Bar Int is ambiguous, but it also fails 1851 -- the termination condition, because 'a' appears more often 1852 -- in the constraint than in the head 1853 ; undecidable_ok <- xoptM LangExt.UndecidableInstances 1854 ; if undecidable_ok 1855 then checkAmbiguity ctxt ty 1856 else checkInstTermination theta tau 1857 1858 ; traceTc "cvi 2" (ppr ty) 1859 1860 ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of 1861 IsValid -> return () -- Check succeeded 1862 NotValid msg -> addErrTc (instTypeErr clas inst_tys msg) 1863 1864 ; traceTc "End checkValidInstance }" empty 1865 1866 ; return () } 1867 where 1868 (_tvs, theta, tau) = tcSplitSigmaTy ty 1869 is_tc_app = case tau of { TyConApp {} -> True; _ -> False } 1870 TyConApp tc inst_tys = tau -- See Note [Instances and constraint synonyms] 1871 mb_cls = tyConClass_maybe tc 1872 Just clas = mb_cls 1873 arity_ok = inst_tys `lengthIs` classArity clas 1874 1875 -- The location of the "head" of the instance 1876 head_loc = getLoc (getLHsInstDeclHead hs_type) 1877 1878{- 1879Note [Paterson conditions] 1880~~~~~~~~~~~~~~~~~~~~~~~~~~ 1881Termination test: the so-called "Paterson conditions" (see Section 5 of 1882"Understanding functional dependencies via Constraint Handling Rules, 1883JFP Jan 2007). 1884 1885We check that each assertion in the context satisfies: 1886 (1) no variable has more occurrences in the assertion than in the head, and 1887 (2) the assertion has fewer constructors and variables (taken together 1888 and counting repetitions) than the head. 1889This is only needed with -fglasgow-exts, as Haskell 98 restrictions 1890(which have already been checked) guarantee termination. 1891 1892The underlying idea is that 1893 1894 for any ground substitution, each assertion in the 1895 context has fewer type constructors than the head. 1896-} 1897 1898checkInstTermination :: ThetaType -> TcPredType -> TcM () 1899-- See Note [Paterson conditions] 1900checkInstTermination theta head_pred 1901 = check_preds emptyVarSet theta 1902 where 1903 head_fvs = fvType head_pred 1904 head_size = sizeType head_pred 1905 1906 check_preds :: VarSet -> [PredType] -> TcM () 1907 check_preds foralld_tvs preds = mapM_ (check foralld_tvs) preds 1908 1909 check :: VarSet -> PredType -> TcM () 1910 check foralld_tvs pred 1911 = case classifyPredType pred of 1912 EqPred {} -> return () -- See #4200. 1913 IrredPred {} -> check2 foralld_tvs pred (sizeType pred) 1914 ClassPred cls tys 1915 | isTerminatingClass cls 1916 -> return () 1917 1918 | isCTupleClass cls -- Look inside tuple predicates; #8359 1919 -> check_preds foralld_tvs tys 1920 1921 | otherwise -- Other ClassPreds 1922 -> check2 foralld_tvs pred bogus_size 1923 where 1924 bogus_size = 1 + sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys) 1925 -- See Note [Invisible arguments and termination] 1926 1927 ForAllPred tvs _ head_pred' 1928 -> check (foralld_tvs `extendVarSetList` binderVars tvs) head_pred' 1929 -- Termination of the quantified predicate itself is checked 1930 -- when the predicates are individually checked for validity 1931 1932 check2 foralld_tvs pred pred_size 1933 | not (null bad_tvs) = failWithTc (noMoreMsg bad_tvs what (ppr head_pred)) 1934 | not (isTyFamFree pred) = failWithTc (nestedMsg what) 1935 | pred_size >= head_size = failWithTc (smallerMsg what (ppr head_pred)) 1936 | otherwise = return () 1937 -- isTyFamFree: see Note [Type families in instance contexts] 1938 where 1939 what = text "constraint" <+> quotes (ppr pred) 1940 bad_tvs = filterOut (`elemVarSet` foralld_tvs) (fvType pred) 1941 \\ head_fvs 1942 1943smallerMsg :: SDoc -> SDoc -> SDoc 1944smallerMsg what inst_head 1945 = vcat [ hang (text "The" <+> what) 1946 2 (sep [ text "is no smaller than" 1947 , text "the instance head" <+> quotes inst_head ]) 1948 , parens undecidableMsg ] 1949 1950noMoreMsg :: [TcTyVar] -> SDoc -> SDoc -> SDoc 1951noMoreMsg tvs what inst_head 1952 = vcat [ hang (text "Variable" <> plural tvs1 <+> quotes (pprWithCommas ppr tvs1) 1953 <+> occurs <+> text "more often") 1954 2 (sep [ text "in the" <+> what 1955 , text "than in the instance head" <+> quotes inst_head ]) 1956 , parens undecidableMsg ] 1957 where 1958 tvs1 = nub tvs 1959 occurs = if isSingleton tvs1 then text "occurs" 1960 else text "occur" 1961 1962undecidableMsg, constraintKindsMsg :: SDoc 1963undecidableMsg = text "Use UndecidableInstances to permit this" 1964constraintKindsMsg = text "Use ConstraintKinds to permit this" 1965 1966{- Note [Type families in instance contexts] 1967~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1968Are these OK? 1969 type family F a 1970 instance F a => C (Maybe [a]) where ... 1971 intance C (F a) => C [[[a]]] where ... 1972 1973No: the type family in the instance head might blow up to an 1974arbitrarily large type, depending on how 'a' is instantiated. 1975So we require UndecidableInstances if we have a type family 1976in the instance head. #15172. 1977 1978Note [Invisible arguments and termination] 1979~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1980When checking the Paterson conditions for termination an instance 1981declaration, we check for the number of "constructors and variables" 1982in the instance head and constraints. Question: Do we look at 1983 1984 * All the arguments, visible or invisible? 1985 * Just the visible arguments? 1986 1987I think both will ensure termination, provided we are consistent. 1988Currently we are /not/ consistent, which is really a bug. It's 1989described in #15177, which contains a number of examples. 1990The suspicious bits are the calls to filterOutInvisibleTypes. 1991-} 1992 1993 1994{- 1995************************************************************************ 1996* * 1997 Checking type instance well-formedness and termination 1998* * 1999************************************************************************ 2000-} 2001 2002checkValidCoAxiom :: CoAxiom Branched -> TcM () 2003checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches }) 2004 = do { mapM_ (checkValidCoAxBranch fam_tc) branch_list 2005 ; foldlM_ check_branch_compat [] branch_list } 2006 where 2007 branch_list = fromBranches branches 2008 injectivity = tyConInjectivityInfo fam_tc 2009 2010 check_branch_compat :: [CoAxBranch] -- previous branches in reverse order 2011 -> CoAxBranch -- current branch 2012 -> TcM [CoAxBranch]-- current branch : previous branches 2013 -- Check for 2014 -- (a) this branch is dominated by previous ones 2015 -- (b) failure of injectivity 2016 check_branch_compat prev_branches cur_branch 2017 | cur_branch `isDominatedBy` prev_branches 2018 = do { addWarnAt NoReason (coAxBranchSpan cur_branch) $ 2019 inaccessibleCoAxBranch fam_tc cur_branch 2020 ; return prev_branches } 2021 | otherwise 2022 = do { check_injectivity prev_branches cur_branch 2023 ; return (cur_branch : prev_branches) } 2024 2025 -- Injectivity check: check whether a new (CoAxBranch) can extend 2026 -- already checked equations without violating injectivity 2027 -- annotation supplied by the user. 2028 -- See Note [Verifying injectivity annotation] in FamInstEnv 2029 check_injectivity prev_branches cur_branch 2030 | Injective inj <- injectivity 2031 = do { dflags <- getDynFlags 2032 ; let conflicts = 2033 fst $ foldl' (gather_conflicts inj prev_branches cur_branch) 2034 ([], 0) prev_branches 2035 ; reportConflictingInjectivityErrs fam_tc conflicts cur_branch 2036 ; reportInjectivityErrors dflags ax cur_branch inj } 2037 | otherwise 2038 = return () 2039 2040 gather_conflicts inj prev_branches cur_branch (acc, n) branch 2041 -- n is 0-based index of branch in prev_branches 2042 = case injectiveBranches inj cur_branch branch of 2043 -- Case 1B2 in Note [Verifying injectivity annotation] in FamInstEnv 2044 InjectivityUnified ax1 ax2 2045 | ax1 `isDominatedBy` (replace_br prev_branches n ax2) 2046 -> (acc, n + 1) 2047 | otherwise 2048 -> (branch : acc, n + 1) 2049 InjectivityAccepted -> (acc, n + 1) 2050 2051 -- Replace n-th element in the list. Assumes 0-based indexing. 2052 replace_br :: [CoAxBranch] -> Int -> CoAxBranch -> [CoAxBranch] 2053 replace_br brs n br = take n brs ++ [br] ++ drop (n+1) brs 2054 2055 2056-- Check that a "type instance" is well-formed (which includes decidability 2057-- unless -XUndecidableInstances is given). 2058-- 2059checkValidCoAxBranch :: TyCon -> CoAxBranch -> TcM () 2060checkValidCoAxBranch fam_tc 2061 (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs 2062 , cab_lhs = typats 2063 , cab_rhs = rhs, cab_loc = loc }) 2064 = setSrcSpan loc $ 2065 checkValidTyFamEqn fam_tc (tvs++cvs) typats rhs 2066 2067-- | Do validity checks on a type family equation, including consistency 2068-- with any enclosing class instance head, termination, and lack of 2069-- polytypes. 2070checkValidTyFamEqn :: TyCon -- ^ of the type family 2071 -> [Var] -- ^ Bound variables in the equation 2072 -> [Type] -- ^ Type patterns 2073 -> Type -- ^ Rhs 2074 -> TcM () 2075checkValidTyFamEqn fam_tc qvs typats rhs 2076 = do { checkValidTypePats fam_tc typats 2077 2078 -- Check for things used on the right but not bound on the left 2079 ; checkFamPatBinders fam_tc qvs typats rhs 2080 2081 -- Check for oversaturated visible kind arguments in a type family 2082 -- equation. 2083 -- See Note [Oversaturated type family equations] 2084 ; when (isTypeFamilyTyCon fam_tc) $ 2085 case drop (tyConArity fam_tc) typats of 2086 [] -> pure () 2087 spec_arg:_ -> 2088 addErr $ text "Illegal oversaturated visible kind argument:" 2089 <+> quotes (char '@' <> pprParendType spec_arg) 2090 2091 -- The argument patterns, and RHS, are all boxed tau types 2092 -- E.g Reject type family F (a :: k1) :: k2 2093 -- type instance F (forall a. a->a) = ... 2094 -- type instance F Int# = ... 2095 -- type instance F Int = forall a. a->a 2096 -- type instance F Int = Int# 2097 -- See #9357 2098 ; checkValidMonoType rhs 2099 2100 -- We have a decidable instance unless otherwise permitted 2101 ; undecidable_ok <- xoptM LangExt.UndecidableInstances 2102 ; traceTc "checkVTFE" (ppr fam_tc $$ ppr rhs $$ ppr (tcTyFamInsts rhs)) 2103 ; unless undecidable_ok $ 2104 mapM_ addErrTc (checkFamInstRhs fam_tc typats (tcTyFamInsts rhs)) } 2105 2106-- Make sure that each type family application is 2107-- (1) strictly smaller than the lhs, 2108-- (2) mentions no type variable more often than the lhs, and 2109-- (3) does not contain any further type family instances. 2110-- 2111checkFamInstRhs :: TyCon -> [Type] -- LHS 2112 -> [(TyCon, [Type])] -- type family calls in RHS 2113 -> [MsgDoc] 2114checkFamInstRhs lhs_tc lhs_tys famInsts 2115 = mapMaybe check famInsts 2116 where 2117 lhs_size = sizeTyConAppArgs lhs_tc lhs_tys 2118 inst_head = pprType (TyConApp lhs_tc lhs_tys) 2119 lhs_fvs = fvTypes lhs_tys 2120 check (tc, tys) 2121 | not (all isTyFamFree tys) = Just (nestedMsg what) 2122 | not (null bad_tvs) = Just (noMoreMsg bad_tvs what inst_head) 2123 | lhs_size <= fam_app_size = Just (smallerMsg what inst_head) 2124 | otherwise = Nothing 2125 where 2126 what = text "type family application" 2127 <+> quotes (pprType (TyConApp tc tys)) 2128 fam_app_size = sizeTyConAppArgs tc tys 2129 bad_tvs = fvTypes tys \\ lhs_fvs 2130 -- The (\\) is list difference; e.g. 2131 -- [a,b,a,a] \\ [a,a] = [b,a] 2132 -- So we are counting repetitions 2133 2134----------------- 2135checkFamPatBinders :: TyCon 2136 -> [TcTyVar] -- Bound on LHS of family instance 2137 -> [TcType] -- LHS patterns 2138 -> Type -- RHS 2139 -> TcM () 2140-- We do these binder checks now, in tcFamTyPatsAndGen, rather 2141-- than later, in checkValidFamEqn, for two reasons: 2142-- - We have the implicitly and explicitly 2143-- bound type variables conveniently to hand 2144-- - If implicit variables are out of scope it may 2145-- cause a crash; notably in tcConDecl in tcDataFamInstDecl 2146checkFamPatBinders fam_tc qtvs pats rhs 2147 = do { traceTc "checkFamPatBinders" $ 2148 vcat [ debugPprType (mkTyConApp fam_tc pats) 2149 , ppr (mkTyConApp fam_tc pats) 2150 , text "qtvs:" <+> ppr qtvs 2151 , text "rhs_tvs:" <+> ppr (fvVarSet rhs_fvs) 2152 , text "pat_tvs:" <+> ppr pat_tvs 2153 , text "inj_pat_tvs:" <+> ppr inj_pat_tvs ] 2154 2155 -- Check for implicitly-bound tyvars, mentioned on the 2156 -- RHS but not bound on the LHS 2157 -- data T = MkT (forall (a::k). blah) 2158 -- data family D Int = MkD (forall (a::k). blah) 2159 -- In both cases, 'k' is not bound on the LHS, but is used on the RHS 2160 -- We catch the former in kcDeclHeader, and the latter right here 2161 -- See Note [Check type-family instance binders] 2162 ; check_tvs bad_rhs_tvs (text "mentioned in the RHS") 2163 (text "bound on the LHS of") 2164 2165 -- Check for explicitly forall'd variable that is not bound on LHS 2166 -- data instance forall a. T Int = MkT Int 2167 -- See Note [Unused explicitly bound variables in a family pattern] 2168 -- See Note [Check type-family instance binders] 2169 ; check_tvs bad_qtvs (text "bound by a forall") 2170 (text "used in") 2171 } 2172 where 2173 pat_tvs = tyCoVarsOfTypes pats 2174 inj_pat_tvs = fvVarSet $ injectiveVarsOfTypes False pats 2175 -- The type variables that are in injective positions. 2176 -- See Note [Dodgy binding sites in type family instances] 2177 -- NB: The False above is irrelevant, as we never have type families in 2178 -- patterns. 2179 -- 2180 -- NB: It's OK to use the nondeterministic `fvVarSet` function here, 2181 -- since the order of `inj_pat_tvs` is never revealed in an error 2182 -- message. 2183 rhs_fvs = tyCoFVsOfType rhs 2184 used_tvs = pat_tvs `unionVarSet` fvVarSet rhs_fvs 2185 bad_qtvs = filterOut (`elemVarSet` used_tvs) qtvs 2186 -- Bound but not used at all 2187 bad_rhs_tvs = filterOut (`elemVarSet` inj_pat_tvs) (fvVarList rhs_fvs) 2188 -- Used on RHS but not bound on LHS 2189 dodgy_tvs = pat_tvs `minusVarSet` inj_pat_tvs 2190 2191 check_tvs tvs what what2 2192 = unless (null tvs) $ addErrAt (getSrcSpan (head tvs)) $ 2193 hang (text "Type variable" <> plural tvs <+> pprQuotedList tvs 2194 <+> isOrAre tvs <+> what <> comma) 2195 2 (vcat [ text "but not" <+> what2 <+> text "the family instance" 2196 , mk_extra tvs ]) 2197 2198 -- mk_extra: #7536: give a decent error message for 2199 -- type T a = Int 2200 -- type instance F (T a) = a 2201 mk_extra tvs = ppWhen (any (`elemVarSet` dodgy_tvs) tvs) $ 2202 hang (text "The real LHS (expanding synonyms) is:") 2203 2 (pprTypeApp fam_tc (map expandTypeSynonyms pats)) 2204 2205 2206-- | Checks that a list of type patterns is valid in a matching (LHS) 2207-- position of a class instances or type/data family instance. 2208-- 2209-- Specifically: 2210-- * All monotypes 2211-- * No type-family applications 2212checkValidTypePats :: TyCon -> [Type] -> TcM () 2213checkValidTypePats tc pat_ty_args 2214 = do { -- Check that each of pat_ty_args is a monotype. 2215 -- One could imagine generalising to allow 2216 -- instance C (forall a. a->a) 2217 -- but we don't know what all the consequences might be. 2218 traverse_ checkValidMonoType pat_ty_args 2219 2220 -- Ensure that no type family applications occur a type pattern 2221 ; case tcTyConAppTyFamInstsAndVis tc pat_ty_args of 2222 [] -> pure () 2223 ((tf_is_invis_arg, tf_tc, tf_args):_) -> failWithTc $ 2224 ty_fam_inst_illegal_err tf_is_invis_arg 2225 (mkTyConApp tf_tc tf_args) } 2226 where 2227 inst_ty = mkTyConApp tc pat_ty_args 2228 2229 ty_fam_inst_illegal_err :: Bool -> Type -> SDoc 2230 ty_fam_inst_illegal_err invis_arg ty 2231 = pprWithExplicitKindsWhen invis_arg $ 2232 hang (text "Illegal type synonym family application" 2233 <+> quotes (ppr ty) <+> text "in instance" <> colon) 2234 2 (ppr inst_ty) 2235 2236-- Error messages 2237 2238inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc 2239inaccessibleCoAxBranch fam_tc cur_branch 2240 = text "Type family instance equation is overlapped:" $$ 2241 nest 2 (pprCoAxBranchUser fam_tc cur_branch) 2242 2243nestedMsg :: SDoc -> SDoc 2244nestedMsg what 2245 = sep [ text "Illegal nested" <+> what 2246 , parens undecidableMsg ] 2247 2248badATErr :: Name -> Name -> SDoc 2249badATErr clas op 2250 = hsep [text "Class", quotes (ppr clas), 2251 text "does not have an associated type", quotes (ppr op)] 2252 2253 2254------------------------- 2255checkConsistentFamInst :: AssocInstInfo 2256 -> TyCon -- ^ Family tycon 2257 -> CoAxBranch 2258 -> TcM () 2259-- See Note [Checking consistent instantiation] 2260 2261checkConsistentFamInst NotAssociated _ _ 2262 = return () 2263 2264checkConsistentFamInst (InClsInst { ai_class = clas 2265 , ai_tyvars = inst_tvs 2266 , ai_inst_env = mini_env }) 2267 fam_tc branch 2268 = do { traceTc "checkConsistentFamInst" (vcat [ ppr inst_tvs 2269 , ppr arg_triples 2270 , ppr mini_env 2271 , ppr ax_tvs 2272 , ppr ax_arg_tys 2273 , ppr arg_triples ]) 2274 -- Check that the associated type indeed comes from this class 2275 -- See [Mismatched class methods and associated type families] 2276 -- in TcInstDecls. 2277 ; checkTc (Just (classTyCon clas) == tyConAssoc_maybe fam_tc) 2278 (badATErr (className clas) (tyConName fam_tc)) 2279 2280 ; check_match arg_triples 2281 } 2282 where 2283 (ax_tvs, ax_arg_tys, _) = etaExpandCoAxBranch branch 2284 2285 arg_triples :: [(Type,Type, ArgFlag)] 2286 arg_triples = [ (cls_arg_ty, at_arg_ty, vis) 2287 | (fam_tc_tv, vis, at_arg_ty) 2288 <- zip3 (tyConTyVars fam_tc) 2289 (tyConArgFlags fam_tc ax_arg_tys) 2290 ax_arg_tys 2291 , Just cls_arg_ty <- [lookupVarEnv mini_env fam_tc_tv] ] 2292 2293 pp_wrong_at_arg vis 2294 = pprWithExplicitKindsWhen (isInvisibleArgFlag vis) $ 2295 vcat [ text "Type indexes must match class instance head" 2296 , text "Expected:" <+> pp_expected_ty 2297 , text " Actual:" <+> pp_actual_ty ] 2298 2299 -- Fiddling around to arrange that wildcards unconditionally print as "_" 2300 -- We only need to print the LHS, not the RHS at all 2301 -- See Note [Printing conflicts with class header] 2302 (tidy_env1, _) = tidyVarBndrs emptyTidyEnv inst_tvs 2303 (tidy_env2, _) = tidyCoAxBndrsForUser tidy_env1 (ax_tvs \\ inst_tvs) 2304 2305 pp_expected_ty = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc) $ 2306 toIfaceTcArgs fam_tc $ 2307 [ case lookupVarEnv mini_env at_tv of 2308 Just cls_arg_ty -> tidyType tidy_env2 cls_arg_ty 2309 Nothing -> mk_wildcard at_tv 2310 | at_tv <- tyConTyVars fam_tc ] 2311 2312 pp_actual_ty = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc) $ 2313 toIfaceTcArgs fam_tc $ 2314 tidyTypes tidy_env2 ax_arg_tys 2315 2316 mk_wildcard at_tv = mkTyVarTy (mkTyVar tv_name (tyVarKind at_tv)) 2317 tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "_") noSrcSpan 2318 2319 -- For check_match, bind_me, see 2320 -- Note [Matching in the consistent-instantation check] 2321 check_match :: [(Type,Type,ArgFlag)] -> TcM () 2322 check_match triples = go emptyTCvSubst emptyTCvSubst triples 2323 2324 go _ _ [] = return () 2325 go lr_subst rl_subst ((ty1,ty2,vis):triples) 2326 | Just lr_subst1 <- tcMatchTyX_BM bind_me lr_subst ty1 ty2 2327 , Just rl_subst1 <- tcMatchTyX_BM bind_me rl_subst ty2 ty1 2328 = go lr_subst1 rl_subst1 triples 2329 | otherwise 2330 = addErrTc (pp_wrong_at_arg vis) 2331 2332 -- The /scoped/ type variables from the class-instance header 2333 -- should not be alpha-renamed. Inferred ones can be. 2334 no_bind_set = mkVarSet inst_tvs 2335 bind_me tv | tv `elemVarSet` no_bind_set = Skolem 2336 | otherwise = BindMe 2337 2338 2339{- Note [Check type-family instance binders] 2340~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2341In a type family instance, we require (of course), type variables 2342used on the RHS are matched on the LHS. This is checked by 2343checkFamPatBinders. Here is an interesting example: 2344 2345 type family T :: k 2346 type instance T = (Nothing :: Maybe a) 2347 2348Upon a cursory glance, it may appear that the kind variable `a` is unbound 2349since there are no (visible) LHS patterns in `T`. However, there is an 2350*invisible* pattern due to the return kind, so inside of GHC, the instance 2351looks closer to this: 2352 2353 type family T @k :: k 2354 type instance T @(Maybe a) = (Nothing :: Maybe a) 2355 2356Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in 2357fact not unbound. Contrast that with this example (#13985) 2358 2359 type instance T = Proxy (Nothing :: Maybe a) 2360 2361This would looks like this inside of GHC: 2362 2363 type instance T @(*) = Proxy (Nothing :: Maybe a) 2364 2365So this time, `a` is neither bound by a visible nor invisible type pattern on 2366the LHS, so `a` would be reported as not in scope. 2367 2368Finally, here's one more brain-teaser (from #9574). In the example below: 2369 2370 class Funct f where 2371 type Codomain f :: * 2372 instance Funct ('KProxy :: KProxy o) where 2373 type Codomain 'KProxy = NatTr (Proxy :: o -> *) 2374 2375As it turns out, `o` is in scope in this example. That is because `o` is 2376bound by the kind signature of the LHS type pattern 'KProxy. To make this more 2377obvious, one can also write the instance like so: 2378 2379 instance Funct ('KProxy :: KProxy o) where 2380 type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *) 2381 2382Note [Dodgy binding sites in type family instances] 2383~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2384Consider the following example (from #7536): 2385 2386 type T a = Int 2387 type instance F (T a) = a 2388 2389This `F` instance is extremely fishy, since the RHS, `a`, purports to be 2390"bound" by the LHS pattern `T a`. "Bound" has scare quotes around it because 2391`T a` expands to `Int`, which doesn't mention at all, so it's as if one had 2392actually written: 2393 2394 type instance F Int = a 2395 2396That is clearly bogus, so to reject this, we check that every type variable 2397that is mentioned on the RHS is /actually/ bound on the LHS. In other words, 2398we need to do something slightly more sophisticated that just compute the free 2399variables of the LHS patterns. 2400 2401It's tempting to just expand all type synonyms on the LHS and then compute 2402their free variables, but even that isn't sophisticated enough. After all, 2403an impish user could write the following (#17008): 2404 2405 type family ConstType (a :: Type) :: Type where 2406 ConstType _ = Type 2407 2408 type family F (x :: ConstType a) :: Type where 2409 F (x :: ConstType a) = a 2410 2411Just like in the previous example, the `a` on the RHS isn't actually bound 2412on the LHS, but this time a type family is responsible for the deception, not 2413a type synonym. 2414 2415We avoid both issues by requiring that all RHS type variables are mentioned 2416in injective positions on the left-hand side (by way of 2417`injectiveVarsOfTypes`). For instance, the `a` in `T a` is not in an injective 2418position, as `T` is not an injective type constructor, so we do not count that. 2419Similarly for the `a` in `ConstType a`. 2420 2421Note [Matching in the consistent-instantation check] 2422~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2423Matching the class-instance header to family-instance tyvars is 2424tricker than it sounds. Consider (#13972) 2425 class C (a :: k) where 2426 type T k :: Type 2427 instance C Left where 2428 type T (a -> Either a b) = Int 2429 2430Here there are no lexically-scoped variables from (C Left). 2431Yet the real class-instance header is C @(p -> Either @p @q)) (Left @p @q) 2432while the type-family instance is T (a -> Either @a @b) 2433So we allow alpha-renaming of variables that don't come 2434from the class-instance header. 2435 2436We track the lexically-scoped type variables from the 2437class-instance header in ai_tyvars. 2438 2439Here's another example (#14045a) 2440 class C (a :: k) where 2441 data S (a :: k) 2442 instance C (z :: Bool) where 2443 data S :: Bool -> Type where 2444 2445Again, there is no lexical connection, but we will get 2446 class-instance header: C @Bool (z::Bool) 2447 family instance S @Bool (a::Bool) 2448 2449When looking for mis-matches, we check left-to-right, 2450kinds first. If we look at types first, we'll fail to 2451suggest -fprint-explicit-kinds for a mis-match with 2452 T @k vs T @Type 2453somewhere deep inside the type 2454 2455Note [Checking consistent instantiation] 2456~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2457See #11450 for background discussion on this check. 2458 2459 class C a b where 2460 type T a x b 2461 2462With this class decl, if we have an instance decl 2463 instance C ty1 ty2 where ... 2464then the type instance must look like 2465 type T ty1 v ty2 = ... 2466with exactly 'ty1' for 'a', 'ty2' for 'b', and some type 'v' for 'x'. 2467For example: 2468 2469 instance C [p] Int 2470 type T [p] y Int = (p,y,y) 2471 2472Note that 2473 2474* We used to allow completely different bound variables in the 2475 associated type instance; e.g. 2476 instance C [p] Int 2477 type T [q] y Int = ... 2478 But from GHC 8.2 onwards, we don't. It's much simpler this way. 2479 See #11450. 2480 2481* When the class variable isn't used on the RHS of the type instance, 2482 it's tempting to allow wildcards, thus 2483 instance C [p] Int 2484 type T [_] y Int = (y,y) 2485 But it's awkward to do the test, and it doesn't work if the 2486 variable is repeated: 2487 instance C (p,p) Int 2488 type T (_,_) y Int = (y,y) 2489 Even though 'p' is not used on the RHS, we still need to use 'p' 2490 on the LHS to establish the repeated pattern. So to keep it simple 2491 we just require equality. 2492 2493* For variables in associated type families that are not bound by the class 2494 itself, we do _not_ check if they are over-specific. In other words, 2495 it's perfectly acceptable to have an instance like this: 2496 2497 instance C [p] Int where 2498 type T [p] (Maybe x) Int = x 2499 2500 While the first and third arguments to T are required to be exactly [p] and 2501 Int, respectively, since they are bound by C, the second argument is allowed 2502 to be more specific than just a type variable. Furthermore, it is permissible 2503 to define multiple equations for T that differ only in the non-class-bound 2504 argument: 2505 2506 instance C [p] Int where 2507 type T [p] (Maybe x) Int = x 2508 type T [p] (Either x y) Int = x -> y 2509 2510 We once considered requiring that non-class-bound variables in associated 2511 type family instances be instantiated with distinct type variables. However, 2512 that requirement proved too restrictive in practice, as there were examples 2513 of extremely simple associated type family instances that this check would 2514 reject, and fixing them required tiresome boilerplate in the form of 2515 auxiliary type families. For instance, you would have to define the above 2516 example as: 2517 2518 instance C [p] Int where 2519 type T [p] x Int = CAux x 2520 2521 type family CAux x where 2522 CAux (Maybe x) = x 2523 CAux (Either x y) = x -> y 2524 2525 We decided that this restriction wasn't buying us much, so we opted not 2526 to pursue that design (see also GHC #13398). 2527 2528Implementation 2529 * Form the mini-envt from the class type variables a,b 2530 to the instance decl types [p],Int: [a->[p], b->Int] 2531 2532 * Look at the tyvars a,x,b of the type family constructor T 2533 (it shares tyvars with the class C) 2534 2535 * Apply the mini-evnt to them, and check that the result is 2536 consistent with the instance types [p] y Int. (where y can be any type, as 2537 it is not scoped over the class type variables. 2538 2539We make all the instance type variables scope over the 2540type instances, of course, which picks up non-obvious kinds. Eg 2541 class Foo (a :: k) where 2542 type F a 2543 instance Foo (b :: k -> k) where 2544 type F b = Int 2545Here the instance is kind-indexed and really looks like 2546 type F (k->k) (b::k->k) = Int 2547But if the 'b' didn't scope, we would make F's instance too 2548poly-kinded. 2549 2550Note [Printing conflicts with class header] 2551~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2552It's remarkably painful to give a decent error message for conflicts 2553with the class header. Consider 2554 clase C b where 2555 type F a b c 2556 instance C [b] where 2557 type F x Int _ _ = ... 2558 2559Here we want to report a conflict between 2560 Expected: F _ [b] _ 2561 Actual: F x Int _ _ 2562 2563But if the type instance shadows the class variable like this 2564(rename/should_fail/T15828): 2565 instance C [b] where 2566 type forall b. F x (Tree b) _ _ = ... 2567 2568then we must use a fresh variable name 2569 Expected: F _ [b] _ 2570 Actual: F x [b1] _ _ 2571 2572Notice that: 2573 - We want to print an underscore in the "Expected" type in 2574 positions where the class header has no influence over the 2575 parameter. Hence the fancy footwork in pp_expected_ty 2576 2577 - Although the binders in the axiom are aready tidy, we must 2578 re-tidy them to get a fresh variable name when we shadow 2579 2580 - The (ax_tvs \\ inst_tvs) is to avoid tidying one of the 2581 class-instance variables a second time, from 'a' to 'a1' say. 2582 Remember, the ax_tvs of the axiom share identity with the 2583 class-instance variables, inst_tvs.. 2584 2585 - We use tidyCoAxBndrsForUser to get underscores rather than 2586 _1, _2, etc in the axiom tyvars; see the definition of 2587 tidyCoAxBndrsForUser 2588 2589This all seems absurdly complicated. 2590 2591Note [Unused explicitly bound variables in a family pattern] 2592~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2593 2594Why is 'unusedExplicitForAllErr' not just a warning? 2595 2596Consider the following examples: 2597 2598 type instance F a = Maybe b 2599 type instance forall b. F a = Bool 2600 type instance forall b. F a = Maybe b 2601 2602In every case, b is a type variable not determined by the LHS pattern. The 2603first is caught by the renamer, but we catch the last two here. Perhaps one 2604could argue that the second should be accepted, albeit with a warning, but 2605consider the fact that in a type family instance, there is no way to interact 2606with such a varable. At least with @x :: forall a. Int@ we can use visibile 2607type application, like @x \@Bool 1@. (Of course it does nothing, but it is 2608permissible.) In the type family case, the only sensible explanation is that 2609the user has made a mistake -- thus we throw an error. 2610 2611Note [Oversaturated type family equations] 2612~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2613Type family tycons have very rigid arities. We want to reject something like 2614this: 2615 2616 type family Foo :: Type -> Type where 2617 Foo x = ... 2618 2619Because Foo has arity zero (i.e., it doesn't bind anything to the left of the 2620double colon), we want to disallow any equation for Foo that has more than zero 2621arguments, such as `Foo x = ...`. The algorithm here is pretty simple: if an 2622equation has more arguments than the arity of the type family, reject. 2623 2624Things get trickier when visible kind application enters the picture. Consider 2625the following example: 2626 2627 type family Bar (x :: j) :: forall k. Either j k where 2628 Bar 5 @Symbol = ... 2629 2630The arity of Bar is two, since it binds two variables, `j` and `x`. But even 2631though Bar's equation has two arguments, it's still invalid. Imagine the same 2632equation in Core: 2633 2634 Bar Nat 5 Symbol = ... 2635 2636Here, it becomes apparent that Bar is actually taking /three/ arguments! So 2637we can't just rely on a simple counting argument to reject 2638`Bar 5 @Symbol = ...`, since it only has two user-written arguments. 2639Moreover, there's one explicit argument (5) and one visible kind argument 2640(@Symbol), which matches up perfectly with the fact that Bar has one required 2641binder (x) and one specified binder (j), so that's not a valid way to detect 2642oversaturation either. 2643 2644To solve this problem in a robust way, we do the following: 2645 26461. When kind-checking, we count the number of user-written *required* 2647 arguments and check if there is an equal number of required tycon binders. 2648 If not, reject. (See `wrongNumberOfParmsErr` in TcTyClsDecls.) 2649 2650 We perform this step during kind-checking, not during validity checking, 2651 since we can give better error messages if we catch it early. 26522. When validity checking, take all of the (Core) type patterns from on 2653 equation, drop the first n of them (where n is the arity of the type family 2654 tycon), and check if there are any types leftover. If so, reject. 2655 2656 Why does this work? We know that after dropping the first n type patterns, 2657 none of the leftover types can be required arguments, since step (1) would 2658 have already caught that. Moreover, the only places where visible kind 2659 applications should be allowed are in the first n types, since those are the 2660 only arguments that can correspond to binding forms. Therefore, the 2661 remaining arguments must correspond to oversaturated uses of visible kind 2662 applications, which are precisely what we want to reject. 2663 2664Note that we only perform this check for type families, and not for data 2665families. This is because it is perfectly acceptable to oversaturate data 2666family instance equations: see Note [Arity of data families] in FamInstEnv. 2667 2668************************************************************************ 2669* * 2670 Telescope checking 2671* * 2672************************************************************************ 2673 2674Note [Bad TyCon telescopes] 2675~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2676Now that we can mix type and kind variables, there are an awful lot of 2677ways to shoot yourself in the foot. Here are some. 2678 2679 data SameKind :: k -> k -> * -- just to force unification 2680 26811. data T1 a k (b :: k) (x :: SameKind a b) 2682 2683The problem here is that we discover that a and b should have the same 2684kind. But this kind mentions k, which is bound *after* a. 2685(Testcase: dependent/should_fail/BadTelescope) 2686 26872. data T2 a (c :: Proxy b) (d :: Proxy a) (x :: SameKind b d) 2688 2689Note that b is not bound. Yet its kind mentions a. Because we have 2690a nice rule that all implicitly bound variables come before others, 2691this is bogus. 2692 2693To catch these errors, we call checkTyConTelescope during kind-checking 2694datatype declarations. This checks for 2695 2696* Ill-scoped binders. From (1) and (2) above we can get putative 2697 kinds like 2698 T1 :: forall (a:k) (k:*) (b:k). SameKind a b -> * 2699 where 'k' is mentioned a's kind before k is bound 2700 2701 This is easy to check for: just look for 2702 out-of-scope variables in the kind 2703 2704* We should arguably also check for ambiguous binders 2705 but we don't. See Note [Ambiguous kind vars]. 2706 2707See also 2708 * Note [Required, Specified, and Inferred for types] in TcTyClsDecls. 2709 * Note [Keeping scoped variables in order: Explicit] discusses how 2710 this check works for `forall x y z.` written in a type. 2711 2712Note [Ambiguous kind vars] 2713~~~~~~~~~~~~~~~~~~~~~~~~~~ 2714We used to be concerned about ambiguous binders. Suppose we have the kind 2715 S1 :: forall k -> * -> * 2716 S2 :: forall k. * -> * 2717Here S1 is OK, because k is Required, and at a use of S1 we will 2718see (S1 *) or (S1 (*->*)) or whatever. 2719 2720But S2 is /not/ OK because 'k' is Specfied (and hence invisible) and 2721we have no way (ever) to figure out how 'k' should be instantiated. 2722For example if we see (S2 Int), that tells us nothing about k's 2723instantiation. (In this case we'll instantiate it to Any, but that 2724seems wrong.) This is really the same test as we make for ambiguous 2725type in term type signatures. 2726 2727Now, it's impossible for a Specified variable not to occur 2728at all in the kind -- after all, it is Specified so it must have 2729occurred. (It /used/ to be possible; see tests T13983 and T7873. But 2730with the advent of the forall-or-nothing rule for kind variables, 2731those strange cases went away.) 2732 2733But one might worry about 2734 type v k = * 2735 S3 :: forall k. V k -> * 2736which appears to mention 'k' but doesn't really. Or 2737 S4 :: forall k. F k -> * 2738where F is a type function. But we simply don't check for 2739those cases of ambiguity, yet anyway. The worst that can happen 2740is ambiguity at the call sites. 2741 2742Historical note: this test used to be called reportFloatingKvs. 2743-} 2744 2745-- | Check a list of binders to see if they make a valid telescope. 2746-- See Note [Bad TyCon telescopes] 2747type TelescopeAcc 2748 = ( TyVarSet -- Bound earlier in the telescope 2749 , Bool -- At least one binder occurred (in a kind) before 2750 -- it was bound in the telescope. E.g. 2751 ) -- T :: forall (a::k) k. blah 2752 2753checkTyConTelescope :: TyCon -> TcM () 2754checkTyConTelescope tc 2755 | bad_scope 2756 = -- See "Ill-scoped binders" in Note [Bad TyCon telescopes] 2757 addErr $ 2758 vcat [ hang (text "The kind of" <+> quotes (ppr tc) <+> text "is ill-scoped") 2759 2 pp_tc_kind 2760 , extra 2761 , hang (text "Perhaps try this order instead:") 2762 2 (pprTyVars sorted_tvs) ] 2763 2764 | otherwise 2765 = return () 2766 where 2767 tcbs = tyConBinders tc 2768 tvs = binderVars tcbs 2769 sorted_tvs = scopedSort tvs 2770 2771 (_, bad_scope) = foldl add_one (emptyVarSet, False) tcbs 2772 2773 add_one :: TelescopeAcc -> TyConBinder -> TelescopeAcc 2774 add_one (bound, bad_scope) tcb 2775 = ( bound `extendVarSet` tv 2776 , bad_scope || not (isEmptyVarSet (fkvs `minusVarSet` bound)) ) 2777 where 2778 tv = binderVar tcb 2779 fkvs = tyCoVarsOfType (tyVarKind tv) 2780 2781 inferred_tvs = [ binderVar tcb 2782 | tcb <- tcbs, Inferred == tyConBinderArgFlag tcb ] 2783 specified_tvs = [ binderVar tcb 2784 | tcb <- tcbs, Specified == tyConBinderArgFlag tcb ] 2785 2786 pp_inf = parens (text "namely:" <+> pprTyVars inferred_tvs) 2787 pp_spec = parens (text "namely:" <+> pprTyVars specified_tvs) 2788 2789 pp_tc_kind = text "Inferred kind:" <+> ppr tc <+> dcolon <+> ppr_untidy (tyConKind tc) 2790 ppr_untidy ty = pprIfaceType (toIfaceType ty) 2791 -- We need ppr_untidy here because pprType will tidy the type, which 2792 -- will turn the bogus kind we are trying to report 2793 -- T :: forall (a::k) k (b::k) -> blah 2794 -- into a misleadingly sanitised version 2795 -- T :: forall (a::k) k1 (b::k1) -> blah 2796 2797 extra 2798 | null inferred_tvs && null specified_tvs 2799 = empty 2800 | null inferred_tvs 2801 = hang (text "NB: Specified variables") 2802 2 (sep [pp_spec, text "always come first"]) 2803 | null specified_tvs 2804 = hang (text "NB: Inferred variables") 2805 2 (sep [pp_inf, text "always come first"]) 2806 | otherwise 2807 = hang (text "NB: Inferred variables") 2808 2 (vcat [ sep [ pp_inf, text "always come first"] 2809 , sep [text "then Specified variables", pp_spec]]) 2810 2811{- 2812************************************************************************ 2813* * 2814\subsection{Auxiliary functions} 2815* * 2816************************************************************************ 2817-} 2818 2819-- Free variables of a type, retaining repetitions, and expanding synonyms 2820-- This ignores coercions, as coercions aren't user-written 2821fvType :: Type -> [TyCoVar] 2822fvType ty | Just exp_ty <- tcView ty = fvType exp_ty 2823fvType (TyVarTy tv) = [tv] 2824fvType (TyConApp _ tys) = fvTypes tys 2825fvType (LitTy {}) = [] 2826fvType (AppTy fun arg) = fvType fun ++ fvType arg 2827fvType (FunTy _ arg res) = fvType arg ++ fvType res 2828fvType (ForAllTy (Bndr tv _) ty) 2829 = fvType (tyVarKind tv) ++ 2830 filter (/= tv) (fvType ty) 2831fvType (CastTy ty _) = fvType ty 2832fvType (CoercionTy {}) = [] 2833 2834fvTypes :: [Type] -> [TyVar] 2835fvTypes tys = concat (map fvType tys) 2836 2837sizeType :: Type -> Int 2838-- Size of a type: the number of variables and constructors 2839sizeType ty | Just exp_ty <- tcView ty = sizeType exp_ty 2840sizeType (TyVarTy {}) = 1 2841sizeType (TyConApp tc tys) = 1 + sizeTyConAppArgs tc tys 2842sizeType (LitTy {}) = 1 2843sizeType (AppTy fun arg) = sizeType fun + sizeType arg 2844sizeType (FunTy _ arg res) = sizeType arg + sizeType res + 1 2845sizeType (ForAllTy _ ty) = sizeType ty 2846sizeType (CastTy ty _) = sizeType ty 2847sizeType (CoercionTy _) = 0 2848 2849sizeTypes :: [Type] -> Int 2850sizeTypes = foldr ((+) . sizeType) 0 2851 2852sizeTyConAppArgs :: TyCon -> [Type] -> Int 2853sizeTyConAppArgs _tc tys = sizeTypes tys -- (filterOutInvisibleTypes tc tys) 2854 -- See Note [Invisible arguments and termination] 2855 2856-- Size of a predicate 2857-- 2858-- We are considering whether class constraints terminate. 2859-- Equality constraints and constraints for the implicit 2860-- parameter class always terminate so it is safe to say "size 0". 2861-- See #4200. 2862sizePred :: PredType -> Int 2863sizePred ty = goClass ty 2864 where 2865 goClass p = go (classifyPredType p) 2866 2867 go (ClassPred cls tys') 2868 | isTerminatingClass cls = 0 2869 | otherwise = sizeTypes (filterOutInvisibleTypes (classTyCon cls) tys') 2870 -- The filtering looks bogus 2871 -- See Note [Invisible arguments and termination] 2872 go (EqPred {}) = 0 2873 go (IrredPred ty) = sizeType ty 2874 go (ForAllPred _ _ pred) = goClass pred 2875 2876-- | When this says "True", ignore this class constraint during 2877-- a termination check 2878isTerminatingClass :: Class -> Bool 2879isTerminatingClass cls 2880 = isIPClass cls -- Implicit parameter constraints always terminate because 2881 -- there are no instances for them --- they are only solved 2882 -- by "local instances" in expressions 2883 || isEqPredClass cls 2884 || cls `hasKey` typeableClassKey 2885 || cls `hasKey` coercibleTyConKey 2886 2887-- | Tidy before printing a type 2888ppr_tidy :: TidyEnv -> Type -> SDoc 2889ppr_tidy env ty = pprType (tidyType env ty) 2890 2891allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool 2892-- (allDistinctTyVars tvs tys) returns True if tys are 2893-- a) all tyvars 2894-- b) all distinct 2895-- c) disjoint from tvs 2896allDistinctTyVars _ [] = True 2897allDistinctTyVars tkvs (ty : tys) 2898 = case getTyVar_maybe ty of 2899 Nothing -> False 2900 Just tv | tv `elemVarSet` tkvs -> False 2901 | otherwise -> allDistinctTyVars (tkvs `extendVarSet` tv) tys 2902