TcMType.hs 67.1 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,
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
  zonkTidyTcType, zonkTidyOrigin,
69
  tidyEvVar, tidyCt, tidySkolemInfo,
70
  skolemiseRuntimeUnk,
71 72
  zonkTcTyVar, zonkTcTyVars,
  zonkTcTyVarToTyVar, zonkSigTyVarPairs,
73
  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

Simon Peyton Jones's avatar
Simon Peyton Jones committed
82 83 84
  zonkEvVar, zonkWC, zonkSimples,
  zonkId, zonkCoVar,
  zonkCt, zonkSkolemInfo,
85

Richard Eisenberg's avatar
Richard Eisenberg committed
86 87 88 89 90
  tcGetGlobalTyCoVars,

  ------------------------------
  -- Levity polymorphism
  ensureNotLevPoly, checkForLevPoly, checkForLevPolyX, formatLevPolyErr
91 92 93 94 95
  ) where

#include "HsVersions.h"

-- friends:
96 97
import GhcPrelude

98
import TyCoRep
99 100
import TcType
import Type
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
101
import Kind
102
import Coercion
103 104
import Class
import Var
105 106

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

Ian Lynagh's avatar
Ian Lynagh committed
126
import Control.Monad
127
import Maybes
128
import Data.List        ( mapAccumL )
129
import Control.Arrow    ( second )
130

Austin Seipp's avatar
Austin Seipp committed
131 132 133
{-
************************************************************************
*                                                                      *
134
        Kind variables
Austin Seipp's avatar
Austin Seipp committed
135 136 137
*                                                                      *
************************************************************************
-}
138

139 140 141
mkKindName :: Unique -> Name
mkKindName unique = mkSystemName unique kind_var_occ

142 143
kind_var_occ :: OccName -- Just one for all MetaKindVars
                        -- They may be jiggled by tidying
144 145
kind_var_occ = mkOccName tvName "k"

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

dreixel's avatar
dreixel committed
152 153
newMetaKindVars :: Int -> TcM [TcKind]
newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
154

Austin Seipp's avatar
Austin Seipp committed
155 156 157
{-
************************************************************************
*                                                                      *
158
     Evidence variables; range over constraints we can abstract over
Austin Seipp's avatar
Austin Seipp committed
159 160 161
*                                                                      *
************************************************************************
-}
162

163 164 165
newEvVars :: TcThetaType -> TcM [EvVar]
newEvVars theta = mapM newEvVar theta

166
--------------
batterseapower's avatar
batterseapower committed
167

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

newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
174
-- Deals with both equality and non-equality predicates
175 176
newWanted orig t_or_k pty
  = do loc <- getCtLocM orig t_or_k
Simon Peyton Jones's avatar
Simon Peyton Jones committed
177
       d <- if isEqPred pty then HoleDest  <$> newCoercionHole pty
178 179 180
                            else EvVarDest <$> newEvVar pty
       return $ CtWanted { ctev_dest = d
                         , ctev_pred = pty
181
                         , ctev_nosh = WDeriv
182 183 184 185 186
                         , ctev_loc = loc }

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

187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
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' }) }

205 206 207 208 209 210 211 212 213 214
-- | 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
Simon Peyton Jones's avatar
Simon Peyton Jones committed
215
  = do { hole <- newCoercionHole pty
216 217
       ; loc <- getCtLocM origin (Just t_or_k)
       ; emitSimple $ mkNonCanonical $
218 219
         CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole
                  , ctev_nosh = WDeriv, ctev_loc = loc }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
220
       ; return (HoleCo hole) }
221 222 223 224 225 226 227 228 229 230 231
  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
232
                             , ctev_nosh = WDeriv
233 234 235 236 237 238
                             , ctev_loc  = loc }
       ; emitSimple $ mkNonCanonical ctev
       ; return new_cv }

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

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

predTypeOccName :: PredType -> OccName
246
predTypeOccName ty = case classifyPredType ty of
batterseapower's avatar
batterseapower committed
247
    ClassPred cls _ -> mkDictOcc (getOccName cls)
248
    EqPred _ _ _    -> mkVarOccFS (fsLit "co")
batterseapower's avatar
batterseapower committed
249
    IrredPred _     -> mkVarOccFS (fsLit "irred")
250

251 252 253 254 255 256 257 258
{-
************************************************************************
*                                                                      *
        Coercion holes
*                                                                      *
************************************************************************
-}

Simon Peyton Jones's avatar
Simon Peyton Jones committed
259 260 261 262
newCoercionHole :: TcPredType -> TcM CoercionHole
newCoercionHole pred_ty
  = do { co_var <- newEvVar pred_ty
       ; traceTc "New coercion hole:" (ppr co_var)
263
       ; ref <- newMutVar Nothing
Simon Peyton Jones's avatar
Simon Peyton Jones committed
264
       ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
265 266 267

-- | Put a value in a coercion hole
fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
Simon Peyton Jones's avatar
Simon Peyton Jones committed
268
fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co
269
  = do {
Ben Gamari's avatar
Ben Gamari committed
270
#if defined(DEBUG)
271 272
       ; cts <- readTcRef ref
       ; whenIsJust cts $ \old_co ->
Simon Peyton Jones's avatar
Simon Peyton Jones committed
273
         pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co)
274
#endif
Simon Peyton Jones's avatar
Simon Peyton Jones committed
275
       ; traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co)
276 277 278 279
       ; writeTcRef ref (Just co) }

-- | Is a coercion hole filled in?
isFilledCoercionHole :: CoercionHole -> TcM Bool
Simon Peyton Jones's avatar
Simon Peyton Jones committed
280
isFilledCoercionHole (CoercionHole { ch_ref = ref }) = isJust <$> readTcRef ref
281 282 283 284 285 286 287 288 289 290 291 292

-- | 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)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
293
unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
294 295 296 297 298 299

-- | 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.
Simon Peyton Jones's avatar
Simon Peyton Jones committed
300 301
checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
checkCoercionHole cv co
302
  | debugIsOn
Simon Peyton Jones's avatar
Simon Peyton Jones committed
303 304
  = do { cv_ty <- zonkTcType (varType cv)
                  -- co is already zonked, but cv might not be
305
       ; return $
Simon Peyton Jones's avatar
Simon Peyton Jones committed
306
         ASSERT2( ok cv_ty
307
                , (text "Bad coercion hole" <+>
Simon Peyton Jones's avatar
Simon Peyton Jones committed
308 309
                   ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role
                                            , ppr cv_ty ]) )
310 311 312 313
         co }
  | otherwise
  = return co

Simon Peyton Jones's avatar
Simon Peyton Jones committed
314 315 316 317 318 319 320 321 322
  where
    (Pair t1 t2, role) = coercionKindRole co
    ok cv_ty | EqPred cv_rel cv_t1 cv_t2 <- classifyPredType cv_ty
             =  t1 `eqType` cv_t1
             && t2 `eqType` cv_t2
             && role == eqRelRole cv_rel
             | otherwise
             = False

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 365 366 367 368 369 370 371 372 373 374
{-
************************************************************************
*
    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 #.
375 376 377 378 379 380 381 382
newInferExpTypeNoInst :: TcM ExpSigmaType
newInferExpTypeNoInst = newInferExpType False

newInferExpTypeInst :: TcM ExpRhoType
newInferExpTypeInst = newInferExpType True

newInferExpType :: Bool -> TcM ExpType
newInferExpType inst
383
  = do { u <- newUnique
384
       ; tclvl <- getTcLevel
385
       ; traceTc "newOpenInferExpType" (ppr u <+> ppr inst <+> ppr tclvl)
386
       ; ref <- newMutVar Nothing
387
       ; return (Infer (IR { ir_uniq = u, ir_lvl = tclvl
388
                           , ir_ref = ref, ir_inst = inst })) }
389 390 391 392

-- | 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)
393 394
readExpType_maybe (Check ty)                   = return (Just ty)
readExpType_maybe (Infer (IR { ir_ref = ref})) = readMutVar ref
395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414

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

415 416
tauifyExpType :: ExpType -> TcM ExpType
-- ^ Turn a (Infer hole) type into a (Check alpha),
417
-- where alpha is a fresh unification variable
418 419 420
tauifyExpType (Check ty)      = return (Check ty)  -- No-op for (Check ty)
tauifyExpType (Infer inf_res) = do { ty <- inferResultToType inf_res
                                   ; return (Check ty) }
421

422 423 424
-- | Extracts the expected type if there is one, or generates a new
-- TauTv if there isn't.
expTypeToType :: ExpType -> TcM TcType
425 426 427 428 429
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
430 431 432
                      , ir_ref = ref })
  = do { rr  <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
       ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
433
             -- See Note [TcLevel of ExpType]
434 435
       ; writeMutVar ref (Just tau)
       ; traceTc "Forcing ExpType to be monomorphic:"
436
                 (ppr u <+> text ":=" <+> ppr tau)
437
       ; return tau }
438

439

440
{- *********************************************************************
Austin Seipp's avatar
Austin Seipp committed
441
*                                                                      *
442
        SkolemTvs (immutable)
Austin Seipp's avatar
Austin Seipp committed
443
*                                                                      *
444
********************************************************************* -}
445

446 447
tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
                   -- ^ How to instantiate the type variables
448 449
           -> Id                                            -- ^ Type to instantiate
           -> TcM ([(Name, TcTyVar)], TcThetaType, TcType)  -- ^ Result
450
                -- (type vars, preds (incl equalities), rho)
451 452
tcInstType inst_tyvars id
  = case tcSplitForAllTys (idType id) of
453
        ([],    rho) -> let     -- There may be overloading despite no type variables;
454
                                --      (?x :: Int) => Int -> Int
455 456 457
                                (theta, tau) = tcSplitPhiTy rho
                            in
                            return ([], theta, tau)
458

459
        (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
460
                            ; let (theta, tau) = tcSplitPhiTy (substTyAddInScope subst rho)
461 462
                                  tv_prs       = map tyVarName tyvars `zip` tyvars'
                            ; return (tv_prs, theta, tau) }
463

464
tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
465 466
-- Instantiate a type signature with skolem constants.
-- We could give them fresh names, but no need to do so
467 468 469
tcSkolDFunType dfun
  = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
       ; return (map snd tv_prs, theta, tau) }
470

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

478
tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
479
tcSuperSkolTyVar subst tv
480
  = (extendTvSubstWithClone subst tv new_tv, new_tv)
dreixel's avatar
dreixel committed
481
  where
482
    kind   = substTyUnchecked subst (tyVarKind tv)
483 484
    new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv

485 486 487 488 489 490
-- | 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.
491
tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
492 493 494 495
tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst

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

497 498 499 500
tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst

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

503
tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
504 505
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
506
-- Get the location from the monad; this is a complete freshening operation
507
tcInstSkolTyVars' overlappable subst tvs
508
  = do { loc <- getSrcSpanM
509 510
       ; lvl <- getTcLevel
       ; instSkolTyCoVarsX (mkTcSkolTyVar lvl loc overlappable) subst tvs }
511

512 513 514 515 516 517 518
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
519

520
------------------
521
freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
522 523 524
-- ^ Give fresh uniques to a bunch of TyVars, but they stay
--   as TyVars, rather than becoming TcTyVars
-- Used in FamInst.newFamInst, and Inst.newClsInst
525
freshenTyVarBndrs = instSkolTyCoVars mk_tv
526 527
  where
    mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
528

529 530 531 532 533 534 535
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

536
------------------
537 538
type TcTyVarMaker = Unique -> Name -> Kind -> TyCoVar
instSkolTyCoVars :: TcTyVarMaker -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
539
instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
540

541
instSkolTyCoVarsX :: TcTyVarMaker
542 543
                  -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
544

545
instSkolTyCoVarX :: TcTyVarMaker
546 547
                 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
instSkolTyCoVarX mk_tcv subst tycovar
548 549
  = do  { uniq <- newUnique  -- using a new unique is critical. See
                             -- Note [Skolems in zonkSyntaxExpr] in TcHsSyn
550 551 552 553 554 555
        ; 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) }
556
  where
557
    old_name = tyVarName tycovar
558
    kind     = substTyUnchecked subst (tyVarKind tycovar)
559

560 561 562
newFskTyVar :: TcType -> TcM TcTyVar
newFskTyVar fam_ty
  = do { uniq <- newUnique
563 564 565 566 567 568 569
       ; ref  <- newMutVar Flexi
       ; let details = MetaTv { mtv_info  = FlatSkolTv
                              , mtv_ref   = ref
                              , mtv_tclvl = fmvTcLevel }
             name = mkMetaTyVarName uniq (fsLit "fsk")
       ; return (mkTcTyVar name (typeKind fam_ty) details) }

Austin Seipp's avatar
Austin Seipp committed
570
{-
dreixel's avatar
dreixel committed
571 572 573
Note [Kind substitution when instantiating]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we instantiate a bunch of kind and type variables, first we
574
expect them to be topologically sorted.
dreixel's avatar
dreixel committed
575 576 577 578 579
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
580
  [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
dreixel's avatar
dreixel committed
581
we want
582
  [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
dreixel's avatar
dreixel committed
583
instead of the buggous
584
  [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
dreixel's avatar
dreixel committed
585

586

Austin Seipp's avatar
Austin Seipp committed
587 588
************************************************************************
*                                                                      *
589
        MetaTvs (meta type variables; mutable)
Austin Seipp's avatar
Austin Seipp committed
590 591 592
*                                                                      *
************************************************************************
-}
593

594 595 596 597 598 599 600
-- a SigTv can unify with type *variables* only, including other SigTvs
-- and skolems. Sometimes, they can unify with type variables that the
-- user would rather keep distinct; see #11203 for an example.
-- So, any client of this
-- function needs to either allow the SigTvs to unify with each other
-- (say, for pattern-bound scoped type variables), or check that they
-- don't (say, with a call to findDubSigTvs).
601 602
newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
Jan Stolarek's avatar
Jan Stolarek committed
603
  = do { details <- newMetaDetails SigTv
604
       ; return (mkTcTyVar name kind details) }
605

606 607 608 609 610 611 612 613
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
       ; let details = MetaTv { mtv_info  = FlatMetaTv
                              , mtv_ref   = ref
614
                              , mtv_tclvl = fmvTcLevel }
615 616 617
             name = mkMetaTyVarName uniq (fsLit "s")
       ; return (mkTcTyVar name (typeKind fam_ty) details) }

618 619 620
newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails info
  = do { ref <- newMutVar Flexi
621
       ; tclvl <- getTcLevel
622 623 624
       ; return (MetaTv { mtv_info = info
                        , mtv_ref = ref
                        , mtv_tclvl = tclvl }) }
625

626 627 628
cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
cloneMetaTyVar tv
  = ASSERT( isTcTyVar tv )
629
    do  { uniq <- newUnique
630 631
        ; ref  <- newMutVar Flexi
        ; let name'    = setNameUnique (tyVarName tv) uniq
632
              details' = case tcTyVarDetails tv of
633 634 635 636
                           details@(MetaTv {}) -> details { mtv_ref = ref }
                           _ -> pprPanic "cloneMetaTyVar" (ppr tv)
        ; return (mkTcTyVar name' (tyVarKind tv) details') }

dreixel's avatar
dreixel committed
637
-- Works for both type and kind variables
638 639
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
640
                      readMutVar (metaTyVarRef tyvar)
641

642 643 644
isFilledMetaTyVar :: TyVar -> TcM Bool
-- True of a filled-in (Indirect) meta type variable
isFilledMetaTyVar tv
645
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
646 647
  = do  { details <- readMutVar ref
        ; return (isIndirect details) }
648 649
  | otherwise = return False

650
isUnfilledMetaTyVar :: TyVar -> TcM Bool
651
-- True of a un-filled-in (Flexi) meta type variable
652
isUnfilledMetaTyVar tv
653
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
654 655
  = do  { details <- readMutVar ref
        ; return (isFlexi details) }
656 657 658
  | otherwise = return False

--------------------
dreixel's avatar
dreixel committed
659
-- Works with both type and kind variables
660
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
661 662
-- Write into a currently-empty MetaTyVar

Ian Lynagh's avatar
Ian Lynagh committed
663
writeMetaTyVar tyvar ty
664
  | not debugIsOn
665
  = writeMetaTyVarRef tyvar (metaTyVarRef tyvar) ty
666 667 668 669 670 671

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

672
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
673 674 675 676
  = writeMetaTyVarRef tyvar ref ty

  | otherwise
  = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
677
    return ()
678 679 680

--------------------
writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
681
-- Here the tyvar is for error checking only;
682 683
-- the ref cell must be for the same tyvar
writeMetaTyVarRef tyvar ref ty
684
  | not debugIsOn
685 686 687
  = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
                                   <+> text ":=" <+> ppr ty)
       ; writeTcRef ref (Indirect ty) }
688

689
  -- Everything from here on only happens if DEBUG is on
690
  | otherwise
691
  = do { meta_details <- readMutVar ref;
dreixel's avatar
dreixel committed
692
       -- Zonk kinds to allow the error check to work
693 694
       ; zonked_tv_kind <- zonkTcType tv_kind
       ; zonked_ty_kind <- zonkTcType ty_kind
695
       ; let kind_check_ok = isPredTy tv_kind  -- Don't check kinds for updates
696 697
                                               -- to coercion variables.  Why not??
                          || isConstraintKind zonked_tv_kind
698
                          || tcEqKind zonked_ty_kind zonked_tv_kind
699 700
             -- Hack alert! isConstraintKind: see TcHsType
             -- Note [Extra-constraint holes in partial type signatures]
701 702 703 704 705 706 707

             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
708 709

       -- Check for double updates
710 711 712 713 714 715 716 717 718 719 720
       ; 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) }
721 722 723
  where
    tv_kind = tyVarKind tyvar
    ty_kind = typeKind ty
724

725 726 727
    tv_lvl = tcTyVarLevel tyvar
    ty_lvl = tcTypeLevel ty

728
    level_check_ok = isFlattenTyVar tyvar
729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746
                  || 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.
-}

747 748 749 750
{-
% Generating fresh variables for pattern match check
-}

751 752 753 754
-- UNINSTANTIATED VERSION OF tcInstSkolTyCoVars
genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
                   -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
-- Precondition: tyvars should be scoping-ordered
755 756
-- see Note [Kind substitution when instantiating]
-- Get the location from the monad; this is a complete freshening operation
757 758
genInstSkolTyVarsX loc subst tvs
  = instSkolTyCoVarsX (mkTcSkolTyVar topTcLevel loc False) subst tvs
759

Austin Seipp's avatar
Austin Seipp committed
760 761 762
{-
************************************************************************
*                                                                      *
763
        MetaTvs: TauTvs
Austin Seipp's avatar
Austin Seipp committed
764 765
*                                                                      *
************************************************************************
766 767 768 769 770 771 772 773 774 775 776 777 778

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
779
-}
780

781 782 783 784 785 786
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 = mkSystemName uniq (mkTyVarOccFS str)

787 788 789 790 791 792 793 794
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"
795
                        FlatSkolTv  -> fsLit "fsk"
796 797 798 799
                        SigTv       -> fsLit "a"
        ; details <- newMetaDetails meta_info
        ; return (mkTcTyVar name kind details) }

800 801 802 803 804 805 806 807 808 809 810 811 812 813 814
cloneAnonMetaTyVar :: MetaInfo -> TyVar -> TcKind -> TcM TcTyVar
-- Same as newAnonMetaTyVar, but use a supplied TyVar as the source of the print-name
cloneAnonMetaTyVar info tv kind
  = do  { uniq    <- newUnique
        ; details <- newMetaDetails info
        ; let name = mkSystemName uniq (getOccName tv)
                       -- See Note [Name of an instantiated type variable]
        ; return (mkTcTyVar name kind details) }

{- 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.
-}

815
newFlexiTyVar :: Kind -> TcM TcTyVar
816
newFlexiTyVar kind = newAnonMetaTyVar TauTv kind
817

818
newFlexiTyVarTy :: Kind -> TcM TcType
819 820
newFlexiTyVarTy kind = do
    tc_tyvar <- newFlexiTyVar kind
821
    return (mkTyVarTy tc_tyvar)
822 823

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

826 827 828 829 830
newOpenTypeKind :: TcM TcKind
newOpenTypeKind
  = do { rr <- newFlexiTyVarTy runtimeRepTy
       ; return (tYPE rr) }

831
-- | Create a tyvar that can be a lifted or unlifted type.
832
-- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
833 834
newOpenFlexiTyVarTy :: TcM TcType
newOpenFlexiTyVarTy
835 836
  = do { kind <- newOpenTypeKind
       ; newFlexiTyVarTy kind }
837

838 839 840 841
newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst

newMetaTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
842
-- Instantiate with META type variables
843 844 845
-- Note that this works for a sequence of kind, type, and coercion variables
-- variables.  Eg    [ (k:*), (a:k->k) ]
--             Gives [ (k7:*), (a8:k7->k7) ]
846
newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
847
    -- emptyTCvSubst has an empty in-scope set, but that's fine here
dreixel's avatar
dreixel committed
848 849 850
    -- Since the tyvars are freshly made, they cannot possibly be
    -- captured by any existing for-alls.

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

856 857 858 859
newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- Just like newMetaTyVars, but start with an existing substitution.
newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst

860 861
newMetaSigTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
-- Just like newMetaTyVarX, but make a SigTv
862 863
newMetaSigTyVarX subst tyvar = new_meta_tv_x SigTv subst tyvar

864 865 866 867