TcMType.lhs 36 KB
Newer Older
1
%
2
% (c) The University of Glasgow 2006
3
4
5
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
%

6
7
8
9
Monadic type operations

This module contains monadic operations over types that contain
mutable type variables
10
11

\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
12
13
14
15
16
17
18
{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

19
module TcMType (
20
  TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
21
22
23

  --------------------------------
  -- Creating new mutable type variables
24
  newFlexiTyVar,
25
26
  newFlexiTyVarTy,		-- Kind -> TcM TcType
  newFlexiTyVarTys,		-- Int -> Kind -> TcM [TcType]
27
  newPolyFlexiTyVarTy,
28
  newMetaKindVar, newMetaKindVars, mkKindSigVar,
29
  mkTcTyVarName, cloneMetaTyVar, 
30

31
  newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
32
  newMetaDetails, isFilledMetaTyVar, isFlexiMetaTyVar,
33
34

  --------------------------------
35
  -- Creating new evidence variables
36
  newEvVar, newEvVars, newEq, newDict,
37
  newWantedEvVar, newWantedEvVars,
38
  newTcEvBinds, addTcEvBind,
39
  newFlatWanteds,
40

41
42
  --------------------------------
  -- Instantiation
43
  tcInstTyVars, tcInstSigTyVars, newSigTyVar,
Simon Peyton Jones's avatar
Simon Peyton Jones committed
44
  tcInstType, 
45
  tcInstSkolTyVars, tcInstSkolTyVarsLoc, tcInstSuperSkolTyVars,
46
47
  tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX,
  tcInstSkolTyVar, tcInstSkolType,
48
  tcSkolDFunType, tcSuperSkolTyVars,
49

50
  --------------------------------
51
  growThetaTyVars, quantifyPred, 
52

53
54
  --------------------------------
  -- Zonking
55
  zonkTcPredType, 
56
  skolemiseSigTv, skolemiseUnboundMetaTyVar,
57
  zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, 
58
  zonkQuantifiedTyVar, zonkQuantifiedTyVars,
Ian Lynagh's avatar
Ian Lynagh committed
59
  zonkTcType, zonkTcTypes, zonkTcThetaType,
60

61
  zonkTcKind, defaultKindVarToStar,
62
  zonkEvVar, zonkWC, zonkId, zonkCt, zonkCts, zonkSkolemInfo,
63

64
  tcGetGlobalTyVars, 
65
66
67
68
69
  ) where

#include "HsVersions.h"

-- friends:
70
71
import TypeRep
import TcType
72
import TcEvidence
73
74
75
76
import Type
import Class
import TyCon
import Var
77
78

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

Ian Lynagh's avatar
Ian Lynagh committed
91
import Control.Monad
92
import Data.List        ( partition, mapAccumL )
93
94
95
96
97
\end{code}


%************************************************************************
%*									*
98
	Kind variables
99
100
101
102
%*									*
%************************************************************************

\begin{code}
103
104
105
106
107
108
109
mkKindName :: Unique -> Name
mkKindName unique = mkSystemName unique kind_var_occ

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

dreixel's avatar
dreixel committed
110
newMetaKindVar :: TcM TcKind
111
newMetaKindVar = do { uniq <- newUnique
112
113
114
		    ; details <- newMetaDetails TauTv
                    ; let kv = mkTcTyVar (mkKindName uniq) superKind details
		    ; return (mkTyVarTy kv) }
115

dreixel's avatar
dreixel committed
116
117
newMetaKindVars :: Int -> TcM [TcKind]
newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
118
119
120
121

mkKindSigVar :: Name -> KindVar
-- Use the specified name; don't clone it
mkKindSigVar n = mkTcTyVar n superKind (SkolemTv False)
122
\end{code}
123
124


125
126
%************************************************************************
%*									*
127
     Evidence variables; range over constraints we can abstract over
128
129
130
131
%*									*
%************************************************************************

\begin{code}
132
133
134
135
newEvVars :: TcThetaType -> TcM [EvVar]
newEvVars theta = mapM newEvVar theta

newWantedEvVar :: TcPredType -> TcM EvVar 
batterseapower's avatar
batterseapower committed
136
newWantedEvVar = newEvVar
137
138
139
140

newWantedEvVars :: TcThetaType -> TcM [EvVar] 
newWantedEvVars theta = mapM newWantedEvVar theta 

141
--------------
batterseapower's avatar
batterseapower committed
142

143
144
newEvVar :: TcPredType -> TcM EvVar
-- Creates new *rigid* variables for predicates
145
newEvVar ty = do { name <- newSysName (predTypeOccName ty) 
batterseapower's avatar
batterseapower committed
146
                 ; return (mkLocalId name ty) }
147

batterseapower's avatar
batterseapower committed
148
149
newEq :: TcType -> TcType -> TcM EvVar
newEq ty1 ty2
150
  = do { name <- newSysName (mkVarOccFS (fsLit "cobox"))
151
       ; return (mkLocalId name (mkTcEqPred ty1 ty2)) }
152
153
154

newDict :: Class -> [TcType] -> TcM DictId
newDict cls tys 
155
  = do { name <- newSysName (mkDictOcc (getOccName cls))
batterseapower's avatar
batterseapower committed
156
157
158
       ; return (mkLocalId name (mkClassPred cls tys)) }

predTypeOccName :: PredType -> OccName
159
predTypeOccName ty = case classifyPredType ty of
batterseapower's avatar
batterseapower committed
160
161
162
163
    ClassPred cls _ -> mkDictOcc (getOccName cls)
    EqPred _ _      -> mkVarOccFS (fsLit "cobox")
    TuplePred _     -> mkVarOccFS (fsLit "tup")
    IrredPred _     -> mkVarOccFS (fsLit "irred")
164
165
\end{code}

166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
*********************************************************************************
*                                                                               * 
*                   Wanted constraints
*                                                                               *
*********************************************************************************

\begin{code}
newFlatWanteds :: CtOrigin -> ThetaType -> TcM [Ct]
newFlatWanteds orig theta
  = do { loc <- getCtLoc orig
       ; mapM (inst_to_wanted loc) theta }
  where 
    inst_to_wanted loc pty 
          = do { v <- newWantedEvVar pty 
               ; return $ mkNonCanonical loc $
                 CtWanted { ctev_evar = v
                          , ctev_pred = pty } }
\end{code}
184

185
186
%************************************************************************
%*									*
187
	SkolemTvs (immutable)
188
189
%*									*
%************************************************************************
190

191
\begin{code}
192
tcInstType :: ([TyVar] -> TcM (TvSubst, [TcTyVar]))     -- How to instantiate the type variables
193
194
195
196
197
198
199
200
201
202
	   -> TcType 					-- Type to instantiate
	   -> TcM ([TcTyVar], TcThetaType, TcType)	-- Result
		-- (type vars (excl coercion vars), preds (incl equalities), rho)
tcInstType inst_tyvars ty
  = case tcSplitForAllTys ty of
	([],     rho) -> let	-- There may be overloading despite no type variables;
				-- 	(?x :: Int) => Int -> Int
			   (theta, tau) = tcSplitPhiTy rho
			 in
			 return ([], theta, tau)
203

204
205
	(tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
			    ; let (theta, tau) = tcSplitPhiTy (substTy subst rho)
206
			    ; return (tyvars', theta, tau) }
207

208
tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
209
210
-- Instantiate a type signature with skolem constants, but 
-- do *not* give them fresh names, because we want the name to
211
-- be in the type environment: it is lexically scoped.
212
tcSkolDFunType ty = tcInstType (\tvs -> return (tcSuperSkolTyVars tvs)) ty
213

214
tcSuperSkolTyVars :: [TyVar] -> (TvSubst, [TcTyVar])
215
-- Make skolem constants, but do *not* give them new names, as above
216
-- Moreover, make them "super skolems"; see comments with superSkolemTv
dreixel's avatar
dreixel committed
217
-- see Note [Kind substitution when instantiating]
218
-- Precondition: tyvars should be ordered (kind vars first)
219
tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar (mkTopTvSubst [])
220
221
222
223

tcSuperSkolTyVar :: TvSubst -> TyVar -> (TvSubst, TcTyVar)
tcSuperSkolTyVar subst tv
  = (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv)
dreixel's avatar
dreixel committed
224
  where
225
226
227
    kind   = substTy subst (tyVarKind tv)
    new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv

228
229
tcInstSkolTyVar :: SrcSpan -> Bool -> TvSubst -> TyVar
                -> TcRnIf gbl lcl (TvSubst, TcTyVar)
230
-- Instantiate the tyvar, using 
231
232
233
--      * the occ-name and kind of the supplied tyvar, 
--      * the unique from the monad,
--      * the location either from the tyvar (skol_info = SigSkol)
234
--                     or from the monad (otherwise)
235
tcInstSkolTyVar loc overlappable subst tyvar
236
237
238
239
  = do  { uniq <- newUnique
        ; let new_name = mkInternalName uniq occ loc
              new_tv   = mkTcTyVar new_name kind (SkolemTv overlappable)
        ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
240
241
242
  where
    old_name = tyVarName tyvar
    occ      = nameOccName old_name
dreixel's avatar
dreixel committed
243
    kind     = substTy subst (tyVarKind tyvar)
244

245
-- Wrappers
246
247
248
249
-- we need to be able to do this from outside the TcM monad:
tcInstSkolTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TvSubst, [TcTyVar])
tcInstSkolTyVarsLoc loc = mapAccumLM (tcInstSkolTyVar loc False) (mkTopTvSubst [])

250
251
252
253
tcInstSkolTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
tcInstSkolTyVars = tcInstSkolTyVarsX (mkTopTvSubst [])

tcInstSuperSkolTyVars :: [TyVar] -> TcM [TcTyVar]
254
tcInstSuperSkolTyVars = fmap snd . tcInstSkolTyVars' True  (mkTopTvSubst [])
dreixel's avatar
dreixel committed
255

256
257
258
259
tcInstSkolTyVarsX, tcInstSuperSkolTyVarsX
  :: TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
tcInstSkolTyVarsX      subst = tcInstSkolTyVars' False subst
tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True  subst
260

261
262
263
tcInstSkolTyVars' :: Bool -> TvSubst -> [TyVar] -> TcM (TvSubst, [TcTyVar])
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
264
265
266
tcInstSkolTyVars' isSuperSkol subst tvs
  = do { loc <- getSrcSpanM
       ; mapAccumLM (tcInstSkolTyVar loc isSuperSkol) subst tvs }
267

268
tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
269
270
-- Instantiate a type with fresh skolem constants
-- Binding location comes from the monad
271
tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
272

273
tcInstSigTyVars :: [TyVar] -> TcM (TvSubst, [TcTyVar])
274
275
-- Make meta SigTv type variables for patten-bound scoped type varaibles
-- We use SigTvs for them, so that they can't unify with arbitrary types
dreixel's avatar
dreixel committed
276
277
-- Precondition: tyvars should be ordered (kind vars first)
-- see Note [Kind substitution when instantiating]
278
279
280
tcInstSigTyVars = mapAccumLM tcInstSigTyVar (mkTopTvSubst [])
	-- The tyvars are freshly made, by tcInstSigTyVar
        -- So mkTopTvSubst [] is ok
281
282
283

tcInstSigTyVar :: TvSubst -> TyVar -> TcM (TvSubst, TcTyVar)
tcInstSigTyVar subst tv
284
285
286
287
288
  = do { new_tv <- newSigTyVar (tyVarName tv) (substTy subst (tyVarKind tv))
       ; return (extendTvSubst subst tv (mkTyVarTy new_tv), new_tv) }

newSigTyVar :: Name -> Kind -> TcM TcTyVar
newSigTyVar name kind
289
  = do { uniq <- newUnique
290
       ; let name' = setNameUnique name uniq
291
                      -- Use the same OccName so that the tidy-er
292
                      -- doesn't gratuitously rename 'a' to 'a0' etc
293
294
295
296
297
298
299
300
       ; details <- newMetaDetails SigTv
       ; return (mkTcTyVar name' kind details) }

newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails info 
  = do { ref <- newMutVar Flexi
       ; untch <- getUntouchables
       ; return (MetaTv { mtv_info = info, mtv_ref = ref, mtv_untch = untch }) }
301
302
\end{code}

dreixel's avatar
dreixel committed
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
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)]

318
319
320

%************************************************************************
%*									*
321
	MetaTvs (meta type variables; mutable)
322
323
324
325
%*									*
%************************************************************************

\begin{code}
326
newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
327
-- Make a new meta tyvar out of thin air
328
newMetaTyVar meta_info kind
329
  = do	{ uniq <- newUnique
330
331
        ; let name = mkTcTyVarName uniq s
              s = case meta_info of
332
333
334
                        PolyTv -> fsLit "s"
                        TauTv  -> fsLit "t"
                        SigTv  -> fsLit "a"
335
336
        ; details <- newMetaDetails meta_info
	; return (mkTcTyVar name kind details) }
337

338
339
340
341
342
343
344
345
346
347
348
cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
cloneMetaTyVar tv
  = ASSERT( isTcTyVar tv )
    do	{ uniq <- newUnique
        ; ref  <- newMutVar Flexi
        ; let name'    = setNameUnique (tyVarName tv) uniq
              details' = case tcTyVarDetails tv of 
                           details@(MetaTv {}) -> details { mtv_ref = ref }
                           _ -> pprPanic "cloneMetaTyVar" (ppr tv)
        ; return (mkTcTyVar name' (tyVarKind tv) details') }

349
350
351
352
353
mkTcTyVarName :: Unique -> FastString -> Name
-- Make sure that fresh TcTyVar names finish with a digit
-- leaving the un-cluttered names free for user names
mkTcTyVarName uniq str = mkSysTvName uniq str

dreixel's avatar
dreixel committed
354
-- Works for both type and kind variables
355
356
357
358
readMetaTyVar :: TyVar -> TcM MetaDetails
readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
		      readMutVar (metaTvRef tyvar)

359
360
361
362
isFilledMetaTyVar :: TyVar -> TcM Bool
-- True of a filled-in (Indirect) meta type variable
isFilledMetaTyVar tv
  | not (isTcTyVar tv) = return False
363
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
364
365
366
367
  = do 	{ details <- readMutVar ref
	; return (isIndirect details) }
  | otherwise = return False

368
369
370
371
isFlexiMetaTyVar :: TyVar -> TcM Bool
-- True of a un-filled-in (Flexi) meta type variable
isFlexiMetaTyVar tv
  | not (isTcTyVar tv) = return False
372
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
373
374
375
376
377
  = do 	{ details <- readMutVar ref
	; return (isFlexi details) }
  | otherwise = return False

--------------------
dreixel's avatar
dreixel committed
378
-- Works with both type and kind variables
379
writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
380
381
-- Write into a currently-empty MetaTyVar

Ian Lynagh's avatar
Ian Lynagh committed
382
writeMetaTyVar tyvar ty
383
384
385
386
387
388
389
390
  | not debugIsOn 
  = 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 ()

391
  | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
392
393
394
395
  = writeMetaTyVarRef tyvar ref ty

  | otherwise
  = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
396
    return ()
397
398
399
400
401
402
403
404
405
406
407

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

-- Everything from here on only happens if DEBUG is on
408
  | otherwise
409
  = do { meta_details <- readMutVar ref; 
dreixel's avatar
dreixel committed
410
411
412
413
414
       -- Zonk kinds to allow the error check to work
       ; zonked_tv_kind <- zonkTcKind tv_kind 
       ; zonked_ty_kind <- zonkTcKind ty_kind

       -- Check for double updates
415
416
       ; ASSERT2( isFlexi meta_details, 
                  hang (text "Double update of meta tyvar")
417
418
419
                   2 (ppr tyvar $$ ppr meta_details) )

         traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
dreixel's avatar
dreixel committed
420
421
422
       ; writeMutVar ref (Indirect ty) 
       ; when (   not (isPredTy tv_kind) 
                    -- Don't check kinds for updates to coercion variables
423
               && not (zonked_ty_kind `tcIsSubKind` zonked_tv_kind))
dreixel's avatar
dreixel committed
424
425
426
427
428
       $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
                        2 (    ppr tyvar <+> text "::" <+> ppr tv_kind 
                           <+> text ":=" 
                           <+> ppr ty    <+> text "::" <+> ppr ty_kind) )
         (return ()) }
429
430
431
  where
    tv_kind = tyVarKind tyvar
    ty_kind = typeKind ty
432
433
\end{code}

434
435
436
437
438
439
440
441
442
443
444
445

%************************************************************************
%*									*
	MetaTvs: TauTvs
%*									*
%************************************************************************

\begin{code}
newFlexiTyVar :: Kind -> TcM TcTyVar
newFlexiTyVar kind = newMetaTyVar TauTv kind

newFlexiTyVarTy  :: Kind -> TcM TcType
446
447
448
newFlexiTyVarTy kind = do
    tc_tyvar <- newFlexiTyVar kind
    return (TyVarTy tc_tyvar)
449
450

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

453
454
455
456
newPolyFlexiTyVarTy :: TcM TcType
newPolyFlexiTyVarTy = do { tv <- newMetaTyVar PolyTv liftedTypeKind
                         ; return (TyVarTy tv) }

457
tcInstTyVars :: [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
458
-- Instantiate with META type variables
459
460
461
-- Note that this works for a sequence of kind and type
-- variables.  Eg    [ (k:BOX), (a:k->k) ]
--             Gives [ (k7:BOX), (a8:k7->k7) ]
dreixel's avatar
dreixel committed
462
463
464
465
466
tcInstTyVars tyvars = tcInstTyVarsX emptyTvSubst tyvars
    -- 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.

467
468
tcInstTyVarsX :: TvSubst -> [TKVar] -> TcM ([TcTyVar], [TcType], TvSubst)
-- The "X" part is because of extending the substitution
dreixel's avatar
dreixel committed
469
tcInstTyVarsX subst tyvars =
470
  do { (subst', tyvars') <- mapAccumLM tcInstTyVarX subst tyvars
dreixel's avatar
dreixel committed
471
472
     ; return (tyvars', mkTyVarTys tyvars', subst') }

473
tcInstTyVarX :: TvSubst -> TKVar -> TcM (TvSubst, TcTyVar)
dreixel's avatar
dreixel committed
474
475
-- Make a new unification variable tyvar whose Name and Kind come from
-- an existing TyVar. We substitute kind variables in the kind.
476
tcInstTyVarX subst tyvar
477
478
  = do  { uniq <- newUnique
        ; details <- newMetaDetails TauTv
dreixel's avatar
dreixel committed
479
480
        ; let name   = mkSystemName uniq (getOccName tyvar)
              kind   = substTy subst (tyVarKind tyvar)
481
              new_tv = mkTcTyVar name kind details 
dreixel's avatar
dreixel committed
482
        ; return (extendTvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
483
484
485
486
487
\end{code}


%************************************************************************
%*									*
488
\subsection{Zonking -- the exernal interfaces}
489
490
491
%*									*
%************************************************************************

492
493
494
@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.
495
496

\begin{code}
497
498
499
tcGetGlobalTyVars :: TcM TcTyVarSet
tcGetGlobalTyVars
  = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
500
501
       ; gbl_tvs  <- readMutVar gtv_var
       ; gbl_tvs' <- zonkTyVarsAndFV gbl_tvs
502
503
       ; writeMutVar gtv_var gbl_tvs'
       ; return gbl_tvs' }
504
  where
505
506
507
508
509
\end{code}

-----------------  Type variables

\begin{code}
510
511
512
513
514
515
516
517
518
519
520
521
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
   -- we have TyVars in scopeadded (only) in 
   -- TcHsType.tcTyClTyVars, but it seems
   -- painful to make them into TcTyVars there

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

522
zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
523
zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
524
525

-----------------  Types
dreixel's avatar
dreixel committed
526
527
528
zonkTyVarKind :: TyVar -> TcM TyVar
zonkTyVarKind tv = do { kind' <- zonkTcKind (tyVarKind tv)
                      ; return (setTyVarKind tv kind') }
529

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

533
zonkTcThetaType :: TcThetaType -> TcM TcThetaType
534
zonkTcThetaType theta = mapM zonkTcPredType theta
535

536
zonkTcPredType :: TcPredType -> TcM TcPredType
batterseapower's avatar
batterseapower committed
537
zonkTcPredType = zonkTcType
538
539
540
541
542
543
\end{code}

-------------------  These ...ToType, ...ToKind versions
		     are used at the end of type checking

\begin{code}
dreixel's avatar
dreixel committed
544
defaultKindVarToStar :: TcTyVar -> TcM Kind
dreixel's avatar
dreixel committed
545
546
-- We have a meta-kind: unify it with '*'
defaultKindVarToStar kv 
547
  = do { ASSERT ( isKindVar kv && isMetaTyVar kv )
dreixel's avatar
dreixel committed
548
549
         writeMetaTyVar kv liftedTypeKind
       ; return liftedTypeKind }
dreixel's avatar
dreixel committed
550

551
zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
552
-- A kind variable k may occur *after* a tyvar mentioning k in its kind
dreixel's avatar
dreixel committed
553
zonkQuantifiedTyVars tyvars
554
  = do { let (kvs, tvs) = partition isKindVar tyvars
555
556
             (meta_kvs, skolem_kvs) = partition isMetaTyVar kvs

dreixel's avatar
dreixel committed
557
558
559
560
             -- In the non-PolyKinds case, default the kind variables
             -- to *, and zonk the tyvars as usual.  Notice that this
             -- may make zonkQuantifiedTyVars return a shorter list
             -- than it was passed, but that's ok
561
562
563
564
565
566
567
568
569
570
571
       ; poly_kinds <- xoptM Opt_PolyKinds
       ; qkvs <- if poly_kinds 
                 then return kvs
                 else WARN ( not (null skolem_kvs), ppr skolem_kvs )
                      do { mapM_ defaultKindVarToStar meta_kvs
                         ; return skolem_kvs }  -- Should be empty

       ; mapM zonkQuantifiedTyVar (qkvs ++ tvs) }
           -- Because of the order, any kind variables
           -- mentioned in the kinds of the type variables refer to
           -- the now-quantified versions
572

573
zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
574
575
576
577
-- 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)
-- 			-- see notes with Kind.defaultKind
578
-- The meta tyvar is updated to point to the new skolem TyVar.  Now any 
579
580
581
-- bound occurences of the original type variable will get zonked to 
-- the immutable version.
--
582
-- We leave skolem TyVars alone; they are immutable.
dreixel's avatar
dreixel committed
583
584
585
--
-- This function is called on both kind and type variables,
-- but kind variables *only* if PolyKinds is on.
586
zonkQuantifiedTyVar tv
587
588
  = ASSERT2( isTcTyVar tv, ppr tv ) 
    case tcTyVarDetails tv of
dreixel's avatar
dreixel committed
589
      SkolemTv {} -> do { kind <- zonkTcKind (tyVarKind tv)
590
                        ; return $ setTyVarKind tv kind }
591
592
593
	-- It might be a skolem type variable, 
	-- for example from a user type signature

594
      MetaTv { mtv_ref = ref } ->
Ian Lynagh's avatar
Ian Lynagh committed
595
596
597
598
599
600
601
602
603
          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
604
605
606
      _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk

skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
607
608
609
610
611
-- 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]
612
skolemiseUnboundMetaTyVar tv details
613
  = ASSERT2( isMetaTyVar tv, ppr tv ) 
614
615
616
    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
617
618
        ; kind <- zonkTcKind (tyVarKind tv)
        ; let final_kind = defaultKind kind
619
620
              final_name = mkInternalName uniq (getOccName tv) span
              final_tv   = mkTcTyVar final_name final_kind details
dreixel's avatar
dreixel committed
621
622
623

        ; writeMetaTyVar tv (mkTyVarTy final_tv)
        ; return final_tv }
624
625
626
627
628
629
630
631
632
633
634

skolemiseSigTv :: TcTyVar -> TcM TcTyVar
-- In TcBinds we create SigTvs for type signatures
-- but for singleton groups we want them to really be skolems
-- which do not unify with each other
skolemiseSigTv tv  
  = ASSERT2( isSigTyVar tv, ppr tv )
    do { writeMetaTyVarRef tv (metaTvRef tv) (mkTyVarTy skol_tv)
       ; return skol_tv }
  where
    skol_tv = setTcTyVarDetails tv (SkolemTv False)
635
636
\end{code}

637
638
\begin{code}
zonkImplication :: Implication -> TcM Implication
639
640
zonkImplication implic@(Implic { ic_untch  = untch
                               , ic_binds  = binds_var
641
                               , ic_skols  = skols
642
                               , ic_given  = given
643
                               , ic_wanted = wanted
644
                               , ic_info   = info })
645
646
  = do { skols'  <- mapM zonkTcTyVarBndr skols  -- Need to zonk their kinds!
                                                -- as Trac #7230 showed
647
       ; given'  <- mapM zonkEvVar given
648
       ; info'   <- zonkSkolemInfo info
649
       ; wanted' <- zonkWCRec binds_var untch wanted
650
651
       ; return (implic { ic_skols = skols'
                        , ic_given = given'
652
                        , ic_fsks  = []  -- Zonking removes all FlatSkol tyvars
653
                        , ic_wanted = wanted'
654
                        , ic_info = info' }) }
655
656
657
658
659

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

660

661
662
663
zonkWC :: EvBindsVar -- May add new bindings for wanted family equalities in here
       -> WantedConstraints -> TcM WantedConstraints
zonkWC binds_var wc
664
665
  = do { untch <- getUntouchables
       ; zonkWCRec binds_var untch wc }
666
667
668
669
670
671

zonkWCRec :: EvBindsVar
          -> Untouchables
          -> WantedConstraints -> TcM WantedConstraints
zonkWCRec binds_var untch (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
  = do { flat'   <- zonkFlats binds_var untch flat
672
       ; implic' <- mapBagM zonkImplication implic
673
       ; insol'  <- zonkCts insol -- No need to do the more elaborate zonkFlats thing
674
675
       ; return (WC { wc_flat = flat', wc_impl = implic', wc_insol = insol' }) }

676
677
678
zonkFlats :: EvBindsVar -> Untouchables -> Cts -> TcM Cts
-- This zonks and unflattens a bunch of flat constraints
-- See Note [Unflattening while zonking]
679
680
681
682
zonkFlats binds_var untch cts
  = do { -- See Note [How to unflatten]
         cts <- foldrBagM unflatten_one emptyCts cts
       ; zonkCts cts }
683
684
  where
    unflatten_one orig_ct cts
685
686
      = do { zct <- zonkCt orig_ct                -- First we need to fully zonk 
           ; mct <- try_zonk_fun_eq orig_ct zct   -- Then try to solve if family equation
687
           ; return $ maybe cts (`consBag` cts) mct }
688
689
690
691
692
693
694
695
696
697
698
699

    try_zonk_fun_eq orig_ct zct   -- See Note [How to unflatten]
      | EqPred ty_lhs ty_rhs <- classifyPredType (ctPred zct)
          -- NB: zonking de-classifies the constraint,
          --     so we can't look for CFunEqCan
      , Just tv <- getTyVar_maybe ty_rhs
      , ASSERT2( not (isFloatedTouchableMetaTyVar untch tv), ppr tv )
        isTouchableMetaTyVar untch tv
      , typeKind ty_lhs `tcIsSubKind` tyVarKind tv
      , not (tv `elemVarSet` tyVarsOfType ty_lhs)
--       , Just ty_lhs' <- occurCheck tv ty_lhs
      = ASSERT2( isWantedCt orig_ct, ppr orig_ct )
Simon Peyton Jones's avatar
Simon Peyton Jones committed
700
        ASSERT2( case tcSplitTyConApp_maybe ty_lhs of { Just (tc,_) -> isSynFamilyTyCon tc; _ -> False }, ppr orig_ct )
701
702
703
704
705
706
707
708
709
710
        do { writeMetaTyVar tv ty_lhs
           ; let evterm = EvCoercion (mkTcReflCo ty_lhs)
                 evvar  = ctev_evar (cc_ev zct)
           ; addTcEvBind binds_var evvar evterm
           ; traceTc "zonkFlats/unflattening" $
             vcat [ text "zct = " <+> ppr zct,
                    text "binds_var = " <+> ppr binds_var ]
           ; return Nothing }
      | otherwise
      = return (Just zct)
711
712
713
714
715
716
717
718
719
720
721
722
\end{code}

Note [Unflattening while zonking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A bunch of wanted constraints could contain wanted equations of the form
(F taus ~ alpha) where alpha is either an ordinary unification variable, or
a flatten unification variable.

These are ordinary wanted constraints and can/should be solved by
ordinary unification alpha := F taus. However the constraint solving
algorithm does not do that, as their 'inert' form is F taus ~ alpha.

723
Hence, we need an extra step to 'unflatten' these equations by
724
725
726
727
728
729
730
731
732
performing unification. This unification, if it happens at the end of
constraint solving, cannot produce any more interactions in the
constraint solver so it is safe to do it as the very very last step.

We choose therefore to do it during zonking, in the function
zonkFlats. This is in analgoy to the zonking of given flatten skolems
which are eliminated in favor of the underlying type that they are
equal to.

733
Note that, because we now have to affect *evidence* while zonking
734
735
736
737
(setting some evidence binds to identities), we have to pass to the
zonkWC function an evidence variable to collect all the extra
variables.

738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
Note [How to unflatten]
~~~~~~~~~~~~~~~~~~~~~~~
How do we unflatten during zonking.  Consider a bunch of flat constraints.
Consider them one by one.  For each such constraint C
  * Zonk C (to apply current substitution)
  * If C is of form F tys ~ alpha, 
       where alpha is touchable
       and   alpha is not mentioned in tys
    then unify alpha := F tys
         and discard C

After processing all the flat constraints, zonk them again to propagate
the inforamtion from later ones to earlier ones.  Eg
  Start:  (F alpha ~ beta, G Int ~ alpha)
  Then we get beta := F alpha
              alpha := G Int
  but we must apply the second unification to the first constraint.


757
\begin{code}
758
759
760
zonkCts :: Cts -> TcM Cts
zonkCts = mapBagM zonkCt

761
zonkCt :: Ct -> TcM Ct
762
763
764
zonkCt ct@(CHoleCan { cc_ev = ev })
  = do { ev' <- zonkCtEvidence ev
       ; return $ ct { cc_ev = ev' } }
765
zonkCt ct
766
767
768
  = do { fl' <- zonkCtEvidence (cc_ev ct)
       ; return (CNonCanonical { cc_ev = fl'
                               , cc_loc = cc_loc ct }) }
769

770
zonkCtEvidence :: CtEvidence -> TcM CtEvidence
771
772
773
zonkCtEvidence ctev@(CtGiven { ctev_pred = pred }) 
  = do { pred' <- zonkTcType pred
       ; return (ctev { ctev_pred = pred'}) }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
774
zonkCtEvidence ctev@(CtWanted { ctev_pred = pred })
775
776
  = do { pred' <- zonkTcType pred
       ; return (ctev { ctev_pred = pred' }) }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
777
zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
778
779
  = do { pred' <- zonkTcType pred
       ; return (ctev { ctev_pred = pred' }) }
780
781
782
783
784
785
786
787
788

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
789
790
\end{code}

791
792
Note [Silly Type Synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
Consider this:
	type C u a = u	-- Note 'a' unused

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

	bar :: Num u => u
	bar = foo (\t -> t + t)

* 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:
	{Num (C d a)} =>  C d a -> C d a
  where a is fresh.

* Now abstract over the 'a', but float out the Num (C d a) constraint
810
  because it does not 'really' mention a.  (see exactTyVarsOfType)
811
  The arg to foo becomes
Ian Lynagh's avatar
Ian Lynagh committed
812
	\/\a -> \t -> t+t
813
814
815

* So we get a dict binding for Num (C d a), which is zonked to give
	a = ()
816
817
818
819
  [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!]
820

Ian Lynagh's avatar
Ian Lynagh committed
821
* Then the \/\a abstraction has a zonked 'a' in it.
822

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

826
827
828
829
830
831
832
833
834
835
836
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

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

dreixel's avatar
dreixel committed
839
  forall a. () => ((String -> String -> String) ~ a)
840
841
842
843
844
845
846
847
848
849
850
851
852
853

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
854
(which we require for a quantified variable), but is still a TcTyVar that the
855
856
simplifier knows how to deal with.

857
858
859

%************************************************************************
%*									*
860
\subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
861
862
863
864
865
866
%*									*
%*		For internal use only!					*
%*									*
%************************************************************************

\begin{code}
867
868
869
870
871
872
-- 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') }

873
874
875
876
-- For unbound, mutable tyvars, zonkType uses the function given to it
-- For tyvars bound at a for-all, zonkType zonks them to an immutable
--	type variable and zonks the kind too

877
878
zonkTcType :: TcType -> TcM TcType
zonkTcType ty
879
880
  = go ty
  where
881
882
883
    go (TyConApp tc tys) = do tys' <- mapM go tys
                              return (TyConApp tc tys')

884
    go (LitTy n)         = return (LitTy n)
885

886
887
888
889
890
891
892
    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')
893
894
895
		-- NB the mkAppTy; we might have instantiated a
		-- type variable to a type constructor, so we need
		-- to pull the TyConApp to the top.
896
897

	-- The two interesting cases!
898
    go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
899
		       | otherwise	 = TyVarTy <$> updateTyVarKindM go tyvar
900
		-- Ordinary (non Tc) tyvars occur inside quantified types
901

902
903
904
905
906
907
908
909
910
911
912
913
    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),
-- rather it is always a skolems.  BUT it may have a kind 
-- that has not yet been zonked, and may include kind
-- unification variables.
zonkTcTyVarBndr tyvar
  = ASSERT2( isImmutableTyVar tyvar, ppr tyvar ) do
    updateTyVarKindM zonkTcType tyvar
914
915
916
917
918
919
920
921
922

zonkTcTyVar :: TcTyVar -> TcM TcType
-- Simply look through all Flexis
zonkTcTyVar tv
  = ASSERT2( isTcTyVar tv, ppr tv ) do
    case tcTyVarDetails tv of
      SkolemTv {}   -> zonk_kind_and_return
      RuntimeUnk {} -> zonk_kind_and_return
      FlatSkol ty   -> zonkTcType ty
923
924
925
926
927
      MetaTv { mtv_ref = ref }
         -> do { cts <- readMutVar ref
               ; case cts of
	            Flexi       -> zonk_kind_and_return
	            Indirect ty -> zonkTcType ty }
928
929
930
  where
    zonk_kind_and_return = do { z_tv <- zonkTyVarKind tv
                              ; return (TyVarTy z_tv) }
931
932
933
934
\end{code}



935
936
937
938
939
940
941
942
%************************************************************************
%*									*
			Zonking kinds
%*									*
%************************************************************************

\begin{code}
zonkTcKind :: TcKind -> TcM TcKind
943
zonkTcKind k = zonkTcType k
944
945
\end{code}
			
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
Note [Inheriting implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this:

	f x = (x::Int) + ?y

where f is *not* a top-level binding.
From the RHS of f we'll get the constraint (?y::Int).
There are two types we might infer for f:

	f :: Int -> Int

(so we get ?y from the context of f's definition), or

	f :: (?y::Int) => Int -> Int

At first you might think the first was better, becuase then
?y behaves like a free variable of the definition, rather than
having to be passed at each call site.  But of course, the WHOLE
IDEA is that ?y should be passed at each call site (that's what
dynamic binding means) so we'd better infer the second.

BOTTOM LINE: when *inferring types* you *must* quantify 
over implicit parameters. See the predicate isFreeWhenInferring.

971
\begin{code}
972
973
974
975
976
977
quantifyPred :: TyVarSet      -- Quantifying over these
	     -> PredType -> Bool	    -- True <=> quantify over this wanted
quantifyPred qtvs pred
  | isIPPred pred = True  -- Note [Inheriting implicit parameters]
  | otherwise	  = tyVarsOfType pred `intersectsVarSet` qtvs

978
growThetaTyVars :: TcThetaType -> TyVarSet -> TyVarSet
979
-- See Note [Growing the tau-tvs using constraints]
980
981
982
983
growThetaTyVars theta tvs
  | null theta = tvs
  | otherwise  = fixVarSet mk_next tvs
  where
984
985
986
987
988
    mk_next tvs = foldr grow_one tvs theta
    grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs

growPredTyVars :: TcPredType
               -> TyVarSet	-- The set to extend
989
990
	       -> TyVarSet	-- TyVars of the predicate if it intersects the set, 
growPredTyVars pred tvs 
991
   | isIPPred pred                   = pred_tvs   -- Always quantify over implicit parameers
992
993
   | pred_tvs `intersectsVarSet` tvs = pred_tvs
   | otherwise                       = emptyVarSet
994
  where
995
    pred_tvs = tyVarsOfType pred
996
997
998
\end{code}
    

Simon Peyton Jones's avatar
Simon Peyton Jones committed
999