1{- 2(c) The University of Glasgow 2006 3(c) The GRASP/AQUA Project, Glasgow University, 1992-1998 4 5 6Type subsumption and unification 7-} 8 9{-# LANGUAGE CPP, DeriveFunctor, MultiWayIf, TupleSections, 10 ScopedTypeVariables #-} 11 12module TcUnify ( 13 -- Full-blown subsumption 14 tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET, 15 tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS, 16 tcSubTypeDS_NC_O, tcSubTypeET, 17 checkConstraints, checkTvConstraints, 18 buildImplicationFor, emitResidualTvConstraint, 19 20 -- Various unifications 21 unifyType, unifyKind, 22 uType, promoteTcType, 23 swapOverTyVars, canSolveByUnification, 24 25 -------------------------------- 26 -- Holes 27 tcInferInst, tcInferNoInst, 28 matchExpectedListTy, 29 matchExpectedTyConApp, 30 matchExpectedAppTy, 31 matchExpectedFunTys, 32 matchActualFunTys, matchActualFunTysPart, 33 matchExpectedFunKind, 34 35 metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..) 36 37 ) where 38 39#include "HsVersions.h" 40 41import GhcPrelude 42 43import GHC.Hs 44import TyCoRep 45import TyCoPpr( debugPprType ) 46import TcMType 47import TcRnMonad 48import TcType 49import Type 50import Coercion 51import TcEvidence 52import Constraint 53import Predicate 54import TcOrigin 55import Name( isSystemName ) 56import Inst 57import TyCon 58import TysWiredIn 59import TysPrim( tYPE ) 60import Var 61import VarSet 62import VarEnv 63import ErrUtils 64import DynFlags 65import BasicTypes 66import Bag 67import Util 68import qualified GHC.LanguageExtensions as LangExt 69import Outputable 70 71import Data.Maybe( isNothing ) 72import Control.Monad 73import Control.Arrow ( second ) 74 75{- 76************************************************************************ 77* * 78 matchExpected functions 79* * 80************************************************************************ 81 82Note [Herald for matchExpectedFunTys] 83~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 84The 'herald' always looks like: 85 "The equation(s) for 'f' have" 86 "The abstraction (\x.e) takes" 87 "The section (+ x) expects" 88 "The function 'f' is applied to" 89 90This is used to construct a message of form 91 92 The abstraction `\Just 1 -> ...' takes two arguments 93 but its type `Maybe a -> a' has only one 94 95 The equation(s) for `f' have two arguments 96 but its type `Maybe a -> a' has only one 97 98 The section `(f 3)' requires 'f' to take two arguments 99 but its type `Int -> Int' has only one 100 101 The function 'f' is applied to two arguments 102 but its type `Int -> Int' has only one 103 104When visible type applications (e.g., `f @Int 1 2`, as in #13902) enter the 105picture, we have a choice in deciding whether to count the type applications as 106proper arguments: 107 108 The function 'f' is applied to one visible type argument 109 and two value arguments 110 but its type `forall a. a -> a` has only one visible type argument 111 and one value argument 112 113Or whether to include the type applications as part of the herald itself: 114 115 The expression 'f @Int' is applied to two arguments 116 but its type `Int -> Int` has only one 117 118The latter is easier to implement and is arguably easier to understand, so we 119choose to implement that option. 120 121Note [matchExpectedFunTys] 122~~~~~~~~~~~~~~~~~~~~~~~~~~ 123matchExpectedFunTys checks that a sigma has the form 124of an n-ary function. It passes the decomposed type to the 125thing_inside, and returns a wrapper to coerce between the two types 126 127It's used wherever a language construct must have a functional type, 128namely: 129 A lambda expression 130 A function definition 131 An operator section 132 133This function must be written CPS'd because it needs to fill in the 134ExpTypes produced for arguments before it can fill in the ExpType 135passed in. 136 137-} 138 139-- Use this one when you have an "expected" type. 140matchExpectedFunTys :: forall a. 141 SDoc -- See Note [Herald for matchExpectedFunTys] 142 -> Arity 143 -> ExpRhoType -- deeply skolemised 144 -> ([ExpSigmaType] -> ExpRhoType -> TcM a) 145 -- must fill in these ExpTypes here 146 -> TcM (a, HsWrapper) 147-- If matchExpectedFunTys n ty = (_, wrap) 148-- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty, 149-- where [t1, ..., tn], ty_r are passed to the thing_inside 150matchExpectedFunTys herald arity orig_ty thing_inside 151 = case orig_ty of 152 Check ty -> go [] arity ty 153 _ -> defer [] arity orig_ty 154 where 155 go acc_arg_tys 0 ty 156 = do { result <- thing_inside (reverse acc_arg_tys) (mkCheckExpType ty) 157 ; return (result, idHsWrapper) } 158 159 go acc_arg_tys n ty 160 | Just ty' <- tcView ty = go acc_arg_tys n ty' 161 162 go acc_arg_tys n (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) 163 = ASSERT( af == VisArg ) 164 do { (result, wrap_res) <- go (mkCheckExpType arg_ty : acc_arg_tys) 165 (n-1) res_ty 166 ; return ( result 167 , mkWpFun idHsWrapper wrap_res arg_ty res_ty doc ) } 168 where 169 doc = text "When inferring the argument type of a function with type" <+> 170 quotes (ppr orig_ty) 171 172 go acc_arg_tys n ty@(TyVarTy tv) 173 | isMetaTyVar tv 174 = do { cts <- readMetaTyVar tv 175 ; case cts of 176 Indirect ty' -> go acc_arg_tys n ty' 177 Flexi -> defer acc_arg_tys n (mkCheckExpType ty) } 178 179 -- In all other cases we bale out into ordinary unification 180 -- However unlike the meta-tyvar case, we are sure that the 181 -- number of arguments doesn't match arity of the original 182 -- type, so we can add a bit more context to the error message 183 -- (cf #7869). 184 -- 185 -- It is not always an error, because specialized type may have 186 -- different arity, for example: 187 -- 188 -- > f1 = f2 'a' 189 -- > f2 :: Monad m => m Bool 190 -- > f2 = undefined 191 -- 192 -- But in that case we add specialized type into error context 193 -- anyway, because it may be useful. See also #9605. 194 go acc_arg_tys n ty = addErrCtxtM mk_ctxt $ 195 defer acc_arg_tys n (mkCheckExpType ty) 196 197 ------------ 198 defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (a, HsWrapper) 199 defer acc_arg_tys n fun_ty 200 = do { more_arg_tys <- replicateM n newInferExpTypeNoInst 201 ; res_ty <- newInferExpTypeInst 202 ; result <- thing_inside (reverse acc_arg_tys ++ more_arg_tys) res_ty 203 ; more_arg_tys <- mapM readExpType more_arg_tys 204 ; res_ty <- readExpType res_ty 205 ; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty 206 ; wrap <- tcSubTypeDS AppOrigin GenSigCtxt unif_fun_ty fun_ty 207 -- Not a good origin at all :-( 208 ; return (result, wrap) } 209 210 ------------ 211 mk_ctxt :: TidyEnv -> TcM (TidyEnv, MsgDoc) 212 mk_ctxt env = do { (env', ty) <- zonkTidyTcType env orig_tc_ty 213 ; let (args, _) = tcSplitFunTys ty 214 n_actual = length args 215 (env'', orig_ty') = tidyOpenType env' orig_tc_ty 216 ; return ( env'' 217 , mk_fun_tys_msg orig_ty' ty n_actual arity herald) } 218 where 219 orig_tc_ty = checkingExpType "matchExpectedFunTys" orig_ty 220 -- this is safe b/c we're called from "go" 221 222-- Like 'matchExpectedFunTys', but used when you have an "actual" type, 223-- for example in function application 224matchActualFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys] 225 -> CtOrigin 226 -> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType 227 -> Arity 228 -> TcSigmaType 229 -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) 230-- If matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r) 231-- then wrap : ty ~> (t1 -> ... -> tn -> ty_r) 232matchActualFunTys herald ct_orig mb_thing arity ty 233 = matchActualFunTysPart herald ct_orig mb_thing arity ty [] arity 234 235-- | Variant of 'matchActualFunTys' that works when supplied only part 236-- (that is, to the right of some arrows) of the full function type 237matchActualFunTysPart :: SDoc -- See Note [Herald for matchExpectedFunTys] 238 -> CtOrigin 239 -> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType 240 -> Arity 241 -> TcSigmaType 242 -> [TcSigmaType] -- reversed args. See (*) below. 243 -> Arity -- overall arity of the function, for errs 244 -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) 245matchActualFunTysPart herald ct_orig mb_thing arity orig_ty 246 orig_old_args full_arity 247 = go arity orig_old_args orig_ty 248-- Does not allocate unnecessary meta variables: if the input already is 249-- a function, we just take it apart. Not only is this efficient, 250-- it's important for higher rank: the argument might be of form 251-- (forall a. ty) -> other 252-- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd 253-- hide the forall inside a meta-variable 254 255-- (*) Sometimes it's necessary to call matchActualFunTys with only part 256-- (that is, to the right of some arrows) of the type of the function in 257-- question. (See TcExpr.tcArgs.) This argument is the reversed list of 258-- arguments already seen (that is, not part of the TcSigmaType passed 259-- in elsewhere). 260 261 where 262 -- This function has a bizarre mechanic: it accumulates arguments on 263 -- the way down and also builds an argument list on the way up. Why: 264 -- 1. The returns args list and the accumulated args list might be different. 265 -- The accumulated args include all the arg types for the function, 266 -- including those from before this function was called. The returned 267 -- list should include only those arguments produced by this call of 268 -- matchActualFunTys 269 -- 270 -- 2. The HsWrapper can be built only on the way up. It seems (more) 271 -- bizarre to build the HsWrapper but not the arg_tys. 272 -- 273 -- Refactoring is welcome. 274 go :: Arity 275 -> [TcSigmaType] -- accumulator of arguments (reversed) 276 -> TcSigmaType -- the remainder of the type as we're processing 277 -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) 278 go 0 _ ty = return (idHsWrapper, [], ty) 279 280 go n acc_args ty 281 | not (null tvs && null theta) 282 = do { (wrap1, rho) <- topInstantiate ct_orig ty 283 ; (wrap2, arg_tys, res_ty) <- go n acc_args rho 284 ; return (wrap2 <.> wrap1, arg_tys, res_ty) } 285 where 286 (tvs, theta, _) = tcSplitSigmaTy ty 287 288 go n acc_args ty 289 | Just ty' <- tcView ty = go n acc_args ty' 290 291 go n acc_args (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) 292 = ASSERT( af == VisArg ) 293 do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty : acc_args) res_ty 294 ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r doc 295 , arg_ty : tys, ty_r ) } 296 where 297 doc = text "When inferring the argument type of a function with type" <+> 298 quotes (ppr orig_ty) 299 300 go n acc_args ty@(TyVarTy tv) 301 | isMetaTyVar tv 302 = do { cts <- readMetaTyVar tv 303 ; case cts of 304 Indirect ty' -> go n acc_args ty' 305 Flexi -> defer n ty } 306 307 -- In all other cases we bale out into ordinary unification 308 -- However unlike the meta-tyvar case, we are sure that the 309 -- number of arguments doesn't match arity of the original 310 -- type, so we can add a bit more context to the error message 311 -- (cf #7869). 312 -- 313 -- It is not always an error, because specialized type may have 314 -- different arity, for example: 315 -- 316 -- > f1 = f2 'a' 317 -- > f2 :: Monad m => m Bool 318 -- > f2 = undefined 319 -- 320 -- But in that case we add specialized type into error context 321 -- anyway, because it may be useful. See also #9605. 322 go n acc_args ty = addErrCtxtM (mk_ctxt (reverse acc_args) ty) $ 323 defer n ty 324 325 ------------ 326 defer n fun_ty 327 = do { arg_tys <- replicateM n newOpenFlexiTyVarTy 328 ; res_ty <- newOpenFlexiTyVarTy 329 ; let unif_fun_ty = mkVisFunTys arg_tys res_ty 330 ; co <- unifyType mb_thing fun_ty unif_fun_ty 331 ; return (mkWpCastN co, arg_tys, res_ty) } 332 333 ------------ 334 mk_ctxt :: [TcSigmaType] -> TcSigmaType -> TidyEnv -> TcM (TidyEnv, MsgDoc) 335 mk_ctxt arg_tys res_ty env 336 = do { let ty = mkVisFunTys arg_tys res_ty 337 ; (env1, zonked) <- zonkTidyTcType env ty 338 -- zonking might change # of args 339 ; let (zonked_args, _) = tcSplitFunTys zonked 340 n_actual = length zonked_args 341 (env2, unzonked) = tidyOpenType env1 ty 342 ; return ( env2 343 , mk_fun_tys_msg unzonked zonked n_actual full_arity herald) } 344 345mk_fun_tys_msg :: TcType -- the full type passed in (unzonked) 346 -> TcType -- the full type passed in (zonked) 347 -> Arity -- the # of args found 348 -> Arity -- the # of args wanted 349 -> SDoc -- overall herald 350 -> SDoc 351mk_fun_tys_msg full_ty ty n_args full_arity herald 352 = herald <+> speakNOf full_arity (text "argument") <> comma $$ 353 if n_args == full_arity 354 then text "its type is" <+> quotes (pprType full_ty) <> 355 comma $$ 356 text "it is specialized to" <+> quotes (pprType ty) 357 else sep [text "but its type" <+> quotes (pprType ty), 358 if n_args == 0 then text "has none" 359 else text "has only" <+> speakN n_args] 360 361---------------------- 362matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType) 363-- Special case for lists 364matchExpectedListTy exp_ty 365 = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty 366 ; return (co, elt_ty) } 367 368--------------------- 369matchExpectedTyConApp :: TyCon -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> * 370 -> TcRhoType -- orig_ty 371 -> TcM (TcCoercionN, -- T k1 k2 k3 a b c ~N orig_ty 372 [TcSigmaType]) -- Element types, k1 k2 k3 a b c 373 374-- It's used for wired-in tycons, so we call checkWiredInTyCon 375-- Precondition: never called with FunTyCon 376-- Precondition: input type :: * 377-- Postcondition: (T k1 k2 k3 a b c) is well-kinded 378 379matchExpectedTyConApp tc orig_ty 380 = ASSERT(tc /= funTyCon) go orig_ty 381 where 382 go ty 383 | Just ty' <- tcView ty 384 = go ty' 385 386 go ty@(TyConApp tycon args) 387 | tc == tycon -- Common case 388 = return (mkTcNomReflCo ty, args) 389 390 go (TyVarTy tv) 391 | isMetaTyVar tv 392 = do { cts <- readMetaTyVar tv 393 ; case cts of 394 Indirect ty -> go ty 395 Flexi -> defer } 396 397 go _ = defer 398 399 -- If the common case does not occur, instantiate a template 400 -- T k1 .. kn t1 .. tm, and unify with the original type 401 -- Doing it this way ensures that the types we return are 402 -- kind-compatible with T. For example, suppose we have 403 -- matchExpectedTyConApp T (f Maybe) 404 -- where data T a = MkT a 405 -- Then we don't want to instantiate T's data constructors with 406 -- (a::*) ~ Maybe 407 -- because that'll make types that are utterly ill-kinded. 408 -- This happened in #7368 409 defer 410 = do { (_, arg_tvs) <- newMetaTyVars (tyConTyVars tc) 411 ; traceTc "matchExpectedTyConApp" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs) 412 ; let args = mkTyVarTys arg_tvs 413 tc_template = mkTyConApp tc args 414 ; co <- unifyType Nothing tc_template orig_ty 415 ; return (co, args) } 416 417---------------------- 418matchExpectedAppTy :: TcRhoType -- orig_ty 419 -> TcM (TcCoercion, -- m a ~N orig_ty 420 (TcSigmaType, TcSigmaType)) -- Returns m, a 421-- If the incoming type is a mutable type variable of kind k, then 422-- matchExpectedAppTy returns a new type variable (m: * -> k); note the *. 423 424matchExpectedAppTy orig_ty 425 = go orig_ty 426 where 427 go ty 428 | Just ty' <- tcView ty = go ty' 429 430 | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty 431 = return (mkTcNomReflCo orig_ty, (fun_ty, arg_ty)) 432 433 go (TyVarTy tv) 434 | isMetaTyVar tv 435 = do { cts <- readMetaTyVar tv 436 ; case cts of 437 Indirect ty -> go ty 438 Flexi -> defer } 439 440 go _ = defer 441 442 -- Defer splitting by generating an equality constraint 443 defer 444 = do { ty1 <- newFlexiTyVarTy kind1 445 ; ty2 <- newFlexiTyVarTy kind2 446 ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty 447 ; return (co, (ty1, ty2)) } 448 449 orig_kind = tcTypeKind orig_ty 450 kind1 = mkVisFunTy liftedTypeKind orig_kind 451 kind2 = liftedTypeKind -- m :: * -> k 452 -- arg type :: * 453 454{- 455************************************************************************ 456* * 457 Subsumption checking 458* * 459************************************************************************ 460 461Note [Subsumption checking: tcSubType] 462~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 463All the tcSubType calls have the form 464 tcSubType actual_ty expected_ty 465which checks 466 actual_ty <= expected_ty 467 468That is, that a value of type actual_ty is acceptable in 469a place expecting a value of type expected_ty. I.e. that 470 471 actual ty is more polymorphic than expected_ty 472 473It returns a coercion function 474 co_fn :: actual_ty ~ expected_ty 475which takes an HsExpr of type actual_ty into one of type 476expected_ty. 477 478These functions do not actually check for subsumption. They check if 479expected_ty is an appropriate annotation to use for something of type 480actual_ty. This difference matters when thinking about visible type 481application. For example, 482 483 forall a. a -> forall b. b -> b 484 DOES NOT SUBSUME 485 forall a b. a -> b -> b 486 487because the type arguments appear in a different order. (Neither does 488it work the other way around.) BUT, these types are appropriate annotations 489for one another. Because the user directs annotations, it's OK if some 490arguments shuffle around -- after all, it's what the user wants. 491Bottom line: none of this changes with visible type application. 492 493There are a number of wrinkles (below). 494 495Notice that Wrinkle 1 and 2 both require eta-expansion, which technically 496may increase termination. We just put up with this, in exchange for getting 497more predictable type inference. 498 499Wrinkle 1: Note [Deep skolemisation] 500~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 501We want (forall a. Int -> a -> a) <= (Int -> forall a. a->a) 502(see section 4.6 of "Practical type inference for higher rank types") 503So we must deeply-skolemise the RHS before we instantiate the LHS. 504 505That is why tc_sub_type starts with a call to tcSkolemise (which does the 506deep skolemisation), and then calls the DS variant (which assumes 507that expected_ty is deeply skolemised) 508 509Wrinkle 2: Note [Co/contra-variance of subsumption checking] 510~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 511Consider g :: (Int -> Int) -> Int 512 f1 :: (forall a. a -> a) -> Int 513 f1 = g 514 515 f2 :: (forall a. a -> a) -> Int 516 f2 x = g x 517f2 will typecheck, and it would be odd/fragile if f1 did not. 518But f1 will only typecheck if we have that 519 (Int->Int) -> Int <= (forall a. a->a) -> Int 520And that is only true if we do the full co/contravariant thing 521in the subsumption check. That happens in the FunTy case of 522tcSubTypeDS_NC_O, and is the sole reason for the WpFun form of 523HsWrapper. 524 525Another powerful reason for doing this co/contra stuff is visible 526in #9569, involving instantiation of constraint variables, 527and again involving eta-expansion. 528 529Wrinkle 3: Note [Higher rank types] 530~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 531Consider tc150: 532 f y = \ (x::forall a. a->a). blah 533The following happens: 534* We will infer the type of the RHS, ie with a res_ty = alpha. 535* Then the lambda will split alpha := beta -> gamma. 536* And then we'll check tcSubType IsSwapped beta (forall a. a->a) 537 538So it's important that we unify beta := forall a. a->a, rather than 539skolemising the type. 540-} 541 542 543-- | Call this variant when you are in a higher-rank situation and 544-- you know the right-hand type is deeply skolemised. 545tcSubTypeHR :: CtOrigin -- ^ of the actual type 546 -> Maybe (HsExpr GhcRn) -- ^ If present, it has type ty_actual 547 -> TcSigmaType -> ExpRhoType -> TcM HsWrapper 548tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt 549 550------------------------ 551tcSubTypeET :: CtOrigin -> UserTypeCtxt 552 -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper 553-- If wrap = tc_sub_type_et t1 t2 554-- => wrap :: t1 ~> t2 555tcSubTypeET orig ctxt (Check ty_actual) ty_expected 556 = tc_sub_tc_type eq_orig orig ctxt ty_actual ty_expected 557 where 558 eq_orig = TypeEqOrigin { uo_actual = ty_expected 559 , uo_expected = ty_actual 560 , uo_thing = Nothing 561 , uo_visible = True } 562 563tcSubTypeET _ _ (Infer inf_res) ty_expected 564 = ASSERT2( not (ir_inst inf_res), ppr inf_res $$ ppr ty_expected ) 565 -- An (Infer inf_res) ExpSigmaType passed into tcSubTypeET never 566 -- has the ir_inst field set. Reason: in patterns (which is what 567 -- tcSubTypeET is used for) do not aggressively instantiate 568 do { co <- fill_infer_result ty_expected inf_res 569 -- Since ir_inst is false, we can skip fillInferResult 570 -- and go straight to fill_infer_result 571 572 ; return (mkWpCastN (mkTcSymCo co)) } 573 574------------------------ 575tcSubTypeO :: CtOrigin -- ^ of the actual type 576 -> UserTypeCtxt -- ^ of the expected type 577 -> TcSigmaType 578 -> ExpRhoType 579 -> TcM HsWrapper 580tcSubTypeO orig ctxt ty_actual ty_expected 581 = addSubTypeCtxt ty_actual ty_expected $ 582 do { traceTc "tcSubTypeDS_O" (vcat [ pprCtOrigin orig 583 , pprUserTypeCtxt ctxt 584 , ppr ty_actual 585 , ppr ty_expected ]) 586 ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected } 587 588addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a 589addSubTypeCtxt ty_actual ty_expected thing_inside 590 | isRhoTy ty_actual -- If there is no polymorphism involved, the 591 , isRhoExpTy ty_expected -- TypeEqOrigin stuff (added by the _NC functions) 592 = thing_inside -- gives enough context by itself 593 | otherwise 594 = addErrCtxtM mk_msg thing_inside 595 where 596 mk_msg tidy_env 597 = do { (tidy_env, ty_actual) <- zonkTidyTcType tidy_env ty_actual 598 -- might not be filled if we're debugging. ugh. 599 ; mb_ty_expected <- readExpType_maybe ty_expected 600 ; (tidy_env, ty_expected) <- case mb_ty_expected of 601 Just ty -> second mkCheckExpType <$> 602 zonkTidyTcType tidy_env ty 603 Nothing -> return (tidy_env, ty_expected) 604 ; ty_expected <- readExpType ty_expected 605 ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected 606 ; let msg = vcat [ hang (text "When checking that:") 607 4 (ppr ty_actual) 608 , nest 2 (hang (text "is more polymorphic than:") 609 2 (ppr ty_expected)) ] 610 ; return (tidy_env, msg) } 611 612--------------- 613-- The "_NC" variants do not add a typechecker-error context; 614-- the caller is assumed to do that 615 616tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper 617-- Checks that actual <= expected 618-- Returns HsWrapper :: actual ~ expected 619tcSubType_NC ctxt ty_actual ty_expected 620 = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) 621 ; tc_sub_tc_type origin origin ctxt ty_actual ty_expected } 622 where 623 origin = TypeEqOrigin { uo_actual = ty_actual 624 , uo_expected = ty_expected 625 , uo_thing = Nothing 626 , uo_visible = True } 627 628tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper 629-- Just like tcSubType, but with the additional precondition that 630-- ty_expected is deeply skolemised (hence "DS") 631tcSubTypeDS orig ctxt ty_actual ty_expected 632 = addSubTypeCtxt ty_actual ty_expected $ 633 do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) 634 ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected } 635 636tcSubTypeDS_NC_O :: CtOrigin -- origin used for instantiation only 637 -> UserTypeCtxt 638 -> Maybe (HsExpr GhcRn) 639 -> TcSigmaType -> ExpRhoType -> TcM HsWrapper 640-- Just like tcSubType, but with the additional precondition that 641-- ty_expected is deeply skolemised 642tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected 643 = case ty_expected of 644 Infer inf_res -> fillInferResult inst_orig ty_actual inf_res 645 Check ty -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty 646 where 647 eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty 648 , uo_thing = ppr <$> m_thing 649 , uo_visible = True } 650 651--------------- 652tc_sub_tc_type :: CtOrigin -- used when calling uType 653 -> CtOrigin -- used when instantiating 654 -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper 655-- If wrap = tc_sub_type t1 t2 656-- => wrap :: t1 ~> t2 657tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected 658 | definitely_poly ty_expected -- See Note [Don't skolemise unnecessarily] 659 , not (possibly_poly ty_actual) 660 = do { traceTc "tc_sub_tc_type (drop to equality)" $ 661 vcat [ text "ty_actual =" <+> ppr ty_actual 662 , text "ty_expected =" <+> ppr ty_expected ] 663 ; mkWpCastN <$> 664 uType TypeLevel eq_orig ty_actual ty_expected } 665 666 | otherwise -- This is the general case 667 = do { traceTc "tc_sub_tc_type (general case)" $ 668 vcat [ text "ty_actual =" <+> ppr ty_actual 669 , text "ty_expected =" <+> ppr ty_expected ] 670 ; (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $ 671 \ _ sk_rho -> 672 tc_sub_type_ds eq_orig inst_orig ctxt 673 ty_actual sk_rho 674 ; return (sk_wrap <.> inner_wrap) } 675 where 676 possibly_poly ty 677 | isForAllTy ty = True 678 | Just (_, res) <- splitFunTy_maybe ty = possibly_poly res 679 | otherwise = False 680 -- NB *not* tcSplitFunTy, because here we want 681 -- to decompose type-class arguments too 682 683 definitely_poly ty 684 | (tvs, theta, tau) <- tcSplitSigmaTy ty 685 , (tv:_) <- tvs 686 , null theta 687 , isInsolubleOccursCheck NomEq tv tau 688 = True 689 | otherwise 690 = False 691 692{- Note [Don't skolemise unnecessarily] 693~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 694Suppose we are trying to solve 695 (Char->Char) <= (forall a. a->a) 696We could skolemise the 'forall a', and then complain 697that (Char ~ a) is insoluble; but that's a pretty obscure 698error. It's better to say that 699 (Char->Char) ~ (forall a. a->a) 700fails. 701 702So roughly: 703 * if the ty_expected has an outermost forall 704 (i.e. skolemisation is the next thing we'd do) 705 * and the ty_actual has no top-level polymorphism (but looking deeply) 706then we can revert to simple equality. But we need to be careful. 707These examples are all fine: 708 709 * (Char -> forall a. a->a) <= (forall a. Char -> a -> a) 710 Polymorphism is buried in ty_actual 711 712 * (Char->Char) <= (forall a. Char -> Char) 713 ty_expected isn't really polymorphic 714 715 * (Char->Char) <= (forall a. (a~Char) => a -> a) 716 ty_expected isn't really polymorphic 717 718 * (Char->Char) <= (forall a. F [a] Char -> Char) 719 where type instance F [x] t = t 720 ty_expected isn't really polymorphic 721 722If we prematurely go to equality we'll reject a program we should 723accept (e.g. #13752). So the test (which is only to improve 724error message) is very conservative: 725 * ty_actual is /definitely/ monomorphic 726 * ty_expected is /definitely/ polymorphic 727-} 728 729--------------- 730tc_sub_type_ds :: CtOrigin -- used when calling uType 731 -> CtOrigin -- used when instantiating 732 -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper 733-- If wrap = tc_sub_type_ds t1 t2 734-- => wrap :: t1 ~> t2 735-- Here is where the work actually happens! 736-- Precondition: ty_expected is deeply skolemised 737tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected 738 = do { traceTc "tc_sub_type_ds" $ 739 vcat [ text "ty_actual =" <+> ppr ty_actual 740 , text "ty_expected =" <+> ppr ty_expected ] 741 ; go ty_actual ty_expected } 742 where 743 go ty_a ty_e | Just ty_a' <- tcView ty_a = go ty_a' ty_e 744 | Just ty_e' <- tcView ty_e = go ty_a ty_e' 745 746 go (TyVarTy tv_a) ty_e 747 = do { lookup_res <- lookupTcTyVar tv_a 748 ; case lookup_res of 749 Filled ty_a' -> 750 do { traceTc "tcSubTypeDS_NC_O following filled act meta-tyvar:" 751 (ppr tv_a <+> text "-->" <+> ppr ty_a') 752 ; tc_sub_type_ds eq_orig inst_orig ctxt ty_a' ty_e } 753 Unfilled _ -> unify } 754 755 -- Historical note (Sept 16): there was a case here for 756 -- go ty_a (TyVarTy alpha) 757 -- which, in the impredicative case unified alpha := ty_a 758 -- where th_a is a polytype. Not only is this probably bogus (we 759 -- simply do not have decent story for impredicative types), but it 760 -- caused #12616 because (also bizarrely) 'deriving' code had 761 -- -XImpredicativeTypes on. I deleted the entire case. 762 763 go (FunTy { ft_af = VisArg, ft_arg = act_arg, ft_res = act_res }) 764 (FunTy { ft_af = VisArg, ft_arg = exp_arg, ft_res = exp_res }) 765 = -- See Note [Co/contra-variance of subsumption checking] 766 do { res_wrap <- tc_sub_type_ds eq_orig inst_orig ctxt act_res exp_res 767 ; arg_wrap <- tc_sub_tc_type eq_orig given_orig GenSigCtxt exp_arg act_arg 768 -- GenSigCtxt: See Note [Setting the argument context] 769 ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res doc) } 770 -- arg_wrap :: exp_arg ~> act_arg 771 -- res_wrap :: act-res ~> exp_res 772 where 773 given_orig = GivenOrigin (SigSkol GenSigCtxt exp_arg []) 774 doc = text "When checking that" <+> quotes (ppr ty_actual) <+> 775 text "is more polymorphic than" <+> quotes (ppr ty_expected) 776 777 go ty_a ty_e 778 | let (tvs, theta, _) = tcSplitSigmaTy ty_a 779 , not (null tvs && null theta) 780 = do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a 781 ; body_wrap <- tc_sub_type_ds 782 (eq_orig { uo_actual = in_rho 783 , uo_expected = ty_expected }) 784 inst_orig ctxt in_rho ty_e 785 ; return (body_wrap <.> in_wrap) } 786 787 | otherwise -- Revert to unification 788 = inst_and_unify 789 -- It's still possible that ty_actual has nested foralls. Instantiate 790 -- these, as there's no way unification will succeed with them in. 791 -- See typecheck/should_compile/T11305 for an example of when this 792 -- is important. The problem is that we're checking something like 793 -- a -> forall b. b -> b <= alpha beta gamma 794 -- where we end up with alpha := (->) 795 796 inst_and_unify = do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual 797 798 -- If we haven't recurred through an arrow, then 799 -- the eq_orig will list ty_actual. In this case, 800 -- we want to update the origin to reflect the 801 -- instantiation. If we *have* recurred through 802 -- an arrow, it's better not to update. 803 ; let eq_orig' = case eq_orig of 804 TypeEqOrigin { uo_actual = orig_ty_actual } 805 | orig_ty_actual `tcEqType` ty_actual 806 , not (isIdHsWrapper wrap) 807 -> eq_orig { uo_actual = rho_a } 808 _ -> eq_orig 809 810 ; cow <- uType TypeLevel eq_orig' rho_a ty_expected 811 ; return (mkWpCastN cow <.> wrap) } 812 813 814 -- use versions without synonyms expanded 815 unify = mkWpCastN <$> uType TypeLevel eq_orig ty_actual ty_expected 816 817{- Note [Settting the argument context] 818~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 819Consider we are doing the ambiguity check for the (bogus) 820 f :: (forall a b. C b => a -> a) -> Int 821 822We'll call 823 tcSubType ((forall a b. C b => a->a) -> Int ) 824 ((forall a b. C b => a->a) -> Int ) 825 826with a UserTypeCtxt of (FunSigCtxt "f"). Then we'll do the co/contra thing 827on the argument type of the (->) -- and at that point we want to switch 828to a UserTypeCtxt of GenSigCtxt. Why? 829 830* Error messages. If we stick with FunSigCtxt we get errors like 831 * Could not deduce: C b 832 from the context: C b0 833 bound by the type signature for: 834 f :: forall a b. C b => a->a 835 But of course f does not have that type signature! 836 Example tests: T10508, T7220a, Simple14 837 838* Implications. We may decide to build an implication for the whole 839 ambiguity check, but we don't need one for each level within it, 840 and TcUnify.alwaysBuildImplication checks the UserTypeCtxt. 841 See Note [When to build an implication] 842-} 843 844----------------- 845-- needs both un-type-checked (for origins) and type-checked (for wrapping) 846-- expressions 847tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType 848 -> TcM (HsExpr GhcTcId) 849tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr 850 851-- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more 852-- convenient. 853tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType 854 -> TcM (HsExpr GhcTcId) 855tcWrapResultO orig rn_expr expr actual_ty res_ty 856 = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty 857 , text "Expected:" <+> ppr res_ty ]) 858 ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt 859 (Just rn_expr) actual_ty res_ty 860 ; return (mkHsWrap cow expr) } 861 862 863{- ********************************************************************** 864%* * 865 ExpType functions: tcInfer, fillInferResult 866%* * 867%********************************************************************* -} 868 869-- | Infer a type using a fresh ExpType 870-- See also Note [ExpType] in TcMType 871-- Does not attempt to instantiate the inferred type 872tcInferNoInst :: (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) 873tcInferNoInst = tcInfer False 874 875tcInferInst :: (ExpRhoType -> TcM a) -> TcM (a, TcRhoType) 876tcInferInst = tcInfer True 877 878tcInfer :: Bool -> (ExpSigmaType -> TcM a) -> TcM (a, TcSigmaType) 879tcInfer instantiate tc_check 880 = do { res_ty <- newInferExpType instantiate 881 ; result <- tc_check res_ty 882 ; res_ty <- readExpType res_ty 883 ; return (result, res_ty) } 884 885fillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper 886-- If wrap = fillInferResult t1 t2 887-- => wrap :: t1 ~> t2 888-- See Note [Deep instantiation of InferResult] 889fillInferResult orig ty inf_res@(IR { ir_inst = instantiate_me }) 890 | instantiate_me 891 = do { (wrap, rho) <- deeplyInstantiate orig ty 892 ; co <- fill_infer_result rho inf_res 893 ; return (mkWpCastN co <.> wrap) } 894 895 | otherwise 896 = do { co <- fill_infer_result ty inf_res 897 ; return (mkWpCastN co) } 898 899fill_infer_result :: TcType -> InferResult -> TcM TcCoercionN 900-- If wrap = fill_infer_result t1 t2 901-- => wrap :: t1 ~> t2 902fill_infer_result orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl 903 , ir_ref = ref }) 904 = do { (ty_co, ty_to_fill_with) <- promoteTcType res_lvl orig_ty 905 906 ; traceTc "Filling ExpType" $ 907 ppr u <+> text ":=" <+> ppr ty_to_fill_with 908 909 ; when debugIsOn (check_hole ty_to_fill_with) 910 911 ; writeTcRef ref (Just ty_to_fill_with) 912 913 ; return ty_co } 914 where 915 check_hole ty -- Debug check only 916 = do { let ty_lvl = tcTypeLevel ty 917 ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl), 918 ppr u $$ ppr res_lvl $$ ppr ty_lvl $$ 919 ppr ty <+> dcolon <+> ppr (tcTypeKind ty) $$ ppr orig_ty ) 920 ; cts <- readTcRef ref 921 ; case cts of 922 Just already_there -> pprPanic "writeExpType" 923 (vcat [ ppr u 924 , ppr ty 925 , ppr already_there ]) 926 Nothing -> return () } 927 928{- Note [Deep instantiation of InferResult] 929~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 930In some cases we want to deeply instantiate before filling in 931an InferResult, and in some cases not. That's why InferReult 932has the ir_inst flag. 933 934ir_inst = True: deeply instantiate 935---------------------------------- 936 9371. Consider 938 f x = (*) 939 We want to instantiate the type of (*) before returning, else we 940 will infer the type 941 f :: forall {a}. a -> forall b. Num b => b -> b -> b 942 This is surely confusing for users. 943 944 And worse, the monomorphism restriction won't work properly. The MR is 945 dealt with in simplifyInfer, and simplifyInfer has no way of 946 instantiating. This could perhaps be worked around, but it may be 947 hard to know even when instantiation should happen. 948 9492. Another reason. Consider 950 f :: (?x :: Int) => a -> a 951 g y = let ?x = 3::Int in f 952 Here want to instantiate f's type so that the ?x::Int constraint 953 gets discharged by the enclosing implicit-parameter binding. 954 955ir_inst = False: do not instantiate 956----------------------------------- 957 9581. Consider this (which uses visible type application): 959 960 (let { f :: forall a. a -> a; f x = x } in f) @Int 961 962 We'll call TcExpr.tcInferFun to infer the type of the (let .. in f) 963 And we don't want to instantite the type of 'f' when we reach it, 964 else the outer visible type application won't work 965 9662. :type +v. When we say 967 968 :type +v const @Int 969 970 we really want `forall b. Int -> b -> Int`. Note that this is *not* 971 instantiated. 972 9733. Pattern bindings. For example: 974 975 foo x 976 | blah <- const @Int 977 = (blah x False, blah x 'z') 978 979 Note that `blah` is polymorphic. (This isn't a terribly compelling 980 reason, but the choice of ir_inst does matter here.) 981 982Discussion 983---------- 984We thought that we should just remove the ir_inst flag, in favor of 985always instantiating. Essentially: motivations (1) and (3) for ir_inst = False 986are not terribly exciting. However, motivation (2) is quite important. 987Furthermore, there really was not much of a simplification of the code 988in removing ir_inst, and working around it to enable flows like what we 989see in (2) is annoying. This was done in #17173. 990 991-} 992 993{- ********************************************************************* 994* * 995 Promoting types 996* * 997********************************************************************* -} 998 999promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType) 1000-- See Note [Promoting a type] 1001-- promoteTcType level ty = (co, ty') 1002-- * Returns ty' whose max level is just 'level' 1003-- and whose kind is ~# to the kind of 'ty' 1004-- and whose kind has form TYPE rr 1005-- * and co :: ty ~ ty' 1006-- * and emits constraints to justify the coercion 1007promoteTcType dest_lvl ty 1008 = do { cur_lvl <- getTcLevel 1009 ; if (cur_lvl `sameDepthAs` dest_lvl) 1010 then dont_promote_it 1011 else promote_it } 1012 where 1013 promote_it :: TcM (TcCoercion, TcType) 1014 promote_it -- Emit a constraint (alpha :: TYPE rr) ~ ty 1015 -- where alpha and rr are fresh and from level dest_lvl 1016 = do { rr <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy 1017 ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr) 1018 ; let eq_orig = TypeEqOrigin { uo_actual = ty 1019 , uo_expected = prom_ty 1020 , uo_thing = Nothing 1021 , uo_visible = False } 1022 1023 ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty 1024 ; return (co, prom_ty) } 1025 1026 dont_promote_it :: TcM (TcCoercion, TcType) 1027 dont_promote_it -- Check that ty :: TYPE rr, for some (fresh) rr 1028 = do { res_kind <- newOpenTypeKind 1029 ; let ty_kind = tcTypeKind ty 1030 kind_orig = TypeEqOrigin { uo_actual = ty_kind 1031 , uo_expected = res_kind 1032 , uo_thing = Nothing 1033 , uo_visible = False } 1034 ; ki_co <- uType KindLevel kind_orig (tcTypeKind ty) res_kind 1035 ; let co = mkTcGReflRightCo Nominal ty ki_co 1036 ; return (co, ty `mkCastTy` ki_co) } 1037 1038{- Note [Promoting a type] 1039~~~~~~~~~~~~~~~~~~~~~~~~~~ 1040Consider (#12427) 1041 1042 data T where 1043 MkT :: (Int -> Int) -> a -> T 1044 1045 h y = case y of MkT v w -> v 1046 1047We'll infer the RHS type with an expected type ExpType of 1048 (IR { ir_lvl = l, ir_ref = ref, ... ) 1049where 'l' is the TcLevel of the RHS of 'h'. Then the MkT pattern 1050match will increase the level, so we'll end up in tcSubType, trying to 1051unify the type of v, 1052 v :: Int -> Int 1053with the expected type. But this attempt takes place at level (l+1), 1054rightly so, since v's type could have mentioned existential variables, 1055(like w's does) and we want to catch that. 1056 1057So we 1058 - create a new meta-var alpha[l+1] 1059 - fill in the InferRes ref cell 'ref' with alpha 1060 - emit an equality constraint, thus 1061 [W] alpha[l+1] ~ (Int -> Int) 1062 1063That constraint will float outwards, as it should, unless v's 1064type mentions a skolem-captured variable. 1065 1066This approach fails if v has a higher rank type; see 1067Note [Promotion and higher rank types] 1068 1069 1070Note [Promotion and higher rank types] 1071~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1072If v had a higher-rank type, say v :: (forall a. a->a) -> Int, 1073then we'd emit an equality 1074 [W] alpha[l+1] ~ ((forall a. a->a) -> Int) 1075which will sadly fail because we can't unify a unification variable 1076with a polytype. But there is nothing really wrong with the program 1077here. 1078 1079We could just about solve this by "promote the type" of v, to expose 1080its polymorphic "shape" while still leaving constraints that will 1081prevent existential escape. But we must be careful! Exposing 1082the "shape" of the type is precisely what we must NOT do under 1083a GADT pattern match! So in this case we might promote the type 1084to 1085 (forall a. a->a) -> alpha[l+1] 1086and emit the constraint 1087 [W] alpha[l+1] ~ Int 1088Now the promoted type can fill the ref cell, while the emitted 1089equality can float or not, according to the usual rules. 1090 1091But that's not quite right! We are exposing the arrow! We could 1092deal with that too: 1093 (forall a. mu[l+1] a a) -> alpha[l+1] 1094with constraints 1095 [W] alpha[l+1] ~ Int 1096 [W] mu[l+1] ~ (->) 1097Here we abstract over the '->' inside the forall, in case that 1098is subject to an equality constraint from a GADT match. 1099 1100Note that we kept the outer (->) because that's part of 1101the polymorphic "shape". And because of impredicativity, 1102GADT matches can't give equalities that affect polymorphic 1103shape. 1104 1105This reasoning just seems too complicated, so I decided not 1106to do it. These higher-rank notes are just here to record 1107the thinking. 1108-} 1109 1110{- ********************************************************************* 1111* * 1112 Generalisation 1113* * 1114********************************************************************* -} 1115 1116-- | Take an "expected type" and strip off quantifiers to expose the 1117-- type underneath, binding the new skolems for the @thing_inside@. 1118-- The returned 'HsWrapper' has type @specific_ty -> expected_ty@. 1119tcSkolemise :: UserTypeCtxt -> TcSigmaType 1120 -> ([TcTyVar] -> TcType -> TcM result) 1121 -- ^ These are only ever used for scoped type variables. 1122 -> TcM (HsWrapper, result) 1123 -- ^ The expression has type: spec_ty -> expected_ty 1124 1125tcSkolemise ctxt expected_ty thing_inside 1126 -- We expect expected_ty to be a forall-type 1127 -- If not, the call is a no-op 1128 = do { traceTc "tcSkolemise" Outputable.empty 1129 ; (wrap, tv_prs, given, rho') <- deeplySkolemise expected_ty 1130 1131 ; lvl <- getTcLevel 1132 ; when debugIsOn $ 1133 traceTc "tcSkolemise" $ vcat [ 1134 ppr lvl, 1135 text "expected_ty" <+> ppr expected_ty, 1136 text "inst tyvars" <+> ppr tv_prs, 1137 text "given" <+> ppr given, 1138 text "inst type" <+> ppr rho' ] 1139 1140 -- Generally we must check that the "forall_tvs" havn't been constrained 1141 -- The interesting bit here is that we must include the free variables 1142 -- of the expected_ty. Here's an example: 1143 -- runST (newVar True) 1144 -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool)) 1145 -- for (newVar True), with s fresh. Then we unify with the runST's arg type 1146 -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool. 1147 -- So now s' isn't unconstrained because it's linked to a. 1148 -- 1149 -- However [Oct 10] now that the untouchables are a range of 1150 -- TcTyVars, all this is handled automatically with no need for 1151 -- extra faffing around 1152 1153 ; let tvs' = map snd tv_prs 1154 skol_info = SigSkol ctxt expected_ty tv_prs 1155 1156 ; (ev_binds, result) <- checkConstraints skol_info tvs' given $ 1157 thing_inside tvs' rho' 1158 1159 ; return (wrap <.> mkWpLet ev_binds, result) } 1160 -- The ev_binds returned by checkConstraints is very 1161 -- often empty, in which case mkWpLet is a no-op 1162 1163-- | Variant of 'tcSkolemise' that takes an ExpType 1164tcSkolemiseET :: UserTypeCtxt -> ExpSigmaType 1165 -> (ExpRhoType -> TcM result) 1166 -> TcM (HsWrapper, result) 1167tcSkolemiseET _ et@(Infer {}) thing_inside 1168 = (idHsWrapper, ) <$> thing_inside et 1169tcSkolemiseET ctxt (Check ty) thing_inside 1170 = tcSkolemise ctxt ty $ \_ -> thing_inside . mkCheckExpType 1171 1172checkConstraints :: SkolemInfo 1173 -> [TcTyVar] -- Skolems 1174 -> [EvVar] -- Given 1175 -> TcM result 1176 -> TcM (TcEvBinds, result) 1177 1178checkConstraints skol_info skol_tvs given thing_inside 1179 = do { implication_needed <- implicationNeeded skol_info skol_tvs given 1180 1181 ; if implication_needed 1182 then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside 1183 ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted 1184 ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs) 1185 ; emitImplications implics 1186 ; return (ev_binds, result) } 1187 1188 else -- Fast path. We check every function argument with 1189 -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints. 1190 -- So this fast path is well-exercised 1191 do { res <- thing_inside 1192 ; return (emptyTcEvBinds, res) } } 1193 1194checkTvConstraints :: SkolemInfo 1195 -> [TcTyVar] -- Skolem tyvars 1196 -> TcM result 1197 -> TcM result 1198 1199checkTvConstraints skol_info skol_tvs thing_inside 1200 = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside 1201 ; emitResidualTvConstraint skol_info Nothing skol_tvs tclvl wanted 1202 ; return result } 1203 1204emitResidualTvConstraint :: SkolemInfo -> Maybe SDoc -> [TcTyVar] 1205 -> TcLevel -> WantedConstraints -> TcM () 1206emitResidualTvConstraint skol_info m_telescope skol_tvs tclvl wanted 1207 | isEmptyWC wanted 1208 , isNothing m_telescope || skol_tvs `lengthAtMost` 1 1209 -- If m_telescope is (Just d), we must do the bad-telescope check, 1210 -- so we must /not/ discard the implication even if there are no 1211 -- wanted constraints. See Note [Checking telescopes] in Constraint. 1212 -- Lacking this check led to #16247 1213 = return () 1214 1215 | otherwise 1216 = do { ev_binds <- newNoTcEvBinds 1217 ; implic <- newImplication 1218 ; let status | insolubleWC wanted = IC_Insoluble 1219 | otherwise = IC_Unsolved 1220 -- If the inner constraints are insoluble, 1221 -- we should mark the outer one similarly, 1222 -- so that insolubleWC works on the outer one 1223 1224 ; emitImplication $ 1225 implic { ic_status = status 1226 , ic_tclvl = tclvl 1227 , ic_skols = skol_tvs 1228 , ic_no_eqs = True 1229 , ic_telescope = m_telescope 1230 , ic_wanted = wanted 1231 , ic_binds = ev_binds 1232 , ic_info = skol_info } } 1233 1234implicationNeeded :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM Bool 1235-- See Note [When to build an implication] 1236implicationNeeded skol_info skol_tvs given 1237 | null skol_tvs 1238 , null given 1239 , not (alwaysBuildImplication skol_info) 1240 = -- Empty skolems and givens 1241 do { tc_lvl <- getTcLevel 1242 ; if not (isTopTcLevel tc_lvl) -- No implication needed if we are 1243 then return False -- already inside an implication 1244 else 1245 do { dflags <- getDynFlags -- If any deferral can happen, 1246 -- we must build an implication 1247 ; return (gopt Opt_DeferTypeErrors dflags || 1248 gopt Opt_DeferTypedHoles dflags || 1249 gopt Opt_DeferOutOfScopeVariables dflags) } } 1250 1251 | otherwise -- Non-empty skolems or givens 1252 = return True -- Definitely need an implication 1253 1254alwaysBuildImplication :: SkolemInfo -> Bool 1255-- See Note [When to build an implication] 1256alwaysBuildImplication _ = False 1257 1258{- Commmented out for now while I figure out about error messages. 1259 See #14185 1260 1261alwaysBuildImplication (SigSkol ctxt _ _) 1262 = case ctxt of 1263 FunSigCtxt {} -> True -- RHS of a binding with a signature 1264 _ -> False 1265alwaysBuildImplication (RuleSkol {}) = True 1266alwaysBuildImplication (InstSkol {}) = True 1267alwaysBuildImplication (FamInstSkol {}) = True 1268alwaysBuildImplication _ = False 1269-} 1270 1271buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar] 1272 -> [EvVar] -> WantedConstraints 1273 -> TcM (Bag Implication, TcEvBinds) 1274buildImplicationFor tclvl skol_info skol_tvs given wanted 1275 | isEmptyWC wanted && null given 1276 -- Optimisation : if there are no wanteds, and no givens 1277 -- don't generate an implication at all. 1278 -- Reason for the (null given): we don't want to lose 1279 -- the "inaccessible alternative" error check 1280 = return (emptyBag, emptyTcEvBinds) 1281 1282 | otherwise 1283 = ASSERT2( all (isSkolemTyVar <||> isTyVarTyVar) skol_tvs, ppr skol_tvs ) 1284 -- Why allow TyVarTvs? Because implicitly declared kind variables in 1285 -- non-CUSK type declarations are TyVarTvs, and we need to bring them 1286 -- into scope as a skolem in an implication. This is OK, though, 1287 -- because TyVarTvs will always remain tyvars, even after unification. 1288 do { ev_binds_var <- newTcEvBinds 1289 ; implic <- newImplication 1290 ; let implic' = implic { ic_tclvl = tclvl 1291 , ic_skols = skol_tvs 1292 , ic_given = given 1293 , ic_wanted = wanted 1294 , ic_binds = ev_binds_var 1295 , ic_info = skol_info } 1296 1297 ; return (unitBag implic', TcEvBinds ev_binds_var) } 1298 1299{- Note [When to build an implication] 1300~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1301Suppose we have some 'skolems' and some 'givens', and we are 1302considering whether to wrap the constraints in their scope into an 1303implication. We must /always/ so if either 'skolems' or 'givens' are 1304non-empty. But what if both are empty? You might think we could 1305always drop the implication. Other things being equal, the fewer 1306implications the better. Less clutter and overhead. But we must 1307take care: 1308 1309* If we have an unsolved [W] g :: a ~# b, and -fdefer-type-errors, 1310 we'll make a /term-level/ evidence binding for 'g = error "blah"'. 1311 We must have an EvBindsVar those bindings!, otherwise they end up as 1312 top-level unlifted bindings, which are verboten. This only matters 1313 at top level, so we check for that 1314 See also Note [Deferred errors for coercion holes] in TcErrors. 1315 cf #14149 for an example of what goes wrong. 1316 1317* If you have 1318 f :: Int; f = f_blah 1319 g :: Bool; g = g_blah 1320 If we don't build an implication for f or g (no tyvars, no givens), 1321 the constraints for f_blah and g_blah are solved together. And that 1322 can yield /very/ confusing error messages, because we can get 1323 [W] C Int b1 -- from f_blah 1324 [W] C Int b2 -- from g_blan 1325 and fundpes can yield [D] b1 ~ b2, even though the two functions have 1326 literally nothing to do with each other. #14185 is an example. 1327 Building an implication keeps them separage. 1328-} 1329 1330{- 1331************************************************************************ 1332* * 1333 Boxy unification 1334* * 1335************************************************************************ 1336 1337The exported functions are all defined as versions of some 1338non-exported generic functions. 1339-} 1340 1341unifyType :: Maybe (HsExpr GhcRn) -- ^ If present, has type 'ty1' 1342 -> TcTauType -> TcTauType -> TcM TcCoercionN 1343-- Actual and expected types 1344-- Returns a coercion : ty1 ~ ty2 1345unifyType thing ty1 ty2 = traceTc "utype" (ppr ty1 $$ ppr ty2 $$ ppr thing) >> 1346 uType TypeLevel origin ty1 ty2 1347 where 1348 origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 1349 , uo_thing = ppr <$> thing 1350 , uo_visible = True } -- always called from a visible context 1351 1352unifyKind :: Maybe (HsType GhcRn) -> TcKind -> TcKind -> TcM CoercionN 1353unifyKind thing ty1 ty2 = traceTc "ukind" (ppr ty1 $$ ppr ty2 $$ ppr thing) >> 1354 uType KindLevel origin ty1 ty2 1355 where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 1356 , uo_thing = ppr <$> thing 1357 , uo_visible = True } -- also always from a visible context 1358 1359--------------- 1360 1361{- 1362%************************************************************************ 1363%* * 1364 uType and friends 1365%* * 1366%************************************************************************ 1367 1368uType is the heart of the unifier. 1369-} 1370 1371uType, uType_defer 1372 :: TypeOrKind 1373 -> CtOrigin 1374 -> TcType -- ty1 is the *actual* type 1375 -> TcType -- ty2 is the *expected* type 1376 -> TcM CoercionN 1377 1378-------------- 1379-- It is always safe to defer unification to the main constraint solver 1380-- See Note [Deferred unification] 1381uType_defer t_or_k origin ty1 ty2 1382 = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2 1383 1384 -- Error trace only 1385 -- NB. do *not* call mkErrInfo unless tracing is on, 1386 -- because it is hugely expensive (#5631) 1387 ; whenDOptM Opt_D_dump_tc_trace $ do 1388 { ctxt <- getErrCtxt 1389 ; doc <- mkErrInfo emptyTidyEnv ctxt 1390 ; traceTc "utype_defer" (vcat [ debugPprType ty1 1391 , debugPprType ty2 1392 , pprCtOrigin origin 1393 , doc]) 1394 ; traceTc "utype_defer2" (ppr co) 1395 } 1396 ; return co } 1397 1398-------------- 1399uType t_or_k origin orig_ty1 orig_ty2 1400 = do { tclvl <- getTcLevel 1401 ; traceTc "u_tys" $ vcat 1402 [ text "tclvl" <+> ppr tclvl 1403 , sep [ ppr orig_ty1, text "~", ppr orig_ty2] 1404 , pprCtOrigin origin] 1405 ; co <- go orig_ty1 orig_ty2 1406 ; if isReflCo co 1407 then traceTc "u_tys yields no coercion" Outputable.empty 1408 else traceTc "u_tys yields coercion:" (ppr co) 1409 ; return co } 1410 where 1411 go :: TcType -> TcType -> TcM CoercionN 1412 -- The arguments to 'go' are always semantically identical 1413 -- to orig_ty{1,2} except for looking through type synonyms 1414 1415 -- Unwrap casts before looking for variables. This way, we can easily 1416 -- recognize (t |> co) ~ (t |> co), which is nice. Previously, we 1417 -- didn't do it this way, and then the unification above was deferred. 1418 go (CastTy t1 co1) t2 1419 = do { co_tys <- uType t_or_k origin t1 t2 1420 ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) } 1421 1422 go t1 (CastTy t2 co2) 1423 = do { co_tys <- uType t_or_k origin t1 t2 1424 ; return (mkCoherenceRightCo Nominal t2 co2 co_tys) } 1425 1426 -- Variables; go for uUnfilledVar 1427 -- Note that we pass in *original* (before synonym expansion), 1428 -- so that type variables tend to get filled in with 1429 -- the most informative version of the type 1430 go (TyVarTy tv1) ty2 1431 = do { lookup_res <- lookupTcTyVar tv1 1432 ; case lookup_res of 1433 Filled ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1) 1434 ; go ty1 ty2 } 1435 Unfilled _ -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 } 1436 go ty1 (TyVarTy tv2) 1437 = do { lookup_res <- lookupTcTyVar tv2 1438 ; case lookup_res of 1439 Filled ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2) 1440 ; go ty1 ty2 } 1441 Unfilled _ -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 } 1442 1443 -- See Note [Expanding synonyms during unification] 1444 go ty1@(TyConApp tc1 []) (TyConApp tc2 []) 1445 | tc1 == tc2 1446 = return $ mkNomReflCo ty1 1447 1448 -- See Note [Expanding synonyms during unification] 1449 -- 1450 -- Also NB that we recurse to 'go' so that we don't push a 1451 -- new item on the origin stack. As a result if we have 1452 -- type Foo = Int 1453 -- and we try to unify Foo ~ Bool 1454 -- we'll end up saying "can't match Foo with Bool" 1455 -- rather than "can't match "Int with Bool". See #4535. 1456 go ty1 ty2 1457 | Just ty1' <- tcView ty1 = go ty1' ty2 1458 | Just ty2' <- tcView ty2 = go ty1 ty2' 1459 1460 -- Functions (or predicate functions) just check the two parts 1461 go (FunTy _ fun1 arg1) (FunTy _ fun2 arg2) 1462 = do { co_l <- uType t_or_k origin fun1 fun2 1463 ; co_r <- uType t_or_k origin arg1 arg2 1464 ; return $ mkFunCo Nominal co_l co_r } 1465 1466 -- Always defer if a type synonym family (type function) 1467 -- is involved. (Data families behave rigidly.) 1468 go ty1@(TyConApp tc1 _) ty2 1469 | isTypeFamilyTyCon tc1 = defer ty1 ty2 1470 go ty1 ty2@(TyConApp tc2 _) 1471 | isTypeFamilyTyCon tc2 = defer ty1 ty2 1472 1473 go (TyConApp tc1 tys1) (TyConApp tc2 tys2) 1474 -- See Note [Mismatched type lists and application decomposition] 1475 | tc1 == tc2, equalLength tys1 tys2 1476 = ASSERT2( isGenerativeTyCon tc1 Nominal, ppr tc1 ) 1477 do { cos <- zipWith3M (uType t_or_k) origins' tys1 tys2 1478 ; return $ mkTyConAppCo Nominal tc1 cos } 1479 where 1480 origins' = map (\is_vis -> if is_vis then origin else toInvisibleOrigin origin) 1481 (tcTyConVisibilities tc1) 1482 1483 go (LitTy m) ty@(LitTy n) 1484 | m == n 1485 = return $ mkNomReflCo ty 1486 1487 -- See Note [Care with type applications] 1488 -- Do not decompose FunTy against App; 1489 -- it's often a type error, so leave it for the constraint solver 1490 go (AppTy s1 t1) (AppTy s2 t2) 1491 = go_app (isNextArgVisible s1) s1 t1 s2 t2 1492 1493 go (AppTy s1 t1) (TyConApp tc2 ts2) 1494 | Just (ts2', t2') <- snocView ts2 1495 = ASSERT( not (mustBeSaturated tc2) ) 1496 go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2' 1497 1498 go (TyConApp tc1 ts1) (AppTy s2 t2) 1499 | Just (ts1', t1') <- snocView ts1 1500 = ASSERT( not (mustBeSaturated tc1) ) 1501 go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2 1502 1503 go (CoercionTy co1) (CoercionTy co2) 1504 = do { let ty1 = coercionType co1 1505 ty2 = coercionType co2 1506 ; kco <- uType KindLevel 1507 (KindEqOrigin orig_ty1 (Just orig_ty2) origin 1508 (Just t_or_k)) 1509 ty1 ty2 1510 ; return $ mkProofIrrelCo Nominal kco co1 co2 } 1511 1512 -- Anything else fails 1513 -- E.g. unifying for-all types, which is relative unusual 1514 go ty1 ty2 = defer ty1 ty2 1515 1516 ------------------ 1517 defer ty1 ty2 -- See Note [Check for equality before deferring] 1518 | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1) 1519 | otherwise = uType_defer t_or_k origin ty1 ty2 1520 1521 ------------------ 1522 go_app vis s1 t1 s2 t2 1523 = do { co_s <- uType t_or_k origin s1 s2 1524 ; let arg_origin 1525 | vis = origin 1526 | otherwise = toInvisibleOrigin origin 1527 ; co_t <- uType t_or_k arg_origin t1 t2 1528 ; return $ mkAppCo co_s co_t } 1529 1530{- Note [Check for equality before deferring] 1531~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1532Particularly in ambiguity checks we can get equalities like (ty ~ ty). 1533If ty involves a type function we may defer, which isn't very sensible. 1534An egregious example of this was in test T9872a, which has a type signature 1535 Proxy :: Proxy (Solutions Cubes) 1536Doing the ambiguity check on this signature generates the equality 1537 Solutions Cubes ~ Solutions Cubes 1538and currently the constraint solver normalises both sides at vast cost. 1539This little short-cut in 'defer' helps quite a bit. 1540 1541Note [Care with type applications] 1542~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1543Note: type applications need a bit of care! 1544They can match FunTy and TyConApp, so use splitAppTy_maybe 1545NB: we've already dealt with type variables and Notes, 1546so if one type is an App the other one jolly well better be too 1547 1548Note [Mismatched type lists and application decomposition] 1549~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1550When we find two TyConApps, you might think that the argument lists 1551are guaranteed equal length. But they aren't. Consider matching 1552 w (T x) ~ Foo (T x y) 1553We do match (w ~ Foo) first, but in some circumstances we simply create 1554a deferred constraint; and then go ahead and match (T x ~ T x y). 1555This came up in #3950. 1556 1557So either 1558 (a) either we must check for identical argument kinds 1559 when decomposing applications, 1560 1561 (b) or we must be prepared for ill-kinded unification sub-problems 1562 1563Currently we adopt (b) since it seems more robust -- no need to maintain 1564a global invariant. 1565 1566Note [Expanding synonyms during unification] 1567~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1568We expand synonyms during unification, but: 1569 * We expand *after* the variable case so that we tend to unify 1570 variables with un-expanded type synonym. This just makes it 1571 more likely that the inferred types will mention type synonyms 1572 understandable to the user 1573 1574 * Similarly, we expand *after* the CastTy case, just in case the 1575 CastTy wraps a variable. 1576 1577 * We expand *before* the TyConApp case. For example, if we have 1578 type Phantom a = Int 1579 and are unifying 1580 Phantom Int ~ Phantom Char 1581 it is *wrong* to unify Int and Char. 1582 1583 * The problem case immediately above can happen only with arguments 1584 to the tycon. So we check for nullary tycons *before* expanding. 1585 This is particularly helpful when checking (* ~ *), because * is 1586 now a type synonym. 1587 1588Note [Deferred Unification] 1589~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1590We may encounter a unification ty1 ~ ty2 that cannot be performed syntactically, 1591and yet its consistency is undetermined. Previously, there was no way to still 1592make it consistent. So a mismatch error was issued. 1593 1594Now these unifications are deferred until constraint simplification, where type 1595family instances and given equations may (or may not) establish the consistency. 1596Deferred unifications are of the form 1597 F ... ~ ... 1598or x ~ ... 1599where F is a type function and x is a type variable. 1600E.g. 1601 id :: x ~ y => x -> y 1602 id e = e 1603 1604involves the unification x = y. It is deferred until we bring into account the 1605context x ~ y to establish that it holds. 1606 1607If available, we defer original types (rather than those where closed type 1608synonyms have already been expanded via tcCoreView). This is, as usual, to 1609improve error messages. 1610 1611 1612************************************************************************ 1613* * 1614 uUnfilledVar and friends 1615* * 1616************************************************************************ 1617 1618@uunfilledVar@ is called when at least one of the types being unified is a 1619variable. It does {\em not} assume that the variable is a fixed point 1620of the substitution; rather, notice that @uVar@ (defined below) nips 1621back into @uTys@ if it turns out that the variable is already bound. 1622-} 1623 1624---------- 1625uUnfilledVar :: CtOrigin 1626 -> TypeOrKind 1627 -> SwapFlag 1628 -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar 1629 -- definitely not a /filled/ meta-tyvar 1630 -> TcTauType -- Type 2 1631 -> TcM Coercion 1632-- "Unfilled" means that the variable is definitely not a filled-in meta tyvar 1633-- It might be a skolem, or untouchable, or meta 1634 1635uUnfilledVar origin t_or_k swapped tv1 ty2 1636 = do { ty2 <- zonkTcType ty2 1637 -- Zonk to expose things to the 1638 -- occurs check, and so that if ty2 1639 -- looks like a type variable then it 1640 -- /is/ a type variable 1641 ; uUnfilledVar1 origin t_or_k swapped tv1 ty2 } 1642 1643---------- 1644uUnfilledVar1 :: CtOrigin 1645 -> TypeOrKind 1646 -> SwapFlag 1647 -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar 1648 -- definitely not a /filled/ meta-tyvar 1649 -> TcTauType -- Type 2, zonked 1650 -> TcM Coercion 1651uUnfilledVar1 origin t_or_k swapped tv1 ty2 1652 | Just tv2 <- tcGetTyVar_maybe ty2 1653 = go tv2 1654 1655 | otherwise 1656 = uUnfilledVar2 origin t_or_k swapped tv1 ty2 1657 1658 where 1659 -- 'go' handles the case where both are 1660 -- tyvars so we might want to swap 1661 -- E.g. maybe tv2 is a meta-tyvar and tv1 is not 1662 go tv2 | tv1 == tv2 -- Same type variable => no-op 1663 = return (mkNomReflCo (mkTyVarTy tv1)) 1664 1665 | swapOverTyVars tv1 tv2 -- Distinct type variables 1666 -- Swap meta tyvar to the left if poss 1667 = do { tv1 <- zonkTyCoVarKind tv1 1668 -- We must zonk tv1's kind because that might 1669 -- not have happened yet, and it's an invariant of 1670 -- uUnfilledTyVar2 that ty2 is fully zonked 1671 -- Omitting this caused #16902 1672 ; uUnfilledVar2 origin t_or_k (flipSwap swapped) 1673 tv2 (mkTyVarTy tv1) } 1674 1675 | otherwise 1676 = uUnfilledVar2 origin t_or_k swapped tv1 ty2 1677 1678---------- 1679uUnfilledVar2 :: CtOrigin 1680 -> TypeOrKind 1681 -> SwapFlag 1682 -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar 1683 -- definitely not a /filled/ meta-tyvar 1684 -> TcTauType -- Type 2, zonked 1685 -> TcM Coercion 1686uUnfilledVar2 origin t_or_k swapped tv1 ty2 1687 = do { dflags <- getDynFlags 1688 ; cur_lvl <- getTcLevel 1689 ; go dflags cur_lvl } 1690 where 1691 go dflags cur_lvl 1692 | canSolveByUnification cur_lvl tv1 ty2 1693 , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2 1694 = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2') (tyVarKind tv1) 1695 ; traceTc "uUnfilledVar2 ok" $ 1696 vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) 1697 , ppr ty2 <+> dcolon <+> ppr (tcTypeKind ty2) 1698 , ppr (isTcReflCo co_k), ppr co_k ] 1699 1700 ; if isTcReflCo co_k 1701 -- Only proceed if the kinds match 1702 -- NB: tv1 should still be unfilled, despite the kind unification 1703 -- because tv1 is not free in ty2 (or, hence, in its kind) 1704 then do { writeMetaTyVar tv1 ty2' 1705 ; return (mkTcNomReflCo ty2') } 1706 1707 else defer } -- This cannot be solved now. See TcCanonical 1708 -- Note [Equalities with incompatible kinds] 1709 1710 | otherwise 1711 = do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2) 1712 -- Occurs check or an untouchable: just defer 1713 -- NB: occurs check isn't necessarily fatal: 1714 -- eg tv1 occured in type family parameter 1715 ; defer } 1716 1717 ty1 = mkTyVarTy tv1 1718 kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k) 1719 1720 defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2 1721 1722swapOverTyVars :: TcTyVar -> TcTyVar -> Bool 1723swapOverTyVars tv1 tv2 1724 -- Level comparison: see Note [TyVar/TyVar orientation] 1725 | lvl1 `strictlyDeeperThan` lvl2 = False 1726 | lvl2 `strictlyDeeperThan` lvl1 = True 1727 1728 -- Priority: see Note [TyVar/TyVar orientation] 1729 | pri1 > pri2 = False 1730 | pri2 > pri1 = True 1731 1732 -- Names: see Note [TyVar/TyVar orientation] 1733 | isSystemName tv2_name, not (isSystemName tv1_name) = True 1734 1735 | otherwise = False 1736 1737 where 1738 lvl1 = tcTyVarLevel tv1 1739 lvl2 = tcTyVarLevel tv2 1740 pri1 = lhsPriority tv1 1741 pri2 = lhsPriority tv2 1742 tv1_name = Var.varName tv1 1743 tv2_name = Var.varName tv2 1744 1745 1746lhsPriority :: TcTyVar -> Int 1747-- Higher => more important to be on the LHS 1748-- See Note [TyVar/TyVar orientation] 1749lhsPriority tv 1750 = ASSERT2( isTyVar tv, ppr tv) 1751 case tcTyVarDetails tv of 1752 RuntimeUnk -> 0 1753 SkolemTv {} -> 0 1754 MetaTv { mtv_info = info } -> case info of 1755 FlatSkolTv -> 1 1756 TyVarTv -> 2 1757 TauTv -> 3 1758 FlatMetaTv -> 4 1759{- Note [TyVar/TyVar orientation] 1760~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1761Given (a ~ b), should we orient the CTyEqCan as (a~b) or (b~a)? 1762This is a surprisingly tricky question! 1763 1764First note: only swap if you have to! 1765 See Note [Avoid unnecessary swaps] 1766 1767So we look for a positive reason to swap, using a three-step test: 1768 1769* Level comparison. If 'a' has deeper level than 'b', 1770 put 'a' on the left. See Note [Deeper level on the left] 1771 1772* Priority. If the levels are the same, look at what kind of 1773 type variable it is, using 'lhsPriority' 1774 1775 - FlatMetaTv: Always put on the left. 1776 See Note [Fmv Orientation Invariant] 1777 NB: FlatMetaTvs always have the current level, never an 1778 outer one. So nothing can be deeper than a FlatMetaTv 1779 1780 1781 - TyVarTv/TauTv: if we have tyv_tv ~ tau_tv, put tau_tv 1782 on the left because there are fewer 1783 restrictions on updating TauTvs 1784 1785 - TyVarTv/TauTv: put on the left either 1786 a) Because it's touchable and can be unified, or 1787 b) Even if it's not touchable, TcSimplify.floatEqualities 1788 looks for meta tyvars on the left 1789 1790 - FlatSkolTv: Put on the left in preference to a SkolemTv 1791 See Note [Eliminate flat-skols] 1792 1793* Names. If the level and priority comparisons are all 1794 equal, try to eliminate a TyVars with a System Name in 1795 favour of ones with a Name derived from a user type signature 1796 1797* Age. At one point in the past we tried to break any remaining 1798 ties by eliminating the younger type variable, based on their 1799 Uniques. See Note [Eliminate younger unification variables] 1800 (which also explains why we don't do this any more) 1801 1802Note [Deeper level on the left] 1803~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1804The most important thing is that we want to put tyvars with 1805the deepest level on the left. The reason to do so differs for 1806Wanteds and Givens, but either way, deepest wins! Simple. 1807 1808* Wanteds. Putting the deepest variable on the left maximise the 1809 chances that it's a touchable meta-tyvar which can be solved. 1810 1811* Givens. Suppose we have something like 1812 forall a[2]. b[1] ~ a[2] => beta[1] ~ a[2] 1813 1814 If we orient the Given a[2] on the left, we'll rewrite the Wanted to 1815 (beta[1] ~ b[1]), and that can float out of the implication. 1816 Otherwise it can't. By putting the deepest variable on the left 1817 we maximise our changes of eliminating skolem capture. 1818 1819 See also TcSMonad Note [Let-bound skolems] for another reason 1820 to orient with the deepest skolem on the left. 1821 1822 IMPORTANT NOTE: this test does a level-number comparison on 1823 skolems, so it's important that skolems have (accurate) level 1824 numbers. 1825 1826See #15009 for an further analysis of why "deepest on the left" 1827is a good plan. 1828 1829Note [Fmv Orientation Invariant] 1830~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1831 * We always orient a constraint 1832 fmv ~ alpha 1833 with fmv on the left, even if alpha is 1834 a touchable unification variable 1835 1836Reason: doing it the other way round would unify alpha:=fmv, but that 1837really doesn't add any info to alpha. But a later constraint alpha ~ 1838Int might unlock everything. Comment:9 of #12526 gives a detailed 1839example. 1840 1841WARNING: I've gone to and fro on this one several times. 1842I'm now pretty sure that unifying alpha:=fmv is a bad idea! 1843So orienting with fmvs on the left is a good thing. 1844 1845This example comes from IndTypesPerfMerge. (Others include 1846T10226, T10009.) 1847 From the ambiguity check for 1848 f :: (F a ~ a) => a 1849 we get: 1850 [G] F a ~ a 1851 [WD] F alpha ~ alpha, alpha ~ a 1852 1853 From Givens we get 1854 [G] F a ~ fsk, fsk ~ a 1855 1856 Now if we flatten we get 1857 [WD] alpha ~ fmv, F alpha ~ fmv, alpha ~ a 1858 1859 Now, if we unified alpha := fmv, we'd get 1860 [WD] F fmv ~ fmv, [WD] fmv ~ a 1861 And now we are stuck. 1862 1863So instead the Fmv Orientation Invariant puts the fmv on the 1864left, giving 1865 [WD] fmv ~ alpha, [WD] F alpha ~ fmv, [WD] alpha ~ a 1866 1867 Now we get alpha:=a, and everything works out 1868 1869Note [Eliminate flat-skols] 1870~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1871Suppose we have [G] Num (F [a]) 1872then we flatten to 1873 [G] Num fsk 1874 [G] F [a] ~ fsk 1875where fsk is a flatten-skolem (FlatSkolTv). Suppose we have 1876 type instance F [a] = a 1877then we'll reduce the second constraint to 1878 [G] a ~ fsk 1879and then replace all uses of 'a' with fsk. That's bad because 1880in error messages instead of saying 'a' we'll say (F [a]). In all 1881places, including those where the programmer wrote 'a' in the first 1882place. Very confusing! See #7862. 1883 1884Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate 1885the fsk. 1886 1887Note [Avoid unnecessary swaps] 1888~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1889If we swap without actually improving matters, we can get an infinite loop. 1890Consider 1891 work item: a ~ b 1892 inert item: b ~ c 1893We canonicalise the work-item to (a ~ c). If we then swap it before 1894adding to the inert set, we'll add (c ~ a), and therefore kick out the 1895inert guy, so we get 1896 new work item: b ~ c 1897 inert item: c ~ a 1898And now the cycle just repeats 1899 1900Note [Eliminate younger unification variables] 1901~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1902Given a choice of unifying 1903 alpha := beta or beta := alpha 1904we try, if possible, to eliminate the "younger" one, as determined 1905by `ltUnique`. Reason: the younger one is less likely to appear free in 1906an existing inert constraint, and hence we are less likely to be forced 1907into kicking out and rewriting inert constraints. 1908 1909This is a performance optimisation only. It turns out to fix 1910#14723 all by itself, but clearly not reliably so! 1911 1912It's simple to implement (see nicer_to_update_tv2 in swapOverTyVars). 1913But, to my surprise, it didn't seem to make any significant difference 1914to the compiler's performance, so I didn't take it any further. Still 1915it seemed to too nice to discard altogether, so I'm leaving these 1916notes. SLPJ Jan 18. 1917-} 1918 1919-- @trySpontaneousSolve wi@ solves equalities where one side is a 1920-- touchable unification variable. 1921-- Returns True <=> spontaneous solve happened 1922canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool 1923canSolveByUnification tclvl tv xi 1924 | isTouchableMetaTyVar tclvl tv 1925 = case metaTyVarInfo tv of 1926 TyVarTv -> is_tyvar xi 1927 _ -> True 1928 1929 | otherwise -- Untouchable 1930 = False 1931 where 1932 is_tyvar xi 1933 = case tcGetTyVar_maybe xi of 1934 Nothing -> False 1935 Just tv -> case tcTyVarDetails tv of 1936 MetaTv { mtv_info = info } 1937 -> case info of 1938 TyVarTv -> True 1939 _ -> False 1940 SkolemTv {} -> True 1941 RuntimeUnk -> True 1942 1943{- Note [Prevent unification with type families] 1944~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1945We prevent unification with type families because of an uneasy compromise. 1946It's perfectly sound to unify with type families, and it even improves the 1947error messages in the testsuite. It also modestly improves performance, at 1948least in some cases. But it's disastrous for test case perf/compiler/T3064. 1949Here is the problem: Suppose we have (F ty) where we also have [G] F ty ~ a. 1950What do we do? Do we reduce F? Or do we use the given? Hard to know what's 1951best. GHC reduces. This is a disaster for T3064, where the type's size 1952spirals out of control during reduction. (We're not helped by the fact that 1953the flattener re-flattens all the arguments every time around.) If we prevent 1954unification with type families, then the solver happens to use the equality 1955before expanding the type family. 1956 1957It would be lovely in the future to revisit this problem and remove this 1958extra, unnecessary check. But we retain it for now as it seems to work 1959better in practice. 1960 1961Note [Refactoring hazard: checkTauTvUpdate] 1962~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1963I (Richard E.) have a sad story about refactoring this code, retained here 1964to prevent others (or a future me!) from falling into the same traps. 1965 1966It all started with #11407, which was caused by the fact that the TyVarTy 1967case of defer_me didn't look in the kind. But it seemed reasonable to 1968simply remove the defer_me check instead. 1969 1970It referred to two Notes (since removed) that were out of date, and the 1971fast_check code in occurCheckExpand seemed to do just about the same thing as 1972defer_me. The one piece that defer_me did that wasn't repeated by 1973occurCheckExpand was the type-family check. (See Note [Prevent unification 1974with type families].) So I checked the result of occurCheckExpand for any 1975type family occurrences and deferred if there were any. This was done 1976in commit e9bf7bb5cc9fb3f87dd05111aa23da76b86a8967 . 1977 1978This approach turned out not to be performant, because the expanded 1979type was bigger than the original type, and tyConsOfType (needed to 1980see if there are any type family occurrences) looks through type 1981synonyms. So it then struck me that we could dispense with the 1982defer_me check entirely. This simplified the code nicely, and it cut 1983the allocations in T5030 by half. But, as documented in Note [Prevent 1984unification with type families], this destroyed performance in 1985T3064. Regardless, I missed this regression and the change was 1986committed as 3f5d1a13f112f34d992f6b74656d64d95a3f506d . 1987 1988Bottom lines: 1989 * defer_me is back, but now fixed w.r.t. #11407. 1990 * Tread carefully before you start to refactor here. There can be 1991 lots of hard-to-predict consequences. 1992 1993Note [Type synonyms and the occur check] 1994~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1995Generally speaking we try to update a variable with type synonyms not 1996expanded, which improves later error messages, unless looking 1997inside a type synonym may help resolve a spurious occurs check 1998error. Consider: 1999 type A a = () 2000 2001 f :: (A a -> a -> ()) -> () 2002 f = \ _ -> () 2003 2004 x :: () 2005 x = f (\ x p -> p x) 2006 2007We will eventually get a constraint of the form t ~ A t. The ok function above will 2008properly expand the type (A t) to just (), which is ok to be unified with t. If we had 2009unified with the original type A t, we would lead the type checker into an infinite loop. 2010 2011Hence, if the occurs check fails for a type synonym application, then (and *only* then), 2012the ok function expands the synonym to detect opportunities for occurs check success using 2013the underlying definition of the type synonym. 2014 2015The same applies later on in the constraint interaction code; see TcInteract, 2016function @occ_check_ok@. 2017 2018Note [Non-TcTyVars in TcUnify] 2019~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2020Because the same code is now shared between unifying types and unifying 2021kinds, we sometimes will see proper TyVars floating around the unifier. 2022Example (from test case polykinds/PolyKinds12): 2023 2024 type family Apply (f :: k1 -> k2) (x :: k1) :: k2 2025 type instance Apply g y = g y 2026 2027When checking the instance declaration, we first *kind-check* the LHS 2028and RHS, discovering that the instance really should be 2029 2030 type instance Apply k3 k4 (g :: k3 -> k4) (y :: k3) = g y 2031 2032During this kind-checking, all the tyvars will be TcTyVars. Then, however, 2033as a second pass, we desugar the RHS (which is done in functions prefixed 2034with "tc" in TcTyClsDecls"). By this time, all the kind-vars are proper 2035TyVars, not TcTyVars, get some kind unification must happen. 2036 2037Thus, we always check if a TyVar is a TcTyVar before asking if it's a 2038meta-tyvar. 2039 2040This used to not be necessary for type-checking (that is, before * :: *) 2041because expressions get desugared via an algorithm separate from 2042type-checking (with wrappers, etc.). Types get desugared very differently, 2043causing this wibble in behavior seen here. 2044-} 2045 2046data LookupTyVarResult -- The result of a lookupTcTyVar call 2047 = Unfilled TcTyVarDetails -- SkolemTv or virgin MetaTv 2048 | Filled TcType 2049 2050lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult 2051lookupTcTyVar tyvar 2052 | MetaTv { mtv_ref = ref } <- details 2053 = do { meta_details <- readMutVar ref 2054 ; case meta_details of 2055 Indirect ty -> return (Filled ty) 2056 Flexi -> do { is_touchable <- isTouchableTcM tyvar 2057 -- Note [Unifying untouchables] 2058 ; if is_touchable then 2059 return (Unfilled details) 2060 else 2061 return (Unfilled vanillaSkolemTv) } } 2062 | otherwise 2063 = return (Unfilled details) 2064 where 2065 details = tcTyVarDetails tyvar 2066 2067{- 2068Note [Unifying untouchables] 2069~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2070We treat an untouchable type variable as if it was a skolem. That 2071ensures it won't unify with anything. It's a slight hack, because 2072we return a made-up TcTyVarDetails, but I think it works smoothly. 2073-} 2074 2075-- | Breaks apart a function kind into its pieces. 2076matchExpectedFunKind 2077 :: Outputable fun 2078 => fun -- ^ type, only for errors 2079 -> Arity -- ^ n: number of desired arrows 2080 -> TcKind -- ^ fun_ kind 2081 -> TcM Coercion -- ^ co :: fun_kind ~ (arg1 -> ... -> argn -> res) 2082 2083matchExpectedFunKind hs_ty n k = go n k 2084 where 2085 go 0 k = return (mkNomReflCo k) 2086 2087 go n k | Just k' <- tcView k = go n k' 2088 2089 go n k@(TyVarTy kvar) 2090 | isMetaTyVar kvar 2091 = do { maybe_kind <- readMetaTyVar kvar 2092 ; case maybe_kind of 2093 Indirect fun_kind -> go n fun_kind 2094 Flexi -> defer n k } 2095 2096 go n (FunTy _ arg res) 2097 = do { co <- go (n-1) res 2098 ; return (mkTcFunCo Nominal (mkTcNomReflCo arg) co) } 2099 2100 go n other 2101 = defer n other 2102 2103 defer n k 2104 = do { arg_kinds <- newMetaKindVars n 2105 ; res_kind <- newMetaKindVar 2106 ; let new_fun = mkVisFunTys arg_kinds res_kind 2107 origin = TypeEqOrigin { uo_actual = k 2108 , uo_expected = new_fun 2109 , uo_thing = Just (ppr hs_ty) 2110 , uo_visible = True 2111 } 2112 ; uType KindLevel origin k new_fun } 2113 2114{- ********************************************************************* 2115* * 2116 Occurrence checking 2117* * 2118********************************************************************* -} 2119 2120 2121{- Note [Occurrence checking: look inside kinds] 2122~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2123Suppose we are considering unifying 2124 (alpha :: *) ~ Int -> (beta :: alpha -> alpha) 2125This may be an error (what is that alpha doing inside beta's kind?), 2126but we must not make the mistake of actually unifying or we'll 2127build an infinite data structure. So when looking for occurrences 2128of alpha in the rhs, we must look in the kinds of type variables 2129that occur there. 2130 2131NB: we may be able to remove the problem via expansion; see 2132 Note [Occurs check expansion]. So we have to try that. 2133 2134Note [Checking for foralls] 2135~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2136Unless we have -XImpredicativeTypes (which is a totally unsupported 2137feature), we do not want to unify 2138 alpha ~ (forall a. a->a) -> Int 2139So we look for foralls hidden inside the type, and it's convenient 2140to do that at the same time as the occurs check (which looks for 2141occurrences of alpha). 2142 2143However, it's not just a question of looking for foralls /anywhere/! 2144Consider 2145 (alpha :: forall k. k->*) ~ (beta :: forall k. k->*) 2146This is legal; e.g. dependent/should_compile/T11635. 2147 2148We don't want to reject it because of the forall in beta's kind, 2149but (see Note [Occurrence checking: look inside kinds]) we do 2150need to look in beta's kind. So we carry a flag saying if a 'forall' 2151is OK, and sitch the flag on when stepping inside a kind. 2152 2153Why is it OK? Why does it not count as impredicative polymorphism? 2154The reason foralls are bad is because we reply on "seeing" foralls 2155when doing implicit instantiation. But the forall inside the kind is 2156fine. We'll generate a kind equality constraint 2157 (forall k. k->*) ~ (forall k. k->*) 2158to check that the kinds of lhs and rhs are compatible. If alpha's 2159kind had instead been 2160 (alpha :: kappa) 2161then this kind equality would rightly complain about unifying kappa 2162with (forall k. k->*) 2163 2164-} 2165 2166data MetaTyVarUpdateResult a 2167 = MTVU_OK a 2168 | MTVU_Bad -- Forall, predicate, or type family 2169 | MTVU_Occurs 2170 deriving (Functor) 2171 2172instance Applicative MetaTyVarUpdateResult where 2173 pure = MTVU_OK 2174 (<*>) = ap 2175 2176instance Monad MetaTyVarUpdateResult where 2177 MTVU_OK x >>= k = k x 2178 MTVU_Bad >>= _ = MTVU_Bad 2179 MTVU_Occurs >>= _ = MTVU_Occurs 2180 2181occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult () 2182-- Just for error-message generation; so we return MetaTyVarUpdateResult 2183-- so the caller can report the right kind of error 2184-- Check whether 2185-- a) the given variable occurs in the given type. 2186-- b) there is a forall in the type (unless we have -XImpredicativeTypes) 2187occCheckForErrors dflags tv ty 2188 = case preCheck dflags True tv ty of 2189 MTVU_OK _ -> MTVU_OK () 2190 MTVU_Bad -> MTVU_Bad 2191 MTVU_Occurs -> case occCheckExpand [tv] ty of 2192 Nothing -> MTVU_Occurs 2193 Just _ -> MTVU_OK () 2194 2195---------------- 2196metaTyVarUpdateOK :: DynFlags 2197 -> TcTyVar -- tv :: k1 2198 -> TcType -- ty :: k2 2199 -> Maybe TcType -- possibly-expanded ty 2200-- (metaTyVarUpdateOK tv ty) 2201-- We are about to update the meta-tyvar tv with ty 2202-- Check (a) that tv doesn't occur in ty (occurs check) 2203-- (b) that ty does not have any foralls 2204-- (in the impredicative case), or type functions 2205-- 2206-- We have two possible outcomes: 2207-- (1) Return the type to update the type variable with, 2208-- [we know the update is ok] 2209-- (2) Return Nothing, 2210-- [the update might be dodgy] 2211-- 2212-- Note that "Nothing" does not mean "definite error". For example 2213-- type family F a 2214-- type instance F Int = Int 2215-- consider 2216-- a ~ F a 2217-- This is perfectly reasonable, if we later get a ~ Int. For now, though, 2218-- we return Nothing, leaving it to the later constraint simplifier to 2219-- sort matters out. 2220-- 2221-- See Note [Refactoring hazard: checkTauTvUpdate] 2222 2223metaTyVarUpdateOK dflags tv ty 2224 = case preCheck dflags False tv ty of 2225 -- False <=> type families not ok 2226 -- See Note [Prevent unification with type families] 2227 MTVU_OK _ -> Just ty 2228 MTVU_Bad -> Nothing -- forall, predicate, or type function 2229 MTVU_Occurs -> occCheckExpand [tv] ty 2230 2231preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult () 2232-- A quick check for 2233-- (a) a forall type (unless -XImpredicativeTypes) 2234-- (b) a predicate type (unless -XImpredicativeTypes) 2235-- (c) a type family 2236-- (d) an occurrence of the type variable (occurs check) 2237-- 2238-- For (a), (b), and (c) we check only the top level of the type, NOT 2239-- inside the kinds of variables it mentions. But for (c) we do 2240-- look in the kinds of course. 2241 2242preCheck dflags ty_fam_ok tv ty 2243 = fast_check ty 2244 where 2245 details = tcTyVarDetails tv 2246 impredicative_ok = canUnifyWithPolyType dflags details 2247 2248 ok :: MetaTyVarUpdateResult () 2249 ok = MTVU_OK () 2250 2251 fast_check :: TcType -> MetaTyVarUpdateResult () 2252 fast_check (TyVarTy tv') 2253 | tv == tv' = MTVU_Occurs 2254 | otherwise = fast_check_occ (tyVarKind tv') 2255 -- See Note [Occurrence checking: look inside kinds] 2256 2257 fast_check (TyConApp tc tys) 2258 | bad_tc tc = MTVU_Bad 2259 | otherwise = mapM fast_check tys >> ok 2260 fast_check (LitTy {}) = ok 2261 fast_check (FunTy{ft_af = af, ft_arg = a, ft_res = r}) 2262 | InvisArg <- af 2263 , not impredicative_ok = MTVU_Bad 2264 | otherwise = fast_check a >> fast_check r 2265 fast_check (AppTy fun arg) = fast_check fun >> fast_check arg 2266 fast_check (CastTy ty co) = fast_check ty >> fast_check_co co 2267 fast_check (CoercionTy co) = fast_check_co co 2268 fast_check (ForAllTy (Bndr tv' _) ty) 2269 | not impredicative_ok = MTVU_Bad 2270 | tv == tv' = ok 2271 | otherwise = do { fast_check_occ (tyVarKind tv') 2272 ; fast_check_occ ty } 2273 -- Under a forall we look only for occurrences of 2274 -- the type variable 2275 2276 -- For kinds, we only do an occurs check; we do not worry 2277 -- about type families or foralls 2278 -- See Note [Checking for foralls] 2279 fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = MTVU_Occurs 2280 | otherwise = ok 2281 2282 -- For coercions, we are only doing an occurs check here; 2283 -- no bother about impredicativity in coercions, as they're 2284 -- inferred 2285 fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = MTVU_Occurs 2286 | otherwise = ok 2287 2288 bad_tc :: TyCon -> Bool 2289 bad_tc tc 2290 | not (impredicative_ok || isTauTyCon tc) = True 2291 | not (ty_fam_ok || isFamFreeTyCon tc) = True 2292 | otherwise = False 2293 2294canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool 2295canUnifyWithPolyType dflags details 2296 = case details of 2297 MetaTv { mtv_info = TyVarTv } -> False 2298 MetaTv { mtv_info = TauTv } -> xopt LangExt.ImpredicativeTypes dflags 2299 _other -> True 2300 -- We can have non-meta tyvars in given constraints 2301