1{- 2(c) The University of Glasgow 2006 3(c) The GRASP/AQUA Project, Glasgow University, 1992-1998 4 5 6Monadic type operations 7 8This module contains monadic operations over types that contain 9mutable type variables. 10-} 11 12{-# LANGUAGE CPP, TupleSections, MultiWayIf #-} 13 14module TcMType ( 15 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet, 16 17 -------------------------------- 18 -- Creating new mutable type variables 19 newFlexiTyVar, 20 newFlexiTyVarTy, -- Kind -> TcM TcType 21 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] 22 newOpenFlexiTyVarTy, newOpenTypeKind, 23 newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel, 24 cloneMetaTyVar, 25 newFmvTyVar, newFskTyVar, 26 27 readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, 28 newMetaDetails, isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar, 29 30 -------------------------------- 31 -- Expected types 32 ExpType(..), ExpSigmaType, ExpRhoType, 33 mkCheckExpType, 34 newInferExpType, newInferExpTypeInst, newInferExpTypeNoInst, 35 readExpType, readExpType_maybe, 36 expTypeToType, checkingExpType_maybe, checkingExpType, 37 tauifyExpType, inferResultToType, 38 39 -------------------------------- 40 -- Creating new evidence variables 41 newEvVar, newEvVars, newDict, 42 newWanted, newWanteds, newHoleCt, cloneWanted, cloneWC, 43 emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars, 44 emitDerivedEqs, 45 newTcEvBinds, newNoTcEvBinds, addTcEvBind, 46 47 newCoercionHole, fillCoercionHole, isFilledCoercionHole, 48 unpackCoercionHole, unpackCoercionHole_maybe, 49 checkCoercionHole, 50 51 newImplication, 52 53 -------------------------------- 54 -- Instantiation 55 newMetaTyVars, newMetaTyVarX, newMetaTyVarsX, 56 newMetaTyVarTyVars, newMetaTyVarTyVarX, 57 newTyVarTyVar, cloneTyVarTyVar, 58 newPatSigTyVar, newSkolemTyVar, newWildCardX, 59 tcInstType, 60 tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt, 61 tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX, 62 63 freshenTyVarBndrs, freshenCoVarBndrsX, 64 65 -------------------------------- 66 -- Zonking and tidying 67 zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, 68 tidyEvVar, tidyCt, tidySkolemInfo, 69 zonkTcTyVar, zonkTcTyVars, 70 zonkTcTyVarToTyVar, zonkTyVarTyVarPairs, 71 zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkDTyCoVarSetAndFV, 72 zonkTyCoVarsAndFVList, 73 candidateQTyVarsOfType, candidateQTyVarsOfKind, 74 candidateQTyVarsOfTypes, candidateQTyVarsOfKinds, 75 CandidatesQTvs(..), delCandidates, candidateKindVars, partitionCandidates, 76 zonkAndSkolemise, skolemiseQuantifiedTyVar, 77 defaultTyVar, quantifyTyVars, isQuantifiableTv, 78 zonkTcType, zonkTcTypes, zonkCo, 79 zonkTyCoVarKind, 80 81 zonkEvVar, zonkWC, zonkSimples, 82 zonkId, zonkCoVar, 83 zonkCt, zonkSkolemInfo, 84 85 skolemiseUnboundMetaTyVar, 86 87 ------------------------------ 88 -- Levity polymorphism 89 ensureNotLevPoly, checkForLevPoly, checkForLevPolyX, formatLevPolyErr 90 ) where 91 92#include "HsVersions.h" 93 94-- friends: 95import GhcPrelude 96 97import TyCoRep 98import TyCoPpr 99import TcType 100import Type 101import TyCon 102import Coercion 103import Class 104import Var 105import Predicate 106import TcOrigin 107 108-- others: 109import TcRnMonad -- TcType, amongst others 110import Constraint 111import TcEvidence 112import Id 113import Name 114import VarSet 115import TysWiredIn 116import TysPrim 117import VarEnv 118import NameEnv 119import PrelNames 120import Util 121import Outputable 122import FastString 123import Bag 124import Pair 125import UniqSet 126import DynFlags 127import qualified GHC.LanguageExtensions as LangExt 128import BasicTypes ( TypeOrKind(..) ) 129 130import Control.Monad 131import Maybes 132import Data.List ( mapAccumL ) 133import Control.Arrow ( second ) 134import qualified Data.Semigroup as Semi 135 136{- 137************************************************************************ 138* * 139 Kind variables 140* * 141************************************************************************ 142-} 143 144mkKindName :: Unique -> Name 145mkKindName unique = mkSystemName unique kind_var_occ 146 147kind_var_occ :: OccName -- Just one for all MetaKindVars 148 -- They may be jiggled by tidying 149kind_var_occ = mkOccName tvName "k" 150 151newMetaKindVar :: TcM TcKind 152newMetaKindVar 153 = do { details <- newMetaDetails TauTv 154 ; uniq <- newUnique 155 ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details 156 ; traceTc "newMetaKindVar" (ppr kv) 157 ; return (mkTyVarTy kv) } 158 159newMetaKindVars :: Int -> TcM [TcKind] 160newMetaKindVars n = replicateM n newMetaKindVar 161 162{- 163************************************************************************ 164* * 165 Evidence variables; range over constraints we can abstract over 166* * 167************************************************************************ 168-} 169 170newEvVars :: TcThetaType -> TcM [EvVar] 171newEvVars theta = mapM newEvVar theta 172 173-------------- 174 175newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar 176-- Creates new *rigid* variables for predicates 177newEvVar ty = do { name <- newSysName (predTypeOccName ty) 178 ; return (mkLocalIdOrCoVar name ty) } 179 180newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence 181-- Deals with both equality and non-equality predicates 182newWanted orig t_or_k pty 183 = do loc <- getCtLocM orig t_or_k 184 d <- if isEqPrimPred pty then HoleDest <$> newCoercionHole pty 185 else EvVarDest <$> newEvVar pty 186 return $ CtWanted { ctev_dest = d 187 , ctev_pred = pty 188 , ctev_nosh = WDeriv 189 , ctev_loc = loc } 190 191newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence] 192newWanteds orig = mapM (newWanted orig Nothing) 193 194-- | Create a new 'CHoleCan' 'Ct'. 195newHoleCt :: Hole -> Id -> Type -> TcM Ct 196newHoleCt hole ev ty = do 197 loc <- getCtLocM HoleOrigin Nothing 198 pure $ CHoleCan { cc_ev = CtWanted { ctev_pred = ty 199 , ctev_dest = EvVarDest ev 200 , ctev_nosh = WDeriv 201 , ctev_loc = loc } 202 , cc_hole = hole } 203 204---------------------------------------------- 205-- Cloning constraints 206---------------------------------------------- 207 208cloneWanted :: Ct -> TcM Ct 209cloneWanted ct 210 | ev@(CtWanted { ctev_dest = HoleDest {}, ctev_pred = pty }) <- ctEvidence ct 211 = do { co_hole <- newCoercionHole pty 212 ; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) } 213 | otherwise 214 = return ct 215 216cloneWC :: WantedConstraints -> TcM WantedConstraints 217-- Clone all the evidence bindings in 218-- a) the ic_bind field of any implications 219-- b) the CoercionHoles of any wanted constraints 220-- so that solving the WantedConstraints will not have any visible side 221-- effect, /except/ from causing unifications 222cloneWC wc@(WC { wc_simple = simples, wc_impl = implics }) 223 = do { simples' <- mapBagM cloneWanted simples 224 ; implics' <- mapBagM cloneImplication implics 225 ; return (wc { wc_simple = simples', wc_impl = implics' }) } 226 227cloneImplication :: Implication -> TcM Implication 228cloneImplication implic@(Implic { ic_binds = binds, ic_wanted = inner_wanted }) 229 = do { binds' <- cloneEvBindsVar binds 230 ; inner_wanted' <- cloneWC inner_wanted 231 ; return (implic { ic_binds = binds', ic_wanted = inner_wanted' }) } 232 233---------------------------------------------- 234-- Emitting constraints 235---------------------------------------------- 236 237-- | Emits a new Wanted. Deals with both equalities and non-equalities. 238emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm 239emitWanted origin pty 240 = do { ev <- newWanted origin Nothing pty 241 ; emitSimple $ mkNonCanonical ev 242 ; return $ ctEvTerm ev } 243 244emitDerivedEqs :: CtOrigin -> [(TcType,TcType)] -> TcM () 245-- Emit some new derived nominal equalities 246emitDerivedEqs origin pairs 247 | null pairs 248 = return () 249 | otherwise 250 = do { loc <- getCtLocM origin Nothing 251 ; emitSimples (listToBag (map (mk_one loc) pairs)) } 252 where 253 mk_one loc (ty1, ty2) 254 = mkNonCanonical $ 255 CtDerived { ctev_pred = mkPrimEqPred ty1 ty2 256 , ctev_loc = loc } 257 258-- | Emits a new equality constraint 259emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion 260emitWantedEq origin t_or_k role ty1 ty2 261 = do { hole <- newCoercionHole pty 262 ; loc <- getCtLocM origin (Just t_or_k) 263 ; emitSimple $ mkNonCanonical $ 264 CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole 265 , ctev_nosh = WDeriv, ctev_loc = loc } 266 ; return (HoleCo hole) } 267 where 268 pty = mkPrimEqPredRole role ty1 ty2 269 270-- | Creates a new EvVar and immediately emits it as a Wanted. 271-- No equality predicates here. 272emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar 273emitWantedEvVar origin ty 274 = do { new_cv <- newEvVar ty 275 ; loc <- getCtLocM origin Nothing 276 ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv 277 , ctev_pred = ty 278 , ctev_nosh = WDeriv 279 , ctev_loc = loc } 280 ; emitSimple $ mkNonCanonical ctev 281 ; return new_cv } 282 283emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar] 284emitWantedEvVars orig = mapM (emitWantedEvVar orig) 285 286newDict :: Class -> [TcType] -> TcM DictId 287newDict cls tys 288 = do { name <- newSysName (mkDictOcc (getOccName cls)) 289 ; return (mkLocalId name (mkClassPred cls tys)) } 290 291predTypeOccName :: PredType -> OccName 292predTypeOccName ty = case classifyPredType ty of 293 ClassPred cls _ -> mkDictOcc (getOccName cls) 294 EqPred {} -> mkVarOccFS (fsLit "co") 295 IrredPred {} -> mkVarOccFS (fsLit "irred") 296 ForAllPred {} -> mkVarOccFS (fsLit "df") 297 298-- | Create a new 'Implication' with as many sensible defaults for its fields 299-- as possible. Note that the 'ic_tclvl', 'ic_binds', and 'ic_info' fields do 300-- /not/ have sensible defaults, so they are initialized with lazy thunks that 301-- will 'panic' if forced, so one should take care to initialize these fields 302-- after creation. 303-- 304-- This is monadic to look up the 'TcLclEnv', which is used to initialize 305-- 'ic_env', and to set the -Winaccessible-code flag. See 306-- Note [Avoid -Winaccessible-code when deriving] in TcInstDcls. 307newImplication :: TcM Implication 308newImplication 309 = do env <- getLclEnv 310 warn_inaccessible <- woptM Opt_WarnInaccessibleCode 311 return (implicationPrototype { ic_env = env 312 , ic_warn_inaccessible = warn_inaccessible }) 313 314{- 315************************************************************************ 316* * 317 Coercion holes 318* * 319************************************************************************ 320-} 321 322newCoercionHole :: TcPredType -> TcM CoercionHole 323newCoercionHole pred_ty 324 = do { co_var <- newEvVar pred_ty 325 ; traceTc "New coercion hole:" (ppr co_var) 326 ; ref <- newMutVar Nothing 327 ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } } 328 329-- | Put a value in a coercion hole 330fillCoercionHole :: CoercionHole -> Coercion -> TcM () 331fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co 332 = do { 333#if defined(DEBUG) 334 ; cts <- readTcRef ref 335 ; whenIsJust cts $ \old_co -> 336 pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co) 337#endif 338 ; traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co) 339 ; writeTcRef ref (Just co) } 340 341-- | Is a coercion hole filled in? 342isFilledCoercionHole :: CoercionHole -> TcM Bool 343isFilledCoercionHole (CoercionHole { ch_ref = ref }) = isJust <$> readTcRef ref 344 345-- | Retrieve the contents of a coercion hole. Panics if the hole 346-- is unfilled 347unpackCoercionHole :: CoercionHole -> TcM Coercion 348unpackCoercionHole hole 349 = do { contents <- unpackCoercionHole_maybe hole 350 ; case contents of 351 Just co -> return co 352 Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) } 353 354-- | Retrieve the contents of a coercion hole, if it is filled 355unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion) 356unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref 357 358-- | Check that a coercion is appropriate for filling a hole. (The hole 359-- itself is needed only for printing. 360-- Always returns the checked coercion, but this return value is necessary 361-- so that the input coercion is forced only when the output is forced. 362checkCoercionHole :: CoVar -> Coercion -> TcM Coercion 363checkCoercionHole cv co 364 | debugIsOn 365 = do { cv_ty <- zonkTcType (varType cv) 366 -- co is already zonked, but cv might not be 367 ; return $ 368 ASSERT2( ok cv_ty 369 , (text "Bad coercion hole" <+> 370 ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role 371 , ppr cv_ty ]) ) 372 co } 373 | otherwise 374 = return co 375 376 where 377 (Pair t1 t2, role) = coercionKindRole co 378 ok cv_ty | EqPred cv_rel cv_t1 cv_t2 <- classifyPredType cv_ty 379 = t1 `eqType` cv_t1 380 && t2 `eqType` cv_t2 381 && role == eqRelRole cv_rel 382 | otherwise 383 = False 384 385{- 386************************************************************************ 387* 388 Expected types 389* 390************************************************************************ 391 392Note [ExpType] 393~~~~~~~~~~~~~~ 394 395An ExpType is used as the "expected type" when type-checking an expression. 396An ExpType can hold a "hole" that can be filled in by the type-checker. 397This allows us to have one tcExpr that works in both checking mode and 398synthesis mode (that is, bidirectional type-checking). Previously, this 399was achieved by using ordinary unification variables, but we don't need 400or want that generality. (For example, #11397 was caused by doing the 401wrong thing with unification variables.) Instead, we observe that these 402holes should 403 4041. never be nested 4052. never appear as the type of a variable 4063. be used linearly (never be duplicated) 407 408By defining ExpType, separately from Type, we can achieve goals 1 and 2 409statically. 410 411See also [wiki:typechecking] 412 413Note [TcLevel of ExpType] 414~~~~~~~~~~~~~~~~~~~~~~~~~ 415Consider 416 417 data G a where 418 MkG :: G Bool 419 420 foo MkG = True 421 422This is a classic untouchable-variable / ambiguous GADT return type 423scenario. But, with ExpTypes, we'll be inferring the type of the RHS. 424And, because there is only one branch of the case, we won't trigger 425Note [Case branches must never infer a non-tau type] of TcMatches. 426We thus must track a TcLevel in an Inferring ExpType. If we try to 427fill the ExpType and find that the TcLevels don't work out, we 428fill the ExpType with a tau-tv at the low TcLevel, hopefully to 429be worked out later by some means. This is triggered in 430test gadt/gadt-escape1. 431 432-} 433 434-- actual data definition is in TcType 435 436-- | Make an 'ExpType' suitable for inferring a type of kind * or #. 437newInferExpTypeNoInst :: TcM ExpSigmaType 438newInferExpTypeNoInst = newInferExpType False 439 440newInferExpTypeInst :: TcM ExpRhoType 441newInferExpTypeInst = newInferExpType True 442 443newInferExpType :: Bool -> TcM ExpType 444newInferExpType inst 445 = do { u <- newUnique 446 ; tclvl <- getTcLevel 447 ; traceTc "newOpenInferExpType" (ppr u <+> ppr inst <+> ppr tclvl) 448 ; ref <- newMutVar Nothing 449 ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl 450 , ir_ref = ref, ir_inst = inst })) } 451 452-- | Extract a type out of an ExpType, if one exists. But one should always 453-- exist. Unless you're quite sure you know what you're doing. 454readExpType_maybe :: ExpType -> TcM (Maybe TcType) 455readExpType_maybe (Check ty) = return (Just ty) 456readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref 457 458-- | Extract a type out of an ExpType. Otherwise, panics. 459readExpType :: ExpType -> TcM TcType 460readExpType exp_ty 461 = do { mb_ty <- readExpType_maybe exp_ty 462 ; case mb_ty of 463 Just ty -> return ty 464 Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) } 465 466-- | Returns the expected type when in checking mode. 467checkingExpType_maybe :: ExpType -> Maybe TcType 468checkingExpType_maybe (Check ty) = Just ty 469checkingExpType_maybe _ = Nothing 470 471-- | Returns the expected type when in checking mode. Panics if in inference 472-- mode. 473checkingExpType :: String -> ExpType -> TcType 474checkingExpType _ (Check ty) = ty 475checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et) 476 477tauifyExpType :: ExpType -> TcM ExpType 478-- ^ Turn a (Infer hole) type into a (Check alpha), 479-- where alpha is a fresh unification variable 480tauifyExpType (Check ty) = return (Check ty) -- No-op for (Check ty) 481tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res 482 ; return (Check ty) } 483 484-- | Extracts the expected type if there is one, or generates a new 485-- TauTv if there isn't. 486expTypeToType :: ExpType -> TcM TcType 487expTypeToType (Check ty) = return ty 488expTypeToType (Infer inf_res) = inferResultToType inf_res 489 490inferResultToType :: InferResult -> TcM Type 491inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl 492 , ir_ref = ref }) 493 = do { rr <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy 494 ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr) 495 -- See Note [TcLevel of ExpType] 496 ; writeMutVar ref (Just tau) 497 ; traceTc "Forcing ExpType to be monomorphic:" 498 (ppr u <+> text ":=" <+> ppr tau) 499 ; return tau } 500 501 502{- ********************************************************************* 503* * 504 SkolemTvs (immutable) 505* * 506********************************************************************* -} 507 508tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar])) 509 -- ^ How to instantiate the type variables 510 -> Id -- ^ Type to instantiate 511 -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result 512 -- (type vars, preds (incl equalities), rho) 513tcInstType inst_tyvars id 514 = case tcSplitForAllTys (idType id) of 515 ([], rho) -> let -- There may be overloading despite no type variables; 516 -- (?x :: Int) => Int -> Int 517 (theta, tau) = tcSplitPhiTy rho 518 in 519 return ([], theta, tau) 520 521 (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars 522 ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho) 523 tv_prs = map tyVarName tyvars `zip` tyvars' 524 ; return (tv_prs, theta, tau) } 525 526tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType) 527-- Instantiate a type signature with skolem constants. 528-- We could give them fresh names, but no need to do so 529tcSkolDFunType dfun 530 = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun 531 ; return (map snd tv_prs, theta, tau) } 532 533tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar]) 534-- Make skolem constants, but do *not* give them new names, as above 535-- Moreover, make them "super skolems"; see comments with superSkolemTv 536-- see Note [Kind substitution when instantiating] 537-- Precondition: tyvars should be ordered by scoping 538tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst 539 540tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar) 541tcSuperSkolTyVar subst tv 542 = (extendTvSubstWithClone subst tv new_tv, new_tv) 543 where 544 kind = substTyUnchecked subst (tyVarKind tv) 545 new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv 546 547-- | Given a list of @['TyVar']@, skolemize the type variables, 548-- returning a substitution mapping the original tyvars to the 549-- skolems, and the list of newly bound skolems. 550tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) 551-- See Note [Skolemising type variables] 552tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst 553 554tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar]) 555-- See Note [Skolemising type variables] 556tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False 557 558tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) 559-- See Note [Skolemising type variables] 560tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst 561 562tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar]) 563-- See Note [Skolemising type variables] 564tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst 565 566tcInstSkolTyVarsPushLevel :: Bool -> TCvSubst -> [TyVar] 567 -> TcM (TCvSubst, [TcTyVar]) 568-- Skolemise one level deeper, hence pushTcLevel 569-- See Note [Skolemising type variables] 570tcInstSkolTyVarsPushLevel overlappable subst tvs 571 = do { tc_lvl <- getTcLevel 572 ; let pushed_lvl = pushTcLevel tc_lvl 573 ; tcInstSkolTyVarsAt pushed_lvl overlappable subst tvs } 574 575tcInstSkolTyVarsAt :: TcLevel -> Bool 576 -> TCvSubst -> [TyVar] 577 -> TcM (TCvSubst, [TcTyVar]) 578tcInstSkolTyVarsAt lvl overlappable subst tvs 579 = freshenTyCoVarsX new_skol_tv subst tvs 580 where 581 details = SkolemTv lvl overlappable 582 new_skol_tv name kind = mkTcTyVar name kind details 583 584------------------ 585freshenTyVarBndrs :: [TyVar] -> TcM (TCvSubst, [TyVar]) 586-- ^ Give fresh uniques to a bunch of TyVars, but they stay 587-- as TyVars, rather than becoming TcTyVars 588-- Used in FamInst.newFamInst, and Inst.newClsInst 589freshenTyVarBndrs = freshenTyCoVars mkTyVar 590 591freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcM (TCvSubst, [CoVar]) 592-- ^ Give fresh uniques to a bunch of CoVars 593-- Used in FamInst.newFamInst 594freshenCoVarBndrsX subst = freshenTyCoVarsX mkCoVar subst 595 596------------------ 597freshenTyCoVars :: (Name -> Kind -> TyCoVar) 598 -> [TyVar] -> TcM (TCvSubst, [TyCoVar]) 599freshenTyCoVars mk_tcv = freshenTyCoVarsX mk_tcv emptyTCvSubst 600 601freshenTyCoVarsX :: (Name -> Kind -> TyCoVar) 602 -> TCvSubst -> [TyCoVar] 603 -> TcM (TCvSubst, [TyCoVar]) 604freshenTyCoVarsX mk_tcv = mapAccumLM (freshenTyCoVarX mk_tcv) 605 606freshenTyCoVarX :: (Name -> Kind -> TyCoVar) 607 -> TCvSubst -> TyCoVar -> TcM (TCvSubst, TyCoVar) 608-- This a complete freshening operation: 609-- the skolems have a fresh unique, and a location from the monad 610-- See Note [Skolemising type variables] 611freshenTyCoVarX mk_tcv subst tycovar 612 = do { loc <- getSrcSpanM 613 ; uniq <- newUnique 614 ; let old_name = tyVarName tycovar 615 new_name = mkInternalName uniq (getOccName old_name) loc 616 new_kind = substTyUnchecked subst (tyVarKind tycovar) 617 new_tcv = mk_tcv new_name new_kind 618 subst1 = extendTCvSubstWithClone subst tycovar new_tcv 619 ; return (subst1, new_tcv) } 620 621{- Note [Skolemising type variables] 622~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 623The tcInstSkolTyVars family of functions instantiate a list of TyVars 624to fresh skolem TcTyVars. Important notes: 625 626a) Level allocation. We generally skolemise /before/ calling 627 pushLevelAndCaptureConstraints. So we want their level to the level 628 of the soon-to-be-created implication, which has a level ONE HIGHER 629 than the current level. Hence the pushTcLevel. It feels like a 630 slight hack. 631 632b) The [TyVar] should be ordered (kind vars first) 633 See Note [Kind substitution when instantiating] 634 635c) It's a complete freshening operation: the skolems have a fresh 636 unique, and a location from the monad 637 638d) The resulting skolems are 639 non-overlappable for tcInstSkolTyVars, 640 but overlappable for tcInstSuperSkolTyVars 641 See TcDerivInfer Note [Overlap and deriving] for an example 642 of where this matters. 643 644Note [Kind substitution when instantiating] 645~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 646When we instantiate a bunch of kind and type variables, first we 647expect them to be topologically sorted. 648Then we have to instantiate the kind variables, build a substitution 649from old variables to the new variables, then instantiate the type 650variables substituting the original kind. 651 652Exemple: If we want to instantiate 653 [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)] 654we want 655 [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)] 656instead of the buggous 657 [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)] 658 659 660************************************************************************ 661* * 662 MetaTvs (meta type variables; mutable) 663* * 664************************************************************************ 665-} 666 667{- 668Note [TyVarTv] 669~~~~~~~~~~~~ 670 671A TyVarTv can unify with type *variables* only, including other TyVarTvs and 672skolems. Sometimes, they can unify with type variables that the user would 673rather keep distinct; see #11203 for an example. So, any client of this 674function needs to either allow the TyVarTvs to unify with each other or check 675that they don't (say, with a call to findDubTyVarTvs). 676 677Before #15050 this (under the name SigTv) was used for ScopedTypeVariables in 678patterns, to make sure these type variables only refer to other type variables, 679but this restriction was dropped, and ScopedTypeVariables can now refer to full 680types (GHC Proposal 29). 681 682The remaining uses of newTyVarTyVars are 683* In kind signatures, see 684 TcTyClsDecls Note [Inferring kinds for type declarations] 685 and Note [Kind checking for GADTs] 686* In partial type signatures, see Note [Quantified variables in partial type signatures] 687-} 688 689newMetaTyVarName :: FastString -> TcM Name 690-- Makes a /System/ Name, which is eagerly eliminated by 691-- the unifier; see TcUnify.nicer_to_update_tv1, and 692-- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2) 693newMetaTyVarName str 694 = do { uniq <- newUnique 695 ; return (mkSystemName uniq (mkTyVarOccFS str)) } 696 697cloneMetaTyVarName :: Name -> TcM Name 698cloneMetaTyVarName name 699 = do { uniq <- newUnique 700 ; return (mkSystemName uniq (nameOccName name)) } 701 -- See Note [Name of an instantiated type variable] 702 703{- Note [Name of an instantiated type variable] 704~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 705At the moment we give a unification variable a System Name, which 706influences the way it is tidied; see TypeRep.tidyTyVarBndr. 707-} 708 709newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar 710-- Make a new meta tyvar out of thin air 711newAnonMetaTyVar meta_info kind 712 = do { let s = case meta_info of 713 TauTv -> fsLit "t" 714 FlatMetaTv -> fsLit "fmv" 715 FlatSkolTv -> fsLit "fsk" 716 TyVarTv -> fsLit "a" 717 ; name <- newMetaTyVarName s 718 ; details <- newMetaDetails meta_info 719 ; let tyvar = mkTcTyVar name kind details 720 ; traceTc "newAnonMetaTyVar" (ppr tyvar) 721 ; return tyvar } 722 723-- makes a new skolem tv 724newSkolemTyVar :: Name -> Kind -> TcM TcTyVar 725newSkolemTyVar name kind 726 = do { lvl <- getTcLevel 727 ; return (mkTcTyVar name kind (SkolemTv lvl False)) } 728 729newTyVarTyVar :: Name -> Kind -> TcM TcTyVar 730-- See Note [TyVarTv] 731-- Does not clone a fresh unique 732newTyVarTyVar name kind 733 = do { details <- newMetaDetails TyVarTv 734 ; let tyvar = mkTcTyVar name kind details 735 ; traceTc "newTyVarTyVar" (ppr tyvar) 736 ; return tyvar } 737 738cloneTyVarTyVar :: Name -> Kind -> TcM TcTyVar 739-- See Note [TyVarTv] 740-- Clones a fresh unique 741cloneTyVarTyVar name kind 742 = do { details <- newMetaDetails TyVarTv 743 ; uniq <- newUnique 744 ; let name' = name `setNameUnique` uniq 745 tyvar = mkTcTyVar name' kind details 746 -- Don't use cloneMetaTyVar, which makes a SystemName 747 -- We want to keep the original more user-friendly Name 748 -- In practical terms that means that in error messages, 749 -- when the Name is tidied we get 'a' rather than 'a0' 750 ; traceTc "cloneTyVarTyVar" (ppr tyvar) 751 ; return tyvar } 752 753newPatSigTyVar :: Name -> Kind -> TcM TcTyVar 754newPatSigTyVar name kind 755 = do { details <- newMetaDetails TauTv 756 ; uniq <- newUnique 757 ; let name' = name `setNameUnique` uniq 758 tyvar = mkTcTyVar name' kind details 759 -- Don't use cloneMetaTyVar; 760 -- same reasoning as in newTyVarTyVar 761 ; traceTc "newPatSigTyVar" (ppr tyvar) 762 ; return tyvar } 763 764cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar 765-- Make a fresh MetaTyVar, basing the name 766-- on that of the supplied TyVar 767cloneAnonMetaTyVar info tv kind 768 = do { details <- newMetaDetails info 769 ; name <- cloneMetaTyVarName (tyVarName tv) 770 ; let tyvar = mkTcTyVar name kind details 771 ; traceTc "cloneAnonMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)) 772 ; return tyvar } 773 774newFskTyVar :: TcType -> TcM TcTyVar 775newFskTyVar fam_ty 776 = do { details <- newMetaDetails FlatSkolTv 777 ; name <- newMetaTyVarName (fsLit "fsk") 778 ; return (mkTcTyVar name (tcTypeKind fam_ty) details) } 779 780newFmvTyVar :: TcType -> TcM TcTyVar 781-- Very like newMetaTyVar, except sets mtv_tclvl to one less 782-- so that the fmv is untouchable. 783newFmvTyVar fam_ty 784 = do { details <- newMetaDetails FlatMetaTv 785 ; name <- newMetaTyVarName (fsLit "s") 786 ; return (mkTcTyVar name (tcTypeKind fam_ty) details) } 787 788newMetaDetails :: MetaInfo -> TcM TcTyVarDetails 789newMetaDetails info 790 = do { ref <- newMutVar Flexi 791 ; tclvl <- getTcLevel 792 ; return (MetaTv { mtv_info = info 793 , mtv_ref = ref 794 , mtv_tclvl = tclvl }) } 795 796cloneMetaTyVar :: TcTyVar -> TcM TcTyVar 797cloneMetaTyVar tv 798 = ASSERT( isTcTyVar tv ) 799 do { ref <- newMutVar Flexi 800 ; name' <- cloneMetaTyVarName (tyVarName tv) 801 ; let details' = case tcTyVarDetails tv of 802 details@(MetaTv {}) -> details { mtv_ref = ref } 803 _ -> pprPanic "cloneMetaTyVar" (ppr tv) 804 tyvar = mkTcTyVar name' (tyVarKind tv) details' 805 ; traceTc "cloneMetaTyVar" (ppr tyvar) 806 ; return tyvar } 807 808-- Works for both type and kind variables 809readMetaTyVar :: TyVar -> TcM MetaDetails 810readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar ) 811 readMutVar (metaTyVarRef tyvar) 812 813isFilledMetaTyVar_maybe :: TcTyVar -> TcM (Maybe Type) 814isFilledMetaTyVar_maybe tv 815 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv 816 = do { cts <- readTcRef ref 817 ; case cts of 818 Indirect ty -> return (Just ty) 819 Flexi -> return Nothing } 820 | otherwise 821 = return Nothing 822 823isFilledMetaTyVar :: TyVar -> TcM Bool 824-- True of a filled-in (Indirect) meta type variable 825isFilledMetaTyVar tv = isJust <$> isFilledMetaTyVar_maybe tv 826 827isUnfilledMetaTyVar :: TyVar -> TcM Bool 828-- True of a un-filled-in (Flexi) meta type variable 829-- NB: Not the opposite of isFilledMetaTyVar 830isUnfilledMetaTyVar tv 831 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv 832 = do { details <- readMutVar ref 833 ; return (isFlexi details) } 834 | otherwise = return False 835 836-------------------- 837-- Works with both type and kind variables 838writeMetaTyVar :: TcTyVar -> TcType -> TcM () 839-- Write into a currently-empty MetaTyVar 840 841writeMetaTyVar tyvar ty 842 | not debugIsOn 843 = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty 844 845-- Everything from here on only happens if DEBUG is on 846 | not (isTcTyVar tyvar) 847 = ASSERT2( False, text "Writing to non-tc tyvar" <+> ppr tyvar ) 848 return () 849 850 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar 851 = writeMetaTyVarRef tyvar ref ty 852 853 | otherwise 854 = ASSERT2( False, text "Writing to non-meta tyvar" <+> ppr tyvar ) 855 return () 856 857-------------------- 858writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM () 859-- Here the tyvar is for error checking only; 860-- the ref cell must be for the same tyvar 861writeMetaTyVarRef tyvar ref ty 862 | not debugIsOn 863 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar) 864 <+> text ":=" <+> ppr ty) 865 ; writeTcRef ref (Indirect ty) } 866 867 -- Everything from here on only happens if DEBUG is on 868 | otherwise 869 = do { meta_details <- readMutVar ref; 870 -- Zonk kinds to allow the error check to work 871 ; zonked_tv_kind <- zonkTcType tv_kind 872 ; zonked_ty_kind <- zonkTcType ty_kind 873 ; let kind_check_ok = tcIsConstraintKind zonked_tv_kind 874 || tcEqKind zonked_ty_kind zonked_tv_kind 875 -- Hack alert! tcIsConstraintKind: see TcHsType 876 -- Note [Extra-constraint holes in partial type signatures] 877 878 kind_msg = hang (text "Ill-kinded update to meta tyvar") 879 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind) 880 <+> text ":=" 881 <+> ppr ty <+> text "::" <+> (ppr zonked_ty_kind) ) 882 883 ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty) 884 885 -- Check for double updates 886 ; MASSERT2( isFlexi meta_details, double_upd_msg meta_details ) 887 888 -- Check for level OK 889 -- See Note [Level check when unifying] 890 ; MASSERT2( level_check_ok, level_check_msg ) 891 892 -- Check Kinds ok 893 ; MASSERT2( kind_check_ok, kind_msg ) 894 895 -- Do the write 896 ; writeMutVar ref (Indirect ty) } 897 where 898 tv_kind = tyVarKind tyvar 899 ty_kind = tcTypeKind ty 900 901 tv_lvl = tcTyVarLevel tyvar 902 ty_lvl = tcTypeLevel ty 903 904 level_check_ok = not (ty_lvl `strictlyDeeperThan` tv_lvl) 905 level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty 906 907 double_upd_msg details = hang (text "Double update of meta tyvar") 908 2 (ppr tyvar $$ ppr details) 909 910{- Note [Level check when unifying] 911~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 912When unifying 913 alpha:lvl := ty 914we expect that the TcLevel of 'ty' will be <= lvl. 915However, during unflatting we do 916 fuv:l := ty:(l+1) 917which is usually wrong; hence the check isFmmvTyVar in level_check_ok. 918See Note [TcLevel assignment] in TcType. 919-} 920 921{- 922% Generating fresh variables for pattern match check 923-} 924 925 926{- 927************************************************************************ 928* * 929 MetaTvs: TauTvs 930* * 931************************************************************************ 932 933Note [Never need to instantiate coercion variables] 934~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 935With coercion variables sloshing around in types, it might seem that we 936sometimes need to instantiate coercion variables. This would be problematic, 937because coercion variables inhabit unboxed equality (~#), and the constraint 938solver thinks in terms only of boxed equality (~). The solution is that 939we never need to instantiate coercion variables in the first place. 940 941The tyvars that we need to instantiate come from the types of functions, 942data constructors, and patterns. These will never be quantified over 943coercion variables, except for the special case of the promoted Eq#. But, 944that can't ever appear in user code, so we're safe! 945-} 946 947 948newFlexiTyVar :: Kind -> TcM TcTyVar 949newFlexiTyVar kind = newAnonMetaTyVar TauTv kind 950 951newFlexiTyVarTy :: Kind -> TcM TcType 952newFlexiTyVarTy kind = do 953 tc_tyvar <- newFlexiTyVar kind 954 return (mkTyVarTy tc_tyvar) 955 956newFlexiTyVarTys :: Int -> Kind -> TcM [TcType] 957newFlexiTyVarTys n kind = replicateM n (newFlexiTyVarTy kind) 958 959newOpenTypeKind :: TcM TcKind 960newOpenTypeKind 961 = do { rr <- newFlexiTyVarTy runtimeRepTy 962 ; return (tYPE rr) } 963 964-- | Create a tyvar that can be a lifted or unlifted type. 965-- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh 966newOpenFlexiTyVarTy :: TcM TcType 967newOpenFlexiTyVarTy 968 = do { kind <- newOpenTypeKind 969 ; newFlexiTyVarTy kind } 970 971newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) 972-- Instantiate with META type variables 973-- Note that this works for a sequence of kind, type, and coercion variables 974-- variables. Eg [ (k:*), (a:k->k) ] 975-- Gives [ (k7:*), (a8:k7->k7) ] 976newMetaTyVars = newMetaTyVarsX emptyTCvSubst 977 -- emptyTCvSubst has an empty in-scope set, but that's fine here 978 -- Since the tyvars are freshly made, they cannot possibly be 979 -- captured by any existing for-alls. 980 981newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar]) 982-- Just like newMetaTyVars, but start with an existing substitution. 983newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst 984 985newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar) 986-- Make a new unification variable tyvar whose Name and Kind come from 987-- an existing TyVar. We substitute kind variables in the kind. 988newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar 989 990newMetaTyVarTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) 991newMetaTyVarTyVars = mapAccumLM newMetaTyVarTyVarX emptyTCvSubst 992 993newMetaTyVarTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar) 994-- Just like newMetaTyVarX, but make a TyVarTv 995newMetaTyVarTyVarX subst tyvar = new_meta_tv_x TyVarTv subst tyvar 996 997newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar) 998newWildCardX subst tv 999 = do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv)) 1000 ; return (extendTvSubstWithClone subst tv new_tv, new_tv) } 1001 1002new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar) 1003new_meta_tv_x info subst tv 1004 = do { new_tv <- cloneAnonMetaTyVar info tv substd_kind 1005 ; let subst1 = extendTvSubstWithClone subst tv new_tv 1006 ; return (subst1, new_tv) } 1007 where 1008 substd_kind = substTyUnchecked subst (tyVarKind tv) 1009 -- NOTE: #12549 is fixed so we could use 1010 -- substTy here, but the tc_infer_args problem 1011 -- is not yet fixed so leaving as unchecked for now. 1012 -- OLD NOTE: 1013 -- Unchecked because we call newMetaTyVarX from 1014 -- tcInstTyBinder, which is called from tcInferApps 1015 -- which does not yet take enough trouble to ensure 1016 -- the in-scope set is right; e.g. #12785 trips 1017 -- if we use substTy here 1018 1019newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType 1020newMetaTyVarTyAtLevel tc_lvl kind 1021 = do { ref <- newMutVar Flexi 1022 ; name <- newMetaTyVarName (fsLit "p") 1023 ; let details = MetaTv { mtv_info = TauTv 1024 , mtv_ref = ref 1025 , mtv_tclvl = tc_lvl } 1026 ; return (mkTyVarTy (mkTcTyVar name kind details)) } 1027 1028{- ********************************************************************* 1029* * 1030 Finding variables to quantify over 1031* * 1032********************************************************************* -} 1033 1034{- Note [Dependent type variables] 1035~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1036In Haskell type inference we quantify over type variables; but we only 1037quantify over /kind/ variables when -XPolyKinds is on. Without -XPolyKinds 1038we default the kind variables to *. 1039 1040So, to support this defaulting, and only for that reason, when 1041collecting the free vars of a type (in candidateQTyVarsOfType and friends), 1042prior to quantifying, we must keep the type and kind variables separate. 1043 1044But what does that mean in a system where kind variables /are/ type 1045variables? It's a fairly arbitrary distinction based on how the 1046variables appear: 1047 1048 - "Kind variables" appear in the kind of some other free variable 1049 or in the kind of a locally quantified type variable 1050 (forall (a :: kappa). ...) or in the kind of a coercion 1051 (a |> (co :: kappa1 ~ kappa2)). 1052 1053 These are the ones we default to * if -XPolyKinds is off 1054 1055 - "Type variables" are all free vars that are not kind variables 1056 1057E.g. In the type T k (a::k) 1058 'k' is a kind variable, because it occurs in the kind of 'a', 1059 even though it also appears at "top level" of the type 1060 'a' is a type variable, because it doesn't 1061 1062We gather these variables using a CandidatesQTvs record: 1063 DV { dv_kvs: Variables free in the kind of a free type variable 1064 or of a forall-bound type variable 1065 , dv_tvs: Variables sytactically free in the type } 1066 1067So: dv_kvs are the kind variables of the type 1068 (dv_tvs - dv_kvs) are the type variable of the type 1069 1070Note that 1071 1072* A variable can occur in both. 1073 T k (x::k) The first occurrence of k makes it 1074 show up in dv_tvs, the second in dv_kvs 1075 1076* We include any coercion variables in the "dependent", 1077 "kind-variable" set because we never quantify over them. 1078 1079* The "kind variables" might depend on each other; e.g 1080 (k1 :: k2), (k2 :: *) 1081 The "type variables" do not depend on each other; if 1082 one did, it'd be classified as a kind variable! 1083 1084Note [CandidatesQTvs determinism and order] 1085~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1086* Determinism: when we quantify over type variables we decide the 1087 order in which they appear in the final type. Because the order of 1088 type variables in the type can end up in the interface file and 1089 affects some optimizations like worker-wrapper, we want this order to 1090 be deterministic. 1091 1092 To achieve that we use deterministic sets of variables that can be 1093 converted to lists in a deterministic order. For more information 1094 about deterministic sets see Note [Deterministic UniqFM] in UniqDFM. 1095 1096* Order: as well as being deterministic, we use an 1097 accumulating-parameter style for candidateQTyVarsOfType so that we 1098 add variables one at a time, left to right. That means we tend to 1099 produce the variables in left-to-right order. This is just to make 1100 it bit more predictable for the programmer. 1101 1102Note [Naughty quantification candidates] 1103~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1104Consider (#14880, dependent/should_compile/T14880-2), suppose 1105we are trying to generalise this type: 1106 1107 forall arg. ... (alpha[tau]:arg) ... 1108 1109We have a metavariable alpha whose kind mentions a skolem variable 1110bound inside the very type we are generalising. 1111This can arise while type-checking a user-written type signature 1112(see the test case for the full code). 1113 1114We cannot generalise over alpha! That would produce a type like 1115 forall {a :: arg}. forall arg. ...blah... 1116The fact that alpha's kind mentions arg renders it completely 1117ineligible for generalisation. 1118 1119However, we are not going to learn any new constraints on alpha, 1120because its kind isn't even in scope in the outer context (but see Wrinkle). 1121So alpha is entirely unconstrained. 1122 1123What then should we do with alpha? During generalization, every 1124metavariable is either (A) promoted, (B) generalized, or (C) zapped 1125(according again to Note [Recipe for checking a signature] in 1126TcHsType). 1127 1128 * We can't generalise it. 1129 * We can't promote it, because its kind prevents that 1130 * We can't simply leave it be, because this type is about to 1131 go into the typing environment (as the type of some let-bound 1132 variable, say), and then chaos erupts when we try to instantiate. 1133 1134So, we zap it, eagerly, to Any. We don't have to do this eager zapping 1135in terms (say, in `length []`) because terms are never re-examined before 1136the final zonk (which zaps any lingering metavariables to Any). 1137 1138We do this eager zapping in candidateQTyVars, which always precedes 1139generalisation, because at that moment we have a clear picture of what 1140skolems are in scope within the type itself (e.g. that 'forall arg'). 1141 1142Wrinkle: 1143 1144We must make absolutely sure that alpha indeed is not 1145from an outer context. (Otherwise, we might indeed learn more information 1146about it.) This can be done easily: we just check alpha's TcLevel. 1147That level must be strictly greater than the ambient TcLevel in order 1148to treat it as naughty. We say "strictly greater than" because the call to 1149candidateQTyVars is made outside the bumped TcLevel, as stated in the 1150comment to candidateQTyVarsOfType. The level check is done in go_tv 1151in collect_cand_qtvs. Skipping this check caused #16517. 1152 1153-} 1154 1155data CandidatesQTvs 1156 -- See Note [Dependent type variables] 1157 -- See Note [CandidatesQTvs determinism and order] 1158 -- 1159 -- Invariants: 1160 -- * All variables are fully zonked, including their kinds 1161 -- * All variables are at a level greater than the ambient level 1162 -- See Note [Use level numbers for quantification] 1163 -- 1164 -- This *can* contain skolems. For example, in `data X k :: k -> Type` 1165 -- we need to know that the k is a dependent variable. This is done 1166 -- by collecting the candidates in the kind after skolemising. It also 1167 -- comes up when generalizing a associated type instance, where instance 1168 -- variables are skolems. (Recall that associated type instances are generalized 1169 -- independently from their enclosing class instance, and the associated 1170 -- type instance may be generalized by more, fewer, or different variables 1171 -- than the class instance.) 1172 -- 1173 = DV { dv_kvs :: DTyVarSet -- "kind" metavariables (dependent) 1174 , dv_tvs :: DTyVarSet -- "type" metavariables (non-dependent) 1175 -- A variable may appear in both sets 1176 -- E.g. T k (x::k) The first occurrence of k makes it 1177 -- show up in dv_tvs, the second in dv_kvs 1178 -- See Note [Dependent type variables] 1179 1180 , dv_cvs :: CoVarSet 1181 -- These are covars. Included only so that we don't repeatedly 1182 -- look at covars' kinds in accumulator. Not used by quantifyTyVars. 1183 } 1184 1185instance Semi.Semigroup CandidatesQTvs where 1186 (DV { dv_kvs = kv1, dv_tvs = tv1, dv_cvs = cv1 }) 1187 <> (DV { dv_kvs = kv2, dv_tvs = tv2, dv_cvs = cv2 }) 1188 = DV { dv_kvs = kv1 `unionDVarSet` kv2 1189 , dv_tvs = tv1 `unionDVarSet` tv2 1190 , dv_cvs = cv1 `unionVarSet` cv2 } 1191 1192instance Monoid CandidatesQTvs where 1193 mempty = DV { dv_kvs = emptyDVarSet, dv_tvs = emptyDVarSet, dv_cvs = emptyVarSet } 1194 mappend = (Semi.<>) 1195 1196instance Outputable CandidatesQTvs where 1197 ppr (DV {dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) 1198 = text "DV" <+> braces (pprWithCommas id [ text "dv_kvs =" <+> ppr kvs 1199 , text "dv_tvs =" <+> ppr tvs 1200 , text "dv_cvs =" <+> ppr cvs ]) 1201 1202 1203candidateKindVars :: CandidatesQTvs -> TyVarSet 1204candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs) 1205 1206partitionCandidates :: CandidatesQTvs -> (TyVar -> Bool) -> (DTyVarSet, CandidatesQTvs) 1207partitionCandidates dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) pred 1208 = (extracted, dvs { dv_kvs = rest_kvs, dv_tvs = rest_tvs }) 1209 where 1210 (extracted_kvs, rest_kvs) = partitionDVarSet pred kvs 1211 (extracted_tvs, rest_tvs) = partitionDVarSet pred tvs 1212 extracted = extracted_kvs `unionDVarSet` extracted_tvs 1213 1214-- | Gathers free variables to use as quantification candidates (in 1215-- 'quantifyTyVars'). This might output the same var 1216-- in both sets, if it's used in both a type and a kind. 1217-- The variables to quantify must have a TcLevel strictly greater than 1218-- the ambient level. (See Wrinkle in Note [Naughty quantification candidates]) 1219-- See Note [CandidatesQTvs determinism and order] 1220-- See Note [Dependent type variables] 1221candidateQTyVarsOfType :: TcType -- not necessarily zonked 1222 -> TcM CandidatesQTvs 1223candidateQTyVarsOfType ty = collect_cand_qtvs False emptyVarSet mempty ty 1224 1225-- | Like 'candidateQTyVarsOfType', but over a list of types 1226-- The variables to quantify must have a TcLevel strictly greater than 1227-- the ambient level. (See Wrinkle in Note [Naughty quantification candidates]) 1228candidateQTyVarsOfTypes :: [Type] -> TcM CandidatesQTvs 1229candidateQTyVarsOfTypes tys = foldlM (collect_cand_qtvs False emptyVarSet) mempty tys 1230 1231-- | Like 'candidateQTyVarsOfType', but consider every free variable 1232-- to be dependent. This is appropriate when generalizing a *kind*, 1233-- instead of a type. (That way, -XNoPolyKinds will default the variables 1234-- to Type.) 1235candidateQTyVarsOfKind :: TcKind -- Not necessarily zonked 1236 -> TcM CandidatesQTvs 1237candidateQTyVarsOfKind ty = collect_cand_qtvs True emptyVarSet mempty ty 1238 1239candidateQTyVarsOfKinds :: [TcKind] -- Not necessarily zonked 1240 -> TcM CandidatesQTvs 1241candidateQTyVarsOfKinds tys = foldM (collect_cand_qtvs True emptyVarSet) mempty tys 1242 1243delCandidates :: CandidatesQTvs -> [Var] -> CandidatesQTvs 1244delCandidates (DV { dv_kvs = kvs, dv_tvs = tvs, dv_cvs = cvs }) vars 1245 = DV { dv_kvs = kvs `delDVarSetList` vars 1246 , dv_tvs = tvs `delDVarSetList` vars 1247 , dv_cvs = cvs `delVarSetList` vars } 1248 1249collect_cand_qtvs 1250 :: Bool -- True <=> consider every fv in Type to be dependent 1251 -> VarSet -- Bound variables (locals only) 1252 -> CandidatesQTvs -- Accumulating parameter 1253 -> Type -- Not necessarily zonked 1254 -> TcM CandidatesQTvs 1255 1256-- Key points: 1257-- * Looks through meta-tyvars as it goes; 1258-- no need to zonk in advance 1259-- 1260-- * Needs to be monadic anyway, because it does the zap-naughty 1261-- stuff; see Note [Naughty quantification candidates] 1262-- 1263-- * Returns fully-zonked CandidateQTvs, including their kinds 1264-- so that subsequent dependency analysis (to build a well 1265-- scoped telescope) works correctly 1266 1267collect_cand_qtvs is_dep bound dvs ty 1268 = go dvs ty 1269 where 1270 is_bound tv = tv `elemVarSet` bound 1271 1272 ----------------- 1273 go :: CandidatesQTvs -> TcType -> TcM CandidatesQTvs 1274 -- Uses accumulating-parameter style 1275 go dv (AppTy t1 t2) = foldlM go dv [t1, t2] 1276 go dv (TyConApp _ tys) = foldlM go dv tys 1277 go dv (FunTy _ arg res) = foldlM go dv [arg, res] 1278 go dv (LitTy {}) = return dv 1279 go dv (CastTy ty co) = do dv1 <- go dv ty 1280 collect_cand_qtvs_co bound dv1 co 1281 go dv (CoercionTy co) = collect_cand_qtvs_co bound dv co 1282 1283 go dv (TyVarTy tv) 1284 | is_bound tv = return dv 1285 | otherwise = do { m_contents <- isFilledMetaTyVar_maybe tv 1286 ; case m_contents of 1287 Just ind_ty -> go dv ind_ty 1288 Nothing -> go_tv dv tv } 1289 1290 go dv (ForAllTy (Bndr tv _) ty) 1291 = do { dv1 <- collect_cand_qtvs True bound dv (tyVarKind tv) 1292 ; collect_cand_qtvs is_dep (bound `extendVarSet` tv) dv1 ty } 1293 1294 ----------------- 1295 go_tv dv@(DV { dv_kvs = kvs, dv_tvs = tvs }) tv 1296 | tv `elemDVarSet` kvs 1297 = return dv -- We have met this tyvar aleady 1298 1299 | not is_dep 1300 , tv `elemDVarSet` tvs 1301 = return dv -- We have met this tyvar aleady 1302 1303 | otherwise 1304 = do { tv_kind <- zonkTcType (tyVarKind tv) 1305 -- This zonk is annoying, but it is necessary, both to 1306 -- ensure that the collected candidates have zonked kinds 1307 -- (#15795) and to make the naughty check 1308 -- (which comes next) works correctly 1309 1310 ; cur_lvl <- getTcLevel 1311 ; if | tcTyVarLevel tv <= cur_lvl 1312 -> return dv -- this variable is from an outer context; skip 1313 -- See Note [Use level numbers ofor quantification] 1314 1315 | intersectsVarSet bound (tyCoVarsOfType tv_kind) 1316 -- the tyvar must not be from an outer context, but we have 1317 -- already checked for this. 1318 -- See Note [Naughty quantification candidates] 1319 -> do { traceTc "Zapping naughty quantifier" $ 1320 vcat [ ppr tv <+> dcolon <+> ppr tv_kind 1321 , text "bound:" <+> pprTyVars (nonDetEltsUniqSet bound) 1322 , text "fvs:" <+> pprTyVars (nonDetEltsUniqSet $ 1323 tyCoVarsOfType tv_kind) ] 1324 1325 ; writeMetaTyVar tv (anyTypeOfKind tv_kind) 1326 1327 -- See Note [Recurring into kinds for candidateQTyVars] 1328 ; collect_cand_qtvs True bound dv tv_kind } 1329 1330 | otherwise 1331 -> do { let tv' = tv `setTyVarKind` tv_kind 1332 dv' | is_dep = dv { dv_kvs = kvs `extendDVarSet` tv' } 1333 | otherwise = dv { dv_tvs = tvs `extendDVarSet` tv' } 1334 -- See Note [Order of accumulation] 1335 1336 -- See Note [Recurring into kinds for candidateQTyVars] 1337 ; collect_cand_qtvs True bound dv' tv_kind } } 1338 1339collect_cand_qtvs_co :: VarSet -- bound variables 1340 -> CandidatesQTvs -> Coercion 1341 -> TcM CandidatesQTvs 1342collect_cand_qtvs_co bound = go_co 1343 where 1344 go_co dv (Refl ty) = collect_cand_qtvs True bound dv ty 1345 go_co dv (GRefl _ ty mco) = do dv1 <- collect_cand_qtvs True bound dv ty 1346 go_mco dv1 mco 1347 go_co dv (TyConAppCo _ _ cos) = foldlM go_co dv cos 1348 go_co dv (AppCo co1 co2) = foldlM go_co dv [co1, co2] 1349 go_co dv (FunCo _ co1 co2) = foldlM go_co dv [co1, co2] 1350 go_co dv (AxiomInstCo _ _ cos) = foldlM go_co dv cos 1351 go_co dv (AxiomRuleCo _ cos) = foldlM go_co dv cos 1352 go_co dv (UnivCo prov _ t1 t2) = do dv1 <- go_prov dv prov 1353 dv2 <- collect_cand_qtvs True bound dv1 t1 1354 collect_cand_qtvs True bound dv2 t2 1355 go_co dv (SymCo co) = go_co dv co 1356 go_co dv (TransCo co1 co2) = foldlM go_co dv [co1, co2] 1357 go_co dv (NthCo _ _ co) = go_co dv co 1358 go_co dv (LRCo _ co) = go_co dv co 1359 go_co dv (InstCo co1 co2) = foldlM go_co dv [co1, co2] 1360 go_co dv (KindCo co) = go_co dv co 1361 go_co dv (SubCo co) = go_co dv co 1362 1363 go_co dv (HoleCo hole) 1364 = do m_co <- unpackCoercionHole_maybe hole 1365 case m_co of 1366 Just co -> go_co dv co 1367 Nothing -> go_cv dv (coHoleCoVar hole) 1368 1369 go_co dv (CoVarCo cv) = go_cv dv cv 1370 1371 go_co dv (ForAllCo tcv kind_co co) 1372 = do { dv1 <- go_co dv kind_co 1373 ; collect_cand_qtvs_co (bound `extendVarSet` tcv) dv1 co } 1374 1375 go_mco dv MRefl = return dv 1376 go_mco dv (MCo co) = go_co dv co 1377 1378 go_prov dv UnsafeCoerceProv = return dv 1379 go_prov dv (PhantomProv co) = go_co dv co 1380 go_prov dv (ProofIrrelProv co) = go_co dv co 1381 go_prov dv (PluginProv _) = return dv 1382 1383 go_cv :: CandidatesQTvs -> CoVar -> TcM CandidatesQTvs 1384 go_cv dv@(DV { dv_cvs = cvs }) cv 1385 | is_bound cv = return dv 1386 | cv `elemVarSet` cvs = return dv 1387 1388 -- See Note [Recurring into kinds for candidateQTyVars] 1389 | otherwise = collect_cand_qtvs True bound 1390 (dv { dv_cvs = cvs `extendVarSet` cv }) 1391 (idType cv) 1392 1393 is_bound tv = tv `elemVarSet` bound 1394 1395{- Note [Order of accumulation] 1396~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1397You might be tempted (like I was) to use unitDVarSet and mappend 1398rather than extendDVarSet. However, the union algorithm for 1399deterministic sets depends on (roughly) the size of the sets. The 1400elements from the smaller set end up to the right of the elements from 1401the larger one. When sets are equal, the left-hand argument to 1402`mappend` goes to the right of the right-hand argument. 1403 1404In our case, if we use unitDVarSet and mappend, we learn that the free 1405variables of (a -> b -> c -> d) are [b, a, c, d], and we then quantify 1406over them in that order. (The a comes after the b because we union the 1407singleton sets as ({a} `mappend` {b}), producing {b, a}. Thereafter, 1408the size criterion works to our advantage.) This is just annoying to 1409users, so I use `extendDVarSet`, which unambiguously puts the new 1410element to the right. 1411 1412Note that the unitDVarSet/mappend implementation would not be wrong 1413against any specification -- just suboptimal and confounding to users. 1414 1415Note [Recurring into kinds for candidateQTyVars] 1416~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1417First, read Note [Closing over free variable kinds] in TyCoFVs, paying 1418attention to the end of the Note about using an empty bound set when 1419traversing a variable's kind. 1420 1421That Note concludes with the recommendation that we empty out the bound 1422set when recurring into the kind of a type variable. Yet, we do not do 1423this here. I have two tasks in order to convince you that this code is 1424right. First, I must show why it is safe to ignore the reasoning in that 1425Note. Then, I must show why is is necessary to contradict the reasoning in 1426that Note. 1427 1428Why it is safe: There can be no 1429shadowing in the candidateQ... functions: they work on the output of 1430type inference, which is seeded by the renamer and its insistence to 1431use different Uniques for different variables. (In contrast, the Core 1432functions work on the output of optimizations, which may introduce 1433shadowing.) Without shadowing, the problem studied by 1434Note [Closing over free variable kinds] in TyCoFVs cannot happen. 1435 1436Why it is necessary: 1437Wiping the bound set would be just plain wrong here. Consider 1438 1439 forall k1 k2 (a :: k1). Proxy k2 (a |> (hole :: k1 ~# k2)) 1440 1441We really don't want to think k1 and k2 are free here. (It's true that we'll 1442never be able to fill in `hole`, but we don't want to go off the rails just 1443because we have an insoluble coercion hole.) So: why is it wrong to wipe 1444the bound variables here but right in Core? Because the final statement 1445in Note [Closing over free variable kinds] in TyCoFVs is wrong: not 1446every variable is either free or bound. A variable can be a hole, too! 1447The reasoning in that Note then breaks down. 1448 1449And the reasoning applies just as well to free non-hole variables, so we 1450retain the bound set always. 1451 1452-} 1453 1454{- ********************************************************************* 1455* * 1456 Quantification 1457* * 1458************************************************************************ 1459 1460Note [quantifyTyVars] 1461~~~~~~~~~~~~~~~~~~~~~ 1462quantifyTyVars is given the free vars of a type that we 1463are about to wrap in a forall. 1464 1465It takes these free type/kind variables (partitioned into dependent and 1466non-dependent variables) skolemises metavariables with a TcLevel greater 1467than the ambient level (see Note [Use level numbers of quantification]). 1468 1469* This function distinguishes between dependent and non-dependent 1470 variables only to keep correct defaulting behavior with -XNoPolyKinds. 1471 With -XPolyKinds, it treats both classes of variables identically. 1472 1473* quantifyTyVars never quantifies over 1474 - a coercion variable (or any tv mentioned in the kind of a covar) 1475 - a runtime-rep variable 1476 1477Note [Use level numbers for quantification] 1478~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1479The level numbers assigned to metavariables are very useful. Not only 1480do they track touchability (Note [TcLevel and untouchable type variables] 1481in TcType), but they also allow us to determine which variables to 1482generalise. The rule is this: 1483 1484 When generalising, quantify only metavariables with a TcLevel greater 1485 than the ambient level. 1486 1487This works because we bump the level every time we go inside a new 1488source-level construct. In a traditional generalisation algorithm, we 1489would gather all free variables that aren't free in an environment. 1490However, if a variable is in that environment, it will always have a lower 1491TcLevel: it came from an outer scope. So we can replace the "free in 1492environment" check with a level-number check. 1493 1494Here is an example: 1495 1496 f x = x + (z True) 1497 where 1498 z y = x * x 1499 1500We start by saying (x :: alpha[1]). When inferring the type of z, we'll 1501quickly discover that z :: alpha[1]. But it would be disastrous to 1502generalise over alpha in the type of z. So we need to know that alpha 1503comes from an outer environment. By contrast, the type of y is beta[2], 1504and we are free to generalise over it. What's the difference between 1505alpha[1] and beta[2]? Their levels. beta[2] has the right TcLevel for 1506generalisation, and so we generalise it. alpha[1] does not, and so 1507we leave it alone. 1508 1509Note that not *every* variable with a higher level will get generalised, 1510either due to the monomorphism restriction or other quirks. See, for 1511example, the code in TcSimplify.decideMonoTyVars and in 1512TcHsType.kindGeneralizeSome, both of which exclude certain otherwise-eligible 1513variables from being generalised. 1514 1515Using level numbers for quantification is implemented in the candidateQTyVars... 1516functions, by adding only those variables with a level strictly higher than 1517the ambient level to the set of candidates. 1518 1519Note [quantifyTyVars determinism] 1520~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1521The results of quantifyTyVars are wrapped in a forall and can end up in the 1522interface file. One such example is inferred type signatures. They also affect 1523the results of optimizations, for example worker-wrapper. This means that to 1524get deterministic builds quantifyTyVars needs to be deterministic. 1525 1526To achieve this CandidatesQTvs is backed by deterministic sets which allows them 1527to be later converted to a list in a deterministic order. 1528 1529For more information about deterministic sets see 1530Note [Deterministic UniqFM] in UniqDFM. 1531-} 1532 1533quantifyTyVars 1534 :: CandidatesQTvs -- See Note [Dependent type variables] 1535 -- Already zonked 1536 -> TcM [TcTyVar] 1537-- See Note [quantifyTyVars] 1538-- Can be given a mixture of TcTyVars and TyVars, in the case of 1539-- associated type declarations. Also accepts covars, but *never* returns any. 1540-- According to Note [Use level numbers for quantification] and the 1541-- invariants on CandidateQTvs, we do not have to filter out variables 1542-- free in the environment here. Just quantify unconditionally, subject 1543-- to the restrictions in Note [quantifyTyVars]. 1544quantifyTyVars dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) 1545 -- short-circuit common case 1546 | isEmptyDVarSet dep_tkvs 1547 , isEmptyDVarSet nondep_tkvs 1548 = do { traceTc "quantifyTyVars has nothing to quantify" empty 1549 ; return [] } 1550 1551 | otherwise 1552 = do { traceTc "quantifyTyVars 1" (ppr dvs) 1553 1554 ; let dep_kvs = scopedSort $ dVarSetElems dep_tkvs 1555 -- scopedSort: put the kind variables into 1556 -- well-scoped order. 1557 -- E.g. [k, (a::k)] not the other way roud 1558 1559 nondep_tvs = dVarSetElems (nondep_tkvs `minusDVarSet` dep_tkvs) 1560 -- See Note [Dependent type variables] 1561 -- The `minus` dep_tkvs removes any kind-level vars 1562 -- e.g. T k (a::k) Since k appear in a kind it'll 1563 -- be in dv_kvs, and is dependent. So remove it from 1564 -- dv_tvs which will also contain k 1565 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV 1566 1567 -- In the non-PolyKinds case, default the kind variables 1568 -- to *, and zonk the tyvars as usual. Notice that this 1569 -- may make quantifyTyVars return a shorter list 1570 -- than it was passed, but that's ok 1571 ; poly_kinds <- xoptM LangExt.PolyKinds 1572 ; dep_kvs' <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs 1573 ; nondep_tvs' <- mapMaybeM (zonk_quant False) nondep_tvs 1574 ; let final_qtvs = dep_kvs' ++ nondep_tvs' 1575 -- Because of the order, any kind variables 1576 -- mentioned in the kinds of the nondep_tvs' 1577 -- now refer to the dep_kvs' 1578 1579 ; traceTc "quantifyTyVars 2" 1580 (vcat [ text "nondep:" <+> pprTyVars nondep_tvs 1581 , text "dep:" <+> pprTyVars dep_kvs 1582 , text "dep_kvs'" <+> pprTyVars dep_kvs' 1583 , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ]) 1584 1585 -- We should never quantify over coercion variables; check this 1586 ; let co_vars = filter isCoVar final_qtvs 1587 ; MASSERT2( null co_vars, ppr co_vars ) 1588 1589 ; return final_qtvs } 1590 where 1591 -- zonk_quant returns a tyvar if it should be quantified over; 1592 -- otherwise, it returns Nothing. The latter case happens for 1593 -- * Kind variables, with -XNoPolyKinds: don't quantify over these 1594 -- * RuntimeRep variables: we never quantify over these 1595 zonk_quant default_kind tkv 1596 | not (isTyVar tkv) 1597 = return Nothing -- this can happen for a covar that's associated with 1598 -- a coercion hole. Test case: typecheck/should_compile/T2494 1599 1600 | not (isTcTyVar tkv) 1601 = return (Just tkv) -- For associated types in a class with a standalone 1602 -- kind signature, we have the class variables in 1603 -- scope, and they are TyVars not TcTyVars 1604 | otherwise 1605 = do { deflt_done <- defaultTyVar default_kind tkv 1606 ; case deflt_done of 1607 True -> return Nothing 1608 False -> do { tv <- skolemiseQuantifiedTyVar tkv 1609 ; return (Just tv) } } 1610 1611isQuantifiableTv :: TcLevel -- Level of the context, outside the quantification 1612 -> TcTyVar 1613 -> Bool 1614isQuantifiableTv outer_tclvl tcv 1615 | isTcTyVar tcv -- Might be a CoVar; change this when gather covars separately 1616 = tcTyVarLevel tcv > outer_tclvl 1617 | otherwise 1618 = False 1619 1620zonkAndSkolemise :: TcTyCoVar -> TcM TcTyCoVar 1621-- A tyvar binder is never a unification variable (TauTv), 1622-- rather it is always a skolem. It *might* be a TyVarTv. 1623-- (Because non-CUSK type declarations use TyVarTvs.) 1624-- Regardless, it may have a kind that has not yet been zonked, 1625-- and may include kind unification variables. 1626zonkAndSkolemise tyvar 1627 | isTyVarTyVar tyvar 1628 -- We want to preserve the binding location of the original TyVarTv. 1629 -- This is important for error messages. If we don't do this, then 1630 -- we get bad locations in, e.g., typecheck/should_fail/T2688 1631 = do { zonked_tyvar <- zonkTcTyVarToTyVar tyvar 1632 ; skolemiseQuantifiedTyVar zonked_tyvar } 1633 1634 | otherwise 1635 = ASSERT2( isImmutableTyVar tyvar || isCoVar tyvar, pprTyVar tyvar ) 1636 zonkTyCoVarKind tyvar 1637 1638skolemiseQuantifiedTyVar :: TcTyVar -> TcM TcTyVar 1639-- The quantified type variables often include meta type variables 1640-- we want to freeze them into ordinary type variables 1641-- The meta tyvar is updated to point to the new skolem TyVar. Now any 1642-- bound occurrences of the original type variable will get zonked to 1643-- the immutable version. 1644-- 1645-- We leave skolem TyVars alone; they are immutable. 1646-- 1647-- This function is called on both kind and type variables, 1648-- but kind variables *only* if PolyKinds is on. 1649 1650skolemiseQuantifiedTyVar tv 1651 = case tcTyVarDetails tv of 1652 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv) 1653 ; return (setTyVarKind tv kind) } 1654 -- It might be a skolem type variable, 1655 -- for example from a user type signature 1656 1657 MetaTv {} -> skolemiseUnboundMetaTyVar tv 1658 1659 _other -> pprPanic "skolemiseQuantifiedTyVar" (ppr tv) -- RuntimeUnk 1660 1661defaultTyVar :: Bool -- True <=> please default this kind variable to * 1662 -> TcTyVar -- If it's a MetaTyVar then it is unbound 1663 -> TcM Bool -- True <=> defaulted away altogether 1664 1665defaultTyVar default_kind tv 1666 | not (isMetaTyVar tv) 1667 = return False 1668 1669 | isTyVarTyVar tv 1670 -- Do not default TyVarTvs. Doing so would violate the invariants 1671 -- on TyVarTvs; see Note [Signature skolems] in TcType. 1672 -- #13343 is an example; #14555 is another 1673 -- See Note [Inferring kinds for type declarations] in TcTyClsDecls 1674 = return False 1675 1676 1677 | isRuntimeRepVar tv -- Do not quantify over a RuntimeRep var 1678 -- unless it is a TyVarTv, handled earlier 1679 = do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv) 1680 ; writeMetaTyVar tv liftedRepTy 1681 ; return True } 1682 1683 | default_kind -- -XNoPolyKinds and this is a kind var 1684 = default_kind_var tv -- so default it to * if possible 1685 1686 | otherwise 1687 = return False 1688 1689 where 1690 default_kind_var :: TyVar -> TcM Bool 1691 -- defaultKindVar is used exclusively with -XNoPolyKinds 1692 -- See Note [Defaulting with -XNoPolyKinds] 1693 -- It takes an (unconstrained) meta tyvar and defaults it. 1694 -- Works only on vars of type *; for other kinds, it issues an error. 1695 default_kind_var kv 1696 | isLiftedTypeKind (tyVarKind kv) 1697 = do { traceTc "Defaulting a kind var to *" (ppr kv) 1698 ; writeMetaTyVar kv liftedTypeKind 1699 ; return True } 1700 | otherwise 1701 = do { addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv') 1702 , text "of kind:" <+> ppr (tyVarKind kv') 1703 , text "Perhaps enable PolyKinds or add a kind signature" ]) 1704 -- We failed to default it, so return False to say so. 1705 -- Hence, it'll get skolemised. That might seem odd, but we must either 1706 -- promote, skolemise, or zap-to-Any, to satisfy TcHsType 1707 -- Note [Recipe for checking a signature] 1708 -- Otherwise we get level-number assertion failures. It doesn't matter much 1709 -- because we are in an error siutation anyway. 1710 ; return False 1711 } 1712 where 1713 (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv 1714 1715skolemiseUnboundMetaTyVar :: TcTyVar -> TcM TyVar 1716-- We have a Meta tyvar with a ref-cell inside it 1717-- Skolemise it, so that we are totally out of Meta-tyvar-land 1718-- We create a skolem TcTyVar, not a regular TyVar 1719-- See Note [Zonking to Skolem] 1720skolemiseUnboundMetaTyVar tv 1721 = ASSERT2( isMetaTyVar tv, ppr tv ) 1722 do { when debugIsOn (check_empty tv) 1723 ; here <- getSrcSpanM -- Get the location from "here" 1724 -- ie where we are generalising 1725 ; kind <- zonkTcType (tyVarKind tv) 1726 ; let tv_name = tyVarName tv 1727 -- See Note [Skolemising and identity] 1728 final_name | isSystemName tv_name 1729 = mkInternalName (nameUnique tv_name) 1730 (nameOccName tv_name) here 1731 | otherwise 1732 = tv_name 1733 final_tv = mkTcTyVar final_name kind details 1734 1735 ; traceTc "Skolemising" (ppr tv <+> text ":=" <+> ppr final_tv) 1736 ; writeMetaTyVar tv (mkTyVarTy final_tv) 1737 ; return final_tv } 1738 1739 where 1740 details = SkolemTv (metaTyVarTcLevel tv) False 1741 check_empty tv -- [Sept 04] Check for non-empty. 1742 = when debugIsOn $ -- See note [Silly Type Synonym] 1743 do { cts <- readMetaTyVar tv 1744 ; case cts of 1745 Flexi -> return () 1746 Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 1747 return () } 1748 1749{- Note [Defaulting with -XNoPolyKinds] 1750~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1751Consider 1752 1753 data Compose f g a = Mk (f (g a)) 1754 1755We infer 1756 1757 Compose :: forall k1 k2. (k2 -> *) -> (k1 -> k2) -> k1 -> * 1758 Mk :: forall k1 k2 (f :: k2 -> *) (g :: k1 -> k2) (a :: k1). 1759 f (g a) -> Compose k1 k2 f g a 1760 1761Now, in another module, we have -XNoPolyKinds -XDataKinds in effect. 1762What does 'Mk mean? Pre GHC-8.0 with -XNoPolyKinds, 1763we just defaulted all kind variables to *. But that's no good here, 1764because the kind variables in 'Mk aren't of kind *, so defaulting to * 1765is ill-kinded. 1766 1767After some debate on #11334, we decided to issue an error in this case. 1768The code is in defaultKindVar. 1769 1770Note [What is a meta variable?] 1771~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1772A "meta type-variable", also know as a "unification variable" is a placeholder 1773introduced by the typechecker for an as-yet-unknown monotype. 1774 1775For example, when we see a call `reverse (f xs)`, we know that we calling 1776 reverse :: forall a. [a] -> [a] 1777So we know that the argument `f xs` must be a "list of something". But what is 1778the "something"? We don't know until we explore the `f xs` a bit more. So we set 1779out what we do know at the call of `reverse` by instantiating its type with a fresh 1780meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the 1781result, is `[alpha]`. The unification variable `alpha` stands for the 1782as-yet-unknown type of the elements of the list. 1783 1784As type inference progresses we may learn more about `alpha`. For example, suppose 1785`f` has the type 1786 f :: forall b. b -> [Maybe b] 1787Then we instantiate `f`'s type with another fresh unification variable, say 1788`beta`; and equate `f`'s result type with reverse's argument type, thus 1789`[alpha] ~ [Maybe beta]`. 1790 1791Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've 1792refined our knowledge about `alpha`. And so on. 1793 1794If you found this Note useful, you may also want to have a look at 1795Section 5 of "Practical type inference for higher rank types" (Peyton Jones, 1796Vytiniotis, Weirich and Shields. J. Functional Programming. 2011). 1797 1798Note [What is zonking?] 1799~~~~~~~~~~~~~~~~~~~~~~~ 1800GHC relies heavily on mutability in the typechecker for efficient operation. 1801For this reason, throughout much of the type checking process meta type 1802variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable 1803variables (known as TcRefs). 1804 1805Zonking is the process of ripping out these mutable variables and replacing them 1806with a real Type. This involves traversing the entire type expression, but the 1807interesting part of replacing the mutable variables occurs in zonkTyVarOcc. 1808 1809There are two ways to zonk a Type: 1810 1811 * zonkTcTypeToType, which is intended to be used at the end of type-checking 1812 for the final zonk. It has to deal with unfilled metavars, either by filling 1813 it with a value like Any or failing (determined by the UnboundTyVarZonker 1814 used). 1815 1816 * zonkTcType, which will happily ignore unfilled metavars. This is the 1817 appropriate function to use while in the middle of type-checking. 1818 1819Note [Zonking to Skolem] 1820~~~~~~~~~~~~~~~~~~~~~~~~ 1821We used to zonk quantified type variables to regular TyVars. However, this 1822leads to problems. Consider this program from the regression test suite: 1823 1824 eval :: Int -> String -> String -> String 1825 eval 0 root actual = evalRHS 0 root actual 1826 1827 evalRHS :: Int -> a 1828 evalRHS 0 root actual = eval 0 root actual 1829 1830It leads to the deferral of an equality (wrapped in an implication constraint) 1831 1832 forall a. () => ((String -> String -> String) ~ a) 1833 1834which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck). 1835In the meantime `a' is zonked and quantified to form `evalRHS's signature. 1836This has the *side effect* of also zonking the `a' in the deferred equality 1837(which at this point is being handed around wrapped in an implication 1838constraint). 1839 1840Finally, the equality (with the zonked `a') will be handed back to the 1841simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop. 1842If we zonk `a' with a regular type variable, we will have this regular type 1843variable now floating around in the simplifier, which in many places assumes to 1844only see proper TcTyVars. 1845 1846We can avoid this problem by zonking with a skolem TcTyVar. The 1847skolem is rigid (which we require for a quantified variable), but is 1848still a TcTyVar that the simplifier knows how to deal with. 1849 1850Note [Skolemising and identity] 1851~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1852In some places, we make a TyVarTv for a binder. E.g. 1853 class C a where ... 1854As Note [Inferring kinds for type declarations] discusses, 1855we make a TyVarTv for 'a'. Later we skolemise it, and we'd 1856like to retain its identity, location info etc. (If we don't 1857retain its identity we'll have to do some pointless swizzling; 1858see TcTyClsDecls.swizzleTcTyConBndrs. If we retain its identity 1859but not its location we'll lose the detailed binding site info. 1860 1861Conclusion: use the Name of the TyVarTv. But we don't want 1862to do that when skolemising random unification variables; 1863there the location we want is the skolemisation site. 1864 1865Fortunately we can tell the difference: random unification 1866variables have System Names. That's why final_name is 1867set based on the isSystemName test. 1868 1869 1870Note [Silly Type Synonyms] 1871~~~~~~~~~~~~~~~~~~~~~~~~~~ 1872Consider this: 1873 type C u a = u -- Note 'a' unused 1874 1875 foo :: (forall a. C u a -> C u a) -> u 1876 foo x = ... 1877 1878 bar :: Num u => u 1879 bar = foo (\t -> t + t) 1880 1881* From the (\t -> t+t) we get type {Num d} => d -> d 1882 where d is fresh. 1883 1884* Now unify with type of foo's arg, and we get: 1885 {Num (C d a)} => C d a -> C d a 1886 where a is fresh. 1887 1888* Now abstract over the 'a', but float out the Num (C d a) constraint 1889 because it does not 'really' mention a. (see exactTyVarsOfType) 1890 The arg to foo becomes 1891 \/\a -> \t -> t+t 1892 1893* So we get a dict binding for Num (C d a), which is zonked to give 1894 a = () 1895 [Note Sept 04: now that we are zonking quantified type variables 1896 on construction, the 'a' will be frozen as a regular tyvar on 1897 quantification, so the floated dict will still have type (C d a). 1898 Which renders this whole note moot; happily!] 1899 1900* Then the \/\a abstraction has a zonked 'a' in it. 1901 1902All very silly. I think its harmless to ignore the problem. We'll end up with 1903a \/\a in the final result but all the occurrences of a will be zonked to () 1904 1905************************************************************************ 1906* * 1907 Zonking types 1908* * 1909************************************************************************ 1910 1911-} 1912 1913zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet 1914-- Zonk a type and take its free variables 1915-- With kind polymorphism it can be essential to zonk *first* 1916-- so that we find the right set of free variables. Eg 1917-- forall k1. forall (a:k2). a 1918-- where k2:=k1 is in the substitution. We don't want 1919-- k2 to look free in this type! 1920zonkTcTypeAndFV ty 1921 = tyCoVarsOfTypeDSet <$> zonkTcType ty 1922 1923zonkTyCoVar :: TyCoVar -> TcM TcType 1924-- Works on TyVars and TcTyVars 1925zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv 1926 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv 1927 | otherwise = ASSERT2( isCoVar tv, ppr tv ) 1928 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv 1929 -- Hackily, when typechecking type and class decls 1930 -- we have TyVars in scope added (only) in 1931 -- TcHsType.bindTyClTyVars, but it seems 1932 -- painful to make them into TcTyVars there 1933 1934zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet 1935zonkTyCoVarsAndFV tycovars 1936 = tyCoVarsOfTypes <$> mapM zonkTyCoVar (nonDetEltsUniqSet tycovars) 1937 -- It's OK to use nonDetEltsUniqSet here because we immediately forget about 1938 -- the ordering by turning it into a nondeterministic set and the order 1939 -- of zonking doesn't matter for determinism. 1940 1941zonkDTyCoVarSetAndFV :: DTyCoVarSet -> TcM DTyCoVarSet 1942zonkDTyCoVarSetAndFV tycovars 1943 = mkDVarSet <$> (zonkTyCoVarsAndFVList $ dVarSetElems tycovars) 1944 1945-- Takes a list of TyCoVars, zonks them and returns a 1946-- deterministically ordered list of their free variables. 1947zonkTyCoVarsAndFVList :: [TyCoVar] -> TcM [TyCoVar] 1948zonkTyCoVarsAndFVList tycovars 1949 = tyCoVarsOfTypesList <$> mapM zonkTyCoVar tycovars 1950 1951zonkTcTyVars :: [TcTyVar] -> TcM [TcType] 1952zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars 1953 1954----------------- Types 1955zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar 1956zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv) 1957 ; return (setTyVarKind tv kind') } 1958 1959zonkTcTypes :: [TcType] -> TcM [TcType] 1960zonkTcTypes tys = mapM zonkTcType tys 1961 1962{- 1963************************************************************************ 1964* * 1965 Zonking constraints 1966* * 1967************************************************************************ 1968-} 1969 1970zonkImplication :: Implication -> TcM Implication 1971zonkImplication implic@(Implic { ic_skols = skols 1972 , ic_given = given 1973 , ic_wanted = wanted 1974 , ic_info = info }) 1975 = do { skols' <- mapM zonkTyCoVarKind skols -- Need to zonk their kinds! 1976 -- as #7230 showed 1977 ; given' <- mapM zonkEvVar given 1978 ; info' <- zonkSkolemInfo info 1979 ; wanted' <- zonkWCRec wanted 1980 ; return (implic { ic_skols = skols' 1981 , ic_given = given' 1982 , ic_wanted = wanted' 1983 , ic_info = info' }) } 1984 1985zonkEvVar :: EvVar -> TcM EvVar 1986zonkEvVar var = do { ty' <- zonkTcType (varType var) 1987 ; return (setVarType var ty') } 1988 1989 1990zonkWC :: WantedConstraints -> TcM WantedConstraints 1991zonkWC wc = zonkWCRec wc 1992 1993zonkWCRec :: WantedConstraints -> TcM WantedConstraints 1994zonkWCRec (WC { wc_simple = simple, wc_impl = implic }) 1995 = do { simple' <- zonkSimples simple 1996 ; implic' <- mapBagM zonkImplication implic 1997 ; return (WC { wc_simple = simple', wc_impl = implic' }) } 1998 1999zonkSimples :: Cts -> TcM Cts 2000zonkSimples cts = do { cts' <- mapBagM zonkCt cts 2001 ; traceTc "zonkSimples done:" (ppr cts') 2002 ; return cts' } 2003 2004{- Note [zonkCt behaviour] 2005~~~~~~~~~~~~~~~~~~~~~~~~~~ 2006zonkCt tries to maintain the canonical form of a Ct. For example, 2007 - a CDictCan should stay a CDictCan; 2008 - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.). 2009 - a CHoleCan should stay a CHoleCan 2010 - a CIrredCan should stay a CIrredCan with its cc_insol flag intact 2011 2012Why?, for example: 2013- For CDictCan, the @TcSimplify.expandSuperClasses@ step, which runs after the 2014 simple wanted and plugin loop, looks for @CDictCan@s. If a plugin is in use, 2015 constraints are zonked before being passed to the plugin. This means if we 2016 don't preserve a canonical form, @expandSuperClasses@ fails to expand 2017 superclasses. This is what happened in #11525. 2018 2019- For CHoleCan, once we forget that it's a hole, we can never recover that info. 2020 2021- For CIrredCan we want to see if a constraint is insoluble with insolubleWC 2022 2023NB: we do not expect to see any CFunEqCans, because zonkCt is only 2024called on unflattened constraints. 2025 2026NB: Constraints are always re-flattened etc by the canonicaliser in 2027@TcCanonical@ even if they come in as CDictCan. Only canonical constraints that 2028are actually in the inert set carry all the guarantees. So it is okay if zonkCt 2029creates e.g. a CDictCan where the cc_tyars are /not/ function free. 2030-} 2031 2032zonkCt :: Ct -> TcM Ct 2033zonkCt ct@(CHoleCan { cc_ev = ev }) 2034 = do { ev' <- zonkCtEvidence ev 2035 ; return $ ct { cc_ev = ev' } } 2036 2037zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args }) 2038 = do { ev' <- zonkCtEvidence ev 2039 ; args' <- mapM zonkTcType args 2040 ; return $ ct { cc_ev = ev', cc_tyargs = args' } } 2041 2042zonkCt (CTyEqCan { cc_ev = ev }) 2043 = mkNonCanonical <$> zonkCtEvidence ev 2044 -- CTyEqCan has some delicate invariants that may be violated by 2045 -- zonking (documented with the Ct type) , so we don't want to create 2046 -- a CTyEqCan here. Besides, this will be canonicalized again anyway, 2047 -- so there is very little benefit in keeping the CTyEqCan constructor. 2048 2049zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_insol flag 2050 = do { ev' <- zonkCtEvidence ev 2051 ; return (ct { cc_ev = ev' }) } 2052 2053zonkCt ct 2054 = ASSERT( not (isCFunEqCan ct) ) 2055 -- We do not expect to see any CFunEqCans, because zonkCt is only called on 2056 -- unflattened constraints. 2057 do { fl' <- zonkCtEvidence (ctEvidence ct) 2058 ; return (mkNonCanonical fl') } 2059 2060zonkCtEvidence :: CtEvidence -> TcM CtEvidence 2061zonkCtEvidence ctev@(CtGiven { ctev_pred = pred }) 2062 = do { pred' <- zonkTcType pred 2063 ; return (ctev { ctev_pred = pred'}) } 2064zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest }) 2065 = do { pred' <- zonkTcType pred 2066 ; let dest' = case dest of 2067 EvVarDest ev -> EvVarDest $ setVarType ev pred' 2068 -- necessary in simplifyInfer 2069 HoleDest h -> HoleDest h 2070 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) } 2071zonkCtEvidence ctev@(CtDerived { ctev_pred = pred }) 2072 = do { pred' <- zonkTcType pred 2073 ; return (ctev { ctev_pred = pred' }) } 2074 2075zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo 2076zonkSkolemInfo (SigSkol cx ty tv_prs) = do { ty' <- zonkTcType ty 2077 ; return (SigSkol cx ty' tv_prs) } 2078zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys 2079 ; return (InferSkol ntys') } 2080 where 2081 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') } 2082zonkSkolemInfo skol_info = return skol_info 2083 2084{- 2085%************************************************************************ 2086%* * 2087\subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar} 2088* * 2089* For internal use only! * 2090* * 2091************************************************************************ 2092 2093-} 2094 2095-- zonkId is used *during* typechecking just to zonk the Id's type 2096zonkId :: TcId -> TcM TcId 2097zonkId id 2098 = do { ty' <- zonkTcType (idType id) 2099 ; return (Id.setIdType id ty') } 2100 2101zonkCoVar :: CoVar -> TcM CoVar 2102zonkCoVar = zonkId 2103 2104-- | A suitable TyCoMapper for zonking a type during type-checking, 2105-- before all metavars are filled in. 2106zonkTcTypeMapper :: TyCoMapper () TcM 2107zonkTcTypeMapper = TyCoMapper 2108 { tcm_tyvar = const zonkTcTyVar 2109 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv) 2110 , tcm_hole = hole 2111 , tcm_tycobinder = \_env tv _vis -> ((), ) <$> zonkTyCoVarKind tv 2112 , tcm_tycon = zonkTcTyCon } 2113 where 2114 hole :: () -> CoercionHole -> TcM Coercion 2115 hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv }) 2116 = do { contents <- readTcRef ref 2117 ; case contents of 2118 Just co -> do { co' <- zonkCo co 2119 ; checkCoercionHole cv co' } 2120 Nothing -> do { cv' <- zonkCoVar cv 2121 ; return $ HoleCo (hole { ch_co_var = cv' }) } } 2122 2123zonkTcTyCon :: TcTyCon -> TcM TcTyCon 2124-- Only called on TcTyCons 2125-- A non-poly TcTyCon may have unification 2126-- variables that need zonking, but poly ones cannot 2127zonkTcTyCon tc 2128 | tcTyConIsPoly tc = return tc 2129 | otherwise = do { tck' <- zonkTcType (tyConKind tc) 2130 ; return (setTcTyConKind tc tck') } 2131 2132-- For unbound, mutable tyvars, zonkType uses the function given to it 2133-- For tyvars bound at a for-all, zonkType zonks them to an immutable 2134-- type variable and zonks the kind too 2135zonkTcType :: TcType -> TcM TcType 2136zonkTcType = mapType zonkTcTypeMapper () 2137 2138-- | "Zonk" a coercion -- really, just zonk any types in the coercion 2139zonkCo :: Coercion -> TcM Coercion 2140zonkCo = mapCoercion zonkTcTypeMapper () 2141 2142zonkTcTyVar :: TcTyVar -> TcM TcType 2143-- Simply look through all Flexis 2144zonkTcTyVar tv 2145 | isTcTyVar tv 2146 = case tcTyVarDetails tv of 2147 SkolemTv {} -> zonk_kind_and_return 2148 RuntimeUnk {} -> zonk_kind_and_return 2149 MetaTv { mtv_ref = ref } 2150 -> do { cts <- readMutVar ref 2151 ; case cts of 2152 Flexi -> zonk_kind_and_return 2153 Indirect ty -> do { zty <- zonkTcType ty 2154 ; writeTcRef ref (Indirect zty) 2155 -- See Note [Sharing in zonking] 2156 ; return zty } } 2157 2158 | otherwise -- coercion variable 2159 = zonk_kind_and_return 2160 where 2161 zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv 2162 ; return (mkTyVarTy z_tv) } 2163 2164-- Variant that assumes that any result of zonking is still a TyVar. 2165-- Should be used only on skolems and TyVarTvs 2166zonkTcTyVarToTyVar :: HasDebugCallStack => TcTyVar -> TcM TcTyVar 2167zonkTcTyVarToTyVar tv 2168 = do { ty <- zonkTcTyVar tv 2169 ; let tv' = case tcGetTyVar_maybe ty of 2170 Just tv' -> tv' 2171 Nothing -> pprPanic "zonkTcTyVarToTyVar" 2172 (ppr tv $$ ppr ty) 2173 ; return tv' } 2174 2175zonkTyVarTyVarPairs :: [(Name,TcTyVar)] -> TcM [(Name,TcTyVar)] 2176zonkTyVarTyVarPairs prs 2177 = mapM do_one prs 2178 where 2179 do_one (nm, tv) = do { tv' <- zonkTcTyVarToTyVar tv 2180 ; return (nm, tv') } 2181 2182{- Note [Sharing in zonking] 2183~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2184Suppose we have 2185 alpha :-> beta :-> gamma :-> ty 2186where the ":->" means that the unification variable has been 2187filled in with Indirect. Then when zonking alpha, it'd be nice 2188to short-circuit beta too, so we end up with 2189 alpha :-> zty 2190 beta :-> zty 2191 gamma :-> zty 2192where zty is the zonked version of ty. That way, if we come across 2193beta later, we'll have less work to do. (And indeed the same for 2194alpha.) 2195 2196This is easily achieved: just overwrite (Indirect ty) with (Indirect 2197zty). Non-systematic perf comparisons suggest that this is a modest 2198win. 2199 2200But c.f Note [Sharing when zonking to Type] in TcHsSyn. 2201 2202%************************************************************************ 2203%* * 2204 Tidying 2205* * 2206************************************************************************ 2207-} 2208 2209zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType) 2210zonkTidyTcType env ty = do { ty' <- zonkTcType ty 2211 ; return (tidyOpenType env ty') } 2212 2213zonkTidyTcTypes :: TidyEnv -> [TcType] -> TcM (TidyEnv, [TcType]) 2214zonkTidyTcTypes = zonkTidyTcTypes' [] 2215 where zonkTidyTcTypes' zs env [] = return (env, reverse zs) 2216 zonkTidyTcTypes' zs env (ty:tys) 2217 = do { (env', ty') <- zonkTidyTcType env ty 2218 ; zonkTidyTcTypes' (ty':zs) env' tys } 2219 2220zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin) 2221zonkTidyOrigin env (GivenOrigin skol_info) 2222 = do { skol_info1 <- zonkSkolemInfo skol_info 2223 ; let skol_info2 = tidySkolemInfo env skol_info1 2224 ; return (env, GivenOrigin skol_info2) } 2225zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act 2226 , uo_expected = exp }) 2227 = do { (env1, act') <- zonkTidyTcType env act 2228 ; (env2, exp') <- zonkTidyTcType env1 exp 2229 ; return ( env2, orig { uo_actual = act' 2230 , uo_expected = exp' }) } 2231zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k) 2232 = do { (env1, ty1') <- zonkTidyTcType env ty1 2233 ; (env2, m_ty2') <- case m_ty2 of 2234 Just ty2 -> second Just <$> zonkTidyTcType env1 ty2 2235 Nothing -> return (env1, Nothing) 2236 ; (env3, orig') <- zonkTidyOrigin env2 orig 2237 ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) } 2238zonkTidyOrigin env (FunDepOrigin1 p1 o1 l1 p2 o2 l2) 2239 = do { (env1, p1') <- zonkTidyTcType env p1 2240 ; (env2, p2') <- zonkTidyTcType env1 p2 2241 ; return (env2, FunDepOrigin1 p1' o1 l1 p2' o2 l2) } 2242zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2) 2243 = do { (env1, p1') <- zonkTidyTcType env p1 2244 ; (env2, p2') <- zonkTidyTcType env1 p2 2245 ; (env3, o1') <- zonkTidyOrigin env2 o1 2246 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) } 2247zonkTidyOrigin env orig = return (env, orig) 2248 2249---------------- 2250tidyCt :: TidyEnv -> Ct -> Ct 2251-- Used only in error reporting 2252-- Also converts it to non-canonical 2253tidyCt env ct 2254 = case ct of 2255 CHoleCan { cc_ev = ev } 2256 -> ct { cc_ev = tidy_ev env ev } 2257 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct)) 2258 where 2259 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence 2260 -- NB: we do not tidy the ctev_evar field because we don't 2261 -- show it in error messages 2262 tidy_ev env ctev@(CtGiven { ctev_pred = pred }) 2263 = ctev { ctev_pred = tidyType env pred } 2264 tidy_ev env ctev@(CtWanted { ctev_pred = pred }) 2265 = ctev { ctev_pred = tidyType env pred } 2266 tidy_ev env ctev@(CtDerived { ctev_pred = pred }) 2267 = ctev { ctev_pred = tidyType env pred } 2268 2269---------------- 2270tidyEvVar :: TidyEnv -> EvVar -> EvVar 2271tidyEvVar env var = setVarType var (tidyType env (varType var)) 2272 2273---------------- 2274tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo 2275tidySkolemInfo env (DerivSkol ty) = DerivSkol (tidyType env ty) 2276tidySkolemInfo env (SigSkol cx ty tv_prs) = tidySigSkol env cx ty tv_prs 2277tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids) 2278tidySkolemInfo env (UnifyForAllSkol ty) = UnifyForAllSkol (tidyType env ty) 2279tidySkolemInfo _ info = info 2280 2281tidySigSkol :: TidyEnv -> UserTypeCtxt 2282 -> TcType -> [(Name,TcTyVar)] -> SkolemInfo 2283-- We need to take special care when tidying SigSkol 2284-- See Note [SigSkol SkolemInfo] in Origin 2285tidySigSkol env cx ty tv_prs 2286 = SigSkol cx (tidy_ty env ty) tv_prs' 2287 where 2288 tv_prs' = mapSnd (tidyTyCoVarOcc env) tv_prs 2289 inst_env = mkNameEnv tv_prs' 2290 2291 tidy_ty env (ForAllTy (Bndr tv vis) ty) 2292 = ForAllTy (Bndr tv' vis) (tidy_ty env' ty) 2293 where 2294 (env', tv') = tidy_tv_bndr env tv 2295 2296 tidy_ty env ty@(FunTy _ arg res) 2297 = ty { ft_arg = tidyType env arg, ft_res = tidy_ty env res } 2298 2299 tidy_ty env ty = tidyType env ty 2300 2301 tidy_tv_bndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar) 2302 tidy_tv_bndr env@(occ_env, subst) tv 2303 | Just tv' <- lookupNameEnv inst_env (tyVarName tv) 2304 = ((occ_env, extendVarEnv subst tv tv'), tv') 2305 2306 | otherwise 2307 = tidyVarBndr env tv 2308 2309------------------------------------------------------------------------- 2310{- 2311%************************************************************************ 2312%* * 2313 Levity polymorphism checks 2314* * 2315************************************************************************ 2316 2317See Note [Levity polymorphism checking] in DsMonad 2318 2319-} 2320 2321-- | According to the rules around representation polymorphism 2322-- (see https://gitlab.haskell.org/ghc/ghc/wikis/no-sub-kinds), no binder 2323-- can have a representation-polymorphic type. This check ensures 2324-- that we respect this rule. It is a bit regrettable that this error 2325-- occurs in zonking, after which we should have reported all errors. 2326-- But it's hard to see where else to do it, because this can be discovered 2327-- only after all solving is done. And, perhaps most importantly, this 2328-- isn't really a compositional property of a type system, so it's 2329-- not a terrible surprise that the check has to go in an awkward spot. 2330ensureNotLevPoly :: Type -- its zonked type 2331 -> SDoc -- where this happened 2332 -> TcM () 2333ensureNotLevPoly ty doc 2334 = whenNoErrs $ -- sometimes we end up zonking bogus definitions of type 2335 -- forall a. a. See, for example, test ghci/scripts/T9140 2336 checkForLevPoly doc ty 2337 2338 -- See Note [Levity polymorphism checking] in DsMonad 2339checkForLevPoly :: SDoc -> Type -> TcM () 2340checkForLevPoly = checkForLevPolyX addErr 2341 2342checkForLevPolyX :: Monad m 2343 => (SDoc -> m ()) -- how to report an error 2344 -> SDoc -> Type -> m () 2345checkForLevPolyX add_err extra ty 2346 | isTypeLevPoly ty 2347 = add_err (formatLevPolyErr ty $$ extra) 2348 | otherwise 2349 = return () 2350 2351formatLevPolyErr :: Type -- levity-polymorphic type 2352 -> SDoc 2353formatLevPolyErr ty 2354 = hang (text "A levity-polymorphic type is not allowed here:") 2355 2 (vcat [ text "Type:" <+> pprWithTYPE tidy_ty 2356 , text "Kind:" <+> pprWithTYPE tidy_ki ]) 2357 where 2358 (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty 2359 tidy_ki = tidyType tidy_env (tcTypeKind ty) 2360