TcMType.hs 66.3 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3 4
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998

5

6 7 8 9
Monadic type operations

This module contains monadic operations over types that contain
mutable type variables
Austin Seipp's avatar
Austin Seipp committed
10
-}
11

12
{-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
Ian Lynagh's avatar
Ian Lynagh committed
13

14
module TcMType (
15
  TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
16 17 18

  --------------------------------
  -- Creating new mutable type variables
19
  newFlexiTyVar,
20 21
  newFlexiTyVarTy,              -- Kind -> TcM TcType
  newFlexiTyVarTys,             -- Int -> Kind -> TcM [TcType]
22 23
  newOpenFlexiTyVarTy, newOpenTypeKind,
  newMetaKindVar, newMetaKindVars, newMetaTyVarTyAtLevel,
24 25
  cloneMetaTyVar,
  newFmvTyVar, newFskTyVar,
26

27
  readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
28
  newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
29

30 31 32
  --------------------------------
  -- Expected types
  ExpType(..), ExpSigmaType, ExpRhoType,
33 34 35 36
  mkCheckExpType,
  newInferExpType, newInferExpTypeInst, newInferExpTypeNoInst,
  readExpType, readExpType_maybe,
  expTypeToType, checkingExpType_maybe, checkingExpType,
37
  tauifyExpType, inferResultToType,
38

39 40 41 42
  --------------------------------
  -- Creating fresh type variables for pm checking
  genInstSkolTyVarsX,

43
  --------------------------------
44
  -- Creating new evidence variables
45
  newEvVar, newEvVars, newDict,
46
  newWanted, newWanteds, cloneWanted, cloneWC,
47
  emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
48
  newTcEvBinds, addTcEvBind,
49

50 51 52 53
  newCoercionHole, fillCoercionHole, isFilledCoercionHole,
  unpackCoercionHole, unpackCoercionHole_maybe,
  checkCoercionHole,

54 55
  --------------------------------
  -- Instantiation
56
  newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
57 58
  newMetaSigTyVars, newMetaSigTyVarX,
  newSigTyVar, newWildCardX,
59
  tcInstType,
60 61
  tcInstSkolTyVars,tcInstSkolTyVarsX,
  tcInstSuperSkolTyVarsX,
62
  tcSkolDFunType, tcSuperSkolTyVars,
63

64
  instSkolTyCoVars, freshenTyVarBndrs, freshenCoVarBndrsX,
65

66
  --------------------------------
67
  -- Zonking and tidying
68 69
  zonkTidyTcType, zonkTidyOrigin,
  mkTypeErrorThing, mkTypeErrorThingArgs,
70
  tidyEvVar, tidyCt, tidySkolemInfo,
71
  skolemiseRuntimeUnk,
72 73
  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTyVar,
  zonkTyCoVarsAndFV, zonkTcTypeAndFV,
74
  zonkTyCoVarsAndFVList,
75
  zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
76
  zonkQuantifiedTyVar, defaultTyVar,
77
  quantifyTyVars,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
78
  zonkTcTyCoVarBndr, zonkTcTyVarBinder,
79
  zonkTcType, zonkTcTypes, zonkCo,
80
  zonkTyCoVarKind, zonkTcTypeMapper,
81

82
  zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
83

Richard Eisenberg's avatar
Richard Eisenberg committed
84 85 86 87 88
  tcGetGlobalTyCoVars,

  ------------------------------
  -- Levity polymorphism
  ensureNotLevPoly, checkForLevPoly, checkForLevPolyX, formatLevPolyErr
89 90 91 92 93
  ) where

#include "HsVersions.h"

-- friends:
94
import TyCoRep
95 96
import TcType
import Type
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
97
import Kind
98
import Coercion
99 100
import Class
import Var
101 102

-- others:
103
import TcRnMonad        -- TcType, amongst others
104
import TcEvidence
105
import Id
106
import Name
107
import VarSet
108 109 110
import TysWiredIn
import TysPrim
import VarEnv
111
import NameEnv
112
import PrelNames
113
import Util
114
import Outputable
115
import FastString
Simon Peyton Jones's avatar
Simon Peyton Jones committed
116
import SrcLoc
117
import Bag
118
import Pair
David Feuer's avatar
David Feuer committed
119
import UniqSet
120
import qualified GHC.LanguageExtensions as LangExt
121

Ian Lynagh's avatar
Ian Lynagh committed
122
import Control.Monad
123
import Maybes
124
import Data.List        ( mapAccumL )
125
import Control.Arrow    ( second )
126

Austin Seipp's avatar
Austin Seipp committed
127 128 129
{-
************************************************************************
*                                                                      *
130
        Kind variables
Austin Seipp's avatar
Austin Seipp committed
131 132 133
*                                                                      *
************************************************************************
-}
134

135 136 137
mkKindName :: Unique -> Name
mkKindName unique = mkSystemName unique kind_var_occ

138 139
kind_var_occ :: OccName -- Just one for all MetaKindVars
                        -- They may be jiggled by tidying
140 141
kind_var_occ = mkOccName tvName "k"

dreixel's avatar
dreixel committed
142
newMetaKindVar :: TcM TcKind
143
newMetaKindVar = do { uniq <- newUnique
144
                    ; details <- newMetaDetails TauTv
145
                    ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
146
                    ; return (mkTyVarTy kv) }
147

dreixel's avatar
dreixel committed
148 149
newMetaKindVars :: Int -> TcM [TcKind]
newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
150

Austin Seipp's avatar
Austin Seipp committed
151 152 153
{-
************************************************************************
*                                                                      *
154
     Evidence variables; range over constraints we can abstract over
Austin Seipp's avatar
Austin Seipp committed
155 156 157
*                                                                      *
************************************************************************
-}
158

159 160 161
newEvVars :: TcThetaType -> TcM [EvVar]
newEvVars theta = mapM newEvVar theta

162
--------------
batterseapower's avatar
batterseapower committed
163

164
newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
165
-- Creates new *rigid* variables for predicates
166
newEvVar ty = do { name <- newSysName (predTypeOccName ty)
167 168 169
                 ; return (mkLocalIdOrCoVar name ty) }

newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
170
-- Deals with both equality and non-equality predicates
171 172 173 174 175 176
newWanted orig t_or_k pty
  = do loc <- getCtLocM orig t_or_k
       d <- if isEqPred pty then HoleDest  <$> newCoercionHole
                            else EvVarDest <$> newEvVar pty
       return $ CtWanted { ctev_dest = d
                         , ctev_pred = pty
177
                         , ctev_nosh = WDeriv
178 179 180 181 182
                         , ctev_loc = loc }

newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
newWanteds orig = mapM (newWanted orig Nothing)

183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200
cloneWanted :: Ct -> TcM CtEvidence
cloneWanted ct
  = newWanted (ctEvOrigin ev) Nothing (ctEvPred ev)
  where
    ev = ctEvidence ct

cloneWC :: WantedConstraints -> TcM WantedConstraints
cloneWC wc@(WC { wc_simple = simples, wc_impl = implics })
  = do { simples' <- mapBagM clone_one simples
       ; implics' <- mapBagM clone_implic implics
       ; return (wc { wc_simple = simples', wc_impl = implics' }) }
  where
    clone_one ct = do { ev <- cloneWanted ct; return (mkNonCanonical ev) }

    clone_implic implic@(Implic { ic_wanted = inner_wanted })
      = do { inner_wanted' <- cloneWC inner_wanted
           ; return (implic { ic_wanted = inner_wanted' }) }

201 202 203 204 205 206 207 208 209 210 211 212 213
-- | Emits a new Wanted. Deals with both equalities and non-equalities.
emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
emitWanted origin pty
  = do { ev <- newWanted origin Nothing pty
       ; emitSimple $ mkNonCanonical ev
       ; return $ ctEvTerm ev }

-- | Emits a new equality constraint
emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
emitWantedEq origin t_or_k role ty1 ty2
  = do { hole <- newCoercionHole
       ; loc <- getCtLocM origin (Just t_or_k)
       ; emitSimple $ mkNonCanonical $
214 215
         CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
                  , ctev_nosh = WDeriv, ctev_loc = loc }
216 217 218 219 220 221 222 223 224 225 226 227
       ; return (mkHoleCo hole role ty1 ty2) }
  where
    pty = mkPrimEqPredRole role ty1 ty2

-- | Creates a new EvVar and immediately emits it as a Wanted.
-- No equality predicates here.
emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
emitWantedEvVar origin ty
  = do { new_cv <- newEvVar ty
       ; loc <- getCtLocM origin Nothing
       ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
                             , ctev_pred = ty
228
                             , ctev_nosh = WDeriv
229 230 231 232 233 234
                             , ctev_loc  = loc }
       ; emitSimple $ mkNonCanonical ctev
       ; return new_cv }

emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
emitWantedEvVars orig = mapM (emitWantedEvVar orig)
235 236

newDict :: Class -> [TcType] -> TcM DictId
237
newDict cls tys
238
  = do { name <- newSysName (mkDictOcc (getOccName cls))
batterseapower's avatar
batterseapower committed
239 240 241
       ; return (mkLocalId name (mkClassPred cls tys)) }

predTypeOccName :: PredType -> OccName
242
predTypeOccName ty = case classifyPredType ty of
batterseapower's avatar
batterseapower committed
243
    ClassPred cls _ -> mkDictOcc (getOccName cls)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
244
    EqPred _ _ _    -> mkVarOccFS (fsLit "cobox")
batterseapower's avatar
batterseapower committed
245
    IrredPred _     -> mkVarOccFS (fsLit "irred")
246

247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265
{-
************************************************************************
*                                                                      *
        Coercion holes
*                                                                      *
************************************************************************
-}

newCoercionHole :: TcM CoercionHole
newCoercionHole
  = do { u <- newUnique
       ; traceTc "New coercion hole:" (ppr u)
       ; ref <- newMutVar Nothing
       ; return $ CoercionHole u ref }

-- | Put a value in a coercion hole
fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
fillCoercionHole (CoercionHole u ref) co
  = do {
Ben Gamari's avatar
Ben Gamari committed
266
#if defined(DEBUG)
267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
       ; cts <- readTcRef ref
       ; whenIsJust cts $ \old_co ->
         pprPanic "Filling a filled coercion hole" (ppr u $$ ppr co $$ ppr old_co)
#endif
       ; traceTc "Filling coercion hole" (ppr u <+> text ":=" <+> ppr co)
       ; writeTcRef ref (Just co) }

-- | Is a coercion hole filled in?
isFilledCoercionHole :: CoercionHole -> TcM Bool
isFilledCoercionHole (CoercionHole _ ref) = isJust <$> readTcRef ref

-- | Retrieve the contents of a coercion hole. Panics if the hole
-- is unfilled
unpackCoercionHole :: CoercionHole -> TcM Coercion
unpackCoercionHole hole
  = do { contents <- unpackCoercionHole_maybe hole
       ; case contents of
           Just co -> return co
           Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }

-- | Retrieve the contents of a coercion hole, if it is filled
unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
unpackCoercionHole_maybe (CoercionHole _ ref) = readTcRef ref

-- | Check that a coercion is appropriate for filling a hole. (The hole
-- itself is needed only for printing. NB: This must be /lazy/ in the coercion,
-- as it's used in TcHsSyn in the presence of knots.
-- Always returns the checked coercion, but this return value is necessary
-- so that the input coercion is forced only when the output is forced.
checkCoercionHole :: Coercion -> CoercionHole -> Role -> Type -> Type -> TcM Coercion
checkCoercionHole co h r t1 t2
-- co is already zonked, but t1 and t2 might not be
  | debugIsOn
  = do { t1 <- zonkTcType t1
       ; t2 <- zonkTcType t2
       ; let (Pair _t1 _t2, _role) = coercionKindRole co
       ; return $
         ASSERT2( t1 `eqType` _t1 && t2 `eqType` _t2 && r == _role
                , (text "Bad coercion hole" <+>
                   ppr h <> colon <+> vcat [ ppr _t1, ppr _t2, ppr _role
                                           , ppr co, ppr t1, ppr t2
                                           , ppr r ]) )
         co }
  | otherwise
  = return co

313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364
{-
************************************************************************
*
    Expected types
*
************************************************************************

Note [ExpType]
~~~~~~~~~~~~~~

An ExpType is used as the "expected type" when type-checking an expression.
An ExpType can hold a "hole" that can be filled in by the type-checker.
This allows us to have one tcExpr that works in both checking mode and
synthesis mode (that is, bidirectional type-checking). Previously, this
was achieved by using ordinary unification variables, but we don't need
or want that generality. (For example, #11397 was caused by doing the
wrong thing with unification variables.) Instead, we observe that these
holes should

1. never be nested
2. never appear as the type of a variable
3. be used linearly (never be duplicated)

By defining ExpType, separately from Type, we can achieve goals 1 and 2
statically.

See also [wiki:Typechecking]

Note [TcLevel of ExpType]
~~~~~~~~~~~~~~~~~~~~~~~~~
Consider

  data G a where
    MkG :: G Bool

  foo MkG = True

This is a classic untouchable-variable / ambiguous GADT return type
scenario. But, with ExpTypes, we'll be inferring the type of the RHS.
And, because there is only one branch of the case, we won't trigger
Note [Case branches must never infer a non-tau type] of TcMatches.
We thus must track a TcLevel in an Inferring ExpType. If we try to
fill the ExpType and find that the TcLevels don't work out, we
fill the ExpType with a tau-tv at the low TcLevel, hopefully to
be worked out later by some means. This is triggered in
test gadt/gadt-escape1.

-}

-- actual data definition is in TcType

-- | Make an 'ExpType' suitable for inferring a type of kind * or #.
365 366 367 368 369 370 371 372
newInferExpTypeNoInst :: TcM ExpSigmaType
newInferExpTypeNoInst = newInferExpType False

newInferExpTypeInst :: TcM ExpRhoType
newInferExpTypeInst = newInferExpType True

newInferExpType :: Bool -> TcM ExpType
newInferExpType inst
373
  = do { u <- newUnique
374
       ; tclvl <- getTcLevel
375
       ; traceTc "newOpenInferExpType" (ppr u <+> ppr inst <+> ppr tclvl)
376
       ; ref <- newMutVar Nothing
377
       ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
378
                           , ir_ref = ref, ir_inst = inst })) }
379 380 381 382

-- | Extract a type out of an ExpType, if one exists. But one should always
-- exist. Unless you're quite sure you know what you're doing.
readExpType_maybe :: ExpType -> TcM (Maybe TcType)
383 384
readExpType_maybe (Check ty)                   = return (Just ty)
readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404

-- | Extract a type out of an ExpType. Otherwise, panics.
readExpType :: ExpType -> TcM TcType
readExpType exp_ty
  = do { mb_ty <- readExpType_maybe exp_ty
       ; case mb_ty of
           Just ty -> return ty
           Nothing -> pprPanic "Unknown expected type" (ppr exp_ty) }

-- | Returns the expected type when in checking mode.
checkingExpType_maybe :: ExpType -> Maybe TcType
checkingExpType_maybe (Check ty) = Just ty
checkingExpType_maybe _          = Nothing

-- | Returns the expected type when in checking mode. Panics if in inference
-- mode.
checkingExpType :: String -> ExpType -> TcType
checkingExpType _   (Check ty) = ty
checkingExpType err et         = pprPanic "checkingExpType" (text err $$ ppr et)

405 406
tauifyExpType :: ExpType -> TcM ExpType
-- ^ Turn a (Infer hole) type into a (Check alpha),
407
-- where alpha is a fresh unification variable
408 409 410
tauifyExpType (Check ty)      = return (Check ty)  -- No-op for (Check ty)
tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
                                   ; return (Check ty) }
411

412 413 414
-- | Extracts the expected type if there is one, or generates a new
-- TauTv if there isn't.
expTypeToType :: ExpType -> TcM TcType
415 416 417 418 419
expTypeToType (Check ty)      = return ty
expTypeToType (Infer inf_res) = inferResultToType inf_res

inferResultToType :: InferResult -> TcM Type
inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
420 421 422
                      , ir_ref = ref })
  = do { rr  <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
       ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
423
             -- See Note [TcLevel of ExpType]
424 425
       ; writeMutVar ref (Just tau)
       ; traceTc "Forcing ExpType to be monomorphic:"
426
                 (ppr u <+> text ":=" <+> ppr tau)
427
       ; return tau }
428

429

430
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
431
*                                                                      *
432
        SkolemTvs (immutable)
Austin Seipp's avatar
Austin Seipp committed
433
*                                                                      *
434
********************************************************************* -}
435

436 437
tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
                   -- ^ How to instantiate the type variables
438 439
           -> Id                                            -- ^ Type to instantiate
           -> TcM ([(Name, TcTyVar)], TcThetaType, TcType)  -- ^ Result
440
                -- (type vars, preds (incl equalities), rho)
441 442
tcInstType inst_tyvars id
  = case tcSplitForAllTys (idType id) of
443
        ([],    rho) -> let     -- There may be overloading despite no type variables;
444
                                --      (?x :: Int) => Int -> Int
445 446 447
                                (theta, tau) = tcSplitPhiTy rho
                            in
                            return ([], theta, tau)
448

449
        (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
450
                            ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
451 452
                                  tv_prs       = map tyVarName tyvars `zip` tyvars'
                            ; return (tv_prs, theta, tau) }
453

454
tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
455 456
-- Instantiate a type signature with skolem constants.
-- We could give them fresh names, but no need to do so
457 458 459
tcSkolDFunType dfun
  = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
       ; return (map snd tv_prs, theta, tau) }
460

461
tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
462
-- Make skolem constants, but do *not* give them new names, as above
463
-- Moreover, make them "super skolems"; see comments with superSkolemTv
dreixel's avatar
dreixel committed
464
-- see Note [Kind substitution when instantiating]
465
-- Precondition: tyvars should be ordered by scoping
466
tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
467

468
tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
469
tcSuperSkolTyVar subst tv
470
  = (extendTvSubstWithClone subst tv new_tv, new_tv)
dreixel's avatar
dreixel committed
471
  where
472
    kind   = substTyUnchecked subst (tyVarKind tv)
473 474
    new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv

475 476 477 478 479 480
-- | Given a list of @['TyVar']@, skolemize the type variables,
-- returning a substitution mapping the original tyvars to the
-- skolems, and the list of newly bound skolems.  See also
-- tcInstSkolTyVars' for a precondition.  The resulting
-- skolems are non-overlappable; see Note [Overlap and deriving]
-- for an example where this matters.
481
tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
482 483 484 485
tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst

tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSkolTyVarsX = tcInstSkolTyVars' False
dreixel's avatar
dreixel committed
486

487 488 489 490
tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst

tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
491
tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
492

493
tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
494 495
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
496
-- Get the location from the monad; this is a complete freshening operation
497
tcInstSkolTyVars' overlappable subst tvs
498
  = do { loc <- getSrcSpanM
499 500
       ; lvl <- getTcLevel
       ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
501

502 503 504 505 506 507 508
mkTcSkolTyVar :: TcLevel -> SrcSpan -> Bool -> TcTyVarMaker
mkTcSkolTyVar lvl loc overlappable
  = \ uniq old_name kind -> mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
                                      kind details
  where
    details = SkolemTv (pushTcLevel lvl) overlappable
              -- NB: skolems bump the level
509

510
------------------
511
freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
512 513 514
-- ^ Give fresh uniques to a bunch of TyVars, but they stay
--   as TyVars, rather than becoming TcTyVars
-- Used in FamInst.newFamInst, and Inst.newClsInst
515
freshenTyVarBndrs = instSkolTyCoVars mk_tv
516 517
  where
    mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
518

519 520 521 522 523 524 525
freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
-- ^ Give fresh uniques to a bunch of CoVars
-- Used in FamInst.newFamInst
freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
  where
    mk_cv uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind

526
------------------
527 528
type TcTyVarMaker = Unique -> Name -> Kind -> TyCoVar
instSkolTyCoVars :: TcTyVarMaker -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
529
instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
530

531
instSkolTyCoVarsX :: TcTyVarMaker
532 533
                  -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
534

535
instSkolTyCoVarX :: TcTyVarMaker
536 537
                 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
instSkolTyCoVarX mk_tcv subst tycovar
538 539
  = do  { uniq <- newUnique  -- using a new unique is critical. See
                             -- Note [Skolems in zonkSyntaxExpr] in TcHsSyn
540 541 542 543 544 545
        ; let new_tcv = mk_tcv uniq old_name kind
              subst1 | isTyVar new_tcv
                     = extendTvSubstWithClone subst tycovar new_tcv
                     | otherwise
                     = extendCvSubstWithClone subst tycovar new_tcv
        ; return (subst1, new_tcv) }
546
  where
547
    old_name = tyVarName tycovar
548
    kind     = substTyUnchecked subst (tyVarKind tycovar)
549

550 551 552 553 554
newFskTyVar :: TcType -> TcM TcTyVar
newFskTyVar fam_ty
  = do { uniq <- newUnique
       ; let name = mkSysTvName uniq (fsLit "fsk")
       ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
Austin Seipp's avatar
Austin Seipp committed
555
{-
dreixel's avatar
dreixel committed
556 557 558
Note [Kind substitution when instantiating]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we instantiate a bunch of kind and type variables, first we
559
expect them to be topologically sorted.
dreixel's avatar
dreixel committed
560 561 562 563 564
Then we have to instantiate the kind variables, build a substitution
from old variables to the new variables, then instantiate the type
variables substituting the original kind.

Exemple: If we want to instantiate
565
  [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
dreixel's avatar
dreixel committed
566
we want
567
  [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
dreixel's avatar
dreixel committed
568
instead of the buggous
569
  [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
dreixel's avatar
dreixel committed
570

571

Austin Seipp's avatar
Austin Seipp committed
572 573
************************************************************************
*                                                                      *
574
        MetaTvs (meta type variables; mutable)
Austin Seipp's avatar
Austin Seipp committed
575 576 577
*                                                                      *
************************************************************************
-}
578

579 580 581 582 583 584
mkMetaTyVarName :: Unique -> FastString -> Name
-- Makes a /System/ Name, which is eagerly eliminated by
-- the unifier; see TcUnify.nicer_to_update_tv1, and
-- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
mkMetaTyVarName uniq str = mkSysTvName uniq str

585 586
newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
Jan Stolarek's avatar
Jan Stolarek committed
587
  = do { details <- newMetaDetails SigTv
588
       ; return (mkTcTyVar name kind details) }
589

590 591 592 593 594 595 596 597 598 599 600 601 602
newFmvTyVar :: TcType -> TcM TcTyVar
-- Very like newMetaTyVar, except sets mtv_tclvl to one less
-- so that the fmv is untouchable.
newFmvTyVar fam_ty
  = do { uniq <- newUnique
       ; ref  <- newMutVar Flexi
       ; cur_lvl <- getTcLevel
       ; let details = MetaTv { mtv_info  = FlatMetaTv
                              , mtv_ref   = ref
                              , mtv_tclvl = fmvTcLevel cur_lvl }
             name = mkMetaTyVarName uniq (fsLit "s")
       ; return (mkTcTyVar name (typeKind fam_ty) details) }

603 604 605
newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails info
  = do { ref <- newMutVar Flexi
606
       ; tclvl <- getTcLevel
607 608 609
       ; return (MetaTv { mtv_info = info
                        , mtv_ref = ref
                        , mtv_tclvl = tclvl }) }
610

611 612 613
cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
cloneMetaTyVar tv
  = ASSERT( isTcTyVar tv )
614
    do  { uniq <- newUnique
615 616
        ; ref  <- newMutVar Flexi
        ; let name'    = setNameUnique (tyVarName tv) uniq
617
              details' = case tcTyVarDetails tv of
618 619 620 621
                           details@(MetaTv {}) -> details { mtv_ref = ref }
                           _ -> pprPanic "cloneMetaTyVar" (ppr tv)
        ; return (mkTcTyVar name' (tyVarKind tv) details') }

dreixel's avatar
dreixel committed
622
-- Works for both type and kind variables
623 624
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
625
                      readMutVar (metaTyVarRef tyvar)
626

627 628 629
isFilledMetaTyVar :: TyVar -> TcM Bool
-- True of a filled-in (Indirect) meta type variable
isFilledMetaTyVar tv
630
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
631 632
  = do  { details <- readMutVar ref
        ; return (isIndirect details) }
633 634
  | otherwise = return False

635
isUnfilledMetaTyVar :: TyVar -> TcM Bool
636
-- True of a un-filled-in (Flexi) meta type variable
637
isUnfilledMetaTyVar tv
638
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
639 640
  = do  { details <- readMutVar ref
        ; return (isFlexi details) }
641 642 643
  | otherwise = return False

--------------------
dreixel's avatar
dreixel committed
644
-- Works with both type and kind variables
645
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
646 647
-- Write into a currently-empty MetaTyVar

Ian Lynagh's avatar
Ian Lynagh committed
648
writeMetaTyVar tyvar ty
649
  | not debugIsOn
650
  = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
651 652 653 654 655 656

-- Everything from here on only happens if DEBUG is on
  | not (isTcTyVar tyvar)
  = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
    return ()

657
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
658 659 660 661
  = writeMetaTyVarRef tyvar ref ty

  | otherwise
  = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
662
    return ()
663 664 665

--------------------
writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
666
-- Here the tyvar is for error checking only;
667 668
-- the ref cell must be for the same tyvar
writeMetaTyVarRef tyvar ref ty
669
  | not debugIsOn
670 671 672
  = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
                                   <+> text ":=" <+> ppr ty)
       ; writeTcRef ref (Indirect ty) }
673

674
  -- Everything from here on only happens if DEBUG is on
675
  | otherwise
676
  = do { meta_details <- readMutVar ref;
dreixel's avatar
dreixel committed
677
       -- Zonk kinds to allow the error check to work
678 679
       ; zonked_tv_kind <- zonkTcType tv_kind
       ; zonked_ty_kind <- zonkTcType ty_kind
680 681 682 683 684 685 686 687 688 689
       ; let kind_check_ok = isPredTy tv_kind  -- Don't check kinds for updates
                                               -- to coercion variables
                          || tcEqKind zonked_ty_kind zonked_tv_kind

             kind_msg = hang (text "Ill-kinded update to meta tyvar")
                           2 (    ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
                              <+> text ":="
                              <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) )

       ; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
dreixel's avatar
dreixel committed
690 691

       -- Check for double updates
692 693 694 695 696 697 698 699 700 701 702
       ; MASSERT2( isFlexi meta_details, double_upd_msg meta_details )

       -- Check for level OK
       -- See Note [Level check when unifying]
       ; MASSERT2( level_check_ok, level_check_msg )

       -- Check Kinds ok
       ; MASSERT2( kind_check_ok, kind_msg )

       -- Do the write
       ; writeMutVar ref (Indirect ty) }
703 704 705
  where
    tv_kind = tyVarKind tyvar
    ty_kind = typeKind ty
706

707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728
    tv_lvl = tcTyVarLevel tyvar
    ty_lvl = tcTypeLevel ty

    level_check_ok = isFmvTyVar tyvar
                  || not (ty_lvl `strictlyDeeperThan` tv_lvl)
    level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty

    double_upd_msg details = hang (text "Double update of meta tyvar")
                                2 (ppr tyvar $$ ppr details)


{- Note [Level check when unifying]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When unifying
     alpha:lvl := ty
we expect that the TcLevel of 'ty' will be <= lvl.
However, during unflatting we do
     fuv:l := ty:(l+1)
which is usually wrong; hence the check isFmmvTyVar in level_check_ok.
See Note [TcLevel assignment] in TcType.
-}

729 730 731 732
{-
% Generating fresh variables for pattern match check
-}

733 734 735 736
-- UNINSTANTIATED VERSION OF tcInstSkolTyCoVars
genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
                   -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
-- Precondition: tyvars should be scoping-ordered
737 738
-- see Note [Kind substitution when instantiating]
-- Get the location from the monad; this is a complete freshening operation
739 740
genInstSkolTyVarsX loc subst tvs
  = instSkolTyCoVarsX (mkTcSkolTyVar topTcLevel loc False) subst tvs
741

Austin Seipp's avatar
Austin Seipp committed
742 743 744
{-
************************************************************************
*                                                                      *
745
        MetaTvs: TauTvs
Austin Seipp's avatar
Austin Seipp committed
746 747
*                                                                      *
************************************************************************
748 749 750 751 752 753 754 755 756 757 758 759 760

Note [Never need to instantiate coercion variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
With coercion variables sloshing around in types, it might seem that we
sometimes need to instantiate coercion variables. This would be problematic,
because coercion variables inhabit unboxed equality (~#), and the constraint
solver thinks in terms only of boxed equality (~). The solution is that
we never need to instantiate coercion variables in the first place.

The tyvars that we need to instantiate come from the types of functions,
data constructors, and patterns. These will never be quantified over
coercion variables, except for the special case of the promoted Eq#. But,
that can't ever appear in user code, so we're safe!
Austin Seipp's avatar
Austin Seipp committed
761
-}
762

763 764 765 766 767 768 769 770 771 772 773 774
newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
-- Make a new meta tyvar out of thin air
newAnonMetaTyVar meta_info kind
  = do  { uniq <- newUnique
        ; let name = mkMetaTyVarName uniq s
              s = case meta_info of
                        TauTv       -> fsLit "t"
                        FlatMetaTv  -> fsLit "fmv"
                        SigTv       -> fsLit "a"
        ; details <- newMetaDetails meta_info
        ; return (mkTcTyVar name kind details) }

775
newFlexiTyVar :: Kind -> TcM TcTyVar
776
newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
777

778
newFlexiTyVarTy :: Kind -> TcM TcType
779 780
newFlexiTyVarTy kind = do
    tc_tyvar <- newFlexiTyVar kind
781
    return (mkTyVarTy tc_tyvar)
782 783

newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
784
newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
785

786 787 788 789 790
newOpenTypeKind :: TcM TcKind
newOpenTypeKind
  = do { rr <- newFlexiTyVarTy runtimeRepTy
       ; return (tYPE rr) }

791
-- | Create a tyvar that can be a lifted or unlifted type.
792
-- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
793 794
newOpenFlexiTyVarTy :: TcM TcType
newOpenFlexiTyVarTy
795 796
  = do { kind <- newOpenTypeKind
       ; newFlexiTyVarTy kind }
797

798 799 800 801
newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst

newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
802
-- Instantiate with META type variables
803 804 805
-- Note that this works for a sequence of kind, type, and coercion variables
-- variables.  Eg    [ (k:*), (a:k->k) ]
--             Gives [ (k7:*), (a8:k7->k7) ]
806
newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
807
    -- emptyTCvSubst has an empty in-scope set, but that's fine here
dreixel's avatar
dreixel committed
808 809 810
    -- Since the tyvars are freshly made, they cannot possibly be
    -- captured by any existing for-alls.

811
newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
dreixel's avatar
dreixel committed
812 813
-- Make a new unification variable tyvar whose Name and Kind come from
-- an existing TyVar. We substitute kind variables in the kind.
814
newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
815

816 817 818 819
newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- Just like newMetaTyVars, but start with an existing substitution.
newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst

820 821
newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-- Just like newMetaTyVarX, but make a SigTv
822 823
newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar

824 825 826 827 828
newWildCardX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
newWildCardX subst tv
  = do { new_tv <- newAnonMetaTyVar TauTv (substTy subst (tyVarKind tv))
       ; return (extendTvSubstWithClone subst tv new_tv, new_tv) }

829
new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
830
new_meta_tv_x info subst tv
831
  = do  { uniq <- newUnique
832
        ; details <- newMetaDetails info
833
        ; let name   = mkSystemName uniq (getOccName tv)
834
                       -- See Note [Name of an instantiated type variable]
835
              kind   = substTyUnchecked subst (tyVarKind tv)
836 837 838 839
                       -- NOTE: Trac #12549 is fixed so we could use
                       -- substTy here, but the tc_infer_args problem
                       -- is not yet fixed so leaving as unchecked for now.
                       -- OLD NOTE:
840 841 842 843 844
                       -- Unchecked because we call newMetaTyVarX from
                       -- tcInstBinderX, which is called from tc_infer_args
                       -- which does not yet take enough trouble to ensure
                       -- the in-scope set is right; e.g. Trac #12785 trips
                       -- if we use substTy here
845
              new_tv = mkTcTyVar name kind details
846
              subst1 = extendTvSubstWithClone subst tv new_tv
847
        ; return (subst1, new_tv) }
848

849 850
newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
newMetaTyVarTyAtLevel tc_lvl kind
851 852 853 854 855 856
  = do  { uniq <- newUnique
        ; ref  <- newMutVar Flexi
        ; let name = mkMetaTyVarName uniq (fsLit "p")
              details = MetaTv { mtv_info  = TauTv
                               , mtv_ref   = ref
                               , mtv_tclvl = tc_lvl }
857
        ; return (mkTyVarTy (mkTcTyVar name kind details)) }
858

Simon Peyton Jones's avatar
Simon Peyton Jones committed
859 860 861 862 863
{- Note [Name of an instantiated type variable]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At the moment we give a unification variable a System Name, which
influences the way it is tidied; see TypeRep.tidyTyVarBndr.

Austin Seipp's avatar
Austin Seipp committed
864 865
************************************************************************
*                                                                      *
866
             Quantification
Austin Seipp's avatar
Austin Seipp committed
867 868
*                                                                      *
************************************************************************
869

870 871
Note [quantifyTyVars]
~~~~~~~~~~~~~~~~~~~~~
872
quantifyTyVars is given the free vars of a type that we
873
are about to wrap in a forall.
874

875 876 877 878 879
It takes these free type/kind variables (partitioned into dependent and
non-dependent variables) and
  1. Zonks them and remove globals and covars
  2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
  3. Calls zonkQuantifiedTyVar on each
880

881
Step (2) is often unimportant, because the kind variable is often
882 883 884 885 886
also free in the type.  Eg
     Typeable k (a::k)
has free vars {k,a}.  But the type (see Trac #7916)
    (f::k->*) (a::k)
has free vars {f,a}, but we must add 'k' as well! Hence step (3).
887

888 889 890
* This function distinguishes between dependent and non-dependent
  variables only to keep correct defaulting behavior with -XNoPolyKinds.
  With -XPolyKinds, it treats both classes of variables identically.
891

892 893 894
* quantifyTyVars never quantifies over
    - a coercion variable
    - a runtime-rep variable
895 896 897 898 899 900 901 902

Note [quantifyTyVars determinism]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The results of quantifyTyVars are wrapped in a forall and can end up in the
interface file. One such example is inferred type signatures. They also affect
the results of optimizations, for example worker-wrapper. This means that to
get deterministic builds quantifyTyVars needs to be deterministic.

903
To achieve this CandidatesQTvs is backed by deterministic sets which allows them
904 905 906 907
to be later converted to a list in a deterministic order.

For more information about deterministic sets see
Note [Deterministic UniqFM] in UniqDFM.
Austin Seipp's avatar
Austin Seipp committed
908
-}
909

910 911
quantifyTyVars
  :: TcTyCoVarSet     -- Global tvs; already zonked
912
  -> CandidatesQTvs   -- See Note [Dependent type variables] in TcType
913
                      -- Already zonked
914
  -> TcM [TcTyVar]
915
-- See Note [quantifyTyVars]
916
-- Can be given a mixture of TcTyVars and TyVars, in the case of
917 918
--   associated type declarations. Also accepts covars, but *never* returns any.

919 920
quantifyTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
  = do { traceTc "quantifyTyVars" (vcat [ppr dvs, ppr gbl_tvs])
921
       ; let all_cvs = filterVarSet isCoVar $ dVarSetToVarSet dep_tkvs
922 923 924 925
             dep_kvs = dVarSetElemsWellScoped $
                       dep_tkvs `dVarSetMinusVarSet` gbl_tvs
                                `dVarSetMinusVarSet` closeOverKinds all_cvs
                 -- dVarSetElemsWellScoped: put the kind variables into
926 927 928 929 930
                 --    well-scoped order.
                 --    E.g.  [k, (a::k)] not the other way roud
                 -- closeOverKinds all_cvs: do not quantify over coercion
                 --    variables, or any any tvs that a covar depends on

931
             nondep_tvs = dVarSetElems $
932 933 934 935 936 937 938 939 940
                          (nondep_tkvs `minusDVarSet` dep_tkvs)
                           `dVarSetMinusVarSet` gbl_tvs
                 -- See Note [Dependent type variables] in TcType
                 -- The `minus` dep_tkvs removes any kind-level vars
                 --    e.g. T k (a::k)   Since k appear in a kind it'll
                 --    be in dv_kvs, and is dependent. So remove it from
                 --    dv_tvs which will also contain k
                 -- No worry about dependent covars here;
                 --    they are all in dep_tkvs
Gabor Greif's avatar
Gabor Greif committed
941
                 -- No worry about scoping, because these are all
942 943
                 --    type variables
                 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
944

dreixel's avatar
dreixel committed
945 946
             -- In the non-PolyKinds case, default the kind variables
             -- to *, and zonk the tyvars as usual.  Notice that this
947
             -- may make quantifyTyVars return a shorter list
dreixel's avatar
dreixel committed
948
             -- than it was passed, but that's ok
949 950 951 952 953 954
       ; poly_kinds  <- xoptM LangExt.PolyKinds
       ; dep_kvs'    <- mapMaybeM (zonk_quant (not poly_kinds)) dep_kvs
       ; nondep_tvs' <- mapMaybeM (zonk_quant False)            nondep_tvs
           -- Because of the order, any kind variables
           -- mentioned in the kinds of the nondep_tvs'
           -- now refer to the dep_kvs'
955

956
       ; traceTc "quantifyTyVars"
957
           (vcat [ text "globals:" <+> ppr gbl_tvs
958 959 960 961
                 , text "nondep:"  <+> pprTyVars nondep_tvs
                 , text "dep:"     <+> pprTyVars dep_kvs
                 , text "dep_kvs'" <+> pprTyVars dep_kvs'
                 , text "nondep_tvs'" <+> pprTyVars nondep_tvs' ])
962

963
       ; return (dep_kvs' ++ nondep_tvs') }
964
  where
965 966 967