TcValidity.hs 56.8 KB
 Austin Seipp committed Dec 03, 2014 1 2 3 4 {- (c) The University of Glasgow 2006 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 -}  Simon Peyton Jones committed Mar 13, 2013 5   Herbert Valerio Riedel committed May 15, 2014 6 7 {-# LANGUAGE CPP #-}  Simon Peyton Jones committed Mar 13, 2013 8 9 module TcValidity ( Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,  Austin Seipp committed Dec 03, 2014 10  expectedKindInCtxt,  Simon Peyton Jones committed Mar 13, 2013 11  checkValidTheta, checkValidFamPats,  Simon Peyton Jones committed Apr 30, 2013 12  checkValidInstance, validDerivPred,  Jan Stolarek committed Sep 03, 2015 13  checkInstTermination,  eir@cis.upenn.edu committed Sep 19, 2015 14  ClsInfo, checkValidCoAxiom, checkValidCoAxBranch,  eir@cis.upenn.edu committed Sep 21, 2015 15  checkValidTyFamEqn,  Simon Peyton Jones committed Jun 02, 2015 16  checkConsistentFamInst,  Simon Peyton Jones committed Mar 13, 2013 17 18 19 20 21 22  arityErr, badATErr ) where #include "HsVersions.h" -- friends:  Simon Peyton Jones committed Nov 21, 2014 23 import TcUnify ( tcSubType_NC )  Simon Peyton Jones committed Oct 03, 2013 24 import TcSimplify ( simplifyAmbiguityCheck )  Simon Peyton Jones committed Mar 13, 2013 25 26 27 import TypeRep import TcType import TcMType  Simon Peyton Jones committed Jun 18, 2015 28 import TysWiredIn ( coercibleClass, eqTyCon )  Simon Peyton Jones committed May 18, 2015 29 import PrelNames  Simon Peyton Jones committed Mar 13, 2013 30 31 32 33 34 35 36 37 38 39 40 import Type import Unify( tcMatchTyX ) import Kind import CoAxiom import Class import TyCon -- others: import HsSyn -- HsType import TcRnMonad -- TcType, amongst others import FunDeps  Jan Stolarek committed Sep 03, 2015 41 42 43 import FamInstEnv ( isDominatedBy, injectiveBranches, InjectivityCheckResult(..) ) import FamInst ( makeInjectivityErrors )  Simon Peyton Jones committed Mar 13, 2013 44 45 46 47 48 49 50 51 52 53 54 55 import Name import VarEnv import VarSet import ErrUtils import DynFlags import Util import ListSetOps import SrcLoc import Outputable import FastString import Control.Monad  Icelandjack committed Feb 13, 2014 56 import Data.Maybe  Simon Peyton Jones committed Mar 13, 2013 57 58 import Data.List ( (\\) )  Austin Seipp committed Dec 03, 2014 59 60 61 {- ************************************************************************ * *  Simon Peyton Jones committed Mar 13, 2013 62  Checking for ambiguity  Austin Seipp committed Dec 03, 2014 63 64 * * ************************************************************************  Simon Peyton Jones committed Mar 04, 2015 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133  Note [The ambiguity check for type signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ checkAmbiguity is a check on *user-supplied type signatures*. It is *purely* there to report functions that cannot possibly be called. So for example we want to reject: f :: C a => Int The idea is there can be no legal calls to 'f' because every call will give rise to an ambiguous constraint. We could soundly omit the ambiguity check on type signatures entirely, at the expense of delaying ambiguity errors to call sites. Indeed, the flag -XAllowAmbiguousTypes switches off the ambiguity check. What about things like this: class D a b | a -> b where .. h :: D Int b => Int The Int may well fix 'b' at the call site, so that signature should not be rejected. Moreover, using *visible* fundeps is too conservative. Consider class X a b where ... class D a b | a -> b where ... instance D a b => X [a] b where... h :: X a b => a -> a Here h's type looks ambiguous in 'b', but here's a legal call: ...(h [True])... That gives rise to a (X [Bool] beta) constraint, and using the instance means we need (D Bool beta) and that fixes 'beta' via D's fundep! Behind all these special cases there is a simple guiding principle. Consider f :: f = ...blah... g :: g = f You would think that the definition of g would surely typecheck! After all f has exactly the same type, and g=f. But in fact f's type is instantiated and the instantiated constraints are solved against the originals, so in the case an ambiguous type it won't work. Consider our earlier example f :: C a => Int. Then in g's definition, we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a), and fail. So in fact we use this as our *definition* of ambiguity. We use a very similar test for *inferred* types, to ensure that they are unambiguous. See Note [Impedence matching] in TcBinds. This test is very conveniently implemented by calling tcSubType This neatly takes account of the functional dependecy stuff above, and implicit parameter (see Note [Implicit parameters and ambiguity]). And this is what checkAmbiguity does. What about this, though? g :: C [a] => Int Is every call to 'g' ambiguous? After all, we might have intance C [a] where ... at the call site. So maybe that type is ok! Indeed even f's quintessentially ambiguous type might, just possibly be callable: with -XFlexibleInstances we could have instance C a where ... and now a call could be legal after all! Well, we'll reject this unless the instance is available *here*. Note [When to call checkAmbiguity] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  eir@cis.upenn.edu committed Sep 19, 2015 134 We call checkAmbiguity  Simon Peyton Jones committed Mar 04, 2015 135 136 137 138  (a) on user-specified type signatures (b) in checkValidType Conncerning (b), you might wonder about nested foralls. What about  Simon Peyton Jones committed Jun 01, 2015 139  f :: forall b. (forall a. Eq a => b) -> b  Simon Peyton Jones committed Mar 04, 2015 140 The nested forall is ambiguous. Originally we called checkAmbiguity  Simon Peyton Jones committed Jun 01, 2015 141 142 143 144 145 146 147 148 in the forall case of check_type, but that had two bad consequences: * We got two error messages about (Eq b) in a nested forall like this: g :: forall a. Eq a => forall b. Eq b => a -> a * If we try to check for ambiguity of an nested forall like (forall a. Eq a => b), the implication constraint doesn't bind all the skolems, which results in "No skolem info" in error messages (see Trac #10432).  Simon Peyton Jones committed Mar 04, 2015 149 To avoid this, we call checkAmbiguity once, at the top, in checkValidType.  Simon Peyton Jones committed Jun 01, 2015 150 151 (I'm still a bit worried about unbound skolems when the type mentions in-scope type variables.)  Simon Peyton Jones committed Mar 04, 2015 152   Simon Peyton Jones committed Jun 01, 2015 153 In fact, because of the co/contra-variance implemented in tcSubType,  Simon Peyton Jones committed Mar 04, 2015 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 this *does* catch function f above. too. Concerning (a) the ambiguity check is only used for *user* types, not for types coming from inteface files. The latter can legitimately have ambiguous types. Example class S a where s :: a -> (Int,Int) instance S Char where s _ = (1,1) f:: S a => [a] -> Int -> (Int,Int) f (_::[a]) x = (a*x,b) where (a,b) = s (undefined::a) Here the worker for f gets the type fw :: forall a. S a => Int -> (# Int, Int #) Note [Implicit parameters and ambiguity] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Only a *class* predicate can give rise to ambiguity An *implicit parameter* cannot. For example: foo :: (?x :: [a]) => Int foo = length ?x  Gabor Greif committed Jul 30, 2015 176 is fine. The call site will supply a particular 'x'  Simon Peyton Jones committed Mar 04, 2015 177 178 179 180 181 182 183 184 185 186 187  Furthermore, the type variables fixed by an implicit parameter propagate to the others. E.g. foo :: (Show a, ?x::[a]) => Int foo = show (?x++?x) The type of foo looks ambiguous. But it isn't, because at a call site we might have let ?x = 5::Int in foo and all is well. In effect, implicit parameters are, well, parameters, so we can take their type variables into account as part of the "tau-tvs" stuff. This is done in the function 'FunDeps.grow'.  Austin Seipp committed Dec 03, 2014 188 -}  Simon Peyton Jones committed Mar 13, 2013 189 190 191  checkAmbiguity :: UserTypeCtxt -> Type -> TcM () checkAmbiguity ctxt ty  Simon Peyton Jones committed May 28, 2013 192 193 194 195 196  | GhciCtxt <- ctxt -- Allow ambiguous types in GHCi's :kind command = return () -- E.g. type family T a :: * -- T :: forall k. k -> * -- Then :k T should work in GHCi, not complain that -- (T k) is ambiguous!  Simon Peyton Jones committed Jun 11, 2014 197  | InfSigCtxt {} <- ctxt -- See Note [Validity of inferred types] in TcBinds  Austin Seipp committed Dec 03, 2014 198  = return ()  Simon Peyton Jones committed Jun 11, 2014 199   Simon Peyton Jones committed May 28, 2013 200  | otherwise  Simon Peyton Jones committed Oct 03, 2013 201  = do { traceTc "Ambiguity check for" (ppr ty)  202 203  ; let free_tkvs = varSetElemsKvsFirst (closeOverKinds (tyVarsOfType ty)) ; (subst, _tvs) <- tcInstSkolTyVars free_tkvs  Simon Peyton Jones committed Oct 03, 2013 204  ; let ty' = substTy subst ty  205 206 207  -- The type might have free TyVars, esp when the ambiguity check -- happens during a call to checkValidType, -- so we skolemise them as TcTyVars.  Simon Peyton Jones committed Mar 13, 2013 208  -- Tiresome; but the type inference engine expects TcTyVars  209 210 211  -- NB: The free tyvar might be (a::k), so k is also free -- and we must skolemise it as well. Hence closeOverKinds. -- (Trac #9222)  Simon Peyton Jones committed Mar 13, 2013 212 213  -- Solve the constraints eagerly because an ambiguous type  Simon Peyton Jones committed Oct 03, 2013 214  -- can cause a cascade of further errors. Since the free  Simon Peyton Jones committed Sep 04, 2013 215  -- tyvars are skolemised, we can safely use tcSimplifyTop  Simon Peyton Jones committed Oct 03, 2013 216 217  ; (_wrap, wanted) <- addErrCtxtM (mk_msg ty') $captureConstraints$  Simon Peyton Jones committed Nov 21, 2014 218  tcSubType_NC ctxt ty' ty'  eir@cis.upenn.edu committed Sep 21, 2015 219 220 221 222 223  ; whenNoErrs \$ -- only run the simplifier if we have a clean -- environment. Otherwise we might trip. -- example: indexed-types/should_fail/BadSock -- fails in DEBUG mode without this simplifyAmbiguityCheck ty wanted  Simon Peyton Jones committed Sep 04, 2013 224   Simon Peyton Jones committed Oct 03, 2013 225  ; traceTc "Done ambiguity check for" (ppr ty) }  Simon Peyton Jones committed Mar 13, 2013 226  where  Simon Peyton Jones committed Oct 03, 2013 227 228  mk_msg ty tidy_env = do { allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes  Simon Peyton Jones committed Nov 21, 2014 229 230  ; (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env ty ; return (tidy_env', mk_msg tidy_ty $$ppWhen (not allow_ambiguous) ambig_msg) }  Simon Peyton Jones committed Mar 13, 2013 231  where  Simon Peyton Jones committed Nov 21, 2014 232  mk_msg ty = pprSigCtxt ctxt (ptext (sLit "the ambiguity check for")) (ppr ty)  Simon Peyton Jones committed Oct 03, 2013 233  ambig_msg = ptext (sLit "To defer the ambiguity check to use sites, enable AllowAmbiguousTypes")  Simon Peyton Jones committed Mar 13, 2013 234   Iavor S. Diatchki committed Nov 16, 2015 235 236 237 238 239 240 241 242 243 244  checkUserTypeError :: Type -> TcM () checkUserTypeError = check where check ty | Just (_,msg) <- isUserErrorTy ty = failWithTc (pprUserTypeErrorTy msg) | Just (_,ts) <- splitTyConApp_maybe ty = mapM_ check ts | Just (t1,t2) <- splitAppTy_maybe ty = check t1 >> check t2 | otherwise = return ()  Austin Seipp committed Dec 03, 2014 245 246 247 {- ************************************************************************ * *  Simon Peyton Jones committed Mar 13, 2013 248  Checking validity of a user-defined type  Austin Seipp committed Dec 03, 2014 249 250 * * ************************************************************************  Simon Peyton Jones committed Mar 13, 2013 251 252  When dealing with a user-written type, we first translate it from an HsType  Austin Seipp committed Dec 03, 2014 253 to a Type, performing kind checking, and then check various things that should  Simon Peyton Jones committed Mar 13, 2013 254 255 256 be true about it. We don't want to perform these checks at the same time as the initial translation because (a) they are unnecessary for interface-file types and (b) when checking a mutually recursive group of type and class decls,  Gabor Greif committed Mar 18, 2015 257 we can't "look" at the tycons/classes yet. Also, the checks are rather  Simon Peyton Jones committed Mar 13, 2013 258 259 diverse, and used to really mess up the other code.  Austin Seipp committed Dec 03, 2014 260 One thing we check for is 'rank'.  Simon Peyton Jones committed Mar 13, 2013 261 262 263 264 265 266 267 268 269 270 271  Rank 0: monotypes (no foralls) Rank 1: foralls at the front only, Rank 0 inside Rank 2: foralls at the front, Rank 1 on left of fn arrow, basic ::= tyvar | T basic ... basic r2 ::= forall tvs. cxt => r2a r2a ::= r1 -> r2a | basic r1 ::= forall tvs. cxt => r0 r0 ::= r0 -> r0 | basic  Austin Seipp committed Dec 03, 2014 272 273  Another thing is to check that type synonyms are saturated.  Simon Peyton Jones committed Mar 13, 2013 274 275 276 277 This might not necessarily show up in kind checking. type A i = i data T k = MkT (k Int) f :: T A -- BAD!  Austin Seipp committed Dec 03, 2014 278 -}  Simon Peyton Jones committed Mar 13, 2013 279 280 281 282  checkValidType :: UserTypeCtxt -> Type -> TcM () -- Checks that the type is valid for the given context -- Not used for instance decls; checkValidInstance instead  Austin Seipp committed Dec 03, 2014 283 checkValidType ctxt ty  Simon Peyton Jones committed Mar 13, 2013 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299  = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty)) ; rankn_flag <- xoptM Opt_RankNTypes ; let gen_rank :: Rank -> Rank gen_rank r | rankn_flag = ArbitraryRank | otherwise = r rank1 = gen_rank r1 rank0 = gen_rank r0 r0 = rankZeroMonoType r1 = LimitedRank True r0 rank = case ctxt of DefaultDeclCtxt-> MustBeMonoType ResSigCtxt -> MustBeMonoType  Simon Peyton Jones committed Nov 21, 2014 300  PatSigCtxt -> rank0  Simon Peyton Jones committed Mar 13, 2013 301 302 303  RuleSigCtxt _ -> rank1 TySynCtxt _ -> rank0  Simon Peyton Jones committed Aug 05, 2015 304 305 306 307  ExprSigCtxt -> rank1 FunSigCtxt {} -> rank1 InfSigCtxt _ -> ArbitraryRank -- Inferred type ConArgCtxt _ -> rank1 -- We are given the type of the entire  Simon Peyton Jones committed Mar 13, 2013 308 309 310 311 312 313 314 315 316 317 318 319  -- constructor, hence rank 1 ForSigCtxt _ -> rank1 SpecInstCtxt -> rank1 ThBrackCtxt -> rank1 GhciCtxt -> ArbitraryRank _ -> panic "checkValidType" -- Can't happen; not used for *user* sigs -- Check the internal validity of the type itself ; check_type ctxt rank ty  Simon Peyton Jones committed Nov 27, 2014 320 321 322  -- Check that the thing has kind Type, and is lifted if necessary. -- Do this *after* check_type, because we can't usefully take -- the kind of an ill-formed type such as (a~Int)  Simon Peyton Jones committed Sep 04, 2013 323  ; check_kind ctxt ty  Simon Peyton Jones committed Nov 27, 2014 324   Iavor S. Diatchki committed Nov 16, 2015 325 326  ; checkUserTypeError ty  Simon Peyton Jones committed Mar 04, 2015 327  -- Check for ambiguous types. See Note [When to call checkAmbiguity]  Simon Peyton Jones committed Mar 04, 2015 328 329  -- NB: this will happen even for monotypes, but that should be cheap; -- and there may be nested foralls for the subtype test to examine  Simon Peyton Jones committed Mar 04, 2015 330 331  ; checkAmbiguity ctxt ty  Simon Peyton Jones committed Sep 04, 2013 332  ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }  Simon Peyton Jones committed Mar 13, 2013 333 334 335 336 337 338 339 340 341  checkValidMonoType :: Type -> TcM () checkValidMonoType ty = check_mono_type SigmaCtxt MustBeMonoType ty check_kind :: UserTypeCtxt -> TcType -> TcM () -- Check that the type's kind is acceptable for the context check_kind ctxt ty | TySynCtxt {} <- ctxt  Simon Peyton Jones committed Nov 27, 2014 342  , returnsConstraintKind actual_kind  Simon Peyton Jones committed Mar 13, 2013 343  = do { ck <- xoptM Opt_ConstraintKinds  Simon Peyton Jones committed Nov 27, 2014 344 345 346 347 348  ; if ck then when (isConstraintKind actual_kind) (do { dflags <- getDynFlags ; check_pred_ty dflags ctxt ty }) else addErrTc (constraintSynErr actual_kind) }  Simon Peyton Jones committed Mar 13, 2013 349 350 351 352 353 354 355 356 357 358 359 360  | Just k <- expectedKindInCtxt ctxt = checkTc (tcIsSubKind actual_kind k) (kindErr actual_kind) | otherwise = return () -- Any kind will do where actual_kind = typeKind ty -- Depending on the context, we might accept any kind (for instance, in a TH -- splice), or only certain kinds (like in type signatures). expectedKindInCtxt :: UserTypeCtxt -> Maybe Kind  kanetw committed Oct 20, 2015 361 362 363 364 365 366 367 368 369 370 expectedKindInCtxt (TySynCtxt _) = Nothing -- Any kind will do expectedKindInCtxt ThBrackCtxt = Nothing expectedKindInCtxt GhciCtxt = Nothing -- The types in a 'default' decl can have varying kinds -- See Note [Extended defaults]" in TcEnv expectedKindInCtxt DefaultDeclCtxt = Nothing expectedKindInCtxt (ForSigCtxt _) = Just liftedTypeKind expectedKindInCtxt InstDeclCtxt = Just constraintKind expectedKindInCtxt SpecInstCtxt = Just constraintKind expectedKindInCtxt _ = Just openTypeKind  Simon Peyton Jones committed Mar 13, 2013 371   Austin Seipp committed Dec 03, 2014 372 {-  Simon Peyton Jones committed Mar 13, 2013 373 374 Note [Higher rank types] ~~~~~~~~~~~~~~~~~~~~~~~~  Austin Seipp committed Dec 03, 2014 375 Technically  Simon Peyton Jones committed Mar 13, 2013 376 377 378 379  Int -> forall a. a->a is still a rank-1 type, but it's not Haskell 98 (Trac #5957). So the validity checker allow a forall after an arrow only if we allow it before -- that is, with Rank2Types or RankNTypes  Austin Seipp committed Dec 03, 2014 380 -}  Simon Peyton Jones committed Mar 13, 2013 381 382 383 384 385 386 387 388  data Rank = ArbitraryRank -- Any rank ok | LimitedRank -- Note [Higher rank types] Bool -- Forall ok at top Rank -- Use for function arguments | MonoType SDoc -- Monotype, with a suggestion of how it could be a polytype  Austin Seipp committed Dec 03, 2014 389   Simon Peyton Jones committed Mar 13, 2013 390 391 392  | MustBeMonoType -- Monotype regardless of flags rankZeroMonoType, tyConArgMonoType, synArgMonoType :: Rank  Joachim Breitner committed Sep 14, 2013 393 rankZeroMonoType = MonoType (ptext (sLit "Perhaps you intended to use RankNTypes or Rank2Types"))  Simon Peyton Jones committed Apr 22, 2015 394 tyConArgMonoType = MonoType (ptext (sLit "GHC doesn't yet support impredicative polymorphism"))  Joachim Breitner committed Sep 14, 2013 395 synArgMonoType = MonoType (ptext (sLit "Perhaps you intended to use LiberalTypeSynonyms"))  Simon Peyton Jones committed Mar 13, 2013 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418  funArgResRank :: Rank -> (Rank, Rank) -- Function argument and result funArgResRank (LimitedRank _ arg_rank) = (arg_rank, LimitedRank (forAllAllowed arg_rank) arg_rank) funArgResRank other_rank = (other_rank, other_rank) forAllAllowed :: Rank -> Bool forAllAllowed ArbitraryRank = True forAllAllowed (LimitedRank forall_ok _) = forall_ok forAllAllowed _ = False ---------------------------------------- check_mono_type :: UserTypeCtxt -> Rank -> KindOrType -> TcM () -- No foralls anywhere -- No unlifted types of any kind check_mono_type ctxt rank ty | isKind ty = return () -- IA0_NOTE: Do we need to check kinds? | otherwise = do { check_type ctxt rank ty ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) } check_type :: UserTypeCtxt -> Rank -> Type -> TcM () -- The args say what the *type context* requires, independent -- of *flag* settings. You test the flag settings at usage sites.  Austin Seipp committed Dec 03, 2014 419 --  Simon Peyton Jones committed Mar 13, 2013 420 421 422 423 424 425 -- Rank is allowed rank for function args -- Rank 0 means no for-alls anywhere check_type ctxt rank ty | not (null tvs && null theta) = do { checkTc (forAllAllowed rank) (forAllTyErr rank ty)  Austin Seipp committed Dec 03, 2014 426  -- Reject e.g. (Maybe (?x::Int => Int)),  Simon Peyton Jones committed Mar 13, 2013 427  -- with a decent error message  Simon Peyton Jones committed May 18, 2015 428 429 430 431 432  ; check_valid_theta SigmaCtxt theta -- Allow type T = ?x::Int => Int -> Int -- but not type T = ?x::Int  Simon Peyton Jones committed Mar 04, 2015 433  ; check_type ctxt rank tau } -- Allow foralls to right of arrow  Simon Peyton Jones committed Mar 13, 2013 434 435  where (tvs, theta, tau) = tcSplitSigmaTy ty  Austin Seipp committed Dec 03, 2014 436   Simon Peyton Jones committed Mar 13, 2013 437 438 439 440 441 442 443 444 445 446 447 448 449 check_type _ _ (TyVarTy _) = return () check_type ctxt rank (FunTy arg_ty res_ty) = do { check_type ctxt arg_rank arg_ty ; check_type ctxt res_rank res_ty } where (arg_rank, res_rank) = funArgResRank rank check_type ctxt rank (AppTy ty1 ty2) = do { check_arg_type ctxt rank ty1 ; check_arg_type ctxt rank ty2 } check_type ctxt rank ty@(TyConApp tc tys)  Jan Stolarek committed Nov 20, 2014 450 451  | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc = check_syn_tc_app ctxt rank ty tc tys  Simon Peyton Jones committed Apr 16, 2013 452 453 454 455 456 457 458 459  | isUnboxedTupleTyCon tc = check_ubx_tuple ctxt ty tys | otherwise = mapM_ (check_arg_type ctxt rank) tys check_type _ _ (LitTy {}) = return () check_type _ _ ty = pprPanic "check_type" (ppr ty) ----------------------------------------  Jan Stolarek committed Nov 20, 2014 460 check_syn_tc_app :: UserTypeCtxt -> Rank -> KindOrType  Simon Peyton Jones committed Apr 16, 2013 461  -> TyCon -> [KindOrType] -> TcM ()  Simon Peyton Jones committed Aug 25, 2014 462 -- Used for type synonyms and type synonym families,  Austin Seipp committed Dec 03, 2014 463 -- which must be saturated,  Simon Peyton Jones committed Aug 25, 2014 464 -- but not data families, which need not be saturated  Simon Peyton Jones committed Apr 16, 2013 465 check_syn_tc_app ctxt rank ty tc tys  Simon Peyton Jones committed Jun 18, 2015 466  | tc_arity <= length tys -- Saturated  Simon Peyton Jones committed Apr 16, 2013 467 468 469 470 471 472 473  -- Check that the synonym has enough args -- This applies equally to open and closed synonyms -- It's OK to have an *over-applied* type synonym -- data Tree a b = ... -- type Foo a = Tree [a] -- f :: Foo a b -> ... = do { -- See Note [Liberal type synonyms]  Simon Peyton Jones committed Mar 13, 2013 474  ; liberal <- xoptM Opt_LiberalTypeSynonyms  Jan Stolarek committed Nov 20, 2014 475  ; if not liberal || isTypeFamilyTyCon tc then  Simon Peyton Jones committed Mar 13, 2013 476  -- For H98 and synonym families, do check the type args  Simon Peyton Jones committed May 30, 2013 477  mapM_ check_arg tys  Simon Peyton Jones committed Mar 13, 2013 478 479  else -- In the liberal case (only for closed syns), expand then check  Austin Seipp committed Dec 03, 2014 480 481  case tcView ty of Just ty' -> check_type ctxt rank ty'  Simon Peyton Jones committed Apr 16, 2013 482 483  Nothing -> pprPanic "check_tau_type" (ppr ty) }  Austin Seipp committed Dec 03, 2014 484  | GhciCtxt <- ctxt -- Accept under-saturated type synonyms in  Simon Peyton Jones committed Apr 16, 2013 485  -- GHCi :kind commands; see Trac #7586  Simon Peyton Jones committed May 30, 2013 486  = mapM_ check_arg tys  Simon Peyton Jones committed Apr 16, 2013 487 488  | otherwise  Simon Peyton Jones committed Jun 18, 2015 489  = failWithTc (tyConArityErr tc tys)  Simon Peyton Jones committed Apr 16, 2013 490 491  where tc_arity = tyConArity tc  Jan Stolarek committed Nov 20, 2014 492 493  check_arg | isTypeFamilyTyCon tc = check_arg_type ctxt rank | otherwise = check_mono_type ctxt synArgMonoType  Austin Seipp committed Dec 03, 2014 494   Simon Peyton Jones committed Apr 16, 2013 495 ----------------------------------------  Austin Seipp committed Dec 03, 2014 496 check_ubx_tuple :: UserTypeCtxt -> KindOrType  Simon Peyton Jones committed Apr 16, 2013 497 498  -> [KindOrType] -> TcM () check_ubx_tuple ctxt ty tys  Simon Peyton Jones committed Mar 13, 2013 499  = do { ub_tuples_allowed <- xoptM Opt_UnboxedTuples  Simon Peyton Jones committed Apr 16, 2013 500  ; checkTc ub_tuples_allowed (ubxArgTyErr ty)  Simon Peyton Jones committed Mar 13, 2013 501   Austin Seipp committed Dec 03, 2014 502  ; impred <- xoptM Opt_ImpredicativeTypes  Simon Peyton Jones committed Mar 13, 2013 503 504 505 506 507  ; let rank' = if impred then ArbitraryRank else tyConArgMonoType -- c.f. check_arg_type -- However, args are allowed to be unlifted, or -- more unboxed tuples, so can't use check_arg_ty ; mapM_ (check_type ctxt rank') tys }  Austin Seipp committed Dec 03, 2014 508   Simon Peyton Jones committed Mar 13, 2013 509 510 511 512 513 514 515 ---------------------------------------- check_arg_type :: UserTypeCtxt -> Rank -> KindOrType -> TcM () -- The sort of type that can instantiate a type variable, -- or be the argument of a type constructor. -- Not an unboxed tuple, but now *can* be a forall (since impredicativity) -- Other unboxed types are very occasionally allowed as type -- arguments depending on the kind of the type constructor  Austin Seipp committed Dec 03, 2014 516 --  Simon Peyton Jones committed Mar 13, 2013 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 -- For example, we want to reject things like: -- -- instance Ord a => Ord (forall s. T s a) -- and -- g :: T s (forall b.b) -- -- NB: unboxed tuples can have polymorphic or unboxed args. -- This happens in the workers for functions returning -- product types with polymorphic components. -- But not in user code. -- Anyway, they are dealt with by a special case in check_tau_type check_arg_type ctxt rank ty | isKind ty = return () -- IA0_NOTE: Do we need to check a kind? | otherwise = do { impred <- xoptM Opt_ImpredicativeTypes ; let rank' = case rank of -- Predictive => must be monotype MustBeMonoType -> MustBeMonoType -- Monotype, regardless _other | impred -> ArbitraryRank | otherwise -> tyConArgMonoType  Austin Seipp committed Dec 03, 2014 537  -- Make sure that MustBeMonoType is propagated,  Simon Peyton Jones committed Mar 13, 2013 538 539 540 541 542 543  -- so that we don't suggest -XImpredicativeTypes in -- (Ord (forall a.a)) => a -> a -- and so that if it Must be a monotype, we check that it is! ; check_type ctxt rank' ty ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }  Austin Seipp committed Dec 03, 2014 544  -- NB the isUnLiftedType test also checks for  Simon Peyton Jones committed Mar 13, 2013 545 546 547 548 549 550  -- T State# -- where there is an illegal partial application of State# (which has -- kind * -> #); see Note [The kind invariant] in TypeRep ---------------------------------------- forAllTyErr :: Rank -> Type -> SDoc  Austin Seipp committed Dec 03, 2014 551 forAllTyErr rank ty  Simon Peyton Jones committed Mar 13, 2013 552 553 554 555  = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty) , suggestion ] where suggestion = case rank of  Joachim Breitner committed Sep 14, 2013 556  LimitedRank {} -> ptext (sLit "Perhaps you intended to use RankNTypes or Rank2Types")  Simon Peyton Jones committed Mar 13, 2013 557  MonoType d -> d  Austin Seipp committed Sep 09, 2014 558  _ -> Outputable.empty -- Polytype is always illegal  Simon Peyton Jones committed Mar 13, 2013 559 560 561 562 563 564 565 566  unliftedArgErr, ubxArgTyErr :: Type -> SDoc unliftedArgErr ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty] ubxArgTyErr ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty] kindErr :: Kind -> SDoc kindErr kind = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]  Austin Seipp committed Dec 03, 2014 567 {-  Simon Peyton Jones committed Mar 13, 2013 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 Note [Liberal type synonyms] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ If -XLiberalTypeSynonyms is on, expand closed type synonyms *before* doing validity checking. This allows us to instantiate a synonym defn with a for-all type, or with a partially-applied type synonym. e.g. type T a b = a type S m = m () f :: S (T Int) Here, T is partially applied, so it's illegal in H98. But if you expand S first, then T we get just f :: Int which is fine. IMPORTANT: suppose T is a type synonym. Then we must do validity checking on an appliation (T ty1 ty2) *either* before expansion (i.e. check ty1, ty2) *or* after expansion (i.e. expand T ty1 ty2, and then check) BUT NOT BOTH If we do both, we get exponential behaviour!! data TIACons1 i r c = c i ::: r c type TIACons2 t x = TIACons1 t (TIACons1 t x) type TIACons3 t x = TIACons2 t (TIACons1 t x) type TIACons4 t x = TIACons2 t (TIACons2 t x) type TIACons7 t x = TIACons4 t (TIACons3 t x)  Austin Seipp committed Dec 03, 2014 597 598 ************************************************************************ * *  Simon Peyton Jones committed Mar 13, 2013 599 \subsection{Checking a theta or source type}  Austin Seipp committed Dec 03, 2014 600 601 * * ************************************************************************  Simon Peyton Jones committed Mar 13, 2013 602   603 604 605 606 607 608 609 610 Note [Implicit parameters in instance decls] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Implicit parameters _only_ allowed in type signatures; not in instance decls, superclasses etc. The reason for not allowing implicit params in instances is a bit subtle. If we allowed instance (?x::Int, Eq a) => Foo [a] where ... then when we saw (e :: (?x::Int) => t)  Gabor Greif committed Mar 25, 2014 611 612 it would be unclear how to discharge all the potential uses of the ?x in e. For example, a constraint Foo [Int] might come out of e, and  613 applying the instance decl would show up two uses of ?x. Trac #8912.  Austin Seipp committed Dec 03, 2014 614 -}  615   Simon Peyton Jones committed Mar 13, 2013 616 checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()  617 checkValidTheta ctxt theta  Simon Peyton Jones committed Mar 13, 2013 618 619 620 621 622 623 624 625 626 627  = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta) ------------------------- check_valid_theta :: UserTypeCtxt -> [PredType] -> TcM () check_valid_theta _ [] = return () check_valid_theta ctxt theta = do { dflags <- getDynFlags ; warnTc (wopt Opt_WarnDuplicateConstraints dflags && notNull dups) (dupPredWarn dups)  Simon Peyton Jones committed Apr 30, 2015 628  ; traceTc "check_valid_theta" (ppr theta)  Simon Peyton Jones committed Mar 13, 2013 629 630 631 632 633 634 635  ; mapM_ (check_pred_ty dflags ctxt) theta } where (_,dups) = removeDups cmpPred theta ------------------------- check_pred_ty :: DynFlags -> UserTypeCtxt -> PredType -> TcM () -- Check the validity of a predicate in a signature  Simon Peyton Jones committed Nov 27, 2014 636 -- Do not look through any type synonyms; any constraint kinded  Simon Peyton Jones committed Mar 13, 2013 637 -- type synonyms have been checked at their definition site  Simon Peyton Jones committed Nov 27, 2014 638 -- C.f. Trac #9838  Simon Peyton Jones committed Mar 13, 2013 639 640  check_pred_ty dflags ctxt pred  Simon Peyton Jones committed Nov 27, 2014 641 642 643 644 645 646 647  = do { checkValidMonoType pred ; check_pred_help False dflags ctxt pred } check_pred_help :: Bool -- True <=> under a type synonym -> DynFlags -> UserTypeCtxt -> PredType -> TcM () check_pred_help under_syn dflags ctxt pred  Simon Peyton Jones committed Apr 30, 2015 648 649  | Just pred' <- coreView pred -- Switch on under_syn when going under a -- synonym (Trac #9838, yuk)  Simon Peyton Jones committed May 18, 2015 650  = check_pred_help True dflags ctxt pred'  Simon Peyton Jones committed Nov 27, 2014 651  | otherwise  Simon Peyton Jones committed Apr 30, 2015 652  = case splitTyConApp_maybe pred of  Simon Peyton Jones committed May 18, 2015 653 654 655 656 657 658 659  Just (tc, tys) | isTupleTyCon tc -> check_tuple_pred under_syn dflags ctxt pred tys | Just cls <- tyConClass_maybe tc -> check_class_pred dflags ctxt pred cls tys -- Includes Coercible | tc hasKey eqTyConKey -> check_eq_pred dflags pred tys  Simon Peyton Jones committed Apr 30, 2015 660 661 662 663  _ -> check_irred_pred under_syn dflags ctxt pred check_eq_pred :: DynFlags -> PredType -> [TcType] -> TcM () check_eq_pred dflags pred tys  eir@cis.upenn.edu committed Dec 12, 2014 664 665  = -- Equational constraints are valid in all contexts if type -- families are permitted  Simon Peyton Jones committed Jun 18, 2015 666 667  do { checkTc (length tys == 3) (tyConArityErr eqTyCon tys)  Simon Peyton Jones committed Apr 30, 2015 668 669  ; checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags) (eqPredTyErr pred) }  eir@cis.upenn.edu committed Dec 12, 2014 670   Simon Peyton Jones committed Nov 27, 2014 671 672 check_tuple_pred :: Bool -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM () check_tuple_pred under_syn dflags ctxt pred ts  eir@cis.upenn.edu committed Dec 12, 2014 673  = do { -- See Note [ConstraintKinds in predicates]  Simon Peyton Jones committed Nov 27, 2014 674  checkTc (under_syn || xopt Opt_ConstraintKinds dflags)  Simon Peyton Jones committed Mar 13, 2013 675  (predTupleErr pred)  Simon Peyton Jones committed Nov 27, 2014 676 677 678  ; mapM_ (check_pred_help under_syn dflags ctxt) ts } -- This case will not normally be executed because without -- -XConstraintKinds tuple types are only kind-checked as *  Simon Peyton Jones committed Mar 13, 2013 679   Simon Peyton Jones committed Nov 27, 2014 680 681 check_irred_pred :: Bool -> DynFlags -> UserTypeCtxt -> PredType -> TcM () check_irred_pred under_syn dflags ctxt pred  Simon Peyton Jones committed Mar 13, 2013 682  -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint  Simon Peyton Jones committed Nov 27, 2014 683 684 685 686 687  -- where X is a type function = do { -- If it looks like (x t1 t2), require ConstraintKinds -- see Note [ConstraintKinds in predicates] -- But (X t1 t2) is always ok because we just require ConstraintKinds -- at the definition site (Trac #9838)  Simon Peyton Jones committed May 18, 2015 688 689 690  failIfTc (not under_syn && not (xopt Opt_ConstraintKinds dflags) && hasTyVarHead pred) (predIrredErr pred)  Simon Peyton Jones committed Nov 27, 2014 691 692 693  -- Make sure it is OK to have an irred pred in this context -- See Note [Irreducible predicates in superclasses]  Simon Peyton Jones committed May 18, 2015 694 695 696 697  ; failIfTc (is_superclass ctxt && not (xopt Opt_UndecidableInstances dflags) && has_tyfun_head pred) (predSuperClassErr pred) }  Simon Peyton Jones committed Nov 27, 2014 698  where  Simon Peyton Jones committed May 18, 2015 699 700 701 702 703  is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False } has_tyfun_head ty = case tcSplitTyConApp_maybe ty of Just (tc, _) -> isTypeFamilyTyCon tc Nothing -> False  Simon Peyton Jones committed Nov 27, 2014 704 705 706 707 708 709 710 711 712 713 714 715 716  {- Note [ConstraintKinds in predicates] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Don't check for -XConstraintKinds under a type synonym, because that was done at the type synonym definition site; see Trac #9838 e.g. module A where type C a = (Eq a, Ix a) -- Needs -XConstraintKinds module B where import A f :: C a => a -> a -- Does *not* need -XConstraintKinds Note [Irreducible predicates in superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~  Simon Peyton Jones committed May 18, 2015 717 Allowing type-family calls in class superclasses is somewhat dangerous  Simon Peyton Jones committed Nov 27, 2014 718 719 720 721 722 723 724 725 because we can write: type family Fooish x :: * -> Constraint type instance Fooish () = Foo class Fooish () a => Foo a where This will cause the constraint simplifier to loop because every time we canonicalise a (Foo a) class constraint we add a (Fooish () a) constraint which will be immediately  Simon Peyton Jones committed May 18, 2015 726 solved to add+canonicalise another (Foo a) constraint. -}  Simon Peyton Jones committed Mar 13, 2013 727 728  -------------------------  Simon Peyton Jones committed Apr 30, 2015 729 730 731 check_class_pred :: DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM () check_class_pred dflags ctxt pred cls tys | isIPClass cls  Simon Peyton Jones committed Jun 18, 2015 732 733  = do { check_arity ; checkTc (okIPCtxt ctxt) (badIPPred pred) }  eir@cis.upenn.edu committed Dec 12, 2014 734   Simon Peyton Jones committed Apr 30, 2015 735  | otherwise  Simon Peyton Jones committed Jun 18, 2015 736  = do { check_arity  Simon Peyton Jones committed Apr 30, 2015 737 738  ; checkTc arg_tys_ok (predTyVarErr pred) } where  Simon Peyton Jones committed Jun 18, 2015 739 740  check_arity = checkTc (classArity cls == length tys) (tyConArityErr (classTyCon cls) tys)  Simon Peyton Jones committed Apr 30, 2015 741 742  flexible_contexts = xopt Opt_FlexibleContexts dflags undecidable_ok = xopt Opt_UndecidableInstances dflags  Simon Peyton Jones committed Mar 13, 2013 743   Simon Peyton Jones committed Apr 30, 2015 744 745 746 747 748 749  arg_tys_ok = case ctxt of SpecInstCtxt -> True -- {-# SPECIALISE instance Eq (T Int) #-} is fine InstDeclCtxt -> checkValidClsArgs (flexible_contexts || undecidable_ok) tys -- Further checks on head and theta -- in checkInstTermination _ -> checkValidClsArgs flexible_contexts tys  Simon Peyton Jones committed Nov 27, 2014 750 751 752 753  ------------------------- okIPCtxt :: UserTypeCtxt -> Bool -- See Note [Implicit parameters in instance decls]  Simon Peyton Jones committed May 18, 2015 754 755 756 757 758 759 760 761 762 763 764 765 okIPCtxt (FunSigCtxt {}) = True okIPCtxt (InfSigCtxt {}) = True okIPCtxt ExprSigCtxt = True okIPCtxt PatSigCtxt = True okIPCtxt ResSigCtxt = True okIPCtxt GenSigCtxt = True okIPCtxt (ConArgCtxt {}) = True okIPCtxt (ForSigCtxt {}) = True -- ?? okIPCtxt ThBrackCtxt = True okIPCtxt GhciCtxt = True okIPCtxt SigmaCtxt = True okIPCtxt (DataTyCtxt {}) = True  Simon Peyton Jones committed Aug 05, 2015 766 okIPCtxt (PatSynCtxt {}) = True  Simon Peyton Jones committed May 18, 2015 767   Simon Peyton Jones committed Nov 27, 2014 768 769 770 okIPCtxt (ClassSCCtxt {}) = False okIPCtxt (InstDeclCtxt {}) = False okIPCtxt (SpecInstCtxt {}) = False  Simon Peyton Jones committed May 18, 2015 771 772 773 okIPCtxt (TySynCtxt {}) = False okIPCtxt (RuleSigCtxt {}) = False okIPCtxt DefaultDeclCtxt = False  Simon Peyton Jones committed Nov 27, 2014 774 775 776  badIPPred :: PredType -> SDoc badIPPred pred = ptext (sLit "Illegal implicit parameter") <+> quotes (ppr pred)  Simon Peyton Jones committed Mar 13, 2013 777   Austin Seipp committed Dec 03, 2014 778 {-  Simon Peyton Jones committed Mar 13, 2013 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 Note [Kind polymorphic type classes] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ MultiParam check: class C f where... -- C :: forall k. k -> Constraint instance C Maybe where... The dictionary gets type [C * Maybe] even if it's not a MultiParam type class. Flexibility check: class C f where... -- C :: forall k. k -> Constraint data D a = D a instance C D where The dictionary gets type [C * (D *)]. IA0_TODO it should be generalized actually.  Austin Seipp committed Dec 03, 2014 797 798 -}  Simon Peyton Jones committed Mar 13, 2013 799 800 801 802 803 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> SDoc checkThetaCtxt ctxt theta = vcat [ptext (sLit "In the context:") <+> pprTheta theta, ptext (sLit "While checking") <+> pprUserTypeCtxt ctxt ]  Simon Peyton Jones committed May 18, 2015 804 805 806 eqPredTyErr, predTyVarErr, predTupleErr, predIrredErr, predSuperClassErr :: PredType -> SDoc eqPredTyErr pred = vcat [ ptext (sLit "Illegal equational constraint") <+> pprType pred , parens (ptext (sLit "Use GADTs or TypeFamilies to permit this")) ]  Simon Peyton Jones committed Apr 30, 2015 807 808 809 predTyVarErr pred = vcat [ hang (ptext (sLit "Non type-variable argument")) 2 (ptext (sLit "in the constraint:") <+> pprType pred) , parens (ptext (sLit "Use FlexibleContexts to permit this")) ]  Simon Peyton Jones committed Mar 13, 2013 810 predTupleErr pred = hang (ptext (sLit "Illegal tuple constraint:") <+> pprType pred)  Simon Peyton Jones committed Nov 27, 2014 811  2 (parens constraintKindsMsg)  Simon Peyton Jones committed Mar 13, 2013 812 predIrredErr pred = hang (ptext (sLit "Illegal constraint:") <+> pprType pred)  Simon Peyton Jones committed Nov 27, 2014 813  2 (parens constraintKindsMsg)  Simon Peyton Jones committed May 18, 2015 814 815 816 817 predSuperClassErr pred = hang (ptext (sLit "Illegal constraint") <+> quotes (pprType pred) <+> ptext (sLit "in a superclass context")) 2 (parens undecidableMsg)  Simon Peyton Jones committed Mar 13, 2013 818 819 820  constraintSynErr :: Type -> SDoc constraintSynErr kind = hang (ptext (sLit "Illegal constraint synonym of kind:") <+> quotes (ppr kind))  Simon Peyton Jones committed Nov 27, 2014 821  2 (parens constraintKindsMsg)  Simon Peyton Jones committed Mar 13, 2013 822 823 824 825  dupPredWarn :: [[PredType]] -> SDoc dupPredWarn dups = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprType (map head dups)  Simon Peyton Jones committed Jun 18, 2015 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 tyConArityErr :: TyCon -> [TcType] -> SDoc -- For type-constructor arity errors, be careful to report -- the number of /type/ arguments required and supplied, -- ignoring the /kind/ arguments, which the user does not see. -- (e.g. Trac #10516) tyConArityErr tc tks = arityErr (tyConFlavour tc) (tyConName tc) tc_type_arity tc_type_args where tvs = tyConTyVars tc kbs :: [Bool] -- True for a Type arg, false for a Kind arg kbs = map isTypeVar tvs -- tc_type_arity = number of *type* args expected -- tc_type_args = number of *type* args encountered tc_type_arity = count id kbs tc_type_args = count (id . fst) (kbs zip tks)  Simon Peyton Jones committed Mar 13, 2013 845 arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc  Simon Peyton Jones committed Jun 18, 2015 846 847 arityErr what name n m = hsep [ ptext (sLit "The") <+> text what, quotes (ppr name), ptext (sLit "should have"),  Austin Seipp committed Dec 03, 2014 848  n_arguments <> comma, text "but has been given",  Simon Peyton Jones committed Mar 13, 2013 849 850 851 852 853 854  if m==0 then text "none" else int m] where n_arguments | n == 0 = ptext (sLit "no arguments") | n == 1 = ptext (sLit "1 argument") | True = hsep [int n, ptext (sLit "arguments")]  Austin Seipp committed Dec 03, 2014 855 856 857 {- ************************************************************************ * *  Simon Peyton Jones committed Mar 13, 2013 858 \subsection{Checking for a decent instance head type}  Austin Seipp committed Dec 03, 2014 859 860 * * ************************************************************************  Simon Peyton Jones committed Mar 13, 2013 861 862 863 864 865 866 867 868 869  @checkValidInstHead@ checks the type {\em and} its syntactic constraints: it must normally look like: @instance Foo (Tycon a b c ...) ...@ The exceptions to this syntactic checking: (1)~if the @GlasgowExts@ flag is on, or (2)~the instance is imported (they must have been compiled elsewhere). In these cases, we let them go through anyway. We can also have instances for functions: @instance Foo (a -> b) ...@.  Austin Seipp committed Dec 03, 2014 870 -}  Simon Peyton Jones committed Mar 13, 2013 871 872 873 874 875  checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM () checkValidInstHead ctxt clas cls_args = do { dflags <- getDynFlags  Joachim Breitner committed Sep 13, 2013 876 877 878  ; checkTc (clas notElem abstractClasses) (instTypeErr clas cls_args abstract_class_msg)  Austin Seipp committed Dec 03, 2014 879  -- Check language restrictions;  Simon Peyton Jones committed Mar 13, 2013 880 881 882 883 884 885 886 887 888 889  -- but not for SPECIALISE isntance pragmas ; let ty_args = dropWhile isKind cls_args ; unless spec_inst_prag  do { checkTc (xopt Opt_TypeSynonymInstances dflags || all tcInstHeadTyNotSynonym ty_args) (instTypeErr clas cls_args head_type_synonym_msg) ; checkTc (xopt Opt_FlexibleInstances dflags || all tcInstHeadTyAppAllTyVars ty_args) (instTypeErr clas cls_args head_type_args_tyvars_msg) ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||  Krzysztof Gogolewski committed Jul 01, 2014 890 891 892  length ty_args == 1 || -- Only count type arguments (xopt Opt_NullaryTypeClasses dflags && null ty_args))  Simon Peyton Jones committed Mar 13, 2013 893 894 895 896 897 898  (instTypeErr clas cls_args head_one_type_msg) } -- May not contain type family applications ; mapM_ checkTyFamFreeness ty_args ; mapM_ checkValidMonoType ty_args  Austin Seipp committed Dec 03, 2014 899 900  -- For now, I only allow tau-types (not polytypes) in -- the head of an instance decl.  Simon Peyton Jones committed Mar 13, 2013 901 902 903 904 905 906 907 908 909 910 911  -- E.g. instance C (forall a. a->a) is rejected -- One could imagine generalising that, but I'm not sure -- what all the consequences might be } where spec_inst_prag = case ctxt of { SpecInstCtxt -> True; _ -> False } head_type_synonym_msg = parens ( text "All instance types must be of the form (T t1 ... tn)"$$ text "where T is not a synonym." $$ Joachim Breitner committed Sep 14, 2013 912  text "Use TypeSynonymInstances if you want to disable this.")  Simon Peyton Jones committed Mar 13, 2013 913 914 915 916 917  head_type_args_tyvars_msg = parens (vcat [ text "All instance types must be of the form (T a1 ... an)", text "where a1 ... an are *distinct type variables*,", text "and each type variable appears at most once in the instance head.",  Joachim Breitner committed Sep 14, 2013 918  text "Use FlexibleInstances if you want to disable this."])  Simon Peyton Jones committed Mar 13, 2013 919 920 921  head_one_type_msg = parens ( text "Only one type can be given in an instance head."$$  owst committed Jun 04, 2014 922  text "Use MultiParamTypeClasses if you want to allow more, or zero.")  Simon Peyton Jones committed Mar 13, 2013 923   Joachim Breitner committed Sep 13, 2013 924 925 926 927  abstract_class_msg = text "The class is abstract, manual instances are not permitted." abstractClasses :: [ Class ]  Joachim Breitner committed Nov 29, 2013 928 abstractClasses = [ coercibleClass ] -- See Note [Coercible Instances]  Joachim Breitner committed Sep 13, 2013 929   Simon Peyton Jones committed Mar 13, 2013 930 931 instTypeErr :: Class -> [Type] -> SDoc -> SDoc instTypeErr cls tys msg  unknown committed Oct 01, 2013 932 933  = hang (hang (ptext (sLit "Illegal instance declaration for")) 2 (quotes (pprClassPred cls tys)))  Simon Peyton Jones committed Mar 13, 2013 934 935  2 msg  Simon Peyton Jones committed Jun 26, 2015 936 937 938 {- Note [Valid 'deriving' predicate] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ validDerivPred checks for OK 'deriving' context. See Note [Exotic  eir@cis.upenn.edu committed Dec 12, 2014 939 derived instance contexts] in TcDeriv. However the predicate is  Simon Peyton Jones committed Mar 13, 2013 940 941 here because it uses sizeTypes, fvTypes.  Simon Peyton Jones committed Jun 26, 2015 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 It checks for three things * No repeated variables (hasNoDups fvs) * No type constructors. This is done by comparing sizeTypes tys == length (fvTypes tys) sizeTypes counts variables and constructors; fvTypes returns variables. So if they are the same, there must be no constructors. But there might be applications thus (f (g x)). * Also check for a bizarre corner case, when the derived instance decl would look like instance C a b => D (T a) where ... Note that 'b' isn't a parameter of T. This gives rise to all sorts of problems; in particular, it's hard to compare solutions for equality when finding the fixpoint, and that means the inferContext loop does not converge. See Trac #5287.  Austin Seipp committed Dec 03, 2014 959 -}  Simon Peyton Jones committed Mar 13, 2013 960 961  validDerivPred :: TyVarSet -> PredType -> Bool  Simon Peyton Jones committed Jun 26, 2015 962 -- See Note [Valid 'deriving' predicate]  Simon Peyton Jones committed Mar 13, 2013 963 964 validDerivPred tv_set pred = case classifyPredType pred of  Simon Peyton Jones committed May 18, 2015 965 966 967  ClassPred _ tys -> check_tys tys EqPred {} -> False -- reject equality constraints _ -> True -- Non-class predicates are ok  Simon Peyton Jones committed Mar 13, 2013 968  where  eir@cis.upenn.edu committed Dec 12, 2014 969  check_tys tys = hasNoDups fvs  Simon Peyton Jones committed Dec 23, 2014 970  && sizeTypes tys == fromIntegral (length fvs)  eir@cis.upenn.edu committed Dec 12, 2014 971  && all (elemVarSet tv_set) fvs  Simon Peyton Jones committed Jun 26, 2015 972 973  where fvs = fvTypes tys  Simon Peyton Jones committed Mar 13, 2013 974   Austin Seipp committed Dec 03, 2014 975 976 977 {- ************************************************************************ * *  Simon Peyton Jones committed Mar 13, 2013 978 \subsection{Checking instance for termination}  Austin Seipp committed Dec 03, 2014 979 980 981 * * ************************************************************************ -}  Simon Peyton Jones committed Mar 13, 2013 982 983 984 985  checkValidInstance :: UserTypeCtxt -> LHsType Name -> Type -> TcM ([TyVar], ThetaType, Class, [Type]) checkValidInstance ctxt hs_type ty  Simon Peyton Jones committed Apr 30, 2013 986 987 988  | Just (clas,inst_tys) <- getClassPredTys_maybe tau , inst_tys lengthIs classArity clas = do { setSrcSpan head_loc (checkValidInstHead ctxt clas inst_tys)  Simon Peyton Jones committed Mar 13, 2013 989 990 991 992 993 994  ; checkValidTheta ctxt theta -- The Termination and Coverate Conditions -- Check that instance inference will terminate (if we care) -- For Haskell 98 this will already have been done by checkValidTheta, -- but as we may be using other extensions we need to check.  Austin Seipp committed Dec 03, 2014 995 996  -- -- Note that the Termination Condition is *more conservative* than  Simon Peyton Jones committed Mar 13, 2013 997 998 999 1000 1001  -- the checkAmbiguity test we do on other type signatures -- e.g. Bar a => Bar Int is ambiguous, but it also fails -- the termination condition, because 'a' appears more often -- in the constraint than in the head ; undecidable_ok <- xoptM Opt_UndecidableInstances  Austin Seipp committed Dec 03, 2014 1002  ; if undecidable_ok  unknown committed Oct 01, 2013 1003 1004 1005 1006  then checkAmbiguity ctxt ty else checkInstTermination inst_tys theta ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of  Simon Peyton Jones committed Jul 25, 2014 1007 1008  IsValid -> return () -- Check succeeded NotValid msg -> addErrTc (instTypeErr clas inst_tys msg)  Simon Peyton Jones committed Apr 30, 2013 1009   Austin Seipp committed Dec 03, 2014 1010 1011 1012  ; return (tvs, theta, clas, inst_tys) } | otherwise  Simon Peyton Jones committed Apr 30, 2013 1013  = failWithTc (ptext (sLit "Malformed instance head:") <+> ppr tau)  Simon Peyton Jones committed Mar 13, 2013 1014  where  Simon Peyton Jones committed Apr 30, 2013 1015  (tvs, theta, tau) = tcSplitSigmaTy ty  Simon Peyton Jones committed Mar 13, 2013 1016 1017 1018  -- The location of the "head" of the instance head_loc = case hs_type of  thomasw committed Nov 28, 2014 1019 1020  L _ (HsForAllTy _ _ _ _ (L loc _)) -> loc L loc _ -> loc  Simon Peyton Jones committed Mar 13, 2013 1021   Austin Seipp committed Dec 03, 2014 1022 {-  Simon Peyton Jones committed Mar 13, 2013 1023 1024 1025 Note [Paterson conditions] ~~~~~~~~~~~~~~~~~~~~~~~~~~ Termination test: the so-called "Paterson conditions" (see Section 5 of  Jan Stolarek committed Sep 03, 2015 1026 "Understanding functional dependencies via Constraint Handling Rules,  Simon Peyton Jones committed Mar 13, 2013 1027 1028 1029 1030 1031 1032 1033 JFP Jan 2007). We check that each assertion in the context satisfies: (1) no variable has more occurrences in the assertion than in the head, and (2) the assertion has fewer constructors and variables (taken together and counting repetitions) than the head. This is only needed with -fglasgow-exts, as Haskell 98 restrictions  Austin Seipp committed Dec 03, 2014 1034 (which have already been checked) guarantee termination.  Simon Peyton Jones committed Mar 13, 2013 1035   Austin Seipp committed Dec 03, 2014 1036 The underlying idea is that  Simon Peyton Jones committed Mar 13, 2013 1037 1038 1039  for any ground substitution, each assertion in the context has fewer type constructors than the head.  Austin Seipp committed Dec 03, 2014 1040 -}  Simon Peyton Jones committed Mar 13, 2013 1041 1042 1043 1044  checkInstTermination :: [TcType] -> ThetaType -> TcM () -- See Note [Paterson conditions] checkInstTermination tys theta  unknown committed Oct 01, 2013 1045  = check_preds theta  Simon Peyton Jones committed Mar 13, 2013 1046  where  Simon Peyton Jones committed Jun 26, 2015 1047 1048  head_fvs = fvTypes tys head_size = sizeTypes tys  unknown committed Oct 01, 2013 1049 1050 1051 1052 1053  check_preds :: [PredType] -> TcM () check_preds preds = mapM_ check preds check :: PredType -> TcM ()  Austin Seipp committed Dec 03, 2014 1054  check pred  Simon Peyton Jones committed Jun 26, 2015 1055 1056 1057 1058 1059 1060 1061 1062  = case classifyPredType pred of EqPred {} -> return () -- See Trac #4200. IrredPred {} -> check2 pred (sizeType pred) ClassPred cls tys | isIPClass cls -> return () -- You can't get to class predicates from implicit params | isCTupleClass cls -- Look inside tuple predicates; Trac #8359