TcMType.hs 38.2 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 #-}
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
  newReturnTyVar, newReturnTyVarTy,
23
  newMetaKindVar, newMetaKindVars,
24
  mkTcTyVarName, cloneMetaTyVar,
25

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

  --------------------------------
30
  -- Creating new evidence variables
31
  newEvVar, newEvVars, newEq, newDict,
32
  newTcEvBinds, addTcEvBind,
33

34 35
  --------------------------------
  -- Instantiation
36
  tcInstTyVars, tcInstTyVarX, newSigTyVar,
37
  tcInstType,
38
  tcInstSkolTyVars, tcInstSuperSkolTyVarsX,
39
  tcInstSigTyVarsLoc, tcInstSigTyVars,
40
  tcInstSkolType,
41
  tcSkolDFunType, tcSuperSkolTyVars,
42

43 44
  instSkolTyVars, freshenTyVarBndrs,

45
  --------------------------------
46 47 48
  -- Zonking and tidying
  zonkTcPredType, zonkTidyTcType, zonkTidyOrigin,
  tidyEvVar, tidyCt, tidySkolemInfo,
49
  skolemiseUnboundMetaTyVar,
50
  zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkTcTypeAndFV,
51
  zonkQuantifiedTyVar, quantifyTyVars,
52
  zonkTcTyVarBndr, zonkTcType, zonkTcTypes, zonkTcThetaType,
53

54
  zonkTcKind, defaultKindVarToStar,
55
  zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
56

57
  tcGetGlobalTyVars,
thomasw's avatar
thomasw committed
58 59 60 61

  --------------------------------
  -- (Named) Wildcards
  newWildcardVar, newWildcardVarMetaKind
62 63 64 65 66
  ) where

#include "HsVersions.h"

-- friends:
67 68 69 70 71
import TypeRep
import TcType
import Type
import Class
import Var
72
import VarEnv
73 74

-- others:
75
import TcRnMonad        -- TcType, amongst others
76
import Id
77
import Name
78
import VarSet
79
import PrelNames
80 81
import DynFlags
import Util
82
import Outputable
83
import FastString
Simon Peyton Jones's avatar
Simon Peyton Jones committed
84
import SrcLoc
85
import Bag
86

Ian Lynagh's avatar
Ian Lynagh committed
87
import Control.Monad
88
import Data.List        ( partition, mapAccumL )
89

Austin Seipp's avatar
Austin Seipp committed
90 91 92
{-
************************************************************************
*                                                                      *
93
        Kind variables
Austin Seipp's avatar
Austin Seipp committed
94 95 96
*                                                                      *
************************************************************************
-}
97

98 99 100
mkKindName :: Unique -> Name
mkKindName unique = mkSystemName unique kind_var_occ

101 102
kind_var_occ :: OccName -- Just one for all MetaKindVars
                        -- They may be jiggled by tidying
103 104
kind_var_occ = mkOccName tvName "k"

dreixel's avatar
dreixel committed
105
newMetaKindVar :: TcM TcKind
106
newMetaKindVar = do { uniq <- newUnique
thomasw's avatar
thomasw committed
107
                    ; details <- newMetaDetails (TauTv False)
108
                    ; let kv = mkTcTyVar (mkKindName uniq) superKind details
109
                    ; return (mkTyVarTy kv) }
110

dreixel's avatar
dreixel committed
111 112
newMetaKindVars :: Int -> TcM [TcKind]
newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
113

Austin Seipp's avatar
Austin Seipp committed
114 115 116
{-
************************************************************************
*                                                                      *
117
     Evidence variables; range over constraints we can abstract over
Austin Seipp's avatar
Austin Seipp committed
118 119 120
*                                                                      *
************************************************************************
-}
121

122 123 124
newEvVars :: TcThetaType -> TcM [EvVar]
newEvVars theta = mapM newEvVar theta

125
--------------
batterseapower's avatar
batterseapower committed
126

127 128
newEvVar :: TcPredType -> TcM EvVar
-- Creates new *rigid* variables for predicates
129
newEvVar ty = do { name <- newSysName (predTypeOccName ty)
batterseapower's avatar
batterseapower committed
130
                 ; return (mkLocalId name ty) }
131

batterseapower's avatar
batterseapower committed
132 133
newEq :: TcType -> TcType -> TcM EvVar
newEq ty1 ty2
134
  = do { name <- newSysName (mkVarOccFS (fsLit "cobox"))
135
       ; return (mkLocalId name (mkTcEqPred ty1 ty2)) }
136 137

newDict :: Class -> [TcType] -> TcM DictId
138
newDict cls tys
139
  = do { name <- newSysName (mkDictOcc (getOccName cls))
batterseapower's avatar
batterseapower committed
140 141 142
       ; return (mkLocalId name (mkClassPred cls tys)) }

predTypeOccName :: PredType -> OccName
143
predTypeOccName ty = case classifyPredType ty of
batterseapower's avatar
batterseapower committed
144
    ClassPred cls _ -> mkDictOcc (getOccName cls)
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
145
    EqPred _ _ _    -> mkVarOccFS (fsLit "cobox")
batterseapower's avatar
batterseapower committed
146
    IrredPred _     -> mkVarOccFS (fsLit "irred")
147 148


Austin Seipp's avatar
Austin Seipp committed
149 150 151
{-
************************************************************************
*                                                                      *
152
        SkolemTvs (immutable)
Austin Seipp's avatar
Austin Seipp committed
153 154 155
*                                                                      *
************************************************************************
-}
156

157
tcInstType :: ([TyVar] -> TcM (TvSubst, [TcTyVar]))     -- How to instantiate the type variables
158 159 160
           -> TcType                                    -- Type to instantiate
           -> TcM ([TcTyVar], TcThetaType, TcType)      -- Result
                -- (type vars (excl coercion vars), preds (incl equalities), rho)
161 162
tcInstType inst_tyvars ty
  = case tcSplitForAllTys ty of
163 164 165 166 167
        ([],     rho) -> let    -- There may be overloading despite no type variables;
                                --      (?x :: Int) => Int -> Int
                           (theta, tau) = tcSplitPhiTy rho
                         in
                         return ([], theta, tau)
168

169 170 171
        (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
                            ; let (theta, tau) = tcSplitPhiTy (substTy subst rho)
                            ; return (tyvars', theta, tau) }
172

173
tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
174 175 176
-- Instantiate a type signature with skolem constants.
-- We could give them fresh names, but no need to do so
tcSkolDFunType ty = tcInstType tcInstSuperSkolTyVars ty
177

178
tcSuperSkolTyVars :: [TyVar] -> (TvSubst, [TcTyVar])
179
-- Make skolem constants, but do *not* give them new names, as above
180
-- Moreover, make them "super skolems"; see comments with superSkolemTv
dreixel's avatar
dreixel committed
181
-- see Note [Kind substitution when instantiating]
182
-- Precondition: tyvars should be ordered (kind vars first)
183
tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar (mkTopTvSubst [])
184 185 186 187

tcSuperSkolTyVar :: TvSubst -> TyVar -> (TvSubst, TcTyVar)
tcSuperSkolTyVar subst tv
  = (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv)
dreixel's avatar
dreixel committed
188
  where
189 190 191
    kind   = substTy subst (tyVarKind tv)
    new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv

192
tcInstSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
193
tcInstSkolTyVars = tcInstSkolTyVars' False emptyTvSubst
194

195 196
tcInstSuperSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTvSubst
dreixel's avatar
dreixel committed
197

198 199
tcInstSuperSkolTyVarsX :: TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
200

201 202 203
tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
204
-- Get the location from the monad; this is a complete freshening operation
205
tcInstSkolTyVars' overlappable subst tvs
206
  = do { loc <- getSrcSpanM
207 208 209 210 211 212 213
       ; instSkolTyVarsX (mkTcSkolTyVar loc overlappable) subst tvs }

mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar
mkTcSkolTyVar loc overlappable uniq old_name kind
  = mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
              kind
              (SkolemTv overlappable)
214

215 216
tcInstSigTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
-- We specify the location
217
tcInstSigTyVarsLoc loc = instSkolTyVars (mkTcSkolTyVar loc False)
218 219 220

tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
-- Get the location from the TyVar itself, not the monad
221 222
tcInstSigTyVars
  = instSkolTyVars mk_tv
223
  where
224 225
    mk_tv uniq old_name kind
       = mkTcTyVar (setNameUnique old_name uniq) kind (SkolemTv False)
226

227
tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
228 229
-- Instantiate a type with fresh skolem constants
-- Binding location comes from the monad
230
tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
231

232 233 234 235 236 237 238 239
------------------
freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
-- ^ Give fresh uniques to a bunch of TyVars, but they stay
--   as TyVars, rather than becoming TcTyVars
-- Used in FamInst.newFamInst, and Inst.newClsInst
freshenTyVarBndrs = instSkolTyVars mk_tv
  where
    mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
240

241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258
------------------
instSkolTyVars :: (Unique -> Name -> Kind -> TyVar)
                -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
instSkolTyVars mk_tv = instSkolTyVarsX mk_tv emptyTvSubst

instSkolTyVarsX :: (Unique -> Name -> Kind -> TyVar)
                -> TvSubst -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TyVar])
instSkolTyVarsX mk_tv = mapAccumLM (instSkolTyVarX mk_tv)

instSkolTyVarX :: (Unique -> Name -> Kind -> TyVar)
               -> TvSubst -> TyVar -> TcRnIf gbl lcl (TvSubst, TyVar)
instSkolTyVarX mk_tv subst tyvar
  = do  { uniq <- newUnique
        ; let new_tv = mk_tv uniq old_name kind
        ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
  where
    old_name = tyVarName tyvar
    kind     = substTy subst (tyVarKind tyvar)
259

Austin Seipp's avatar
Austin Seipp committed
260
{-
dreixel's avatar
dreixel committed
261 262 263 264 265 266 267 268 269 270 271 272 273 274 275
Note [Kind substitution when instantiating]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we instantiate a bunch of kind and type variables, first we
expect them to be sorted (kind variables first, then type variables).
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
  [(k1 :: BOX), (k2 :: BOX), (a :: k1 -> k2), (b :: k1)]
we want
  [(?k1 :: BOX), (?k2 :: BOX), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
instead of the buggous
  [(?k1 :: BOX), (?k2 :: BOX), (?a :: k1 -> k2), (?b :: k1)]

276

Austin Seipp's avatar
Austin Seipp committed
277 278
************************************************************************
*                                                                      *
279
        MetaTvs (meta type variables; mutable)
Austin Seipp's avatar
Austin Seipp committed
280 281 282
*                                                                      *
************************************************************************
-}
283

284
newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
285
-- Make a new meta tyvar out of thin air
286
newMetaTyVar meta_info kind
287
  = do  { uniq <- newUnique
288 289
        ; let name = mkTcTyVarName uniq s
              s = case meta_info of
thomasw's avatar
thomasw committed
290 291 292 293 294
                        ReturnTv    -> fsLit "r"
                        TauTv True  -> fsLit "w"
                        TauTv False -> fsLit "t"
                        FlatMetaTv  -> fsLit "fmv"
                        SigTv       -> fsLit "a"
295
        ; details <- newMetaDetails meta_info
296
        ; return (mkTcTyVar name kind details) }
297

thomasw's avatar
thomasw committed
298 299 300 301 302 303
newNamedMetaTyVar :: Name -> MetaInfo -> Kind -> TcM TcTyVar
-- Make a new meta tyvar out of thin air
newNamedMetaTyVar name meta_info kind
  = do { details <- newMetaDetails meta_info
       ; return (mkTcTyVar name kind details) }

304 305 306 307 308 309 310 311 312 313 314 315
newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
  = do { uniq <- newUnique
       ; let name' = setNameUnique name uniq
                      -- Use the same OccName so that the tidy-er
                      -- doesn't gratuitously rename 'a' to 'a0' etc
       ; details <- newMetaDetails SigTv
       ; return (mkTcTyVar name' kind details) }

newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails info
  = do { ref <- newMutVar Flexi
316 317
       ; tclvl <- getTcLevel
       ; return (MetaTv { mtv_info = info, mtv_ref = ref, mtv_tclvl = tclvl }) }
318

319 320 321
cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
cloneMetaTyVar tv
  = ASSERT( isTcTyVar tv )
322
    do  { uniq <- newUnique
323 324
        ; ref  <- newMutVar Flexi
        ; let name'    = setNameUnique (tyVarName tv) uniq
325
              details' = case tcTyVarDetails tv of
326 327 328 329
                           details@(MetaTv {}) -> details { mtv_ref = ref }
                           _ -> pprPanic "cloneMetaTyVar" (ppr tv)
        ; return (mkTcTyVar name' (tyVarKind tv) details') }

330 331 332
mkTcTyVarName :: Unique -> FastString -> Name
mkTcTyVarName uniq str = mkSysTvName uniq str

dreixel's avatar
dreixel committed
333
-- Works for both type and kind variables
334 335
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
336
                      readMutVar (metaTvRef tyvar)
337

338 339 340 341
isFilledMetaTyVar :: TyVar -> TcM Bool
-- True of a filled-in (Indirect) meta type variable
isFilledMetaTyVar tv
  | not (isTcTyVar tv) = return False
342
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
343 344
  = do  { details <- readMutVar ref
        ; return (isIndirect details) }
345 346
  | otherwise = return False

347
isUnfilledMetaTyVar :: TyVar -> TcM Bool
348
-- True of a un-filled-in (Flexi) meta type variable
349
isUnfilledMetaTyVar tv
350
  | not (isTcTyVar tv) = return False
351
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
352 353
  = do  { details <- readMutVar ref
        ; return (isFlexi details) }
354 355 356
  | otherwise = return False

--------------------
dreixel's avatar
dreixel committed
357
-- Works with both type and kind variables
358
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
359 360
-- Write into a currently-empty MetaTyVar

Ian Lynagh's avatar
Ian Lynagh committed
361
writeMetaTyVar tyvar ty
362
  | not debugIsOn
363 364 365 366 367 368 369
  = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty

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

370
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
371 372 373 374
  = writeMetaTyVarRef tyvar ref ty

  | otherwise
  = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
375
    return ()
376 377 378

--------------------
writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
379
-- Here the tyvar is for error checking only;
380 381
-- the ref cell must be for the same tyvar
writeMetaTyVarRef tyvar ref ty
382
  | not debugIsOn
383 384 385 386
  = do { traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
       ; writeMutVar ref (Indirect ty) }

-- Everything from here on only happens if DEBUG is on
387
  | otherwise
388
  = do { meta_details <- readMutVar ref;
dreixel's avatar
dreixel committed
389
       -- Zonk kinds to allow the error check to work
390
       ; zonked_tv_kind <- zonkTcKind tv_kind
dreixel's avatar
dreixel committed
391 392 393
       ; zonked_ty_kind <- zonkTcKind ty_kind

       -- Check for double updates
394
       ; ASSERT2( isFlexi meta_details,
395
                  hang (text "Double update of meta tyvar")
396 397 398
                   2 (ppr tyvar $$ ppr meta_details) )

         traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
399 400
       ; writeMutVar ref (Indirect ty)
       ; when (   not (isPredTy tv_kind)
dreixel's avatar
dreixel committed
401
                    -- Don't check kinds for updates to coercion variables
402
               && not (zonked_ty_kind `tcIsSubKind` zonked_tv_kind))
dreixel's avatar
dreixel committed
403
       $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
404 405 406
                        2 (    ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
                           <+> text ":="
                           <+> ppr ty    <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) )
dreixel's avatar
dreixel committed
407
         (return ()) }
408 409 410
  where
    tv_kind = tyVarKind tyvar
    ty_kind = typeKind ty
411

Austin Seipp's avatar
Austin Seipp committed
412 413 414
{-
************************************************************************
*                                                                      *
415
        MetaTvs: TauTvs
Austin Seipp's avatar
Austin Seipp committed
416 417 418
*                                                                      *
************************************************************************
-}
419 420

newFlexiTyVar :: Kind -> TcM TcTyVar
thomasw's avatar
thomasw committed
421
newFlexiTyVar kind = newMetaTyVar (TauTv False) kind
422 423

newFlexiTyVarTy  :: Kind -> TcM TcType
424 425 426
newFlexiTyVarTy kind = do
    tc_tyvar <- newFlexiTyVar kind
    return (TyVarTy tc_tyvar)
427 428

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

431 432
newReturnTyVar :: Kind -> TcM TcTyVar
newReturnTyVar kind = newMetaTyVar ReturnTv kind
433

434 435 436
newReturnTyVarTy :: Kind -> TcM TcType
newReturnTyVarTy kind = TyVarTy <$> newReturnTyVar kind

437
tcInstTyVars :: [TKVar] -> TcM (TvSubst, [TcTyVar])
438
-- Instantiate with META type variables
439 440 441
-- Note that this works for a sequence of kind and type
-- variables.  Eg    [ (k:BOX), (a:k->k) ]
--             Gives [ (k7:BOX), (a8:k7->k7) ]
442
tcInstTyVars tyvars = mapAccumLM tcInstTyVarX emptyTvSubst tyvars
dreixel's avatar
dreixel committed
443 444 445 446
    -- emptyTvSubst has an empty in-scope set, but that's fine here
    -- Since the tyvars are freshly made, they cannot possibly be
    -- captured by any existing for-alls.

447
tcInstTyVarX :: TvSubst -> TKVar -> TcM (TvSubst, TcTyVar)
dreixel's avatar
dreixel committed
448 449
-- Make a new unification variable tyvar whose Name and Kind come from
-- an existing TyVar. We substitute kind variables in the kind.
450
tcInstTyVarX subst tyvar
451
  = do  { uniq <- newUnique
thomasw's avatar
thomasw committed
452
        ; details <- newMetaDetails (TauTv False)
dreixel's avatar
dreixel committed
453
        ; let name   = mkSystemName uniq (getOccName tyvar)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
454
                       -- See Note [Name of an instantiated type variable]
dreixel's avatar
dreixel committed
455
              kind   = substTy subst (tyVarKind tyvar)
456
              new_tv = mkTcTyVar name kind details
dreixel's avatar
dreixel committed
457
        ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
458

Simon Peyton Jones's avatar
Simon Peyton Jones committed
459 460 461 462 463
{- 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
464 465
************************************************************************
*                                                                      *
466
             Quantification
Austin Seipp's avatar
Austin Seipp committed
467 468
*                                                                      *
************************************************************************
469

470 471 472 473
Note [quantifyTyVars]
~~~~~~~~~~~~~~~~~~~~~
quantifyTyVars is give the free vars of a type that we
are about to wrap in a forall.
474

475
It takes these free type/kind variables and
476 477 478 479
  1. Zonks them and remove globals
  2. Partitions into type and kind variables (kvs1, tvs)
  3. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
  4. Calls zonkQuantifiedTyVar on each
480

481 482 483 484 485 486
Step (3) is often unimportant, because the kind variable is often
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).
Austin Seipp's avatar
Austin Seipp committed
487
-}
488

489 490
quantifyTyVars :: TcTyVarSet -> TcTyVarSet -> TcM [TcTyVar]
-- See Note [quantifyTyVars]
491
-- The input is a mixture of type and kind variables; a kind variable k
492
--   may occur *after* a tyvar mentioning k in its kind
493
-- Can be given a mixture of TcTyVars and TyVars, in the case of
494 495 496 497 498
--   associated type declarations

quantifyTyVars gbl_tvs tkvs
  = do { tkvs    <- zonkTyVarsAndFV tkvs
       ; gbl_tvs <- zonkTyVarsAndFV gbl_tvs
499
       ; let (kvs, tvs) = partitionVarSet isKindVar (closeOverKinds tkvs `minusVarSet` gbl_tvs)
500
                              -- NB kinds of tvs are zonked by zonkTyVarsAndFV
501
             kvs2 = varSetElems kvs
502
             qtvs = varSetElems tvs
503

dreixel's avatar
dreixel committed
504 505
             -- In the non-PolyKinds case, default the kind variables
             -- to *, and zonk the tyvars as usual.  Notice that this
506
             -- may make quantifyTyVars return a shorter list
dreixel's avatar
dreixel committed
507
             -- than it was passed, but that's ok
508
       ; poly_kinds <- xoptM Opt_PolyKinds
509
       ; qkvs <- if poly_kinds
510 511 512 513
                 then return kvs2
                 else do { let (meta_kvs, skolem_kvs) = partition is_meta kvs2
                               is_meta kv = isTcTyVar kv && isMetaTyVar kv
                         ; mapM_ defaultKindVarToStar meta_kvs
514
                         ; return skolem_kvs }  -- should be empty
515

516
       ; mapM zonk_quant (qkvs ++ qtvs) }
517 518 519
           -- Because of the order, any kind variables
           -- mentioned in the kinds of the type variables refer to
           -- the now-quantified versions
520 521 522 523
  where
    zonk_quant tkv
      | isTcTyVar tkv = zonkQuantifiedTyVar tkv
      | otherwise     = return tkv
524
      -- For associated types, we have the class variables
525
      -- in scope, and they are TyVars not TcTyVars
526

527
zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
528 529 530
-- The quantified type variables often include meta type variables
-- we want to freeze them into ordinary type variables, and
-- default their kind (e.g. from OpenTypeKind to TypeKind)
531 532 533
--                      -- see notes with Kind.defaultKind
-- The meta tyvar is updated to point to the new skolem TyVar.  Now any
-- bound occurrences of the original type variable will get zonked to
534 535
-- the immutable version.
--
536
-- We leave skolem TyVars alone; they are immutable.
dreixel's avatar
dreixel committed
537 538 539
--
-- This function is called on both kind and type variables,
-- but kind variables *only* if PolyKinds is on.
540
zonkQuantifiedTyVar tv
541
  = ASSERT2( isTcTyVar tv, ppr tv )
542
    case tcTyVarDetails tv of
dreixel's avatar
dreixel committed
543
      SkolemTv {} -> do { kind <- zonkTcKind (tyVarKind tv)
544
                        ; return $ setTyVarKind tv kind }
545 546
        -- It might be a skolem type variable,
        -- for example from a user type signature
547

548
      MetaTv { mtv_ref = ref } ->
Ian Lynagh's avatar
Ian Lynagh committed
549 550 551 552 553 554 555 556 557
          do when debugIsOn $ do
                 -- [Sept 04] Check for non-empty.
                 -- See note [Silly Type Synonym]
                 cts <- readMutVar ref
                 case cts of
                     Flexi -> return ()
                     Indirect ty -> WARN( True, ppr tv $$ ppr ty )
                                    return ()
             skolemiseUnboundMetaTyVar tv vanillaSkolemTv
558 559
      _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk

560 561
defaultKindVarToStar :: TcTyVar -> TcM Kind
-- We have a meta-kind: unify it with '*'
562
defaultKindVarToStar kv
563
  = do { ASSERT( isKindVar kv && isMetaTyVar kv )
564 565 566
         writeMetaTyVar kv liftedTypeKind
       ; return liftedTypeKind }

567
skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
568 569 570 571 572
-- We have a Meta tyvar with a ref-cell inside it
-- Skolemise it, including giving it a new Name, so that
--   we are totally out of Meta-tyvar-land
-- We create a skolem TyVar, not a regular TyVar
--   See Note [Zonking to Skolem]
573
skolemiseUnboundMetaTyVar tv details
574
  = ASSERT2( isMetaTyVar tv, ppr tv )
575 576 577
    do  { span <- getSrcSpanM    -- Get the location from "here"
                                 -- ie where we are generalising
        ; uniq <- newUnique      -- Remove it from TcMetaTyVar unique land
dreixel's avatar
dreixel committed
578
        ; kind <- zonkTcKind (tyVarKind tv)
thomasw's avatar
thomasw committed
579 580 581 582 583 584
        ; let tv_name = getOccName tv
              new_tv_name = if isWildcardVar tv
                            then generaliseWildcardVarName tv_name
                            else tv_name
              final_name = mkInternalName uniq new_tv_name span
              final_kind = defaultKind kind
585
              final_tv   = mkTcTyVar final_name final_kind details
dreixel's avatar
dreixel committed
586

587
        ; traceTc "Skolemising" (ppr tv <+> ptext (sLit ":=") <+> ppr final_tv)
dreixel's avatar
dreixel committed
588 589
        ; writeMetaTyVar tv (mkTyVarTy final_tv)
        ; return final_tv }
thomasw's avatar
thomasw committed
590
  where
591
    -- If a wildcard type called _a is generalised, we rename it to w_a
thomasw's avatar
thomasw committed
592 593 594 595
    generaliseWildcardVarName :: OccName -> OccName
    generaliseWildcardVarName name | startsWithUnderscore name
      = mkOccNameFS (occNameSpace name) (appendFS (fsLit "w") (occNameFS name))
    generaliseWildcardVarName name = name
596

Austin Seipp's avatar
Austin Seipp committed
597
{-
598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631
Note [Zonking to Skolem]
~~~~~~~~~~~~~~~~~~~~~~~~
We used to zonk quantified type variables to regular TyVars.  However, this
leads to problems.  Consider this program from the regression test suite:

  eval :: Int -> String -> String -> String
  eval 0 root actual = evalRHS 0 root actual

  evalRHS :: Int -> a
  evalRHS 0 root actual = eval 0 root actual

It leads to the deferral of an equality (wrapped in an implication constraint)

  forall a. () => ((String -> String -> String) ~ a)

which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
In the meantime `a' is zonked and quantified to form `evalRHS's signature.
This has the *side effect* of also zonking the `a' in the deferred equality
(which at this point is being handed around wrapped in an implication
constraint).

Finally, the equality (with the zonked `a') will be handed back to the
simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
If we zonk `a' with a regular type variable, we will have this regular type
variable now floating around in the simplifier, which in many places assumes to
only see proper TcTyVars.

We can avoid this problem by zonking with a skolem.  The skolem is rigid
(which we require for a quantified variable), but is still a TcTyVar that the
simplifier knows how to deal with.

Note [Silly Type Synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:
632
        type C u a = u  -- Note 'a' unused
633

634 635
        foo :: (forall a. C u a -> C u a) -> u
        foo x = ...
636

637 638
        bar :: Num u => u
        bar = foo (\t -> t + t)
639 640 641 642 643

* From the (\t -> t+t) we get type  {Num d} =>  d -> d
  where d is fresh.

* Now unify with type of foo's arg, and we get:
644
        {Num (C d a)} =>  C d a -> C d a
645 646 647 648 649
  where a is fresh.

* Now abstract over the 'a', but float out the Num (C d a) constraint
  because it does not 'really' mention a.  (see exactTyVarsOfType)
  The arg to foo becomes
650
        \/\a -> \t -> t+t
651 652

* So we get a dict binding for Num (C d a), which is zonked to give
653
        a = ()
654 655 656 657 658 659 660 661 662 663
  [Note Sept 04: now that we are zonking quantified type variables
  on construction, the 'a' will be frozen as a regular tyvar on
  quantification, so the floated dict will still have type (C d a).
  Which renders this whole note moot; happily!]

* Then the \/\a abstraction has a zonked 'a' in it.

All very silly.   I think its harmless to ignore the problem.  We'll end up with
a \/\a in the final result but all the occurrences of a will be zonked to ()

Austin Seipp's avatar
Austin Seipp committed
664 665
************************************************************************
*                                                                      *
666
              Zonking types
Austin Seipp's avatar
Austin Seipp committed
667 668
*                                                                      *
************************************************************************
669 670 671 672

@tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
To improve subsequent calls to the same function it writes the zonked set back into
the environment.
Austin Seipp's avatar
Austin Seipp committed
673
-}
674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697

tcGetGlobalTyVars :: TcM TcTyVarSet
tcGetGlobalTyVars
  = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
       ; gbl_tvs  <- readMutVar gtv_var
       ; gbl_tvs' <- zonkTyVarsAndFV gbl_tvs
       ; writeMutVar gtv_var gbl_tvs'
       ; return gbl_tvs' }
  where

zonkTcTypeAndFV :: TcType -> TcM TyVarSet
-- Zonk a type and take its free variables
-- With kind polymorphism it can be essential to zonk *first*
-- so that we find the right set of free variables.  Eg
--    forall k1. forall (a:k2). a
-- where k2:=k1 is in the substitution.  We don't want
-- k2 to look free in this type!
zonkTcTypeAndFV ty = do { ty <- zonkTcType ty; return (tyVarsOfType ty) }

zonkTyVar :: TyVar -> TcM TcType
-- Works on TyVars and TcTyVars
zonkTyVar tv | isTcTyVar tv = zonkTcTyVar tv
             | otherwise    = return (mkTyVarTy tv)
   -- Hackily, when typechecking type and class decls
698
   -- we have TyVars in scopeadded (only) in
699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721
   -- TcHsType.tcTyClTyVars, but it seems
   -- painful to make them into TcTyVars there

zonkTyVarsAndFV :: TyVarSet -> TcM TyVarSet
zonkTyVarsAndFV tyvars = tyVarsOfTypes <$> mapM zonkTyVar (varSetElems tyvars)

zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars

-----------------  Types
zonkTyVarKind :: TyVar -> TcM TyVar
zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
                      ; return (setTyVarKind tv kind') }

zonkTcTypes :: [TcType] -> TcM [TcType]
zonkTcTypes tys = mapM zonkTcType tys

zonkTcThetaType :: TcThetaType -> TcM TcThetaType
zonkTcThetaType theta = mapM zonkTcPredType theta

zonkTcPredType :: TcPredType -> TcM TcPredType
zonkTcPredType = zonkTcType

Austin Seipp's avatar
Austin Seipp committed
722 723 724
{-
************************************************************************
*                                                                      *
725
              Zonking constraints
Austin Seipp's avatar
Austin Seipp committed
726 727 728
*                                                                      *
************************************************************************
-}
729

730
zonkImplication :: Implication -> TcM Implication
731
zonkImplication implic@(Implic { ic_skols  = skols
732
                               , ic_given  = given
733
                               , ic_wanted = wanted
734
                               , ic_info   = info })
735 736
  = do { skols'  <- mapM zonkTcTyVarBndr skols  -- Need to zonk their kinds!
                                                -- as Trac #7230 showed
737
       ; given'  <- mapM zonkEvVar given
738
       ; info'   <- zonkSkolemInfo info
739
       ; wanted' <- zonkWCRec wanted
740 741 742 743
       ; return (implic { ic_skols  = skols'
                        , ic_given  = given'
                        , ic_wanted = wanted'
                        , ic_info   = info' }) }
744 745 746 747 748

zonkEvVar :: EvVar -> TcM EvVar
zonkEvVar var = do { ty' <- zonkTcType (varType var)
                   ; return (setVarType var ty') }

749

750 751
zonkWC :: WantedConstraints -> TcM WantedConstraints
zonkWC wc = zonkWCRec wc
752

753
zonkWCRec :: WantedConstraints -> TcM WantedConstraints
754 755
zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
  = do { simple' <- zonkSimples simple
756
       ; implic' <- mapBagM zonkImplication implic
757 758
       ; insol'  <- zonkSimples insol
       ; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
759

760 761 762 763
zonkSimples :: Cts -> TcM Cts
zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
                     ; traceTc "zonkSimples done:" (ppr cts')
                     ; return cts' }
764 765 766

zonkCt' :: Ct -> TcM Ct
zonkCt' ct = zonkCt ct
767

768
zonkCt :: Ct -> TcM Ct
769 770 771
zonkCt ct@(CHoleCan { cc_ev = ev })
  = do { ev' <- zonkCtEvidence ev
       ; return $ ct { cc_ev = ev' } }
772
zonkCt ct
773
  = do { fl' <- zonkCtEvidence (cc_ev ct)
774
       ; return (mkNonCanonical fl') }
775

776
zonkCtEvidence :: CtEvidence -> TcM CtEvidence
777
zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
778 779
  = do { pred' <- zonkTcType pred
       ; return (ctev { ctev_pred = pred'}) }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
780
zonkCtEvidence ctev@(CtWanted { ctev_pred = pred })
781 782
  = do { pred' <- zonkTcType pred
       ; return (ctev { ctev_pred = pred' }) }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
783
zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
784 785
  = do { pred' <- zonkTcType pred
       ; return (ctev { ctev_pred = pred' }) }
786 787 788 789 790 791 792 793 794

zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
zonkSkolemInfo (SigSkol cx ty)  = do { ty' <- zonkTcType ty
                                     ; return (SigSkol cx ty') }
zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
                                     ; return (InferSkol ntys') }
  where
    do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
zonkSkolemInfo skol_info = return skol_info
795

Austin Seipp's avatar
Austin Seipp committed
796 797 798
{-
************************************************************************
*                                                                      *
799
\subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
Austin Seipp's avatar
Austin Seipp committed
800 801 802 803 804
*                                                                      *
*              For internal use only!                                  *
*                                                                      *
************************************************************************
-}
805

806 807 808 809 810 811
-- zonkId is used *during* typechecking just to zonk the Id's type
zonkId :: TcId -> TcM TcId
zonkId id
  = do { ty' <- zonkTcType (idType id)
       ; return (Id.setIdType id ty') }

812 813
-- For unbound, mutable tyvars, zonkType uses the function given to it
-- For tyvars bound at a for-all, zonkType zonks them to an immutable
814
--      type variable and zonks the kind too
815

816 817
zonkTcType :: TcType -> TcM TcType
zonkTcType ty
818 819
  = go ty
  where
820 821
    go (TyConApp tc tys) = do tys' <- mapM go tys
                              return (TyConApp tc tys')
822 823 824
                -- Do NOT establish Type invariants, because
                -- doing so is strict in the TyCOn.
                -- See Note [Zonking inside the knot] in TcHsType
825

826
    go (LitTy n)         = return (LitTy n)
827

828 829 830 831 832 833 834
    go (FunTy arg res)   = do arg' <- go arg
                              res' <- go res
                              return (FunTy arg' res')

    go (AppTy fun arg)   = do fun' <- go fun
                              arg' <- go arg
                              return (mkAppTy fun' arg')
835 836 837
                -- NB the mkAppTy; we might have instantiated a
                -- type variable to a type constructor, so we need
                -- to pull the TyConApp to the top.
838 839 840
                -- OK to do this because only strict in the structure
                -- not in the TyCon.
                -- See Note [Zonking inside the knot] in TcHsType
841

842
        -- The two interesting cases!
843
    go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
844 845
                       | otherwise       = TyVarTy <$> updateTyVarKindM go tyvar
                -- Ordinary (non Tc) tyvars occur inside quantified types
846

847 848 849 850 851 852
    go (ForAllTy tv ty) = do { tv' <- zonkTcTyVarBndr tv
                             ; ty' <- go ty
                             ; return (ForAllTy tv' ty') }

zonkTcTyVarBndr :: TcTyVar -> TcM TcTyVar
-- A tyvar binder is never a unification variable (MetaTv),
853
-- rather it is always a skolems.  BUT it may have a kind
854 855 856 857 858
-- that has not yet been zonked, and may include kind
-- unification variables.
zonkTcTyVarBndr tyvar
  = ASSERT2( isImmutableTyVar tyvar, ppr tyvar ) do
    updateTyVarKindM zonkTcType tyvar