TcMType.hs 60.6 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 46 47
  newEvVar, newEvVars, newDict,
  newWanted, newWanteds,
  emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
48
  newTcEvBinds, addTcEvBind,
49

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

54 55
  --------------------------------
  -- Instantiation
56 57 58
  newMetaTyVars, newMetaTyVarX,
  newMetaSigTyVars, newMetaSigTyVarX,
  newSigTyVar, newWildCardX,
59
  tcInstType,
60 61
  tcInstSkolTyVars, tcInstSuperSkolTyVarsX,
  tcInstSigTyVars,
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
  skolemiseUnboundMetaTyVar, skolemiseRuntimeUnk,
72 73
  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTyVar,
  zonkTyCoVarsAndFV, zonkTcTypeAndFV,
74
  zonkTyCoVarsAndFVList,
75
  zonkTcTypeAndSplitDepVars, zonkTcTypesAndSplitDepVars,
76
  zonkQuantifiedTyVar,
77
  quantifyTyVars, quantifyZonkedTyVars,
78 79
  zonkTcTyCoVarBndr, zonkTcTyBinder, zonkTyConBinder,
  zonkTcType, zonkTcTypes, zonkCo,
80
  zonkTyCoVarKind, zonkTcTypeMapper,
81

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

84
  tcGetGlobalTyCoVars
85 86 87 88 89
  ) where

#include "HsVersions.h"

-- friends:
90
import TyCoRep
91 92
import TcType
import Type
93
import TyCon( TyConBinder )
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
94
import Kind
95
import Coercion
96 97
import Class
import Var
98 99

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

Ian Lynagh's avatar
Ian Lynagh committed
118
import Control.Monad
119
import Maybes
120
import Data.List        ( mapAccumL )
121
import Control.Arrow    ( second )
122

Austin Seipp's avatar
Austin Seipp committed
123 124 125
{-
************************************************************************
*                                                                      *
126
        Kind variables
Austin Seipp's avatar
Austin Seipp committed
127 128 129
*                                                                      *
************************************************************************
-}
130

131 132 133
mkKindName :: Unique -> Name
mkKindName unique = mkSystemName unique kind_var_occ

134 135
kind_var_occ :: OccName -- Just one for all MetaKindVars
                        -- They may be jiggled by tidying
136 137
kind_var_occ = mkOccName tvName "k"

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

dreixel's avatar
dreixel committed
144 145
newMetaKindVars :: Int -> TcM [TcKind]
newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
146

Austin Seipp's avatar
Austin Seipp committed
147 148 149
{-
************************************************************************
*                                                                      *
150
     Evidence variables; range over constraints we can abstract over
Austin Seipp's avatar
Austin Seipp committed
151 152 153
*                                                                      *
************************************************************************
-}
154

155 156 157
newEvVars :: TcThetaType -> TcM [EvVar]
newEvVars theta = mapM newEvVar theta

158
--------------
batterseapower's avatar
batterseapower committed
159

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

newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
166
-- Deals with both equality and non-equality predicates
167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209
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
                         , ctev_loc = loc }

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

-- | 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 $
           CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole, ctev_loc = loc }
       ; 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
                             , ctev_loc  = loc }
       ; emitSimple $ mkNonCanonical ctev
       ; return new_cv }

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

newDict :: Class -> [TcType] -> TcM DictId
212
newDict cls tys
213
  = do { name <- newSysName (mkDictOcc (getOccName cls))
batterseapower's avatar
batterseapower committed
214 215 216
       ; return (mkLocalId name (mkClassPred cls tys)) }

predTypeOccName :: PredType -> OccName
217
predTypeOccName ty = case classifyPredType ty of
batterseapower's avatar
batterseapower committed
218
    ClassPred cls _ -> mkDictOcc (getOccName cls)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
219
    EqPred _ _ _    -> mkVarOccFS (fsLit "cobox")
batterseapower's avatar
batterseapower committed
220
    IrredPred _     -> mkVarOccFS (fsLit "irred")
221

222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287
{-
************************************************************************
*                                                                      *
        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 {
#ifdef DEBUG
       ; 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

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 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
{-
************************************************************************
*
    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 #.
340 341 342 343 344 345 346 347
newInferExpTypeNoInst :: TcM ExpSigmaType
newInferExpTypeNoInst = newInferExpType False

newInferExpTypeInst :: TcM ExpRhoType
newInferExpTypeInst = newInferExpType True

newInferExpType :: Bool -> TcM ExpType
newInferExpType inst
348
  = do { u <- newUnique
349
       ; tclvl <- getTcLevel
350
       ; traceTc "newOpenInferExpType" (ppr u <+> ppr inst <+> ppr tclvl)
351
       ; ref <- newMutVar Nothing
352
       ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
353
                           , ir_ref = ref, ir_inst = inst })) }
354 355 356 357

-- | 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)
358 359
readExpType_maybe (Check ty)                   = return (Just ty)
readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379

-- | 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)

380 381 382
tauifyExpType :: ExpType -> TcM ExpType
-- ^ Turn a (Infer hole) type into a (Check alpha),
-- where alpha is a fresh unificaiton variable
383 384 385
tauifyExpType (Check ty)      = return (Check ty)  -- No-op for (Check ty)
tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
                                   ; return (Check ty) }
386

387 388 389
-- | Extracts the expected type if there is one, or generates a new
-- TauTv if there isn't.
expTypeToType :: ExpType -> TcM TcType
390 391 392 393 394
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
395 396 397
                      , ir_ref = ref })
  = do { rr  <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
       ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
398
             -- See Note [TcLevel of ExpType]
399 400
       ; writeMutVar ref (Just tau)
       ; traceTc "Forcing ExpType to be monomorphic:"
401
                 (ppr u <+> text ":=" <+> ppr tau)
402
       ; return tau }
403

404

405
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
406
*                                                                      *
407
        SkolemTvs (immutable)
Austin Seipp's avatar
Austin Seipp committed
408
*                                                                      *
409
********************************************************************* -}
410

411 412
tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
                   -- ^ How to instantiate the type variables
413 414
           -> Id                                            -- ^ Type to instantiate
           -> TcM ([(Name, TcTyVar)], TcThetaType, TcType)  -- ^ Result
415
                -- (type vars, preds (incl equalities), rho)
416 417
tcInstType inst_tyvars id
  = case tcSplitForAllTys (idType id) of
418
        ([],    rho) -> let     -- There may be overloading despite no type variables;
419
                                --      (?x :: Int) => Int -> Int
420 421 422
                                (theta, tau) = tcSplitPhiTy rho
                            in
                            return ([], theta, tau)
423

424
        (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
425
                            ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
426 427
                                  tv_prs       = map tyVarName tyvars `zip` tyvars'
                            ; return (tv_prs, theta, tau) }
428

429
tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
430 431
-- Instantiate a type signature with skolem constants.
-- We could give them fresh names, but no need to do so
432 433 434
tcSkolDFunType dfun
  = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
       ; return (map snd tv_prs, theta, tau) }
435

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

443
tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
444
tcSuperSkolTyVar subst tv
445
  = (extendTvSubstWithClone subst tv new_tv, new_tv)
dreixel's avatar
dreixel committed
446
  where
447
    kind   = substTyUnchecked subst (tyVarKind tv)
448 449
    new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv

450 451 452 453 454 455
-- | 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.
456 457
tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSkolTyVars = tcInstSkolTyVars' False emptyTCvSubst
dreixel's avatar
dreixel committed
458

459 460 461 462
tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst

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

465
tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
466 467
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
468
-- Get the location from the monad; this is a complete freshening operation
469
tcInstSkolTyVars' overlappable subst tvs
470
  = do { loc <- getSrcSpanM
471 472
       ; lvl <- getTcLevel
       ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
473

474 475 476 477 478 479 480
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
481

482
tcInstSigTyVars :: SrcSpan -> [TyVar]
483 484 485 486
                -> TcM (TCvSubst, [TcTyVar])
tcInstSigTyVars loc tvs
  = do { lvl <- getTcLevel
       ; instSkolTyCoVars (mkTcSkolTyVar lvl loc False) tvs }
487

488
------------------
489
freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
490 491 492
-- ^ Give fresh uniques to a bunch of TyVars, but they stay
--   as TyVars, rather than becoming TcTyVars
-- Used in FamInst.newFamInst, and Inst.newClsInst
493
freshenTyVarBndrs = instSkolTyCoVars mk_tv
494 495
  where
    mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
496

497 498 499 500 501 502 503
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

504
------------------
505 506
type TcTyVarMaker = Unique -> Name -> Kind -> TyCoVar
instSkolTyCoVars :: TcTyVarMaker -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
507
instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
508

509
instSkolTyCoVarsX :: TcTyVarMaker
510 511
                  -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
512

513
instSkolTyCoVarX :: TcTyVarMaker
514 515
                 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
instSkolTyCoVarX mk_tcv subst tycovar
516 517
  = do  { uniq <- newUnique  -- using a new unique is critical. See
                             -- Note [Skolems in zonkSyntaxExpr] in TcHsSyn
518 519 520 521 522 523
        ; 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) }
524
  where
525
    old_name = tyVarName tycovar
526
    kind     = substTyUnchecked subst (tyVarKind tycovar)
527

528 529 530 531 532
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
533
{-
dreixel's avatar
dreixel committed
534 535 536
Note [Kind substitution when instantiating]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we instantiate a bunch of kind and type variables, first we
537
expect them to be topologically sorted.
dreixel's avatar
dreixel committed
538 539 540 541 542
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
543
  [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
dreixel's avatar
dreixel committed
544
we want
545
  [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
dreixel's avatar
dreixel committed
546
instead of the buggous
547
  [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
dreixel's avatar
dreixel committed
548

549

Austin Seipp's avatar
Austin Seipp committed
550 551
************************************************************************
*                                                                      *
552
        MetaTvs (meta type variables; mutable)
Austin Seipp's avatar
Austin Seipp committed
553 554 555
*                                                                      *
************************************************************************
-}
556

557 558 559 560 561 562
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

563 564
newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
Jan Stolarek's avatar
Jan Stolarek committed
565
  = do { details <- newMetaDetails SigTv
566
       ; return (mkTcTyVar name kind details) }
567

568 569 570 571 572 573 574 575 576 577 578 579 580
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) }

581 582 583
newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails info
  = do { ref <- newMutVar Flexi
584
       ; tclvl <- getTcLevel
585 586 587
       ; return (MetaTv { mtv_info = info
                        , mtv_ref = ref
                        , mtv_tclvl = tclvl }) }
588

589 590 591
cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
cloneMetaTyVar tv
  = ASSERT( isTcTyVar tv )
592
    do  { uniq <- newUnique
593 594
        ; ref  <- newMutVar Flexi
        ; let name'    = setNameUnique (tyVarName tv) uniq
595
              details' = case tcTyVarDetails tv of
596 597 598 599
                           details@(MetaTv {}) -> details { mtv_ref = ref }
                           _ -> pprPanic "cloneMetaTyVar" (ppr tv)
        ; return (mkTcTyVar name' (tyVarKind tv) details') }

dreixel's avatar
dreixel committed
600
-- Works for both type and kind variables
601 602
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
603
                      readMutVar (metaTyVarRef tyvar)
604

605 606 607
isFilledMetaTyVar :: TyVar -> TcM Bool
-- True of a filled-in (Indirect) meta type variable
isFilledMetaTyVar tv
608
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
609 610
  = do  { details <- readMutVar ref
        ; return (isIndirect details) }
611 612
  | otherwise = return False

613
isUnfilledMetaTyVar :: TyVar -> TcM Bool
614
-- True of a un-filled-in (Flexi) meta type variable
615
isUnfilledMetaTyVar tv
616
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
617 618
  = do  { details <- readMutVar ref
        ; return (isFlexi details) }
619 620 621
  | otherwise = return False

--------------------
dreixel's avatar
dreixel committed
622
-- Works with both type and kind variables
623
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
624 625
-- Write into a currently-empty MetaTyVar

Ian Lynagh's avatar
Ian Lynagh committed
626
writeMetaTyVar tyvar ty
627
  | not debugIsOn
628
  = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
629 630 631 632 633 634

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

635
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
636 637 638 639
  = writeMetaTyVarRef tyvar ref ty

  | otherwise
  = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
640
    return ()
641 642 643

--------------------
writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
644
-- Here the tyvar is for error checking only;
645 646
-- the ref cell must be for the same tyvar
writeMetaTyVarRef tyvar ref ty
647
  | not debugIsOn
648 649 650
  = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
                                   <+> text ":=" <+> ppr ty)
       ; writeTcRef ref (Indirect ty) }
651

652
  -- Everything from here on only happens if DEBUG is on
653
  | otherwise
654
  = do { meta_details <- readMutVar ref;
dreixel's avatar
dreixel committed
655
       -- Zonk kinds to allow the error check to work
656 657
       ; zonked_tv_kind <- zonkTcType tv_kind
       ; zonked_ty_kind <- zonkTcType ty_kind
658 659 660 661 662 663 664 665 666 667
       ; 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
668 669

       -- Check for double updates
670 671 672 673 674 675 676 677 678 679 680
       ; 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) }
681 682 683
  where
    tv_kind = tyVarKind tyvar
    ty_kind = typeKind ty
684

685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706
    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.
-}

707 708 709 710
{-
% Generating fresh variables for pattern match check
-}

711 712 713 714
-- UNINSTANTIATED VERSION OF tcInstSkolTyCoVars
genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
                   -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
-- Precondition: tyvars should be scoping-ordered
715 716
-- see Note [Kind substitution when instantiating]
-- Get the location from the monad; this is a complete freshening operation
717 718
genInstSkolTyVarsX loc subst tvs
  = instSkolTyCoVarsX (mkTcSkolTyVar topTcLevel loc False) subst tvs
719

Austin Seipp's avatar
Austin Seipp committed
720 721 722
{-
************************************************************************
*                                                                      *
723
        MetaTvs: TauTvs
Austin Seipp's avatar
Austin Seipp committed
724 725
*                                                                      *
************************************************************************
726 727 728 729 730 731 732 733 734 735 736 737 738

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
739
-}
740

741 742 743 744 745 746 747 748 749 750 751 752
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) }

753
newFlexiTyVar :: Kind -> TcM TcTyVar
754
newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
755

756
newFlexiTyVarTy :: Kind -> TcM TcType
757 758
newFlexiTyVarTy kind = do
    tc_tyvar <- newFlexiTyVar kind
759
    return (mkTyVarTy tc_tyvar)
760 761

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

764 765 766 767 768
newOpenTypeKind :: TcM TcKind
newOpenTypeKind
  = do { rr <- newFlexiTyVarTy runtimeRepTy
       ; return (tYPE rr) }

769
-- | Create a tyvar that can be a lifted or unlifted type.
770
-- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
771 772
newOpenFlexiTyVarTy :: TcM TcType
newOpenFlexiTyVarTy
773 774
  = do { kind <- newOpenTypeKind
       ; newFlexiTyVarTy kind }
775

776 777 778 779
newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst

newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
780
-- Instantiate with META type variables
781 782 783
-- Note that this works for a sequence of kind, type, and coercion variables
-- variables.  Eg    [ (k:*), (a:k->k) ]
--             Gives [ (k7:*), (a8:k7->k7) ]
784
newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
785
    -- emptyTCvSubst has an empty in-scope set, but that's fine here
dreixel's avatar
dreixel committed
786 787 788
    -- Since the tyvars are freshly made, they cannot possibly be
    -- captured by any existing for-alls.

789
newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
dreixel's avatar
dreixel committed
790 791
-- Make a new unification variable tyvar whose Name and Kind come from
-- an existing TyVar. We substitute kind variables in the kind.
792
newMetaTyVarX subst tyvar = new_meta_tv_x TauTv subst tyvar
793 794 795

newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-- Just like newMetaTyVarX, but make a SigTv
796 797
newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar

798 799 800 801 802
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) }

803
new_meta_tv_x :: MetaInfo -> TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
804
new_meta_tv_x info subst tv
805
  = do  { uniq <- newUnique
806
        ; details <- newMetaDetails info
807
        ; let name   = mkSystemName uniq (getOccName tv)
808
                       -- See Note [Name of an instantiated type variable]
809 810 811 812 813 814
              kind   = substTyUnchecked subst (tyVarKind tv)
                       -- 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
815
              new_tv = mkTcTyVar name kind details
816
              subst1 = extendTvSubstWithClone subst tv new_tv
817
        ; return (subst1, new_tv) }
818

819 820
newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType
newMetaTyVarTyAtLevel tc_lvl kind
821 822 823 824 825 826
  = do  { uniq <- newUnique
        ; ref  <- newMutVar Flexi
        ; let name = mkMetaTyVarName uniq (fsLit "p")
              details = MetaTv { mtv_info  = TauTv
                               , mtv_ref   = ref
                               , mtv_tclvl = tc_lvl }
827
        ; return (mkTyVarTy (mkTcTyVar name kind details)) }
828

Simon Peyton Jones's avatar
Simon Peyton Jones committed
829 830 831 832 833
{- 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
834 835
************************************************************************
*                                                                      *
836
             Quantification
Austin Seipp's avatar
Austin Seipp committed
837 838
*                                                                      *
************************************************************************
839

840 841
Note [quantifyTyVars]
~~~~~~~~~~~~~~~~~~~~~
842
quantifyTyVars is given the free vars of a type that we
843
are about to wrap in a forall.
844

845 846 847 848 849
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
850

851
Step (2) is often unimportant, because the kind variable is often
852 853 854 855 856
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).
857

858 859 860
* 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.
861

862 863 864
* quantifyTyVars never quantifies over
    - a coercion variable
    - a runtime-rep variable
865 866 867 868 869 870 871 872 873 874 875 876 877

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.

To achieve this TcDepVars is backed by deterministic sets which allows them
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
878
-}
879

880 881
quantifyTyVars, quantifyZonkedTyVars
  :: TcTyCoVarSet   -- global tvs
882
  -> TcDepVars      -- See Note [Dependent type variables] in TcType
883
  -> TcM [TcTyVar]
884
-- See Note [quantifyTyVars]
885
-- Can be given a mixture of TcTyVars and TyVars, in the case of
886 887
--   associated type declarations. Also accepts covars, but *never* returns any.

888 889
-- The zonked variant assumes everything is already zonked.

890
quantifyTyVars gbl_tvs (DV { dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
891
  = do { dep_tkvs    <- zonkTyCoVarsAndFVDSet dep_tkvs
892
       ; nondep_tkvs <- zonkTyCoVarsAndFVDSet nondep_tkvs
893
       ; gbl_tvs     <- zonkTyCoVarsAndFV gbl_tvs
894 895
       ; quantifyZonkedTyVars gbl_tvs (DV { dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs }) }

896 897 898
quantifyZonkedTyVars gbl_tvs dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
  = do { traceTc "quantifyZonkedTyVars" (vcat [ppr dvs, ppr gbl_tvs])
       ; let all_cvs = filterVarSet isCoVar $ dVarSetToVarSet dep_tkvs
899 900 901 902
             dep_kvs = dVarSetElemsWellScoped $
                       dep_tkvs `dVarSetMinusVarSet` gbl_tvs
                                `dVarSetMinusVarSet` closeOverKinds all_cvs
                 -- dVarSetElemsWellScoped: put the kind variables into
903 904 905