Add kind equalities to GHC.
[ghc.git] / compiler / typecheck / TcMType.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 Monadic type operations
7
8 This module contains monadic operations over types that contain
9 mutable type variables
10 -}
11
12 {-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
13
14 module TcMType (
15 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
16
17 --------------------------------
18 -- Creating new mutable type variables
19 newFlexiTyVar,
20 newFlexiTyVarTy, -- Kind -> TcM TcType
21 newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType]
22 newOpenFlexiTyVarTy,
23 newReturnTyVar, newReturnTyVarTy,
24 newMaybeReturnTyVarTy,
25 newOpenReturnTyVar,
26 newMetaKindVar, newMetaKindVars,
27 cloneMetaTyVar,
28 newFmvTyVar, newFskTyVar,
29
30 newMetaTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef,
31 newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar,
32
33 --------------------------------
34 -- Creating fresh type variables for pm checking
35 genInstSkolTyVarsX,
36
37 --------------------------------
38 -- Creating new evidence variables
39 newEvVar, newEvVars, newDict,
40 newWanted, newWanteds,
41 emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
42 newTcEvBinds, addTcEvBind,
43
44 newCoercionHole, fillCoercionHole, isFilledCoercionHole,
45 unpackCoercionHole, unpackCoercionHole_maybe,
46 checkCoercionHole,
47
48 --------------------------------
49 -- Instantiation
50 tcInstTyVars, tcInstTyVarX,
51 newSigTyVar,
52 tcInstType,
53 tcInstSkolTyVars, tcInstSkolTyVarsLoc, tcInstSuperSkolTyVarsX,
54 tcInstSigTyVarsLoc, tcInstSigTyVars,
55 tcInstSkolType,
56 tcSkolDFunType, tcSuperSkolTyVars,
57
58 instSkolTyCoVars, freshenTyVarBndrs, freshenCoVarBndrsX,
59
60 --------------------------------
61 -- Zonking and tidying
62 zonkTidyTcType, zonkTidyOrigin,
63 mkTypeErrorThing, mkTypeErrorThingArgs,
64 tidyEvVar, tidyCt, tidySkolemInfo,
65 skolemiseUnboundMetaTyVar,
66 zonkTcTyVar, zonkTcTyVars, zonkTyCoVarsAndFV, zonkTcTypeAndFV,
67 zonkQuantifiedTyVar, zonkQuantifiedTyVarOrType, quantifyTyVars,
68 defaultKindVar,
69 zonkTcTyCoVarBndr, zonkTcType, zonkTcTypes, zonkCo,
70 zonkTyCoVarKind, zonkTcTypeMapper,
71
72 zonkEvVar, zonkWC, zonkSimples, zonkId, zonkCt, zonkSkolemInfo,
73
74 tcGetGlobalTyCoVars
75 ) where
76
77 #include "HsVersions.h"
78
79 -- friends:
80 import TyCoRep ( CoercionHole(..) )
81 import TcType
82 import Type
83 import Coercion
84 import Class
85 import Var
86
87 -- others:
88 import TcRnMonad -- TcType, amongst others
89 import TcEvidence
90 import Id
91 import Name
92 import VarSet
93 import TysWiredIn
94 import TysPrim
95 import VarEnv
96 import PrelNames
97 import Util
98 import Outputable
99 import FastString
100 import SrcLoc
101 import Bag
102 import Pair
103 import DynFlags
104
105 import Control.Monad
106 import Maybes
107 import Data.List ( mapAccumL, partition )
108
109 {-
110 ************************************************************************
111 * *
112 Kind variables
113 * *
114 ************************************************************************
115 -}
116
117 mkKindName :: Unique -> Name
118 mkKindName unique = mkSystemName unique kind_var_occ
119
120 kind_var_occ :: OccName -- Just one for all MetaKindVars
121 -- They may be jiggled by tidying
122 kind_var_occ = mkOccName tvName "k"
123
124 newMetaKindVar :: TcM TcKind
125 newMetaKindVar = do { uniq <- newUnique
126 ; details <- newMetaDetails TauTv
127 ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details
128 ; return (mkTyVarTy kv) }
129
130 newMetaKindVars :: Int -> TcM [TcKind]
131 newMetaKindVars n = mapM (\ _ -> newMetaKindVar) (nOfThem n ())
132
133 {-
134 ************************************************************************
135 * *
136 Evidence variables; range over constraints we can abstract over
137 * *
138 ************************************************************************
139 -}
140
141 newEvVars :: TcThetaType -> TcM [EvVar]
142 newEvVars theta = mapM newEvVar theta
143
144 --------------
145
146 newEvVar :: TcPredType -> TcRnIf gbl lcl EvVar
147 -- Creates new *rigid* variables for predicates
148 newEvVar ty = do { name <- newSysName (predTypeOccName ty)
149 ; return (mkLocalIdOrCoVar name ty) }
150
151 -- deals with both equality and non-equality predicates
152 newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
153 newWanted orig t_or_k pty
154 = do loc <- getCtLocM orig t_or_k
155 d <- if isEqPred pty then HoleDest <$> newCoercionHole
156 else EvVarDest <$> newEvVar pty
157 return $ CtWanted { ctev_dest = d
158 , ctev_pred = pty
159 , ctev_loc = loc }
160
161 newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
162 newWanteds orig = mapM (newWanted orig Nothing)
163
164 -- | Emits a new Wanted. Deals with both equalities and non-equalities.
165 emitWanted :: CtOrigin -> TcPredType -> TcM EvTerm
166 emitWanted origin pty
167 = do { ev <- newWanted origin Nothing pty
168 ; emitSimple $ mkNonCanonical ev
169 ; return $ ctEvTerm ev }
170
171 -- | Emits a new equality constraint
172 emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
173 emitWantedEq origin t_or_k role ty1 ty2
174 = do { hole <- newCoercionHole
175 ; loc <- getCtLocM origin (Just t_or_k)
176 ; emitSimple $ mkNonCanonical $
177 CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole, ctev_loc = loc }
178 ; return (mkHoleCo hole role ty1 ty2) }
179 where
180 pty = mkPrimEqPredRole role ty1 ty2
181
182 -- | Creates a new EvVar and immediately emits it as a Wanted.
183 -- No equality predicates here.
184 emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar
185 emitWantedEvVar origin ty
186 = do { new_cv <- newEvVar ty
187 ; loc <- getCtLocM origin Nothing
188 ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv
189 , ctev_pred = ty
190 , ctev_loc = loc }
191 ; emitSimple $ mkNonCanonical ctev
192 ; return new_cv }
193
194 emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
195 emitWantedEvVars orig = mapM (emitWantedEvVar orig)
196
197 newDict :: Class -> [TcType] -> TcM DictId
198 newDict cls tys
199 = do { name <- newSysName (mkDictOcc (getOccName cls))
200 ; return (mkLocalId name (mkClassPred cls tys)) }
201
202 predTypeOccName :: PredType -> OccName
203 predTypeOccName ty = case classifyPredType ty of
204 ClassPred cls _ -> mkDictOcc (getOccName cls)
205 EqPred _ _ _ -> mkVarOccFS (fsLit "cobox")
206 IrredPred _ -> mkVarOccFS (fsLit "irred")
207
208 {-
209 ************************************************************************
210 * *
211 Coercion holes
212 * *
213 ************************************************************************
214 -}
215
216 newCoercionHole :: TcM CoercionHole
217 newCoercionHole
218 = do { u <- newUnique
219 ; traceTc "New coercion hole:" (ppr u)
220 ; ref <- newMutVar Nothing
221 ; return $ CoercionHole u ref }
222
223 -- | Put a value in a coercion hole
224 fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
225 fillCoercionHole (CoercionHole u ref) co
226 = do {
227 #ifdef DEBUG
228 ; cts <- readTcRef ref
229 ; whenIsJust cts $ \old_co ->
230 pprPanic "Filling a filled coercion hole" (ppr u $$ ppr co $$ ppr old_co)
231 #endif
232 ; traceTc "Filling coercion hole" (ppr u <+> text ":=" <+> ppr co)
233 ; writeTcRef ref (Just co) }
234
235 -- | Is a coercion hole filled in?
236 isFilledCoercionHole :: CoercionHole -> TcM Bool
237 isFilledCoercionHole (CoercionHole _ ref) = isJust <$> readTcRef ref
238
239 -- | Retrieve the contents of a coercion hole. Panics if the hole
240 -- is unfilled
241 unpackCoercionHole :: CoercionHole -> TcM Coercion
242 unpackCoercionHole hole
243 = do { contents <- unpackCoercionHole_maybe hole
244 ; case contents of
245 Just co -> return co
246 Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }
247
248 -- | Retrieve the contents of a coercion hole, if it is filled
249 unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
250 unpackCoercionHole_maybe (CoercionHole _ ref) = readTcRef ref
251
252 -- | Check that a coercion is appropriate for filling a hole. (The hole
253 -- itself is needed only for printing. NB: This must be /lazy/ in the coercion,
254 -- as it's used in TcHsSyn in the presence of knots.
255 -- Always returns the checked coercion, but this return value is necessary
256 -- so that the input coercion is forced only when the output is forced.
257 checkCoercionHole :: Coercion -> CoercionHole -> Role -> Type -> Type -> TcM Coercion
258 checkCoercionHole co h r t1 t2
259 -- co is already zonked, but t1 and t2 might not be
260 | debugIsOn
261 = do { t1 <- zonkTcType t1
262 ; t2 <- zonkTcType t2
263 ; let (Pair _t1 _t2, _role) = coercionKindRole co
264 ; return $
265 ASSERT2( t1 `eqType` _t1 && t2 `eqType` _t2 && r == _role
266 , (text "Bad coercion hole" <+>
267 ppr h <> colon <+> vcat [ ppr _t1, ppr _t2, ppr _role
268 , ppr co, ppr t1, ppr t2
269 , ppr r ]) )
270 co }
271 | otherwise
272 = return co
273
274
275 {-
276 ************************************************************************
277 * *
278 SkolemTvs (immutable)
279 * *
280 ************************************************************************
281 -}
282
283 tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
284 -- ^ How to instantiate the type variables
285 -> TcType -- ^ Type to instantiate
286 -> TcM ([TcTyVar], TcThetaType, TcType) -- ^ Result
287 -- (type vars, preds (incl equalities), rho)
288 tcInstType inst_tyvars ty
289 = case tcSplitForAllTys ty of
290 ([], rho) -> let -- There may be overloading despite no type variables;
291 -- (?x :: Int) => Int -> Int
292 (theta, tau) = tcSplitPhiTy rho
293 in
294 return ([], theta, tau)
295
296 (tyvars, rho) -> do { (subst, tyvars') <- inst_tyvars tyvars
297 ; let (theta, tau) = tcSplitPhiTy (substTy subst rho)
298 ; return (tyvars', theta, tau) }
299
300 tcSkolDFunType :: Type -> TcM ([TcTyVar], TcThetaType, TcType)
301 -- Instantiate a type signature with skolem constants.
302 -- We could give them fresh names, but no need to do so
303 tcSkolDFunType ty = tcInstType tcInstSuperSkolTyVars ty
304
305 tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
306 -- Make skolem constants, but do *not* give them new names, as above
307 -- Moreover, make them "super skolems"; see comments with superSkolemTv
308 -- see Note [Kind substitution when instantiating]
309 -- Precondition: tyvars should be ordered by scoping
310 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar (mkTopTCvSubst [])
311
312 tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
313 tcSuperSkolTyVar subst tv
314 = (extendTCvSubst subst tv (mkTyVarTy new_tv), new_tv)
315 where
316 kind = substTy subst (tyVarKind tv)
317 new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
318
319 -- Wrappers
320 -- we need to be able to do this from outside the TcM monad:
321 tcInstSkolTyVarsLoc :: SrcSpan -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
322 tcInstSkolTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
323
324 tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
325 tcInstSkolTyVars = tcInstSkolTyVars' False emptyTCvSubst
326
327 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
328 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
329
330 tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
331 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVars' True subst
332
333 tcInstSkolTyVars' :: Bool -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
334 -- Precondition: tyvars should be ordered (kind vars first)
335 -- see Note [Kind substitution when instantiating]
336 -- Get the location from the monad; this is a complete freshening operation
337 tcInstSkolTyVars' overlappable subst tvs
338 = do { loc <- getSrcSpanM
339 ; instSkolTyCoVarsX (mkTcSkolTyVar loc overlappable) subst tvs }
340
341 mkTcSkolTyVar :: SrcSpan -> Bool -> Unique -> Name -> Kind -> TcTyVar
342 mkTcSkolTyVar loc overlappable uniq old_name kind
343 = mkTcTyVar (mkInternalName uniq (getOccName old_name) loc)
344 kind
345 (SkolemTv overlappable)
346
347 tcInstSigTyVarsLoc :: SrcSpan -> [TyVar]
348 -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
349 -- We specify the location
350 tcInstSigTyVarsLoc loc = instSkolTyCoVars (mkTcSkolTyVar loc False)
351
352 tcInstSigTyVars :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
353 -- Get the location from the TyVar itself, not the monad
354 tcInstSigTyVars
355 = instSkolTyCoVars mk_tv
356 where
357 mk_tv uniq old_name kind
358 = mkTcTyVar (setNameUnique old_name uniq) kind (SkolemTv False)
359
360 tcInstSkolType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
361 -- Instantiate a type with fresh skolem constants
362 -- Binding location comes from the monad
363 tcInstSkolType ty = tcInstType tcInstSkolTyVars ty
364
365 ------------------
366 freshenTyVarBndrs :: [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyVar])
367 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
368 -- as TyVars, rather than becoming TcTyVars
369 -- Used in FamInst.newFamInst, and Inst.newClsInst
370 freshenTyVarBndrs = instSkolTyCoVars mk_tv
371 where
372 mk_tv uniq old_name kind = mkTyVar (setNameUnique old_name uniq) kind
373
374 freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcRnIf gbl lcl (TCvSubst, [CoVar])
375 -- ^ Give fresh uniques to a bunch of CoVars
376 -- Used in FamInst.newFamInst
377 freshenCoVarBndrsX subst = instSkolTyCoVarsX mk_cv subst
378 where
379 mk_cv uniq old_name kind = mkCoVar (setNameUnique old_name uniq) kind
380
381 ------------------
382 instSkolTyCoVars :: (Unique -> Name -> Kind -> TyCoVar)
383 -> [TyVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
384 instSkolTyCoVars mk_tcv = instSkolTyCoVarsX mk_tcv emptyTCvSubst
385
386 instSkolTyCoVarsX :: (Unique -> Name -> Kind -> TyCoVar)
387 -> TCvSubst -> [TyCoVar] -> TcRnIf gbl lcl (TCvSubst, [TyCoVar])
388 instSkolTyCoVarsX mk_tcv = mapAccumLM (instSkolTyCoVarX mk_tcv)
389
390 instSkolTyCoVarX :: (Unique -> Name -> Kind -> TyCoVar)
391 -> TCvSubst -> TyCoVar -> TcRnIf gbl lcl (TCvSubst, TyCoVar)
392 instSkolTyCoVarX mk_tcv subst tycovar
393 = do { uniq <- newUnique
394 ; let new_tv = mk_tcv uniq old_name kind
395 ; return (extendTCvSubst subst tycovar (mk_ty_co new_tv), new_tv) }
396 where
397 old_name = tyVarName tycovar
398 kind = substTy subst (tyVarKind tycovar)
399
400 mk_ty_co v
401 | isTyVar v = mkTyVarTy v
402 | otherwise = mkCoercionTy $ mkCoVarCo v
403
404 newFskTyVar :: TcType -> TcM TcTyVar
405 newFskTyVar fam_ty
406 = do { uniq <- newUnique
407 ; let name = mkSysTvName uniq (fsLit "fsk")
408 ; return (mkTcTyVar name (typeKind fam_ty) (FlatSkol fam_ty)) }
409
410 {-
411 Note [Kind substitution when instantiating]
412 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
413 When we instantiate a bunch of kind and type variables, first we
414 expect them to be topologically sorted.
415 Then we have to instantiate the kind variables, build a substitution
416 from old variables to the new variables, then instantiate the type
417 variables substituting the original kind.
418
419 Exemple: If we want to instantiate
420 [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
421 we want
422 [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
423 instead of the buggous
424 [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
425
426
427 ************************************************************************
428 * *
429 MetaTvs (meta type variables; mutable)
430 * *
431 ************************************************************************
432 -}
433
434 mkMetaTyVarName :: Unique -> FastString -> Name
435 -- Makes a /System/ Name, which is eagerly eliminated by
436 -- the unifier; see TcUnify.nicer_to_update_tv1, and
437 -- TcCanonical.canEqTyVarTyVar (nicer_to_update_tv2)
438 mkMetaTyVarName uniq str = mkSysTvName uniq str
439
440 newMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar
441 -- Make a new meta tyvar out of thin air
442 newMetaTyVar meta_info kind
443 = do { uniq <- newUnique
444 ; let name = mkMetaTyVarName uniq s
445 s = case meta_info of
446 ReturnTv -> fsLit "r"
447 TauTv -> fsLit "t"
448 FlatMetaTv -> fsLit "fmv"
449 SigTv -> fsLit "a"
450 ; details <- newMetaDetails meta_info
451 ; return (mkTcTyVar name kind details) }
452
453 newSigTyVar :: Name -> Kind -> TcM TcTyVar
454 newSigTyVar name kind
455 = do { details <- newMetaDetails SigTv
456 ; return (mkTcTyVar name kind details) }
457
458 newFmvTyVar :: TcType -> TcM TcTyVar
459 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
460 -- so that the fmv is untouchable.
461 newFmvTyVar fam_ty
462 = do { uniq <- newUnique
463 ; ref <- newMutVar Flexi
464 ; cur_lvl <- getTcLevel
465 ; let details = MetaTv { mtv_info = FlatMetaTv
466 , mtv_ref = ref
467 , mtv_tclvl = fmvTcLevel cur_lvl }
468 name = mkMetaTyVarName uniq (fsLit "s")
469 ; return (mkTcTyVar name (typeKind fam_ty) details) }
470
471 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
472 newMetaDetails info
473 = do { ref <- newMutVar Flexi
474 ; tclvl <- getTcLevel
475 ; return (MetaTv { mtv_info = info
476 , mtv_ref = ref
477 , mtv_tclvl = tclvl }) }
478
479 cloneMetaTyVar :: TcTyVar -> TcM TcTyVar
480 cloneMetaTyVar tv
481 = ASSERT( isTcTyVar tv )
482 do { uniq <- newUnique
483 ; ref <- newMutVar Flexi
484 ; let name' = setNameUnique (tyVarName tv) uniq
485 details' = case tcTyVarDetails tv of
486 details@(MetaTv {}) -> details { mtv_ref = ref }
487 _ -> pprPanic "cloneMetaTyVar" (ppr tv)
488 ; return (mkTcTyVar name' (tyVarKind tv) details') }
489
490 -- Works for both type and kind variables
491 readMetaTyVar :: TyVar -> TcM MetaDetails
492 readMetaTyVar tyvar = ASSERT2( isMetaTyVar tyvar, ppr tyvar )
493 readMutVar (metaTvRef tyvar)
494
495 isFilledMetaTyVar :: TyVar -> TcM Bool
496 -- True of a filled-in (Indirect) meta type variable
497 isFilledMetaTyVar tv
498 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
499 = do { details <- readMutVar ref
500 ; return (isIndirect details) }
501 | otherwise = return False
502
503 isUnfilledMetaTyVar :: TyVar -> TcM Bool
504 -- True of a un-filled-in (Flexi) meta type variable
505 isUnfilledMetaTyVar tv
506 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tv
507 = do { details <- readMutVar ref
508 ; return (isFlexi details) }
509 | otherwise = return False
510
511 --------------------
512 -- Works with both type and kind variables
513 writeMetaTyVar :: TcTyVar -> TcType -> TcM ()
514 -- Write into a currently-empty MetaTyVar
515
516 writeMetaTyVar tyvar ty
517 | not debugIsOn
518 = writeMetaTyVarRef tyvar (metaTvRef tyvar) ty
519
520 -- Everything from here on only happens if DEBUG is on
521 | not (isTcTyVar tyvar)
522 = WARN( True, text "Writing to non-tc tyvar" <+> ppr tyvar )
523 return ()
524
525 | MetaTv { mtv_ref = ref } <- tcTyVarDetails tyvar
526 = writeMetaTyVarRef tyvar ref ty
527
528 | otherwise
529 = WARN( True, text "Writing to non-meta tyvar" <+> ppr tyvar )
530 return ()
531
532 --------------------
533 writeMetaTyVarRef :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM ()
534 -- Here the tyvar is for error checking only;
535 -- the ref cell must be for the same tyvar
536 writeMetaTyVarRef tyvar ref ty
537 | not debugIsOn
538 = do { traceTc "writeMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)
539 <+> text ":=" <+> ppr ty)
540 ; writeTcRef ref (Indirect ty) }
541
542 -- Everything from here on only happens if DEBUG is on
543 | otherwise
544 = do { meta_details <- readMutVar ref;
545 -- Zonk kinds to allow the error check to work
546 ; zonked_tv_kind <- zonkTcType tv_kind
547 ; zonked_ty_kind <- zonkTcType ty_kind
548
549 -- Check for double updates
550 ; ASSERT2( isFlexi meta_details,
551 hang (text "Double update of meta tyvar")
552 2 (ppr tyvar $$ ppr meta_details) )
553
554 traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
555 ; writeMutVar ref (Indirect ty)
556 ; when ( not (isPredTy tv_kind)
557 -- Don't check kinds for updates to coercion variables
558 && not (zonked_ty_kind `tcEqKind` zonked_tv_kind))
559 $ WARN( True, hang (text "Ill-kinded update to meta tyvar")
560 2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
561 <+> text ":="
562 <+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) ) )
563 (return ()) }
564 where
565 tv_kind = tyVarKind tyvar
566 ty_kind = typeKind ty
567
568 {-
569 % Generating fresh variables for pattern match check
570 -}
571
572 -- UNINSTANTIATED VERSION OF tcInstSkolTyCoVars
573 genInstSkolTyVarsX :: SrcSpan -> TCvSubst -> [TyVar]
574 -> TcRnIf gbl lcl (TCvSubst, [TcTyVar])
575 -- Precondition: tyvars should be scoping-ordered
576 -- see Note [Kind substitution when instantiating]
577 -- Get the location from the monad; this is a complete freshening operation
578 genInstSkolTyVarsX loc subst tvs = instSkolTyCoVarsX (mkTcSkolTyVar loc False) subst tvs
579
580 {-
581 ************************************************************************
582 * *
583 MetaTvs: TauTvs
584 * *
585 ************************************************************************
586
587 Note [Sort-polymorphic tyvars accept foralls]
588 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
589 Here is a common paradigm:
590 foo :: (forall a. a -> a) -> Int
591 foo = error "urk"
592 To make this work we need to instantiate 'error' with a polytype.
593 A similar case is
594 bar :: Bool -> (forall a. a->a) -> Int
595 bar True = \x. (x 3)
596 bar False = error "urk"
597 Here we need to instantiate 'error' with a polytype.
598
599 But 'error' has an sort-polymorphic type variable, precisely so that
600 we can instantiate it with Int#. So we also allow such type variables
601 to be instantiate with foralls. It's a bit of a hack, but seems
602 straightforward.
603
604 Note [Never need to instantiate coercion variables]
605 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
606 With coercion variables sloshing around in types, it might seem that we
607 sometimes need to instantiate coercion variables. This would be problematic,
608 because coercion variables inhabit unboxed equality (~#), and the constraint
609 solver thinks in terms only of boxed equality (~). The solution is that
610 we never need to instantiate coercion variables in the first place.
611
612 The tyvars that we need to instantiate come from the types of functions,
613 data constructors, and patterns. These will never be quantified over
614 coercion variables, except for the special case of the promoted Eq#. But,
615 that can't ever appear in user code, so we're safe!
616 -}
617
618 newFlexiTyVar :: Kind -> TcM TcTyVar
619 newFlexiTyVar kind = newMetaTyVar TauTv kind
620
621 newFlexiTyVarTy :: Kind -> TcM TcType
622 newFlexiTyVarTy kind = do
623 tc_tyvar <- newFlexiTyVar kind
624 return (mkTyVarTy tc_tyvar)
625
626 newFlexiTyVarTys :: Int -> Kind -> TcM [TcType]
627 newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
628
629 newReturnTyVar :: Kind -> TcM TcTyVar
630 newReturnTyVar kind = newMetaTyVar ReturnTv kind
631
632 newReturnTyVarTy :: Kind -> TcM TcType
633 newReturnTyVarTy kind = mkTyVarTy <$> newReturnTyVar kind
634
635 -- | Either makes a normal Flexi or a ReturnTv Flexi
636 newMaybeReturnTyVarTy :: Bool -- True <=> make a ReturnTv
637 -> Kind -> TcM TcType
638 newMaybeReturnTyVarTy True = newReturnTyVarTy
639 newMaybeReturnTyVarTy False = newFlexiTyVarTy
640
641 -- | Create a tyvar that can be a lifted or unlifted type.
642 newOpenFlexiTyVarTy :: TcM TcType
643 newOpenFlexiTyVarTy
644 = do { lev <- newFlexiTyVarTy levityTy
645 ; newFlexiTyVarTy (tYPE lev) }
646
647 -- | Create a *return* tyvar that can be a lifted or unlifted type.
648 newOpenReturnTyVar :: TcM (TcTyVar, TcKind)
649 newOpenReturnTyVar
650 = do { lev <- newFlexiTyVarTy levityTy -- this doesn't need ReturnTv
651 ; let k = tYPE lev
652 ; tv <- newReturnTyVar k
653 ; return (tv, k) }
654
655 tcInstTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
656 -- Instantiate with META type variables
657 -- Note that this works for a sequence of kind, type, and coercion variables
658 -- variables. Eg [ (k:*), (a:k->k) ]
659 -- Gives [ (k7:*), (a8:k7->k7) ]
660 tcInstTyVars = mapAccumLM tcInstTyVarX emptyTCvSubst
661 -- emptyTCvSubst has an empty in-scope set, but that's fine here
662 -- Since the tyvars are freshly made, they cannot possibly be
663 -- captured by any existing for-alls.
664
665 tcInstTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar)
666 -- Make a new unification variable tyvar whose Name and Kind come from
667 -- an existing TyVar. We substitute kind variables in the kind.
668 tcInstTyVarX subst tyvar
669 = do { uniq <- newUnique
670 -- See Note [Levity polymorphic variables accept foralls]
671 ; let info = if isLevityPolymorphic (tyVarKind tyvar)
672 then ReturnTv
673 else TauTv
674 ; details <- newMetaDetails info
675 ; let name = mkSystemName uniq (getOccName tyvar)
676 -- See Note [Name of an instantiated type variable]
677 kind = substTy subst (tyVarKind tyvar)
678 new_tv = mkTcTyVar name kind details
679 ; return (extendTCvSubst subst tyvar (mkTyVarTy new_tv), new_tv) }
680
681 {- Note [Name of an instantiated type variable]
682 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
683 At the moment we give a unification variable a System Name, which
684 influences the way it is tidied; see TypeRep.tidyTyVarBndr.
685
686 Note [Levity polymorphic variables accept foralls]
687 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
688 Here is a common paradigm:
689 foo :: (forall a. a -> a) -> Int
690 foo = error "urk"
691 To make this work we need to instantiate 'error' with a polytype.
692 A similar case is
693 bar :: Bool -> (forall a. a->a) -> Int
694 bar True = \x. (x 3)
695 bar False = error "urk"
696 Here we need to instantiate 'error' with a polytype.
697
698 But 'error' has a levity polymorphic type variable, precisely so that
699 we can instantiate it with Int#. So we also allow such type variables
700 to be instantiated with foralls. It's a bit of a hack, but seems
701 straightforward.
702
703 ************************************************************************
704 * *
705 Quantification
706 * *
707 ************************************************************************
708
709 Note [quantifyTyVars]
710 ~~~~~~~~~~~~~~~~~~~~~
711 quantifyTyVars is given the free vars of a type that we
712 are about to wrap in a forall.
713
714 It takes these free type/kind variables (partitioned into dependent and
715 non-dependent variables) and
716 1. Zonks them and remove globals and covars
717 2. Extends kvs1 with free kind vars in the kinds of tvs (removing globals)
718 3. Calls zonkQuantifiedTyVar on each
719
720 Step (2) is often unimportant, because the kind variable is often
721 also free in the type. Eg
722 Typeable k (a::k)
723 has free vars {k,a}. But the type (see Trac #7916)
724 (f::k->*) (a::k)
725 has free vars {f,a}, but we must add 'k' as well! Hence step (3).
726
727 This function bothers to distinguish between dependent and non-dependent
728 variables only to keep correct defaulting behavior with -XNoPolyKinds.
729 With -XPolyKinds, it treats both classes of variables identically.
730
731 Note that this function can accept covars, but will never return them.
732 This is because we never want to infer a quantified covar!
733 -}
734
735 quantifyTyVars :: TcTyCoVarSet -- global tvs
736 -> Pair TcTyCoVarSet -- dependent tvs We only distinguish
737 -- nondependent tvs between these for
738 -- -XNoPolyKinds
739 -> TcM [TcTyVar]
740 -- See Note [quantifyTyVars]
741 -- Can be given a mixture of TcTyVars and TyVars, in the case of
742 -- associated type declarations. Also accepts covars, but *never* returns any.
743
744 quantifyTyVars gbl_tvs (Pair dep_tkvs nondep_tkvs)
745 = do { dep_tkvs <- zonkTyCoVarsAndFV dep_tkvs
746 ; nondep_tkvs <- (`minusVarSet` dep_tkvs) <$>
747 zonkTyCoVarsAndFV nondep_tkvs
748 ; gbl_tvs <- zonkTyCoVarsAndFV gbl_tvs
749
750 ; let all_cvs = filterVarSet isCoVar $
751 dep_tkvs `unionVarSet` nondep_tkvs `minusVarSet` gbl_tvs
752 dep_kvs = varSetElemsWellScoped $
753 dep_tkvs `minusVarSet` gbl_tvs
754 `minusVarSet` (closeOverKinds all_cvs)
755 -- remove any tvs that a covar depends on
756
757 nondep_tvs = varSetElemsWellScoped $
758 nondep_tkvs `minusVarSet` gbl_tvs
759 -- no worry about dependent cvs here, as these vars
760 -- are non-dependent
761
762 -- NB kinds of tvs are zonked by zonkTyCoVarsAndFV
763
764 -- In the non-PolyKinds case, default the kind variables
765 -- to *, and zonk the tyvars as usual. Notice that this
766 -- may make quantifyTyVars return a shorter list
767 -- than it was passed, but that's ok
768 ; poly_kinds <- xoptM Opt_PolyKinds
769 ; dep_vars2 <- if poly_kinds
770 then return dep_kvs
771 else do { let (meta_kvs, skolem_kvs) = partition is_meta dep_kvs
772 is_meta kv = isTcTyVar kv && isMetaTyVar kv
773
774 ; mapM_ defaultKindVar meta_kvs
775 ; return skolem_kvs } -- should be empty
776
777 ; let quant_vars = dep_vars2 ++ nondep_tvs
778
779 ; traceTc "quantifyTyVars"
780 (vcat [ text "globals:" <+> ppr gbl_tvs
781 , text "nondep:" <+> ppr nondep_tvs
782 , text "dep:" <+> ppr dep_kvs
783 , text "dep2:" <+> ppr dep_vars2
784 , text "quant_vars:" <+> ppr quant_vars ])
785
786 ; mapMaybeM zonk_quant quant_vars }
787 -- Because of the order, any kind variables
788 -- mentioned in the kinds of the type variables refer to
789 -- the now-quantified versions
790 where
791 zonk_quant tkv
792 | isTcTyVar tkv = zonkQuantifiedTyVar tkv
793 | otherwise = return $ Just tkv
794 -- For associated types, we have the class variables
795 -- in scope, and they are TyVars not TcTyVars
796
797 zonkQuantifiedTyVar :: TcTyVar -> TcM (Maybe TcTyVar)
798 -- The quantified type variables often include meta type variables
799 -- we want to freeze them into ordinary type variables, and
800 -- default their kind (e.g. from TYPE v to TYPE Lifted)
801 -- The meta tyvar is updated to point to the new skolem TyVar. Now any
802 -- bound occurrences of the original type variable will get zonked to
803 -- the immutable version.
804 --
805 -- We leave skolem TyVars alone; they are immutable.
806 --
807 -- This function is called on both kind and type variables,
808 -- but kind variables *only* if PolyKinds is on.
809 --
810 -- This returns a tyvar if it should be quantified over; otherwise,
811 -- it returns Nothing. Nothing is
812 -- returned only if zonkQuantifiedTyVar is passed a Levity meta-tyvar,
813 -- in order to default to Lifted.
814 zonkQuantifiedTyVar tv = left_only `liftM` zonkQuantifiedTyVarOrType tv
815 where left_only :: Either a b -> Maybe a
816 left_only (Left x) = Just x
817 left_only (Right _) = Nothing
818
819 -- | Like zonkQuantifiedTyVar, but if zonking reveals that the tyvar
820 -- should become a type (when defaulting a levity var to Lifted), it
821 -- returns the type instead.
822 zonkQuantifiedTyVarOrType :: TcTyVar -> TcM (Either TcTyVar TcType)
823 zonkQuantifiedTyVarOrType tv
824 = case tcTyVarDetails tv of
825 SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
826 ; return $ Left $ setTyVarKind tv kind }
827 -- It might be a skolem type variable,
828 -- for example from a user type signature
829
830 MetaTv { mtv_ref = ref } ->
831 do when debugIsOn $ do
832 -- [Sept 04] Check for non-empty.
833 -- See note [Silly Type Synonym]
834 cts <- readMutVar ref
835 case cts of
836 Flexi -> return ()
837 Indirect ty -> WARN( True, ppr tv $$ ppr ty )
838 return ()
839 if isLevityVar tv
840 then do { writeMetaTyVar tv liftedDataConTy
841 ; return (Right liftedDataConTy) }
842 else Left `liftM` skolemiseUnboundMetaTyVar tv vanillaSkolemTv
843 _other -> pprPanic "zonkQuantifiedTyVar" (ppr tv) -- FlatSkol, RuntimeUnk
844
845 -- | Take an (unconstrained) meta tyvar and default it. Works only for
846 -- kind vars (of type BOX) and levity vars (of type Levity).
847 defaultKindVar :: TcTyVar -> TcM Kind
848 defaultKindVar kv
849 | ASSERT( isMetaTyVar kv )
850 isLevityVar kv
851 = writeMetaTyVar kv liftedDataConTy >> return liftedDataConTy
852 | otherwise
853 = writeMetaTyVar kv liftedTypeKind >> return liftedTypeKind
854
855 skolemiseUnboundMetaTyVar :: TcTyVar -> TcTyVarDetails -> TcM TyVar
856 -- We have a Meta tyvar with a ref-cell inside it
857 -- Skolemise it, so that
858 -- we are totally out of Meta-tyvar-land
859 -- We create a skolem TyVar, not a regular TyVar
860 -- See Note [Zonking to Skolem]
861 skolemiseUnboundMetaTyVar tv details
862 = ASSERT2( isMetaTyVar tv, ppr tv )
863 do { span <- getSrcSpanM -- Get the location from "here"
864 -- ie where we are generalising
865 ; kind <- zonkTcType (tyVarKind tv)
866 ; let uniq = getUnique tv
867 -- NB: Use same Unique as original tyvar. This is
868 -- important for TcHsType.splitTelescopeTvs to work properly
869
870 tv_name = getOccName tv
871 final_name = mkInternalName uniq tv_name span
872 final_tv = mkTcTyVar final_name kind details
873
874 ; traceTc "Skolemising" (ppr tv <+> ptext (sLit ":=") <+> ppr final_tv)
875 ; writeMetaTyVar tv (mkTyVarTy final_tv)
876 ; return final_tv }
877
878 {-
879 Note [Zonking to Skolem]
880 ~~~~~~~~~~~~~~~~~~~~~~~~
881 We used to zonk quantified type variables to regular TyVars. However, this
882 leads to problems. Consider this program from the regression test suite:
883
884 eval :: Int -> String -> String -> String
885 eval 0 root actual = evalRHS 0 root actual
886
887 evalRHS :: Int -> a
888 evalRHS 0 root actual = eval 0 root actual
889
890 It leads to the deferral of an equality (wrapped in an implication constraint)
891
892 forall a. () => ((String -> String -> String) ~ a)
893
894 which is propagated up to the toplevel (see TcSimplify.tcSimplifyInferCheck).
895 In the meantime `a' is zonked and quantified to form `evalRHS's signature.
896 This has the *side effect* of also zonking the `a' in the deferred equality
897 (which at this point is being handed around wrapped in an implication
898 constraint).
899
900 Finally, the equality (with the zonked `a') will be handed back to the
901 simplifier by TcRnDriver.tcRnSrcDecls calling TcSimplify.tcSimplifyTop.
902 If we zonk `a' with a regular type variable, we will have this regular type
903 variable now floating around in the simplifier, which in many places assumes to
904 only see proper TcTyVars.
905
906 We can avoid this problem by zonking with a skolem. The skolem is rigid
907 (which we require for a quantified variable), but is still a TcTyVar that the
908 simplifier knows how to deal with.
909
910 Note [Silly Type Synonyms]
911 ~~~~~~~~~~~~~~~~~~~~~~~~~~
912 Consider this:
913 type C u a = u -- Note 'a' unused
914
915 foo :: (forall a. C u a -> C u a) -> u
916 foo x = ...
917
918 bar :: Num u => u
919 bar = foo (\t -> t + t)
920
921 * From the (\t -> t+t) we get type {Num d} => d -> d
922 where d is fresh.
923
924 * Now unify with type of foo's arg, and we get:
925 {Num (C d a)} => C d a -> C d a
926 where a is fresh.
927
928 * Now abstract over the 'a', but float out the Num (C d a) constraint
929 because it does not 'really' mention a. (see exactTyVarsOfType)
930 The arg to foo becomes
931 \/\a -> \t -> t+t
932
933 * So we get a dict binding for Num (C d a), which is zonked to give
934 a = ()
935 [Note Sept 04: now that we are zonking quantified type variables
936 on construction, the 'a' will be frozen as a regular tyvar on
937 quantification, so the floated dict will still have type (C d a).
938 Which renders this whole note moot; happily!]
939
940 * Then the \/\a abstraction has a zonked 'a' in it.
941
942 All very silly. I think its harmless to ignore the problem. We'll end up with
943 a \/\a in the final result but all the occurrences of a will be zonked to ()
944
945 ************************************************************************
946 * *
947 Zonking types
948 * *
949 ************************************************************************
950
951 -}
952
953 -- | @tcGetGlobalTyCoVars@ returns a fully-zonked set of *scoped* tyvars free in
954 -- the environment. To improve subsequent calls to the same function it writes
955 -- the zonked set back into the environment. Note that this returns all
956 -- variables free in anything (term-level or type-level) in scope. We thus
957 -- don't have to worry about clashes with things that are not in scope, because
958 -- if they are reachable, then they'll be returned here.
959 tcGetGlobalTyCoVars :: TcM TcTyVarSet
960 tcGetGlobalTyCoVars
961 = do { (TcLclEnv {tcl_tyvars = gtv_var}) <- getLclEnv
962 ; gbl_tvs <- readMutVar gtv_var
963 ; gbl_tvs' <- zonkTyCoVarsAndFV gbl_tvs
964 ; writeMutVar gtv_var gbl_tvs'
965 ; return gbl_tvs' }
966
967 zonkTcTypeAndFV :: TcType -> TcM TyCoVarSet
968 -- Zonk a type and take its free variables
969 -- With kind polymorphism it can be essential to zonk *first*
970 -- so that we find the right set of free variables. Eg
971 -- forall k1. forall (a:k2). a
972 -- where k2:=k1 is in the substitution. We don't want
973 -- k2 to look free in this type!
974 -- NB: This might be called from within the knot, so don't use
975 -- smart constructors. See Note [Zonking within the knot] in TcHsType
976 zonkTcTypeAndFV ty
977 = tyCoVarsOfType <$> mapType (zonkTcTypeMapper { tcm_smart = False }) () ty
978
979 zonkTyCoVar :: TyCoVar -> TcM TcType
980 -- Works on TyVars and TcTyVars
981 zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
982 | isTyVar tv = mkTyVarTy <$> zonkTyCoVarKind tv
983 | otherwise = ASSERT2( isCoVar tv, ppr tv )
984 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
985 -- Hackily, when typechecking type and class decls
986 -- we have TyVars in scopeadded (only) in
987 -- TcHsType.tcTyClTyVars, but it seems
988 -- painful to make them into TcTyVars there
989
990 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
991 zonkTyCoVarsAndFV tycovars = tyCoVarsOfTypes <$> mapM zonkTyCoVar (varSetElems tycovars)
992
993 zonkTcTyVars :: [TcTyVar] -> TcM [TcType]
994 zonkTcTyVars tyvars = mapM zonkTcTyVar tyvars
995
996 ----------------- Types
997 zonkTyCoVarKind :: TyCoVar -> TcM TyCoVar
998 zonkTyCoVarKind tv = do { kind' <- zonkTcType (tyVarKind tv)
999 ; return (setTyVarKind tv kind') }
1000
1001 zonkTcTypes :: [TcType] -> TcM [TcType]
1002 zonkTcTypes tys = mapM zonkTcType tys
1003
1004 {-
1005 ************************************************************************
1006 * *
1007 Zonking constraints
1008 * *
1009 ************************************************************************
1010 -}
1011
1012 zonkImplication :: Implication -> TcM Implication
1013 zonkImplication implic@(Implic { ic_skols = skols
1014 , ic_given = given
1015 , ic_wanted = wanted
1016 , ic_info = info })
1017 = do { skols' <- mapM zonkTcTyCoVarBndr skols -- Need to zonk their kinds!
1018 -- as Trac #7230 showed
1019 ; given' <- mapM zonkEvVar given
1020 ; info' <- zonkSkolemInfo info
1021 ; wanted' <- zonkWCRec wanted
1022 ; return (implic { ic_skols = skols'
1023 , ic_given = given'
1024 , ic_wanted = wanted'
1025 , ic_info = info' }) }
1026
1027 zonkEvVar :: EvVar -> TcM EvVar
1028 zonkEvVar var = do { ty' <- zonkTcType (varType var)
1029 ; return (setVarType var ty') }
1030
1031
1032 zonkWC :: WantedConstraints -> TcM WantedConstraints
1033 zonkWC wc = zonkWCRec wc
1034
1035 zonkWCRec :: WantedConstraints -> TcM WantedConstraints
1036 zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_insol = insol })
1037 = do { simple' <- zonkSimples simple
1038 ; implic' <- mapBagM zonkImplication implic
1039 ; insol' <- zonkSimples insol
1040 ; return (WC { wc_simple = simple', wc_impl = implic', wc_insol = insol' }) }
1041
1042 zonkSimples :: Cts -> TcM Cts
1043 zonkSimples cts = do { cts' <- mapBagM zonkCt' cts
1044 ; traceTc "zonkSimples done:" (ppr cts')
1045 ; return cts' }
1046
1047 zonkCt' :: Ct -> TcM Ct
1048 zonkCt' ct = zonkCt ct
1049
1050 zonkCt :: Ct -> TcM Ct
1051 zonkCt ct@(CHoleCan { cc_ev = ev })
1052 = do { ev' <- zonkCtEvidence ev
1053 ; return $ ct { cc_ev = ev' } }
1054 zonkCt ct
1055 = do { fl' <- zonkCtEvidence (cc_ev ct)
1056 ; return (mkNonCanonical fl') }
1057
1058 zonkCtEvidence :: CtEvidence -> TcM CtEvidence
1059 zonkCtEvidence ctev@(CtGiven { ctev_pred = pred })
1060 = do { pred' <- zonkTcType pred
1061 ; return (ctev { ctev_pred = pred'}) }
1062 zonkCtEvidence ctev@(CtWanted { ctev_pred = pred, ctev_dest = dest })
1063 = do { pred' <- zonkTcType pred
1064 ; let dest' = case dest of
1065 EvVarDest ev -> EvVarDest $ setVarType ev pred'
1066 -- necessary in simplifyInfer
1067 HoleDest h -> HoleDest h
1068 ; return (ctev { ctev_pred = pred', ctev_dest = dest' }) }
1069 zonkCtEvidence ctev@(CtDerived { ctev_pred = pred })
1070 = do { pred' <- zonkTcType pred
1071 ; return (ctev { ctev_pred = pred' }) }
1072
1073 zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo
1074 zonkSkolemInfo (SigSkol cx ty) = do { ty' <- zonkTcType ty
1075 ; return (SigSkol cx ty') }
1076 zonkSkolemInfo (InferSkol ntys) = do { ntys' <- mapM do_one ntys
1077 ; return (InferSkol ntys') }
1078 where
1079 do_one (n, ty) = do { ty' <- zonkTcType ty; return (n, ty') }
1080 zonkSkolemInfo skol_info = return skol_info
1081
1082 {-
1083 %************************************************************************
1084 %* *
1085 \subsection{Zonking -- the main work-horses: zonkTcType, zonkTcTyVar}
1086 * *
1087 * For internal use only! *
1088 * *
1089 ************************************************************************
1090
1091 -}
1092
1093 -- zonkId is used *during* typechecking just to zonk the Id's type
1094 zonkId :: TcId -> TcM TcId
1095 zonkId id
1096 = do { ty' <- zonkTcType (idType id)
1097 ; return (Id.setIdType id ty') }
1098
1099 -- | A suitable TyCoMapper for zonking a type inside the knot, and
1100 -- before all metavars are filled in.
1101 zonkTcTypeMapper :: TyCoMapper () TcM
1102 zonkTcTypeMapper = TyCoMapper
1103 { tcm_smart = True
1104 , tcm_tyvar = const zonkTcTyVar
1105 , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
1106 , tcm_hole = hole
1107 , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv }
1108 where
1109 hole :: () -> CoercionHole -> Role -> Type -> Type
1110 -> TcM Coercion
1111 hole _ h r t1 t2
1112 = do { contents <- unpackCoercionHole_maybe h
1113 ; case contents of
1114 Just co -> do { co <- zonkCo co
1115 ; checkCoercionHole co h r t1 t2 }
1116 Nothing -> do { t1 <- zonkTcType t1
1117 ; t2 <- zonkTcType t2
1118 ; return $ mkHoleCo h r t1 t2 } }
1119
1120
1121 -- For unbound, mutable tyvars, zonkType uses the function given to it
1122 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
1123 -- type variable and zonks the kind too
1124 zonkTcType :: TcType -> TcM TcType
1125 zonkTcType = mapType zonkTcTypeMapper ()
1126
1127 -- | "Zonk" a coercion -- really, just zonk any types in the coercion
1128 zonkCo :: Coercion -> TcM Coercion
1129 zonkCo = mapCoercion zonkTcTypeMapper ()
1130
1131 zonkTcTyCoVarBndr :: TcTyCoVar -> TcM TcTyCoVar
1132 -- A tyvar binder is never a unification variable (MetaTv),
1133 -- rather it is always a skolems. BUT it may have a kind
1134 -- that has not yet been zonked, and may include kind
1135 -- unification variables.
1136 zonkTcTyCoVarBndr tyvar
1137 -- can't use isCoVar, because it looks at a TyCon. Argh.
1138 = ASSERT2( isImmutableTyVar tyvar || (not $ isTyVar tyvar), ppr tyvar ) do
1139 updateTyVarKindM zonkTcType tyvar
1140
1141 zonkTcTyVar :: TcTyVar -> TcM TcType
1142 -- Simply look through all Flexis
1143 zonkTcTyVar tv
1144 | isTcTyVar tv
1145 = case tcTyVarDetails tv of
1146 SkolemTv {} -> zonk_kind_and_return
1147 RuntimeUnk {} -> zonk_kind_and_return
1148 FlatSkol ty -> zonkTcType ty
1149 MetaTv { mtv_ref = ref }
1150 -> do { cts <- readMutVar ref
1151 ; case cts of
1152 Flexi -> zonk_kind_and_return
1153 Indirect ty -> zonkTcType ty }
1154
1155 | otherwise -- coercion variable
1156 = zonk_kind_and_return
1157 where
1158 zonk_kind_and_return = do { z_tv <- zonkTyCoVarKind tv
1159 ; return (mkTyVarTy z_tv) }
1160
1161 {-
1162 %************************************************************************
1163 %* *
1164 Tidying
1165 * *
1166 ************************************************************************
1167 -}
1168
1169 zonkTidyTcType :: TidyEnv -> TcType -> TcM (TidyEnv, TcType)
1170 zonkTidyTcType env ty = do { ty' <- zonkTcType ty
1171 ; return (tidyOpenType env ty') }
1172
1173 -- | Make an 'ErrorThing' storing a type.
1174 mkTypeErrorThing :: TcType -> ErrorThing
1175 mkTypeErrorThing ty = ErrorThing ty (Just $ length $ snd $ splitAppTys ty)
1176 zonkTidyTcType
1177
1178 -- | Make an 'ErrorThing' storing a type, with some extra args known about
1179 mkTypeErrorThingArgs :: TcType -> Int -> ErrorThing
1180 mkTypeErrorThingArgs ty num_args
1181 = ErrorThing ty (Just $ (length $ snd $ splitAppTys ty) + num_args)
1182 zonkTidyTcType
1183
1184 zonkTidyOrigin :: TidyEnv -> CtOrigin -> TcM (TidyEnv, CtOrigin)
1185 zonkTidyOrigin env (GivenOrigin skol_info)
1186 = do { skol_info1 <- zonkSkolemInfo skol_info
1187 ; let (env1, skol_info2) = tidySkolemInfo env skol_info1
1188 ; return (env1, GivenOrigin skol_info2) }
1189 zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
1190 , uo_expected = exp
1191 , uo_thing = m_thing })
1192 = do { (env1, act') <- zonkTidyTcType env act
1193 ; (env2, exp') <- zonkTidyTcType env1 exp
1194 ; (env3, m_thing') <- zonkTidyErrorThing env2 m_thing
1195 ; return ( env3, orig { uo_actual = act'
1196 , uo_expected = exp'
1197 , uo_thing = m_thing' }) }
1198 zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig t_or_k)
1199 = do { (env1, ty1') <- zonkTidyTcType env ty1
1200 ; (env2, ty2') <- zonkTidyTcType env1 ty2
1201 ; (env3, orig') <- zonkTidyOrigin env2 orig
1202 ; return (env3, KindEqOrigin ty1' ty2' orig' t_or_k) }
1203 zonkTidyOrigin env (FunDepOrigin1 p1 l1 p2 l2)
1204 = do { (env1, p1') <- zonkTidyTcType env p1
1205 ; (env2, p2') <- zonkTidyTcType env1 p2
1206 ; return (env2, FunDepOrigin1 p1' l1 p2' l2) }
1207 zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2)
1208 = do { (env1, p1') <- zonkTidyTcType env p1
1209 ; (env2, p2') <- zonkTidyTcType env1 p2
1210 ; (env3, o1') <- zonkTidyOrigin env2 o1
1211 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) }
1212 zonkTidyOrigin env orig = return (env, orig)
1213
1214 zonkTidyErrorThing :: TidyEnv -> Maybe ErrorThing
1215 -> TcM (TidyEnv, Maybe ErrorThing)
1216 zonkTidyErrorThing env (Just (ErrorThing thing n_args zonker))
1217 = do { (env', thing') <- zonker env thing
1218 ; return (env', Just $ ErrorThing thing' n_args zonker) }
1219 zonkTidyErrorThing env Nothing
1220 = return (env, Nothing)
1221
1222 ----------------
1223 tidyCt :: TidyEnv -> Ct -> Ct
1224 -- Used only in error reporting
1225 -- Also converts it to non-canonical
1226 tidyCt env ct
1227 = case ct of
1228 CHoleCan { cc_ev = ev }
1229 -> ct { cc_ev = tidy_ev env ev }
1230 _ -> mkNonCanonical (tidy_ev env (ctEvidence ct))
1231 where
1232 tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
1233 -- NB: we do not tidy the ctev_evar field because we don't
1234 -- show it in error messages
1235 tidy_ev env ctev@(CtGiven { ctev_pred = pred })
1236 = ctev { ctev_pred = tidyType env pred }
1237 tidy_ev env ctev@(CtWanted { ctev_pred = pred })
1238 = ctev { ctev_pred = tidyType env pred }
1239 tidy_ev env ctev@(CtDerived { ctev_pred = pred })
1240 = ctev { ctev_pred = tidyType env pred }
1241
1242 ----------------
1243 tidyEvVar :: TidyEnv -> EvVar -> EvVar
1244 tidyEvVar env var = setVarType var (tidyType env (varType var))
1245
1246 ----------------
1247 tidySkolemInfo :: TidyEnv -> SkolemInfo -> (TidyEnv, SkolemInfo)
1248 tidySkolemInfo env (SigSkol cx ty)
1249 = (env', SigSkol cx ty')
1250 where
1251 (env', ty') = tidyOpenType env ty
1252
1253 tidySkolemInfo env (InferSkol ids)
1254 = (env', InferSkol ids')
1255 where
1256 (env', ids') = mapAccumL do_one env ids
1257 do_one env (name, ty) = (env', (name, ty'))
1258 where
1259 (env', ty') = tidyOpenType env ty
1260
1261 tidySkolemInfo env (UnifyForAllSkol skol_tvs ty)
1262 = (env1, UnifyForAllSkol skol_tvs' ty')
1263 where
1264 env1 = tidyFreeTyCoVars env (tyCoVarsOfType ty `delVarSetList` skol_tvs)
1265 (env2, skol_tvs') = tidyTyCoVarBndrs env1 skol_tvs
1266 ty' = tidyType env2 ty
1267
1268 tidySkolemInfo env info = (env, info)